]> matita.cs.unibo.it Git - helm.git/blob - helm/matita/library/equality.ma
added Variant theorem flavour
[helm.git] / helm / matita / library / equality.ma
1 (**************************************************************************)
2 (*       ___                                                                *)
3 (*      ||M||                                                             *)
4 (*      ||A||       A project by Andrea Asperti                           *)
5 (*      ||T||                                                             *)
6 (*      ||I||       Developers:                                           *)
7 (*      ||T||       A.Asperti, C.Sacerdoti Coen,                          *)
8 (*      ||A||       E.Tassi, S.Zacchiroli                                 *)
9 (*      \   /                                                             *)
10 (*       \ /        This file is distributed under the terms of the       *)
11 (*        v         GNU Lesser General Public License Version 2.1         *)
12 (*                                                                        *)
13 (**************************************************************************)
14
15 set "baseuri" "cic:/matita/equality/".
16
17 inductive eq (A:Type) (x:A) : A \to Prop \def
18     refl_equal : eq A x x.
19
20 theorem sym_eq : \forall A:Type.\forall x,y:A. eq A x y  \to eq A y x.
21 intros. elim H. apply refl_equal.
22 qed.
23
24 theorem trans_eq : \forall A:Type.
25 \forall x,y,z:A. eq A x y  \to eq A y z \to eq A x z.
26 intros.elim H1.assumption.
27 qed.
28
29 theorem eq_ind_r :
30  \forall A:Type.\forall x:A. \forall P: A \to Prop.
31    P x \to \forall y:A. eq A y x \to P y.
32 intros.letin H1' \def sym_eq ? ? ? H1.clearbody H1'.
33 elim H1'.assumption.
34 qed.
35
36 theorem f_equal: \forall  A,B:Type.\forall f:A\to B.
37 \forall x,y:A. eq A x y \to eq B (f x) (f y).
38 intros.elim H.reflexivity.
39 qed.
40
41 default "equality"
42  cic:/matita/equality/eq.ind
43  cic:/matita/equality/sym_eq.con
44  cic:/matita/equality/trans_eq.con
45  cic:/matita/equality/eq_ind.con
46  cic:/matita/equality/eq_ind_r.con. 
47
48 theorem f_equal2: \forall  A,B,C:Type.\forall f:A\to B \to C.
49 \forall x1,x2:A. \forall y1,y2:B.
50 eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2).
51 intros.elim H1.elim H.reflexivity.
52 qed.