Artem Khovanov (Aug 22 2022 at 00:35): Artem Khovanov (Aug 22 2022 at 00:35):How can I access the following sublocale claim outisde of the context of the total_order locale?
sublocale total_order < weak?: weak_total_order
by unfold_locales (rule total_order_total)
Within the total_order locale context, I can use the fact local.weak.weak_total_order_axioms, but I would like to prove something like
total_order A ⟹ weak_total_order A.
Wenda Li (Aug 22 2022 at 01:21):Not sure if I understand the problem correctly, but can't we prove this outside a locale context?
lemma "total_order A ⟹ weak_total_order A"
by (meson partial_order.axioms(1) total_order.axioms(1)
total_order.axioms(2) total_order_axioms_def
weak_partial_order.weak_total_orderI)
Your proof (which sledgehammer finds) re-proves the implication from other facts. I can work around the issue in this case, but I was wondering how to avoid duplicating a more complicated proof.
Wenda Li (Aug 22 2022 at 02:41):My personal practice is to explicitly record such implication (if it will be useful later on) and use it for the sublocale proof:
lemma foo:"total_order A ⟹ weak_total_order A"
sorry
sublocale total_order < weak?: weak_total_order
by (rule foo) (simp add: total_order_axioms)
Last updated: Dec 21 2024 at 16:20 UTC