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 naxiom streicherK : ∀T:Type[0].∀t:T.∀P:t = t → Type[2].P (refl ? t) → ∀p.P p.
 121
 122 ndefinition EQ: ∀A:Type[0]. equivalence_relation A.
 123  #A; napply mk_equivalence_relation
 124   [ napply eq
 125   | napply refl
 126   | #x; #y; #H; nrewrite < H; napply refl
 127   | #x; #y; #z; #Hyx; #Hxz; nrewrite < Hxz; nassumption]
 128 nqed.
 129
 130 naxiom T1 : Type[0].
 131 naxiom T2 : T1 → Type[0].
 132 naxiom t1 : T1.
 133 naxiom t2 : ∀x:T1. T2 x.
 134
 135 ninductive I2 : ∀r1:T1.T2 r1 → Type[0] ≝
 136 | i2c1 : ∀x1:T1.∀x2:T2 x1. I2 x1 x2
 137 | i2c2 : I2 t1 (t2 t1).
 138
 139 (* nlemma i2d : ∀a,b.∀x,y:I2 a b.
 140              ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
 141              ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.
 142              Type[2].
 143 #a;#b;#x;#y;
 144 napply (
 145 match x return (λr1,r2,r.
 146                  ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b.
 147                  ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with
 148   [ i2c1 x1 x2 ⇒ ?
 149   | i2c2 ⇒ ?]
 150 )
 151 [napply (match y return (λr1,r2,r.
 152                      ∀e1: x1 = r1. ∀e2: R1 T1 x1 (λz,p. T2 z) x2 r1 e1 = r2.
 153                      ∀e : R2 T1 x1 (λz,p.T2 z) x2 (λz1,p1,z2,p2. I2 z1 z2) (i2c1 x1 x2) r1 e1 r2 e2 = r. Type[2]) with
 154     [ i2c1 y1 y2 ⇒ ?
 155     | i2c2 ⇒ ? ])
 156  [#e1; #e2; #e;
 157   napply (∀P:Type[1].
 158                      (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
 159                       ∀f: R2 T1 x1 (λz,p.T2 z) x2
 160                           (λz1,p1,z2,p2.eq ?
 161                               (i2c1 (R1 ??? z1 ? (R1 ?? (λm,n.m = y1) f1 ? p1)) ?)
 162                                (*       (R2 ???? (λm1,n1,m2,n2.R1 ?? (λm,n.T2 m) ? ? f1 = y2) f2 ?
 163                                        p1 ? p2)))*)
 164 (*                            (R2 ???? (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2)
 165                                 ? (R1 ?? (λw,q.w = y1) e1 z1 p1)
 166                                 ? (R2 ????
 167                                       (λw1,q1,w2,q2.R1 ?? (λm,n.T2 m) w2 ? q1 = y2)
 168                                       e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
 169   *)                          (i2c1 y1 y2))
 170                           ? y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P)
 171                    → P);
 172   napply (∀P:Type[1].
 173                      (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
 174                       ∀f: R2 T1 x1 (λz,p.T2 z) x2
 175                           (λz1,p1,z2,p2.eq (I2 y1 y2)
 176                             (R2 T1 z1 (λw,q.T2 w) z2 (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2)
 177                                 y1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1)
 178                                 y2 (R2 T1 x1 (λw,q.w = y1) e1
 179                                              (λw1,q1,w2,q2.R1 ??? w2 w1 q1 = y2) e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
 180                             (i2c1 y1 y2))
 181                           e y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P)
 182                    → P);
 183
 184
 185 ndefinition i2d : ∀a,b.∀x,y:I2 a b.
 186                   ∀e1:a = a.∀e2:R1 T1 a (λz,p.T2 z) b a e1 = b.
 187                   ∀e: R2 T1 a (λz,p.T2 z) b (λz1,p1,z2,p2.I2 z1 z2) x a e1 b e2 = y.Type[2] ≝
 188 λa,b,x,y.
 189 match x return (λr1,r2,r.
 190                  ∀e1:r1 = a. ∀e2:R1 T1 r1 (λz,p. T2 z) r2 a e1 = b.
 191                  ∀e :R2 T1 r1 (λz,p. T2 z) r2 (λz1,p1,z2,p2. I2 z1 z2) r a e1 b e2 = y. Type[2]) with
 192   [ i2c1 x1 x2 ⇒
 193     match y return (λr1,r2,r.
 194                      ∀e1: x1 = r1. ∀e2: R1 T1 x1 (λz,p. T2 z) x2 r1 e1 = r2.
 195                      ∀e : R2 T1 x1 (λz,p.T2 z) x2 (λz1,p1,z2,p2. I2 z1 z2) (i2c1 x1 x2) r1 e1 r2 e2 = r. Type[2]) with
 196     [ i2c1 y1 y2 ⇒ λe1,e2,e.∀P:Type[1].
 197                      (∀f1:x1 = y1. ∀f2: R1 T1 x1 (λz,p.T2 z) x2 y1 f1 = y2.
 198                       ∀f: R2 T1 x1 (λz,p.T2 z) x2
 199                           (λz1,p1,z2,p2.eq (I2 y1 y2)
 200                             (R2 T1 z1 (λw,q.T2 w) z2 (λw1,q1,w2,q2.I2 w1 w2) (i2c1 z1 z2)
 201                                 y1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1)
 202                                 y2 (R2 T1 x1 (λw,q.w = y1) e1
 203                                              (λw1,q1,w2,q2.R1 ??? w2 w1 q1 = y2) e2 z1 p1 (R1 T1 x1 (λw,q.w = y1) e1 z1 p1) p2))
 204                             (i2c1 y1 y2))
 205                           e y1 f1 y2 f2 = refl (I2 y1 y2) (i2c1 y1 y2).P)
 206                    → P
 207     | i2c2 ⇒ λe1,e2,e.∀P:Type[1].P ]
 208   | i2c2 ⇒
 209     match y return (λr1,r2,r.
 210                      ∀e1: x1 = r1. ∀e2: R1 ?? (λz,p. T2 z) x2 ? e1 = r2.
 211                      ∀e : R2 ???? (λz1,p1,z2,p2. I2 z1 z2) i2c2 ? e1 ? e2 = r. Type[2]) with
 212     [ i2c1 _ _ ⇒ λe1,e2,e.∀P:Type[1].P
 213     | i2c2 ⇒ λe1,e2,e.∀P:Type[1].
 214                (∀f: R2 ????
 215                     (λz1,p1,z2,p2.eq ? i2c2 i2c2)
 216                     e ? e1 ? e2 = refl ? i2c2.P) → P ] ].
 217
 218 *)