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 eq (A:Type[3]) (x:A) : A → Prop ≝
  18     refl_eq : eq A x x.
  19
  20 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
  21
  22 nlemma eq_rect_r:
  23  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → Type. P a (refl_eq A a) → P x p.
  24  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
  25 nqed.
  26
  27 nlemma eq_ind_r :
  28  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
  29  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_r ? ? ? p0); nassumption.
  30 nqed.
  31
  32 (*
  33 nlemma eq_ind_r :
  34  ∀A.∀a.∀P: ∀x:A. x = a → Prop. P a (refl_eq A a) → ∀x.∀p:eq ? x a.P x p.
  35  #A; #a; #P; #p; #x0; #p0; ngeneralize in match p;
  36 ncases p0; #Heq; nassumption.
  37 nqed.
  38 *)
  39
  40 ntheorem rewrite_l: ∀A:Type[3].∀x.∀P:A → Prop. P x → ∀y. x = y → P y.
  41 #A; #x; #P; #Hx; #y; #Heq;ncases Heq;nassumption.
  42 nqed.
  43
  44 ntheorem sym_eq: ∀A:Type[3].∀x,y:A. x = y → y = x.
  45 #A; #x; #y; #Heq; napply (rewrite_l A x (λz.z=x));
  46 ##[ @; ##| nassumption; ##]
  47 nqed.
  48
  49 ntheorem rewrite_r: ∀A:Type[3].∀x.∀P:A → Prop. P x → ∀y. y = x → P y.
  50 #A; #x; #P; #Hx; #y; #Heq;ncases (sym_eq ? ? ?Heq);nassumption.
  51 nqed.
  52
  53 ntheorem eq_coerc: ∀A,B:Type[2].A→(A=B)→B.
  54 #A; #B; #Ha; #Heq;nelim Heq; nassumption.
  55 nqed.