helm/software/matita/nlibrary/logic/equality.ma

   1 (**************************************************************************)
   2 (*       ___                                                              *)
   3 (*      ||M||                                                             *)
   4 (*      ||A||       A project by Andrea Asperti                           *)
   5 (*      ||T||                                                             *)
   6 (*      ||I||       Developers:                                           *)
   7 (*      ||T||         The HELM team.                                      *)
   8 (*      ||A||         http://helm.cs.unibo.it                             *)
   9 (*      \   /                                                             *)
  10 (*       \ /        This file is distributed under the terms of the       *)
  11 (*        v         GNU General Public License Version 2                  *)
  12 (*                                                                        *)
  13 (**************************************************************************)
  14
  15 include "logic/connectives.ma".
  16 include "properties/relations.ma".
  17
  18 ninductive eq (A: Type[0]) (a: A) : A → CProp[0] ≝
  19  refl: eq A a a.
  20
  21 nlemma eq_rect_CProp0_r':
  22  ∀A.∀a,x.∀p:eq ? x a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → P x p.
  23  #A; #a; #x; #p; ncases p; #P; #H; nassumption.
  24 nqed.
  25
  26 nlemma eq_rect_CProp0_r:
  27  ∀A.∀a.∀P: ∀x:A. eq ? x a → CProp[0]. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  28  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
  29 nqed.
  30
  31 nlemma eq_ind_r :
  32  ∀A.∀a.∀P: ∀x:A. eq ? x a → Prop. P a (refl A a) → ∀x.∀p:eq ? x a.P x p.
  33  #A; #a; #P; #p; #x0; #p0; napply (eq_rect_CProp0_r' ??? p0); nassumption.
  34 nqed.
  35
  36 interpretation "leibnitz's equality" 'eq t x y = (eq t x y).
  37
  38 interpretation "leibnitz's non-equality" 'neq t x y = (Not (eq t x y)).
  39
  40 ndefinition R0 ≝ λT:Type[0].λt:T.t.
  41
  42 ndefinition R1 ≝ eq_rect_Type0.
  43
  44 ndefinition R2 :
  45   ∀T0:Type[0].
  46   ∀a0:T0.
  47   ∀T1:∀x0:T0. a0=x0 → Type[0].
  48   ∀a1:T1 a0 (refl ? a0).
  49   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
  50   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
  51   ∀b0:T0.
  52   ∀e0:a0 = b0.
  53   ∀b1: T1 b0 e0.
  54   ∀e1:R1 ?? T1 a1 ? e0 = b1.
  55   T2 b0 e0 b1 e1.
  56 #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
  57 napply (eq_rect_Type0 ????? e1);
  58 napply (R1 ?? ? ?? e0);
  59 napply a2;
  60 nqed.
  61
  62 ndefinition R3 :
  63   ∀T0:Type[0].
  64   ∀a0:T0.
  65   ∀T1:∀x0:T0. a0=x0 → Type[0].
  66   ∀a1:T1 a0 (refl ? a0).
  67   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
  68   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
  69   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
  70       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
  71   ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
  72   ∀b0:T0.
  73   ∀e0:a0 = b0.
  74   ∀b1: T1 b0 e0.
  75   ∀e1:R1 ?? T1 a1 ? e0 = b1.
  76   ∀b2: T2 b0 e0 b1 e1.
  77   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
  78   T3 b0 e0 b1 e1 b2 e2.
  79 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
  80 napply (eq_rect_Type0 ????? e2);
  81 napply (R2 ?? ? ???? e0 ? e1);
  82 napply a3;
  83 nqed.
  84
  85 ndefinition R4 :
  86   ∀T0:Type[0].
  87   ∀a0:T0.
  88   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
  89   ∀a1:T1 a0 (refl T0 a0).
  90   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
  91   ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
  92   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
  93       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
  94   ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
  95       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
  96   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
  97       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
  98       ∀x3:T3 x0 p0 x1 p1 x2 p2.∀p3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 x0 p0 x1 p1 x2 p2) x3.
  99       Type[0].
 100   ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 101       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
 102       a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 103                    a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
 104                    a3).
 105   ∀b0:T0.
 106   ∀e0:eq (T0 …) a0 b0.
 107   ∀b1: T1 b0 e0.
 108   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 109   ∀b2: T2 b0 e0 b1 e1.
 110   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 111   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 112   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 113   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 114 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
 115 napply (eq_rect_Type0 ????? e3);
 116 napply (R3 ????????? e0 ? e1 ? e2);
 117 napply a4;
 118 nqed.
 119
 120 ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
 121  #A; napply mk_equivalence_relation
 122   [ napply eq
 123   | napply refl
 124   | #x; #y; #H; nrewrite < H; napply refl
 125   | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]
 126 nqed.