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.apply refl_equal.
  39 qed.
  40
  41 theorem f_equal2: \forall  A,B,C:Type.\forall f:A\to B \to C.
  42 \forall x1,x2:A. \forall y1,y2:B.
  43 eq A x1 x2\to eq B y1 y2\to eq C (f x1 y1) (f x2 y2).
  44 intros.elim H1.elim H.apply refl_equal.
  45 qed.