## Stream: General

### Topic: Function between two locale

#### Roland Coghetto (Feb 02 2023 at 04:09):

I try to modify my code (cf IsaGeoCoq AFP)

My first difficulty is the definition of "surj_cong": i.e. to introduce the locales in the definition.
I have other difficulties but this one is blocking me.
Any help is welcome.

Here is an idea, I have of course reduced the local conditions for the example.
In order not to get lost, the main interest is the Test2's lemma and the definition surj_conj
This last definition is not correct.

TestG.thy

``````theory TestG
imports Main
begin

section "First"

typedecl TPoint
locale Tarski_neutral_dimensionless_First =
fixes Bet  :: "TPoint ⇒ TPoint ⇒ TPoint ⇒ bool"
fixes Cong :: "TPoint ⇒ TPoint ⇒ TPoint ⇒ TPoint ⇒ bool"
fixes TPA TPB TPC :: TPoint
assumes cong_pseudo_reflexivity: "∀ a b.  Cong a b b a"
and cong_inner_transitivity: "∀ a b p q r s.
Cong a b p q ∧ Cong a b r s ⟶ Cong p q r s"
and cong_identity: "∀ a b c. Cong a b c c ⟶ a = b"

context Tarski_neutral_dimensionless_First

begin

lemma cong_reflexivity_v1:
shows "Cong A B A B"
using cong_inner_transitivity cong_pseudo_reflexivity by blast

end

section "Second"

locale Tarski_neutral_dimensionless_Second =
fixes M :: "'a set" and Cong
assumes cong_pseudo_reflexivity: "⟦ a ∈ M; b ∈ M⟧ ⟹ Cong a b b a"
and cong_inner_transitivity: "⟦ a ∈ M; b ∈ M;p ∈ M;q ∈ M;r ∈ M;s ∈ M;
Cong a b p q ; Cong a b r s⟧ ⟹ Cong p q r s"

locale Tarski_neutral_dimensionless_Third =
Tarski_neutral_dimensionless_Second +
assumes cong_pseudo_reflexivity: "⟦ a ∈ M; b ∈ M⟧ ⟹ Cong a b b a"
and cong_inner_transitivity: "⟦ a ∈ M; b ∈ M;p ∈ M;q ∈ M;r ∈ M;s ∈ M;
Cong a b p q ; Cong a b r s⟧ ⟹ Cong p q r s"
and cong_identity: "⟦ a ∈ M; b ∈ M;c ∈ M;Cong a b c c⟧ ⟹ a = b"

context Tarski_neutral_dimensionless_Second

begin

lemma cong_reflexivity_v2_1:
assumes "A ∈ M" and "B ∈ M"
shows "Cong A B A B"
by (meson assms(1) assms(2) cong_inner_transitivity cong_pseudo_reflexivity)

lemma cong_reflexivity_v2_2:
assumes "Tarski_neutral_dimensionless_Second M Cong"
assumes "A ∈ M" and "B ∈ M"
shows "Cong A B A B"
by (meson assms(2) assms(3) cong_inner_transitivity cong_pseudo_reflexivity)

lemma cong_reflexivity_v2_3:
assumes "Tarski_neutral_dimensionless_Second N Cong'"
assumes "A ∈ N" and "B ∈ N"
shows "Cong' A B A B"
by (metis Tarski_neutral_dimensionless_Second.cong_inner_transitivity
Tarski_neutral_dimensionless_Second.cong_pseudo_reflexivity
assms(1) assms(2) assms(3))

lemma Test1:
fixes N1 :: "'a set"
fixes N2 :: "'b set"
fixes f :: "'a ⇒ 'b"
assumes "Tarski_neutral_dimensionless_Third N1 Cong1"
and "∀ A2. A2 ∈ N2 ⟶ (∃ A1 ∈ N1. (f A1) = A2)"
and "∀ A B C D. A ∈ N1 ∧ B ∈ N1 ∧ C ∈ N1 ∧ D ∈ N1 ∧ (Cong2 (f A)(f B)(f C)(f D)) ⟶ (Cong1 A B C D)"
shows "∀ A B C. A ∈ N2 ∧ B ∈ N2 ∧ C ∈ N2 ∧ (Cong2 A B C C) ⟶ A = B"
by (metis Tarski_neutral_dimensionless_Third.cong_identity assms(1) assms(2) assms(3))

lemma Test2:
fixes N1 :: "'a set"
fixes N2 :: "'b set"
fixes f :: "'a ⇒ 'b"
assumes "Tarski_neutral_dimensionless_Third N1 Cong1"
and "Tarski_neutral_dimensionless_Second N2 Cong2"
and "∀ A2. A2 ∈ N2 ⟶ (∃ A1 ∈ N1. (f A1) = A2)"
and "∀ A B C D. A ∈ N1 ∧ B ∈ N1 ∧ C ∈ N1 ∧ D ∈ N1 ∧ (Cong2 (f A)(f B)(f C)(f D)) ⟶ (Cong1 A B C D)"
shows "∀ A B C. A ∈ N2 ∧ B ∈ N2 ∧ C ∈ N2 ∧ (Cong2 C C A B) ⟶ A = B"
proof -
have "∀ A B C. A ∈ N2 ∧ B ∈ N2 ∧ C ∈ N2 ∧ (Cong2 A B C C) ⟶ A = B"
by (metis Tarski_neutral_dimensionless_Third.cong_identity assms(1) assms(3) assms(4))
thus ?thesis
by (smt (verit, ccfv_SIG) Tarski_neutral_dimensionless_Second.cong_inner_transitivity Tarski_neutral_dimensionless_Second.cong_pseudo_reflexivity assms(2))
qed

definition surj_cong:: "('a set ⇒ 'b set) ⇒ 'a set ⇒ ('a set ⇒'a set ⇒ 'a set ⇒'a set)
⇒'b set ⇒ ('b set ⇒ 'b set ⇒ 'b set ⇒ 'b set) ⇒ bool"
where
"(surj_cong f) N1 Cong1 N2 Cong2 ≡
(Tarski_neutral_dimensionless_Third N1 Cong1) ∧
(Tarski_neutral_dimensionless_Second N2 Cong2) ∧
(∀ A2. A2 ∈ N2 ⟶ (∃ A1 ∈ N1. (f A1) = A2)) ∧
(∀ A B C D. A ∈ N1 ∧ B ∈ N1 ∧ C ∈ N1 ∧ D ∈ N1 ∧ (Cong2 (f A)(f B)(f C)(f D)) ⟶ (Cong1 A B C D))"

end
end
``````

#### Mathias Fleury (Feb 02 2023 at 06:04):

The error message has nothing to do with locales… Your types are wrong:

``````definition surj_cong:: "('a set ⇒ 'b set) ⇒ 'a set set ⇒ ('a set ⇒ 'a set ⇒ 'a set ⇒ 'a set ⇒ bool)
⇒'b set set ⇒ ('b set ⇒ 'b set ⇒ 'b set ⇒ 'b set ⇒ bool) ⇒ bool"
where
"surj_cong f N1 Cong1 N2 Cong2 ≡
(Tarski_neutral_dimensionless_Third N1 Cong1) ∧
(Tarski_neutral_dimensionless_Second N2 Cong2) ∧
(∀ A2. A2 ∈ N2 ⟶ (∃ A1 ∈ N1. f A1 = A2)) ∧
(∀ A B C D. A ∈ N1 ∧ B ∈ N1 ∧ C ∈ N1 ∧ D ∈ N1 ∧ (Cong2 (f A)(f B)(f C)(f D)) ⟶ (Cong1 A B C D))"
``````

#### Mathias Fleury (Feb 02 2023 at 06:05):

I have no idea what it means. But, I first saw:

``````Type unification failed

Type error in application: incompatible operand type

Operator:  Tarski_neutral_dimensionless_Third N1 :: ('a ⇒ 'a ⇒ 'a ⇒ 'a ⇒ bool) ⇒ bool
Operand:   Cong1 :: 'a set ⇒ 'a set ⇒ 'a set ⇒ 'a set
``````

So I replace the type of Cong1 by `_`

#### Mathias Fleury (Feb 02 2023 at 06:07):

So I got:

``````definition surj_cong:: "('a set ⇒ 'b set) ⇒ 'a set ⇒ _
⇒'b set ⇒ _ ⇒ bool"
``````

Then the error message becomes:

``````Type unification failed

Type error in application: incompatible operand type

Operator:  (=) (f A1) :: 'b set ⇒ bool
Operand:   A2 :: 'b
``````

so A2 is an element instead of a set

#### Mathias Fleury (Feb 02 2023 at 06:08):

BTW, you should not use `typedecl TPoint` for quantifying over types. I have heard that it has worked in the past, but now you should put the type in the locale

#### Roland Coghetto (Feb 04 2023 at 16:33):

I have rewritten my problem completely differently:

locale func =
Tarski_neutral_dimensionless_Second M Cong1 +
Tarski_neutral_dimensionless_Second N Cong2
for M :: "'a set"
and Cong1 :: "'a ⇒'a ⇒'a ⇒ 'a ⇒bool" ("_ , _ ≅⇩M _ , _ " [99,99,99,99] 50)
and N :: "'b set"
and Cong2 :: "'b⇒'b⇒'b⇒'b⇒bool"("_ , _ ≅⇩N _ , _ " [99,99,99,99] 50) +
fixes f :: "'a ⇒ 'b"
assumes surj : "∀ A2. A2 ∈ N2 ⟶ (∃ A1 ∈ N1. f A1 = A2)"
and cong_pres : "∀ A B C D. A ∈ N1 ∧ B ∈ N1 ∧ C ∈ N1 ∧ D ∈ N1 ∧
(f A),(f B)≅⇩N(f C),(f D) ⟶ ( A, B ≅⇩M C, D)"

I test to see if I get the desired results.

#### Roland Coghetto (Feb 04 2023 at 16:46):

It seems to work:

lemma Test3:
assumes "Tarski_neutral_dimensionless_Third M Cong1"
shows "∀ A B C. A ∈ N ∧ B ∈ N ∧ C ∈ N ∧ (C, C ≅⇩N A, B) ⟶ A = B"
proof -
have "∀ A B C. A ∈ N ∧ B ∈ N ∧ C ∈ N ∧ (A, B ≅⇩N C, C) ⟶ A = B"
by (metis Tarski_neutral_dimensionless_Third.cong_identity assms cong_pres surj)
thus ?thesis
by (metis cong_inner_transitivity cong_reflexivity_v2_1)
qed

Sorry for the inconvenience

Last updated: Dec 07 2023 at 08:19 UTC