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