- 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 (file)
index 0000000..3294017
--- /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 15da20a1132aae02cb7df0a5b457096402649eb2..56a8c4120b802e3b65dc73f14417820c22d58855 100644 (file)
--- 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;