From a3d01f7170dd84f90481d53e271580e10e46ae75 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Mon, 24 Nov 2008 17:27:41 +0000
Subject: [PATCH] ...

---
 helm/software/matita/contribs/igft/cantor.ma | 43 ++++++++++++++++++
 helm/software/matita/contribs/igft/depends   |  2 +
 helm/software/matita/contribs/igft/igft.ma   | 48 +++++++++++++++-----
 3 files changed, 81 insertions(+), 12 deletions(-)
 create mode 100644 helm/software/matita/contribs/igft/cantor.ma

diff --git a/helm/software/matita/contribs/igft/cantor.ma b/helm/software/matita/contribs/igft/cantor.ma
new file mode 100644
index 000000000..38e652584
--- /dev/null
+++ b/helm/software/matita/contribs/igft/cantor.ma
@@ -0,0 +1,43 @@
+include "logic/cprop_connectives.ma".
+include "igft.ma".
+
+axiom A: Type.
+axiom S_: A → Ω^A.
+
+inductive Unit : Type := unit : Unit.
+
+definition axs: AxiomSet.
+ constructor 1;
+  [ apply A;
+  | intro; apply Unit;
+  | intros; apply (S_ a)]
+qed.
+
+definition S : axs → Ω^axs ≝ S_.
+
+definition emptyset: Ω^axs ≝ {x | False}.
+
+notation "∅︀" non associative with precedence 90 for @{'emptyset}.
+interpretation "emptyset" 'emptyset = emptyset.
+notation "∅" non associative with precedence 91 for @{'emptyset1}.
+interpretation "emptyset1" 'emptyset1 = emptyset.
+
+definition Z: Ω \sup axs ≝ {x | x ⊲ ∅}.
+
+theorem cantor: ∀a:axs. ¬ (Z ⊆ S a ∧ S a ⊆ Z).
+ intros 2; cases H; clear H;
+ cut (a ⊲ S a);
+  [2: apply infinity; [apply unit] change with (S a ⊲ S a); 
+      intros 2; apply refl; apply H;]
+ cut (a ⊲ ∅︀);
+  [2: apply (trans (S a)); [ assumption ]
+      intros 2; lapply (H2 ? H) as K;
+      change in K with (x ⊲ ∅ );
+      assumption;]
+ cut (a ε S a);
+  [2: apply H1; apply Hcut1;]
+ generalize in match Hcut2; clear Hcut2;
+ elim Hcut1 using covers_elim;
+  [ intros 2; cases H;
+  | intros; apply (H3 a1); [apply H4|apply H4]]
+qed.
diff --git a/helm/software/matita/contribs/igft/depends b/helm/software/matita/contribs/igft/depends
index 6fef337d0..760fb8050 100644
--- a/helm/software/matita/contribs/igft/depends
+++ b/helm/software/matita/contribs/igft/depends
@@ -1 +1,3 @@
+cantor.ma igft.ma logic/cprop_connectives.ma
 igft.ma 
+logic/cprop_connectives.ma 
diff --git a/helm/software/matita/contribs/igft/igft.ma b/helm/software/matita/contribs/igft/igft.ma
index b6da8620f..fb4a92340 100644
--- a/helm/software/matita/contribs/igft/igft.ma
+++ b/helm/software/matita/contribs/igft/igft.ma
@@ -11,6 +11,11 @@ record AxiomSet : Type := {
   C_ : ∀a.I_ a → Ω ^ S
 }.
 
+notation > "∀ident a∈A.P" right associative with precedence 20
+for @{ ∀${ident a} : S $A. $P }.
+notation > "λident a∈A.P" right associative with precedence 20
+for @{ λ${ident a} : S $A. $P }.
+
 notation "'I'" non associative with precedence 90 for @{'I}.
 interpretation "I" 'I = (I_ _).
 notation < "'I' \lpar a \rpar" non associative with precedence 90 for @{'I1 $a}.
@@ -23,7 +28,7 @@ notation < "'C' \lpar a , i \rpar" non associative with precedence 90 for @{'C2
 interpretation "C a i" 'C2 a i = (C_ _ a i).
 
 definition in_subset :=
-  λA:AxiomSet.λa:A.λU:Ω^A.content A U a.
+  λA:AxiomSet.λa∈A.λU:Ω^A.content A U a.
   
 notation "hvbox(a break εU)" non associative with precedence 50 for 
 @{'in_subset $a $U}.
@@ -32,8 +37,14 @@ interpretation "In subset" 'in_subset a U = (in_subset _ a U).
 definition for_all ≝ λA:AxiomSet.λU:Ω^A.λP:A → CProp.∀x.xεU → P x.
 
 inductive covers (A : AxiomSet) (U : Ω ^ A) : A → CProp :=
- | reflexivity : ∀a.aεU → covers A U a
- | infinity : ∀a.∀i : I a. for_all A (C a i) (covers A U)  → covers A U a.
+ | refl_ : ∀a.aεU → covers A U a
+ | infinity_ : ∀a.∀i : I a. for_all A (C a i) (covers A U)  → covers A U a.
+ 
+notation "'refl'" non associative with precedence 90 for @{'refl}. 
+interpretation "refl" 'refl = (refl_ _ _ _).
+
+notation "'infinity'" non associative with precedence 90 for @{'infinity}.  
+interpretation "infinity" 'infinity = (infinity_ _ _ _).
  
 notation "U ⊲ V" non associative with precedence 45
 for @{ 'covers_subsets $U $V}.
@@ -44,22 +55,35 @@ definition subseteq := λA:AxiomSet.λU,V:Ω^A.∀x.xεU → xεV.
 
 interpretation "subseteq" 'subseteq u v = (subseteq _ u v).
 
-definition covers_elim ≝
+
+definition covers_elim_ ≝
  λA:AxiomSet.λU,P: Ω^A.λH1: U ⊆ P. 
-  λH2:∀a:A.∀j:I a. C a j ⊲ U → C a j ⊆ P → aεP.
+  λH2:∀a∈A.∀j:I a. C a j ⊲ U → C a j ⊆ P → aεP.
     let rec aux (a:A) (p:a ⊲ U) on p : aεP ≝
-     match p return λaa.λ_:aa ⊲ U.aa ε P with
-      [ reflexivity a q ⇒ H1 a q
-      | infinity a j q ⇒ H2 a j q (λb.λr. aux b (q b r))]
+     match p return λr.λ_:r ⊲ U.r ε P with
+      [ refl_ a q ⇒ H1 a q
+      | infinity_ a j q ⇒ H2 a j q (λb.λr. aux b (q b r))]
     in
      aux.
-
+     
 interpretation "char" 'subset p = (mk_powerset _ p).  
+     
+definition covers_elim : 
+ ∀A:AxiomSet.∀U: Ω^A.∀P:A→CProp.∀H1: U ⊆ {x | P x}. 
+  ∀H2:∀a∈A.∀j:I a. C a j ⊲ U → C a j ⊆ {x | P x} → P a.
+   ∀a∈A.a ⊲ U → P a.
+change in ⊢ (?→?→?→?→?→?→?→%) with (aε{x|P x});
+intros 3; apply covers_elim_;
+qed.
 
-theorem transitivity: ∀A:AxiomSet.∀a:A.∀U,V. a ⊲ U → U ⊲ V → a ⊲ V.
+theorem trans_: ∀A:AxiomSet.∀a∈A.∀U,V. a ⊲ U → U ⊲ V → a ⊲ V.
  intros;
- apply (covers_elim ?? {a | a ⊲ V} ??? H);
+ elim H using covers_elim;
   [ intros 2; apply (H1 ? H2);
-  | intros; apply (infinity ??? j);
+  | intros; apply (infinity j);
     intros 2; apply (H3 ? H4);]
 qed.
+
+notation "'trans'" non associative with precedence 90 for @{'trans}. 
+interpretation "trans" 'trans = (trans_ _ _).
+
-- 
2.39.2