Coercions are now inserted also around the sources of lambda abstractions.

[helm.git] / helm / matita / contribs / PREDICATIVE-TOPOLOGY / ac_defs.ma

diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
index 6a5b86cf15f1e29f4677dfb994295f16a62b0003..b375c69ada732dd06bc7926a945f3e59baada69b 100644 (file)
--- a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
+++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma
@@ -12,11 +12,11 @@
 (*                                                                        *)
 (**************************************************************************)
 
 (*                                                                        *)
 (**************************************************************************)
 

-set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/ac_defs".
-

 (* Project started Wed Oct 12, 2005 ***************************************)
 
 (* Project started Wed Oct 12, 2005 ***************************************)
 

+set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/ac_defs".

 
 

+include "coq.ma".

 
 (* ACZEL CATEGORIES:
    - We use typoids with a compatible membership relation
 
 (* ACZEL CATEGORIES:
    - We use typoids with a compatible membership relation


@@ -30,7 +30,7 @@ set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/ac_defs".
      of the aceq predicate given inside the category. Then we prove the 
      properties of the equality that usually are axiomatized inside the 
      category structure. This makes categories easier to use
      of the aceq predicate given inside the category. Then we prove the 
      properties of the equality that usually are axiomatized inside the 
      category structure. This makes categories easier to use

-     *) 
+*) 

 
 record AC: Type \def {
    ac: Type;
 
 record AC: Type \def {
    ac: Type;


@@ -41,5 +41,46 @@ record AC: Type \def {
 coercion ac. 
 
 inductive eq (A:AC) (a:A): A \to Prop \def
 coercion ac. 
 
 inductive eq (A:AC) (a:A): A \to Prop \def

-   | eq_refl:   acin ? a \to eq ? a a.
-(*   | eq_sing_r: \forall b,c. eq A a b \to aceq A b c \to eq A a c. *)
+   | eq_refl:   acin ? a \to eq ? a a
+   | eq_sing_r: \forall b,c. 
+                eq ? a b \to acin ? c \to aceq ? b c \to eq ? a c
+   | eq_sing_l: \forall b,c. 
+                eq ? a b \to acin ? c \to aceq ? c b \to eq ? a c.
+
+theorem eq_cl: \forall A,a,b. eq ? a b \to acin A a \land acin A b.
+intros; elim H; clear H; clear b; 
+   [ auto | decompose H2; auto | decompose H2; auto ].
+qed.
+
+theorem eq_trans: \forall A,b,a,c.
+                  eq A b c \to eq ? a b \to eq ? a c.
+intros 5; elim H; clear H; clear c;
+   [ auto 
+   | apply eq_sing_r; [||| apply H4 ]; auto
+   | apply eq_sing_l; [||| apply H4 ]; auto
+   ].
+qed.
+
+theorem eq_conf_rev: \forall A,b,a,c.
+                     eq A c b \to eq ? a b \to eq ? a c.
+intros 5; elim H; clear H; clear b;
+   [ auto 
+   | lapply eq_cl; [ decompose Hletin |||| apply H1 ].
+     apply H2; apply eq_sing_l; [||| apply H4 ]; auto
+   | lapply eq_cl; [ decompose Hletin |||| apply H1 ].
+     apply H2; apply eq_sing_r; [||| apply H4 ]; auto
+   ].
+qed.
+
+theorem eq_sym: \forall A,a,b. eq A a b \to eq A b a.
+intros;
+lapply eq_cl; [ decompose Hletin |||| apply H ].
+auto.
+qed.
+
+theorem eq_conf: \forall A,b,a,c.
+                 eq A a b \to eq ? a c \to eq ? b c.
+intros.
+lapply eq_sym; [|||| apply H ].
+apply eq_trans; [| auto | auto ].
+qed.