## Stream: Beginner Questions

### Topic: Equivalent locales

#### 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 f` in `comp_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 `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"`?

#### 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
``````

#### Lukas Stevens (Feb 05 2021 at 11:19):

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 ∈ UNIV` in 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 `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.

#### 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
``````

#### 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.

#### 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: Aug 13 2022 at 05:18 UTC