From: Ferruccio Guidi Date: Sat, 29 Oct 2005 18:03:03 +0000 (+0000) Subject: Aczel categories finished X-Git-Tag: V_0_7_2_3~164 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=a1dbfbc43a9f01eaf64d4f2cc66d6be1ac6943ce;p=helm.git Aczel categories finished quantification domains started --- diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/ac_defs.ma index 6a5b86cf1..e4ee22311 100644 --- 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 ***************************************) +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/ac_defs". +include "coq.ma". (* ACZEL CATEGORIES: - We use typoids with a compatible membership relation @@ -41,5 +41,46 @@ record AC: Type \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. diff --git a/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma new file mode 100644 index 000000000..cd019ccfc --- /dev/null +++ b/helm/matita/contribs/PREDICATIVE-TOPOLOGY/qd_defs.ma @@ -0,0 +1,26 @@ +(**************************************************************************) +(* ___ *) +(* ||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 *) +(* *) +(**************************************************************************) + +set "baseuri" "cic:/matita/PREDICATIVE-TOPOLOGY/qd_defs". + +include "ac_defs.ma". + +(* QUANTIFICATION DOMAINS +*) + +record QD: Type \def { + qd: AC +}. + +coercion qd.