From 1afd7ec589d63a1b02165211391bce345a33d62f Mon Sep 17 00:00:00 2001
From: Claudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Date: Thu, 3 Jul 2008 21:31:55 +0000
Subject: [PATCH] First few lemmas. But I have some problems in making Matita
 accept my constructor.

---
 .../matita/library/demo/formal_topology.ma    | 107 +++++++++++++++---
 1 file changed, 92 insertions(+), 15 deletions(-)

diff --git a/helm/software/matita/library/demo/formal_topology.ma b/helm/software/matita/library/demo/formal_topology.ma
index 54c6aa629..cb720ffb4 100644
--- a/helm/software/matita/library/demo/formal_topology.ma
+++ b/helm/software/matita/library/demo/formal_topology.ma
@@ -13,25 +13,102 @@
 (**************************************************************************)
 
 include "logic/connectives.ma".
+include "logic/equality.ma".
 
-coinductive fish (A:Type) (i: A → Type) (C: ∀a:A.i a → A → Prop) (U: A → Prop)
-               : A → Prop
-≝
- mk_foo: ∀a:A. (U a ∧ ∀j: i a. ∃y: A. C a j y ∧ fish A i C U y) → fish A i C U a.
+record powerset (A: Type) : Type ≝ { char: A → Prop }.
 
-let corec fish_rec (A:Type) (i: A → Type) (C: ∀a:A.i a → A → Prop) (U: A → Prop)
- (P: A → Prop) (H1: ∀a:A. P a → U a)
-  (H2: ∀a:A. P a → ∀j: i a. ∃y: A. C a j y ∧ P y) :
-   ∀a:A. ∀p: P a. fish A i C U a ≝
+notation "hvbox(2 \sup A)" non associative with precedence 45
+for @{ 'powerset $A }.
+
+interpretation "powerset" 'powerset A = (powerset A).
+
+definition mem ≝ λA.λS:2 \sup A.λx:A. match S with [mk_powerset c ⇒ c x].
+
+notation "hvbox(a break ∈ b)" non associative with precedence 45
+for @{ 'mem $a $b }.
+
+interpretation "mem" 'mem a S = (mem _ S a).
+
+record axiom_set : Type ≝
+ { A:> Type;
+   i: A → Type;
+   C: ∀a:A. i a → 2 \sup A
+ }.
+
+inductive covers (A: axiom_set) (U: 2 \sup A) : A → CProp ≝
+   refl: ∀a:A. a ∈ U → covers A U a
+ | infinity: ∀a:A. ∀j: i ? a. coversl A U (C ? a j) → covers A U a
+with coversl : (2 \sup A) → CProp ≝
+   iter: ∀V:2 \sup A.(∀a:A.a ∈ V → covers A U a) → coversl A U V.
+
+notation "hvbox(a break ◃ b)" non associative with precedence 45
+for @{ 'covers $a $b }.
+
+interpretation "covers" 'covers a U = (covers _ U a).
+interpretation "coversl" 'covers A U = (coversl _ U A).
+
+axiom covers_elim:
+ ∀A:axiom_set.∀U: 2 \sup A.∀P:A → CProp.
+  ∀H1:∀a:A. a ∈ U → P a.
+   ∀H2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → P b) → P a.
+    ∀a:A.∀p:a ◃ U.P a.
+(*
+definition covers_elim ≝
+ λA:axiom_set.λU: 2 \sup A.λP:2 \sup A.
+  λH1:∀a:A. a ∈ U → a ∈ P.
+   λH2:∀a:A.∀j:i ? a. C ? a j ◃ U → (∀b. b ∈ C ? a j → b ∈ P) → a ∈ P.
+    let rec aux (a:A) (p:a ◃ U) : a ∈ P ≝
+     match p return λaa.λ_.aa ∈ P with
+      [ refl a q ⇒ H1 a q
+      | infinity a j q ⇒ H2 a j q (auxl (C ? a j) q)
+      ]
+    and auxl (V: 2 \sup A) (q: V ◃ U) : ∀b. b ∈ V → b ∈ P ≝
+     match q return λVV.λ_.∀b. b ∈ VV → b ∈ P with
+      [ iter VV f ⇒ λb.λr. aux b (f b r) ]
+    in
+     aux.
+*) 
+
+coinductive fish (A:axiom_set) (U: 2 \sup A) : A → Prop ≝
+ mk_fish: ∀a:A. (a ∈ U ∧ ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ fish A U y) → fish A U a.
+
+notation "hvbox(a break ⋉ b)" non associative with precedence 45
+for @{ 'fish $a $b }.
+
+interpretation "fish" 'fish a U = (fish _ U a).
+
+let corec fish_rec (A:axiom_set) (U: 2 \sup A)
+ (P: 2 \sup A) (H1: ∀a:A. a ∈ P → a ∈ U)
+  (H2: ∀a:A. a ∈ P → ∀j: i ? a. ∃y: A. y ∈ C ? a j ∧ y ∈ P) :
+   ∀a:A. ∀p: a ∈ P. a ⋉ U ≝
  λa,p.
-  mk_foo A i C U a
+  mk_fish A U a
    (conj ? ? (H1 ? p)
-   (λj: i a.
+   (λj: i ? a.
     match H2 a p j with
-     [ ex_intro (y: A) (Ha: C a j y ∧ P y) ⇒
+     [ ex_intro (y: A) (Ha: y ∈ C ? a j ∧ y ∈ P) ⇒
         match Ha with
-         [ conj (fHa: C a j y) (sHa: P y) ⇒
-            ex_intro A (λy.C a j y ∧ fish A i C U y) y
-             (conj ? ? fHa (fish_rec A i C U P H1 H2 y sHa))
+         [ conj (fHa: y ∈ C ? a j) (sHa: y ∈ P) ⇒
+            ex_intro A (λy.y ∈ C ? a j ∧ fish A U y) y
+             (conj ? ? fHa (fish_rec A U P H1 H2 y sHa))
          ]
-     ])).
\ No newline at end of file
+     ])).
+
+theorem reflexivity: ∀A:axiom_set.∀a:A.∀V. a ∈ V → a ◃ V.
+ intros;
+ apply refl;
+ assumption.
+qed.
+
+theorem transitivity: ∀A:axiom_set.∀a:A.∀U,V. a ◃ U → U ◃ V → a ◃ V.
+ intros;
+ elim H using covers_elim;
+  [ cases H1 in H2;
+    intro;
+    apply H2;
+    assumption
+  | apply infinity;
+     [ assumption
+     | constructor 1;
+       assumption]]
+qed.
\ No newline at end of file
-- 
2.39.2