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