Lukas Stevens (Feb 05 2021 at 10:33): Lukas Stevens (Feb 05 2021 at 10:33):I have the following two locales
locale comp_fun_commute_on =
fixes S
fixes f
assumes "x ∈ S ==> y ∈ S ==> f y o f x = f x o f y"
begin
...
end
locale comp_fun_commute =
fixes f
assumes "f y o f x = f x o f y"
begin
sublocale comp_fun_commute_on_UNIV?: comp_fun_commute_on UNIV f
by ...
end
lemma (in comp_fun_commute_on) comp_comp_fun_commute_on:
"range g ⊆ S ⟹ comp_fun_commute_on S (f o g)"
by ...
lemma (in comp_fun_commute) comp_comp_fun_commute:
"comp_fun_commute (f o g)"
sorry
As you can see the second locale is a specialised version of the first one where the carrier set is the universe. I want two separate locales since I can remove the assumptions of the form S \<subseteq> UNIV and x ∈ UNIV in comp_fun_commute and to maintain backwards compatability.
Conceptually, I would like to prove the last lemma by applying the introduction rule comp_fun_commute_on UNIV f ==> comp_fun_commute f but I don't have this lemma yet. Do I have to prove that or is there any way to structure the locales differently such that it reflects the fact that comp_fun_commute_on UNIV f = comp_fun_commute f?
Manuel Eberl (Feb 05 2021 at 11:14):Hm, you can do sublocale cfc_on: comp_fun_commute_on UNIV f in comp_fun_commute.
Manuel Eberl (Feb 05 2021 at 11:14):I think there's also the rewrites argument for sublocale that allows you to perform some simplifications on the theorems you get out of the interpretation to get rid of things like x ∈ UNIV.
Lukas Stevens (Feb 05 2021 at 11:16):Manuel Eberl said:
Hm, you can do
sublocale cfc_on: comp_fun_commute_on UNIV fincomp_fun_commute.
That is already in the code sample :wink:
Lukas Stevens (Feb 05 2021 at 11:17):Manuel Eberl said:
I think there's also the
rewritesargument forsublocalethat allows you to perform some simplifications on the theorems you get out of the interpretation to get rid of things likex ∈ UNIV.
I am not really sure how that rewrites thing works. Is it just rewrites "x ∈ UNIV ≡ True"?
Mathias Fleury (Feb 05 2021 at 11:17):isn't your problem a pure typing problem?
Mathias Fleury (Feb 05 2021 at 11:17):g has the wrong type in your second lemma
Lukas Stevens (Feb 05 2021 at 11:18):Baring copy-and-paste mistakes, it typechecks
Mathias Fleury (Feb 05 2021 at 11:18):Is that an option?
locale comp_fun_commute = comp_fun_commute_on UNIV f
for f
Then you will have the assumptions of the form x ∈ UNIV in the locale conclusions.
Lukas Stevens (Feb 05 2021 at 11:20):And the locale assumption is x ∈ UNIV ==> y ∈ UNIV ==> f y o f x = f x o f y instead of f y o f x = f x o f y.
Lukas Stevens (Feb 05 2021 at 11:20):In this case that wouldn't be so bad but if the equivalence of the locales would be non-trivial then you wouldn't want to do that.
Lukas Stevens (Feb 05 2021 at 11:22):Lukas Stevens said:
Then you will have the assumptions of the form
x ∈ UNIVin the locale conclusions.
This would break backwards-compatability as well.
Manuel Eberl (Feb 05 2021 at 11:32):Lukas Stevens said:
Manuel Eberl said:
I think there's also the
rewritesargument forsublocalethat allows you to perform some simplifications on the theorems you get out of the interpretation to get rid of things likex ∈ UNIV.I am not really sure how that rewrites thing works. Is it just
rewrites "x ∈ UNIV ≡ True"?
No idea. It's probably documented somewhere. Or look at how it is used in the distribution. I never really used it myself.
Mathias Fleury (Feb 05 2021 at 11:34):Isn't the problem that locales don't express what you want?
Mathias Fleury (Feb 05 2021 at 11:37):From what I understand, locales instantiation is done in the metalogic, so there is no theorem corresponding to the sublocale.
Lukas Stevens (Feb 05 2021 at 11:37):Mathias Fleury said:
Isn't the problem that locales don't express what you want?
Yeah, it's possible that you can't express that with locales.
Lukas Stevens (Feb 05 2021 at 12:33):Hm, rewrites "(A \<subseteq> UNIV ==> PROP P) ≡ PROP P" does not work.
Manuel Eberl (Feb 05 2021 at 12:43):Seems to be a problem with the prop thing.
Manuel Eberl (Feb 05 2021 at 12:43):axiomatization P :: "'a ⇒ bool"
locale foo =
fixes A :: "'a set"
begin
lemma bar: "X ⊆ A ⟹ P X"
sorry
end
locale bar
begin
sublocale foo UNIV rewrites "Y ⊆ UNIV ≡ True" and "(True ⟹ PROP Q) ≡ PROP Q"
by auto
If you replace the second rewrites rule with (True ⟹ Q) ≡ Trueprop Q it works. But of course that will not be enough for rules with several implications.
Manuel Eberl (Feb 05 2021 at 12:44):No idea what's going on here. Might want to ask on the mailing list.
Last updated: Apr 24 2024 at 04:17 UTC