Stream: Beginner Questions

Topic: Equivalent locales


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Feb 05 2021 at 11:16):

Manuel Eberl said:

Hm, you can do sublocale cfc_on: comp_fun_commute_on UNIV f in comp_fun_commute.

That is already in the code sample :wink:

view this post on Zulip Lukas Stevens (Feb 05 2021 at 11:17):

Manuel Eberl said:

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.

I am not really sure how that rewrites thing works. Is it just rewrites "x ∈ UNIV ≡ True"?

view this post on Zulip Mathias Fleury (Feb 05 2021 at 11:17):

isn't your problem a pure typing problem?

view this post on Zulip Mathias Fleury (Feb 05 2021 at 11:17):

g has the wrong type in your second lemma

view this post on Zulip Lukas Stevens (Feb 05 2021 at 11:18):

Baring copy-and-paste mistakes, it typechecks

view this post on Zulip Mathias Fleury (Feb 05 2021 at 11:18):

Is that an option?

locale comp_fun_commute = comp_fun_commute_on UNIV f
 for f

view this post on Zulip Lukas Stevens (Feb 05 2021 at 11:19):

Then you will have the assumptions of the form x ∈ UNIV in the locale conclusions.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Feb 05 2021 at 11:22):

Lukas Stevens said:

Then you will have the assumptions of the form x ∈ UNIV in the locale conclusions.

This would break backwards-compatability as well.

view this post on Zulip Manuel Eberl (Feb 05 2021 at 11:32):

Lukas Stevens said:

Manuel Eberl said:

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.

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.

view this post on Zulip Mathias Fleury (Feb 05 2021 at 11:34):

Isn't the problem that locales don't express what you want?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Lukas Stevens (Feb 05 2021 at 12:33):

Hm, rewrites "(A \<subseteq> UNIV ==> PROP P) ≡ PROP P" does not work.

view this post on Zulip Manuel Eberl (Feb 05 2021 at 12:43):

Seems to be a problem with the prop thing.

view this post on Zulip 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

view this post on Zulip Manuel Eberl (Feb 05 2021 at 12:44):

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.

view this post on Zulip 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: Sep 25 2021 at 08:21 UTC