From 8ecc06d373faf1ccedec01d87392c66ef2ffd876 Mon Sep 17 00:00:00 2001 From: Ferruccio Guidi Date: Tue, 29 Aug 2006 17:50:20 +0000 Subject: [PATCH] added a preamble file with disambiguation information --- .../contribs/LAMBDA-TYPES/Level-1/Base.ma | 2 +- .../contribs/LAMBDA-TYPES/Level-1/Preamble.ma | 56 +++++++++++++++++++ 2 files changed, 57 insertions(+), 1 deletion(-) create mode 100644 helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Preamble.ma diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma index 09d1f733a..4193eabcc 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Base.ma @@ -16,7 +16,7 @@ set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Base". -include "legacy/coq.ma". +include "Preamble.ma". theorem insert_eq: \forall (S: Set).(\forall (x: S).(\forall (P: ((S \to Prop))).(\forall (G: Prop).(((\forall (y: S).((P y) \to ((eq S y x) \to G)))) \to ((P x) \to G))))) diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Preamble.ma b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Preamble.ma new file mode 100644 index 000000000..1e73acd7a --- /dev/null +++ b/helm/software/matita/contribs/LAMBDA-TYPES/Level-1/Preamble.ma @@ -0,0 +1,56 @@ +(**************************************************************************) +(* ___ *) +(* ||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/LAMBDA-TYPES/Level-1/Preamble". + +include "legacy/coq.ma". + +(* FG/CSC: These aliases should disappear: we would like to write something + * like: "disambiguate in cic:/Coq/*" + *) +alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)". +alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)". +alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)". +alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)". +alias id "plus" = "cic:/Coq/Init/Peano/plus.con". +alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con". +alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con". +alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)". +alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)". +alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)". +alias id "true" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/1)". +alias id "false" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)". +alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)". +alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)". +alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)". +alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con". +alias id "or_introl" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/1)". +alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)". +alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con". +alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)". +alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)". +alias id "minus" = "cic:/Coq/Init/Peano/minus.con". + +theorem f_equal: \forall A,B:Type. \forall f:A \to B. + \forall x,y:A. x = y \to f x = f y. + intros. elim H. reflexivity. +qed. + +theorem sym_eq: \forall A:Type. \forall x,y:A. x = y \to y = x. + intros. rewrite > H. reflexivity. +qed. + +theorem sym_not_eq: \forall A:Type. \forall x,y:A. x \neq y \to y \neq x. + unfold not. intros. apply H. symmetry. assumption. +qed. -- 2.39.2