helm/software/matita/library/demo/cantor.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "demo/formal_topology.ma".
  16 include "datatypes/constructors.ma".
  17
  18 axiom A: Type.
  19 axiom S: A → Ω \sup A.
  20
  21 definition axs: axiom_set.
  22  constructor 1;
  23   [ apply A;
  24   | intro; apply unit;
  25   | intros; apply (S a)]
  26 qed.
  27
  28 definition S' : axs → Ω \sup axs ≝ S.
  29
  30 definition emptyset: Ω \sup axs ≝ {x | False}.
  31
  32 definition Z: Ω \sup axs ≝ {x | x ◃ emptyset}.
  33
  34 theorem cantor: ∀a:axs. ¬ (Z ⊆ S' a ∧ S' a ⊆ Z).
  35  intros 2; cases H; clear H;
  36  cut (a ◃ S' a);
  37   [2: constructor 2; [constructor 1 | whd in ⊢ (? ? ? % ?); apply iter; autobatch]]
  38  cut (a ◃ emptyset);
  39   [2: apply transitivity; [apply (S' a)]
  40        [ assumption
  41        | constructor 1; intros;
  42          lapply (H2 ? H); whd in Hletin; assumption]]
  43  cut (a ∈ S' a);
  44   [2: apply H1; whd; assumption]
  45  generalize in match Hcut2; clear Hcut2;
  46  change with (a ∈ {a | a ∈ S' a → False});
  47  apply (covers_elim ?????? Hcut1);
  48   [ intros 2; simplify; intros; assumption;
  49   | intros; simplify; intros; whd in H3; simplify in H3; apply (H3 a1);
  50      [ assumption
  51      | assumption
  52      ]]
  53 qed.