From cb35a54563cbc0a531fc9c84d887b9e98f2d9378 Mon Sep 17 00:00:00 2001
From: Enrico Tassi <enrico.tassi@inria.fr>
Date: Fri, 28 Aug 2009 08:11:35 +0000
Subject: [PATCH 1/1] alias bug revealed

---
 .../software/matita/nlibrary/topology/igft.ma | 42 ++++++-------------
 1 file changed, 13 insertions(+), 29 deletions(-)

diff --git a/helm/software/matita/nlibrary/topology/igft.ma b/helm/software/matita/nlibrary/topology/igft.ma
index 8e05ca6f4..1fb59f067 100644
--- a/helm/software/matita/nlibrary/topology/igft.ma
+++ b/helm/software/matita/nlibrary/topology/igft.ma
@@ -1,4 +1,3 @@
-
 include "logic/connectives.ma".
 
 nrecord powerset (X : Type[0]) : Type[1] ≝ { char : X → CProp[0] }.
@@ -74,8 +73,7 @@ nlet corec fish_rec (A:axiom_set) (U: Ω^A)
 ##]
 nqed.
 
-alias symbol "covers" = "covers".
-alias symbol "covers" = "covers".
+(*
 ntheorem covers_elim2:
  ∀A: axiom_set. ∀U:Ω^A.∀P: A → CProp[0].
   (∀a:A. a ∈ U → P a) →
@@ -89,33 +87,19 @@ ntheorem covers_elim2:
     nassumption; 
 ##]
 nqed.
+*)
 
-STOP
-
-theorem coreflexivity: ∀A:axiom_set.∀a:A.∀V. a ⋉ V → a ∈ V.
- intros;
- cases H;
- assumption.
-qed.
-
-theorem cotransitivity:
- ∀A:axiom_set.∀a:A.∀U,V. a ⋉ U → (∀b:A. b ⋉ U → b ∈ V) → a ⋉ V.
- intros;
- apply (fish_rec ?? {a|a ⋉ U} ??? H); simplify; intros;
-  [ apply H1; apply H2;
-  | cases H2 in j; clear H2; intro i;
-    cases (H4 i); clear H4; exists[apply a3] assumption]
-qed.
-
-theorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
- intros;
- generalize in match H; clear H; 
- apply (covers_elim ?? {a|a ⋉ V → U ⋉ V} ??? H1);
- clear H1; simplify; intros;
-  [ exists [apply x] assumption
-  | cases H2 in j H H1; clear H2 a1; intros; 
-    cases (H1 i); clear H1; apply (H3 a1); assumption]
-qed.
+alias symbol "fish" (instance 1) = "fish set".
+alias symbol "covers" = "covers".
+ntheorem compatibility: ∀A:axiom_set.∀a:A.∀U,V. a ⋉ V → a ◃ U → U ⋉ V.
+#A; #a; #U; #V; #aV; #aU; ngeneralize in match aV; (* clear aV *)
+nelim aU;
+##[ #b; #bU; #bV; napply ex_intro; ##[ napply b] napply conj; nassumption;
+##| #b; #i; #CaiU; #H; #bV; ncases bV in i CaiU H;
+    #c; #cV; #CciV; #i; #CciU; #H; ncases (CciV i); #x; *; #xCci; #xV;
+    napply H; nassumption;
+##]
+nqed.
 
 definition leq ≝ λA:axiom_set.λa,b:A. a ◃ {y|b=y}.
 
-- 
2.39.2