From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Tue, 4 Nov 2008 10:22:30 +0000 (+0000)
Subject: - A new interesting elimination principle over inductively generated topologies:
X-Git-Tag: make_still_working~4603
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=13f687d1d7cc07a19dcf28e1624f78a3a9d9c840;p=helm.git

- A new interesting elimination principle over inductively generated topologies:
  the elimination principle for general topologies hold!
- A proof of Cantor theorem using formal topologies. By Silvio Valentini.
---

diff --git a/helm/software/matita/library/demo/cantor.ma b/helm/software/matita/library/demo/cantor.ma
new file mode 100644
index 000000000..3294017d7
--- /dev/null
+++ b/helm/software/matita/library/demo/cantor.ma
@@ -0,0 +1,53 @@
+(**************************************************************************)
+(*       ___                                                              *)
+(*      ||M||                                                             *)
+(*      ||A||       A project by Andrea Asperti                           *)
+(*      ||T||                                                             *)
+(*      ||I||       Developers:                                           *)
+(*      ||T||         The HELM team.                                      *)
+(*      ||A||         http://helm.cs.unibo.it                             *)
+(*      \   /                                                             *)
+(*       \ /        This file is distributed under the terms of the       *)
+(*        v         GNU General Public License Version 2                  *)
+(*                                                                        *)
+(**************************************************************************)
+
+include "demo/formal_topology.ma".
+include "datatypes/constructors.ma".
+
+axiom A: Type.
+axiom S: A → Ω \sup A.
+
+definition axs: axiom_set.
+ constructor 1;
+  [ apply A;
+  | intro; apply unit;
+  | intros; apply (S a)]
+qed.
+
+definition S' : axs → Ω \sup axs ≝ S.
+
+definition emptyset: Ω \sup axs ≝ {x | False}.
+
+definition Z: Ω \sup axs ≝ {x | x ◃ emptyset}.
+
+theorem cantor: ∀a:axs. ¬ (Z ⊆ S' a ∧ S' a ⊆ Z).
+ intros 2; cases H; clear H;
+ cut (a ◃ S' a);
+  [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); autobatch]]
+ cut (a ◃ emptyset);
+  [2: apply transitivity; [apply (S' a)]
+       [ assumption
+       | constructor 1; intros;
+         lapply (H2 ? H); whd in Hletin; assumption]]
+ cut (a ∈ S' a);
+  [2: apply H1; whd; assumption]
+ generalize in match Hcut2; clear Hcut2;
+ change with (a ∈ {a | a ∈ S' a → False});
+ apply (covers_elim ?????? Hcut1);
+  [ intros 2; simplify; intros; assumption;
+  | intros; simplify; intros; whd in H3; simplify in H3; apply (H3 a1);
+     [ assumption
+     | assumption
+     ]]
+qed.
diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 15da20a11..56a8c4120 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -109,6 +109,24 @@ theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a 
        assumption]]
 qed.
 
+theorem covers_elim2:
+ ∀A: axiom_set. ∀U:Ω \sup A.∀P: A → CProp.
+  (∀a:A. a ∈ U → P a) →
+   (∀a:A.∀V:Ω \sup A. a ◃ V → V ◃ U → (∀y. y ∈ V → P y) → P a) →
+     ∀a:A. a ◃ U → P a.
+ intros;
+ change with (a ∈ {a | P a});
+ apply (covers_elim ?????? H2);
+  [ intros 2; simplify; apply H; assumption
+  | intros;
+    simplify in H4 ⊢ %;
+    apply H1;
+     [ apply (C ? a1 j);
+     | autobatch;
+     | assumption;
+     | assumption]]
+qed.
+
 theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
  intros;
  cases H;