Stream: General

Topic: Function between two locale


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

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

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

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

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

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

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

view this post on Zulip 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 2024 at 16:22 UTC