1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/Preamble".
17 (* FG: We should include legacy/coq.ma bit it is not working *)
18 (* include "legacy/coq.ma". *)
21 cic:/Coq/Init/Logic/eq.ind
22 cic:/Coq/Init/Logic/sym_eq.con
23 cic:/Coq/Init/Logic/trans_eq.con
24 cic:/Coq/Init/Logic/eq_ind.con
25 cic:/Coq/Init/Logic/eq_ind_r.con
26 cic:/Coq/Init/Logic/f_equal.con
27 cic:/Coq/Init/Logic/f_equal1.con.
30 cic:/Coq/Init/Logic/True.ind.
33 cic:/Coq/Init/Logic/False.ind.
36 cic:/Coq/Init/Logic/absurd.con.
38 interpretation "Coq's leibnitz's equality" 'eq x y = (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y).
39 interpretation "Coq's not equal to (leibnitz)" 'neq x y = (cic:/Coq/Init/Logic/not.con (cic:/Coq/Init/Logic/eq.ind#xpointer(1/1) _ x y)).
40 interpretation "Coq's natural plus" 'plus x y = (cic:/Coq/Init/Peano/plus.con x y).
41 interpretation "Coq's natural 'less or equal to'" 'leq x y = (cic:/Coq/Init/Peano/le.ind#xpointer(1/1) x y).
43 alias id "land" = "cic:/Coq/Init/Logic/and.ind#xpointer(1/1)".
45 (* FG/CSC: These aliases should disappear: we would like to write something
46 * like: "disambiguate in cic:/Coq/*"
48 alias id "True" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1)".
49 alias id "or" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1)".
50 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
51 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
52 alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
53 alias id "le_trans" = "cic:/Coq/Arith/Le/le_trans.con".
54 alias id "le_plus_r" = "cic:/Coq/Arith/Plus/le_plus_r.con".
55 alias id "le" = "cic:/Coq/Init/Peano/le.ind#xpointer(1/1)".
56 alias id "ex" = "cic:/Coq/Init/Logic/ex.ind#xpointer(1/1)".
57 alias id "ex2" = "cic:/Coq/Init/Logic/ex2.ind#xpointer(1/1)".
58 alias id "true" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/1)".
59 alias id "false" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1/2)".
60 alias id "bool" = "cic:/Coq/Init/Datatypes/bool.ind#xpointer(1/1)".
61 alias id "O" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/1)".
62 alias id "S" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1/2)".
63 alias id "eq_ind" = "cic:/Coq/Init/Logic/eq_ind.con".
64 alias id "or_introl" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/1)".
65 alias id "or_intror" = "cic:/Coq/Init/Logic/or.ind#xpointer(1/1/2)".
66 alias id "False_ind" = "cic:/Coq/Init/Logic/False_ind.con".
67 alias id "False" = "cic:/Coq/Init/Logic/False.ind#xpointer(1/1)".
68 alias id "I" = "cic:/Coq/Init/Logic/True.ind#xpointer(1/1/1)".
69 alias id "minus" = "cic:/Coq/Init/Peano/minus.con".
71 theorem f_equal: \forall A,B:Type. \forall f:A \to B.
72 \forall x,y:A. x = y \to f x = f y.
73 intros. elim H. reflexivity.
76 theorem sym_eq: \forall A:Type. \forall x,y:A. x = y \to y = x.
77 intros. rewrite > H. reflexivity.
80 theorem sym_not_eq: \forall A:Type. \forall x,y:A. x \neq y \to y \neq x.
81 unfold not. intros. apply H. symmetry. assumption.
84 theorem plus_reg_l: \forall (n,m,p:nat). n + m = n + p \to m = p.
85 intros. apply plus_reg_l; auto.
88 theorem plus_le_reg_l: \forall p,n,m. p + n <= p + m \to n <= m.
89 intros. apply plus_le_reg_l; auto.
92 definition sym_equal \def sym_eq.