Roland Coghetto (Feb 02 2023 at 04:09): Roland Coghetto (Feb 02 2023 at 04:09):After reading class vs locale
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.
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
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))"
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: Apr 25 2024 at 08:20 UTC