helm/matita/library/logic/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/logic/equality/".
  16
  17 include "higher_order_defs/relations.ma".
  18
  19 inductive eq (A:Type) (x:A) : A \to Prop \def
  20     refl_eq : eq A x x.
  21
  22 (*CSC: the URI must disappear: there is a bug now *)
  23 interpretation "leibnitz's equality"
  24    'eq x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y).
  25 (*CSC: the URI must disappear: there is a bug now *)
  26 interpretation "leibnitz's non-equality"
  27   'neq x y = (cic:/matita/logic/connectives/Not.con
  28     (cic:/matita/logic/equality/eq.ind#xpointer(1/1) _ x y)).
  29
  30 theorem reflexive_eq : \forall A:Type. reflexive A (eq A).
  31 simplify.intros.apply refl_eq.
  32 qed.
  33
  34 theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
  35 simplify.intros.elim H. apply refl_eq.
  36 qed.
  37
  38 theorem sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
  39 \def symmetric_eq.
  40
  41 theorem transitive_eq : \forall A:Type. transitive A (eq A).
  42 simplify.intros.elim H1.assumption.
  43 qed.
  44
  45 theorem trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z
  46 \def transitive_eq.
  47
  48 theorem eq_elim_r:
  49  \forall A:Type.\forall x:A. \forall P: A \to Prop.
  50    P x \to \forall y:A. y=x \to P y.
  51 intros. elim (sym_eq ? ? ? H1).assumption.
  52 qed.
  53
  54 default "equality"
  55  cic:/matita/logic/equality/eq.ind
  56  cic:/matita/logic/equality/sym_eq.con
  57  cic:/matita/logic/equality/trans_eq.con
  58  cic:/matita/logic/equality/eq_ind.con
  59  cic:/matita/logic/equality/eq_elim_r.con.
  60
  61 theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
  62 \forall x,y:A. x=y \to f x = f y.
  63 intros.elim H.reflexivity.
  64 qed.
  65
  66 theorem eq_f2: \forall  A,B,C:Type.\forall f:A\to B \to C.
  67 \forall x1,x2:A. \forall y1,y2:B.
  68 x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2.
  69 intros.elim H1.elim H.reflexivity.
  70 qed.
  71
  72 (*
  73 theorem a:\forall x.x=x\land True.
  74 [
  75 2:intros;
  76   split;
  77   [
  78     exact (refl_eq Prop x);
  79   |
  80     exact I;
  81   ]
  82 1:
  83   skip
  84 ]
  85 qed.
  86 *)
  87