helm/software/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 include "higher_order_defs/relations.ma".
  16
  17 inductive eq (A:Type) (x:A) : A \to Prop \def
  18     refl_eq : eq A x x.
  19
  20 (*CSC: the URI must disappear: there is a bug now *)
  21 interpretation "leibnitz's equality"
  22    'eq t x y = (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y).
  23 (*CSC: the URI must disappear: there is a bug now *)
  24 interpretation "leibnitz's non-equality"
  25   'neq t x y = (cic:/matita/logic/connectives/Not.con
  26     (cic:/matita/logic/equality/eq.ind#xpointer(1/1) t x y)).
  27
  28 theorem eq_rect':
  29  \forall A. \forall x:A. \forall P: \forall y:A. x=y \to Type.
  30   P ? (refl_eq ? x) \to \forall y:A. \forall p:x=y. P y p.
  31  intros.
  32  exact
  33   (match p1 return \lambda y. \lambda p.P y p with
  34     [refl_eq \Rightarrow p]).
  35 qed.
  36
  37 variant reflexive_eq : \forall A:Type. reflexive A (eq A)
  38 \def refl_eq.
  39 (* simplify.intros.apply refl_eq. *)
  40
  41 theorem symmetric_eq: \forall A:Type. symmetric A (eq A).
  42 unfold symmetric.intros.elim H. apply refl_eq.
  43 qed.
  44
  45 variant sym_eq : \forall A:Type.\forall x,y:A. x=y  \to y=x
  46 \def symmetric_eq.
  47
  48 theorem transitive_eq : \forall A:Type. transitive A (eq A).
  49 unfold transitive.intros.elim H1.assumption.
  50 qed.
  51
  52 variant trans_eq : \forall A:Type.\forall x,y,z:A. x=y  \to y=z \to x=z
  53 \def transitive_eq.
  54
  55 theorem eq_elim_r:
  56  \forall A:Type.\forall x:A. \forall P: A \to Prop.
  57    P x \to \forall y:A. y=x \to P y.
  58 intros. elim (sym_eq ? ? ? H1).assumption.
  59 qed.
  60
  61 theorem eq_elim_r':
  62  \forall A:Type.\forall x:A. \forall P: A \to Set.
  63    P x \to \forall y:A. y=x \to P y.
  64 intros. elim (sym_eq ? ? ? H).assumption.
  65 qed.
  66
  67 theorem eq_elim_r'':
  68  \forall A:Type.\forall x:A. \forall P: A \to Type.
  69    P x \to \forall y:A. y=x \to P y.
  70 intros. elim (sym_eq ? ? ? H).assumption.
  71 qed.
  72
  73 theorem eq_f: \forall  A,B:Type.\forall f:A\to B.
  74 \forall x,y:A. x=y \to f x = f y.
  75 intros.elim H.apply refl_eq.
  76 qed.
  77
  78 theorem eq_f': \forall  A,B:Type.\forall f:A\to B.
  79 \forall x,y:A. x=y \to f y = f x.
  80 intros.elim H.apply refl_eq.
  81 qed.
  82
  83 (*  *)
  84 coercion sym_eq.
  85 coercion eq_f.
  86 (* *)
  87
  88 default "equality"
  89  cic:/matita/logic/equality/eq.ind
  90  cic:/matita/logic/equality/sym_eq.con
  91  cic:/matita/logic/equality/transitive_eq.con
  92  cic:/matita/logic/equality/eq_ind.con
  93  cic:/matita/logic/equality/eq_elim_r.con
  94  cic:/matita/logic/equality/eq_rec.con
  95  cic:/matita/logic/equality/eq_elim_r'.con
  96  cic:/matita/logic/equality/eq_rect.con
  97  cic:/matita/logic/equality/eq_elim_r''.con
  98  cic:/matita/logic/equality/eq_f.con
  99 (* *)
 100  cic:/matita/logic/equality/eq_OF_eq.con.
 101 (* *)
 102 (*
 103  cic:/matita/logic/equality/eq_f'.con. (* \x.sym (eq_f x) *)
 104  *)
 105
 106 theorem eq_f2: \forall  A,B,C:Type.\forall f:A\to B \to C.
 107 \forall x1,x2:A. \forall y1,y2:B.
 108 x1=x2 \to y1=y2 \to f x1 y1 = f x2 y2.
 109 intros.elim H1.elim H.reflexivity.
 110 qed.
 111
 112 definition comp \def
 113  \lambda A.
 114   \lambda x,y,y':A.
 115    \lambda eq1:x=y.
 116     \lambda eq2:x=y'.
 117      eq_ind ? ? (\lambda a.a=y') eq2 ? eq1.
 118
 119 lemma trans_sym_eq:
 120  \forall A.
 121   \forall x,y:A.
 122    \forall u:x=y.
 123     comp ? ? ? ? u u = refl_eq ? y.
 124  intros.
 125  apply (eq_rect' ? ? ? ? ? u).
 126  reflexivity.
 127 qed.
 128
 129 definition nu \def
 130  \lambda A.
 131   \lambda H: \forall x,y:A. decidable (x=y).
 132    \lambda x,y. \lambda p:x=y.
 133      match H x y with
 134       [ (or_introl p') \Rightarrow p'
 135       | (or_intror K) \Rightarrow False_ind ? (K p) ].
 136
 137 theorem nu_constant:
 138  \forall A.
 139   \forall H: \forall x,y:A. decidable (x=y).
 140    \forall x,y:A.
 141     \forall u,v:x=y.
 142      nu ? H ? ? u = nu ? H ? ? v.
 143  intros.
 144  unfold nu.
 145  unfold decidable in H.
 146  apply (Or_ind' ? ? ? ? ? (H x y)); simplify.
 147   intro; reflexivity.
 148   intro; elim (q u).
 149 qed.
 150
 151 definition nu_inv \def
 152  \lambda A.
 153   \lambda H: \forall x,y:A. decidable (x=y).
 154    \lambda x,y:A.
 155     \lambda v:x=y.
 156      comp ? ? ? ? (nu ? H ? ? (refl_eq ? x)) v.
 157
 158 theorem nu_left_inv:
 159  \forall A.
 160   \forall H: \forall x,y:A. decidable (x=y).
 161    \forall x,y:A.
 162     \forall u:x=y.
 163      nu_inv ? H ? ? (nu ? H ? ? u) = u.
 164  intros.
 165  apply (eq_rect' ? ? ? ? ? u).
 166  unfold nu_inv.
 167  apply trans_sym_eq.
 168 qed.
 169
 170 theorem eq_to_eq_to_eq_p_q:
 171  \forall A. \forall x,y:A.
 172   (\forall x,y:A. decidable (x=y)) \to
 173    \forall p,q:x=y. p=q.
 174  intros.
 175  rewrite < (nu_left_inv ? H ? ? p).
 176  rewrite < (nu_left_inv ? H ? ? q).
 177  elim (nu_constant ? H ? ? q).
 178  reflexivity.
 179 qed.
 180
 181 (*CSC: alternative proof that does not pollute the environment with
 182   technical lemmata. Unfortunately, it is a pain to do without proper
 183   support for let-ins.
 184 theorem eq_to_eq_to_eq_p_q:
 185  \forall A. \forall x,y:A.
 186   (\forall x,y:A. decidable (x=y)) \to
 187    \forall p,q:x=y. p=q.
 188 intros.
 189 letin nu \def
 190  (\lambda x,y. \lambda p:x=y.
 191    match H x y with
 192     [ (or_introl p') \Rightarrow p'
 193     | (or_intror K) \Rightarrow False_ind ? (K p) ]).
 194 cut
 195  (\forall q:x=y.
 196    eq_ind ? ? (\lambda z. z=y) (nu ? ? q) ? (nu ? ? (refl_eq ? x))
 197    = q).
 198 focus 8.
 199  clear q; clear p.
 200  intro.
 201  apply (eq_rect' ? ? ? ? ? q);
 202  fold simplify (nu ? ? (refl_eq ? x)).
 203  generalize in match (nu ? ? (refl_eq ? x)); intro.
 204  apply
 205   (eq_rect' A x
 206    (\lambda y. \lambda u.
 207     eq_ind A x (\lambda a.a=y) u y u = refl_eq ? y)
 208    ? x H1).
 209  reflexivity.
 210 unfocus.
 211 rewrite < (Hcut p); fold simplify (nu ? ? p).
 212 rewrite < (Hcut q); fold simplify (nu ? ? q).
 213 apply (Or_ind' (x=x) (x \neq x)
 214  (\lambda p:decidable (x=x). eq_ind A x (\lambda z.z=y) (nu x y p) x
 215    ([\lambda H1.eq A x x]
 216     match p with
 217     [(or_introl p') \Rightarrow p'
 218     |(or_intror K) \Rightarrow False_ind (x=x) (K (refl_eq A x))]) =
 219    eq_ind A x (\lambda z.z=y) (nu x y q) x
 220     ([\lambda H1.eq A x x]
 221      match p with
 222     [(or_introl p') \Rightarrow p'
 223     |(or_intror K) \Rightarrow False_ind (x=x) (K (refl_eq A x))]))
 224  ? ? (H x x)).
 225 intro; simplify; reflexivity.
 226 intro q; elim (q (refl_eq ? x)).
 227 qed.
 228 *)
 229
 230 (*
 231 theorem a:\forall x.x=x\land True.
 232 [
 233 2:intros;
 234   split;
 235   [
 236     exact (refl_eq Prop x);
 237   |
 238     exact I;
 239   ]
 240 1:
 241   skip
 242 ]
 243 qed.
 244 *)
 245