helm/software/matita/nlibrary/logic/destruct_bb.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/equality.ma".
  16
  17 (* nlemma prova : ∀T:Type[0].∀a,b:T.∀e:a = b.
  18                ∀P:∀x,y:T.x=y→Prop.P a a (refl T a) → P a b e.
  19 #T;#a;#b;#e;#P;#H;
  20 nrewrite < e;*)
  21
  22 ndefinition R0 ≝ λT:Type[0].λt:T.t.
  23
  24 ndefinition R1 ≝ eq_rect_Type0.
  25
  26 ndefinition R2 :
  27   ∀T0:Type[0].
  28   ∀a0:T0.
  29   ∀T1:∀x0:T0. a0=x0 → Type[0].
  30   ∀a1:T1 a0 (refl ? a0).
  31   ∀T2:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0. R1 ?? T1 a1 ? p0 = x1 → Type[0].
  32   ∀a2:T2 a0 (refl ? a0) a1 (refl ? a1).
  33   ∀b0:T0.
  34   ∀e0:a0 = b0.
  35   ∀b1: T1 b0 e0.
  36   ∀e1:R1 ?? T1 a1 ? e0 = b1.
  37   T2 b0 e0 b1 e1.
  38 #T0;#a0;#T1;#a1;#T2;#a2;#b0;#e0;#b1;#e1;
  39 napply (eq_rect_Type0 ????? e1);
  40 napply (R1 ?? ? ?? e0);
  41 napply a2;
  42 nqed.
  43
  44 ndefinition R3 :
  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   ∀T3:∀x0:T0. ∀p0:a0=x0. ∀x1:T1 x0 p0.∀p1:R1 ?? T1 a1 ? p0 = x1.
  52       ∀x2:T2 x0 p0 x1 p1.R2 ???? T2 a2 x0 p0 ? p1 = x2 → Type[0].
  53   ∀a3:T3 a0 (refl ? a0) a1 (refl ? a1) a2 (refl ? a2).
  54   ∀b0:T0.
  55   ∀e0:a0 = b0.
  56   ∀b1: T1 b0 e0.
  57   ∀e1:R1 ?? T1 a1 ? e0 = b1.
  58   ∀b2: T2 b0 e0 b1 e1.
  59   ∀e2:R2 ???? T2 a2 b0 e0 ? e1 = b2.
  60   T3 b0 e0 b1 e1 b2 e2.
  61 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#b0;#e0;#b1;#e1;#b2;#e2;
  62 napply (eq_rect_Type0 ????? e2);
  63 napply (R2 ?? ? ???? e0 ? e1);
  64 napply a3;
  65 nqed.
  66
  67 (* include "nat/nat.ma".
  68
  69 ninductive nlist : nat → Type[0] ≝
  70 | nnil : nlist O
  71 | ncons : ∀n:nat.nat → nlist n → nlist (S n).
  72
  73 ninductive wrapper : Type[0] ≝
  74 | kw1 : ∀x.∀y:nlist x.wrapper
  75 | kw2 : ∀x.∀y:nlist x.wrapper.
  76
  77 nlemma fie : ∀a,b,c,d.∀e:eq ? (kw1 a b) (kw1 c d).
  78              ∀P:(∀x1.∀x2:nlist x1. ∀y1.∀y2:nlist y1.eq ? (kw1 x1 x2) (kw1 y1 y2) → Prop).
  79              P a b a b (refl ??) → P a b c d e.
  80 #a;#b;#c;#d;#e;#P;#HP;
  81 ndiscriminate e;#e0;
  82 nsubst e0;#e1;
  83 nsubst e1;#E;
  84 (* nsubst E; purtroppo al momento funziona solo nel verso sbagliato *)
  85 nrewrite > E;
  86 napply HP;
  87 nqed.*)
  88
  89 (***************)
  90
  91 ninductive I1 : Type[0] ≝
  92 | k1 : I1.
  93
  94 ninductive I2 : I1 → Type[0] ≝
  95 | k2 : ∀x.I2 x.
  96
  97 ninductive I3 : ∀x:I1.I2 x → Type[0] ≝
  98 | k3 : ∀x,y.I3 x y.
  99
 100 ninductive I4 : ∀x,y.I3 x y → Type[0] ≝
 101 | k4 : ∀x,y.∀z:I3 x y.I4 x y z.
 102
 103 (*alias id "eq" = "cic:/matita/ng/logic/equality/eq.ind(1,0,2)".
 104 alias id "refl" = "cic:/matita/ng/logic/equality/eq.con(0,1,2)".*)
 105
 106 ndefinition R4 :
 107   ∀T0:Type[0].
 108   ∀a0:T0.
 109   ∀T1:∀x0:T0. eq T0 a0 x0 → Type[0].
 110   ∀a1:T1 a0 (refl T0 a0).
 111   ∀T2:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1 → Type[0].
 112   ∀a2:T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1).
 113   ∀T3:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 114       ∀x2:T2 x0 p0 x1 p1.eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2 → Type[0].
 115   ∀a3:T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 116       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2).
 117   ∀T4:∀x0:T0. ∀p0:eq (T0 …) a0 x0. ∀x1:T1 x0 p0.∀p1:eq (T1 …) (R1 T0 a0 T1 a1 x0 p0) x1.
 118       ∀x2:T2 x0 p0 x1 p1.∀p2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 x0 p0 x1 p1) x2.
 119       ∀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.
 120       Type[0].
 121   ∀a4:T4 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 122       a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2)
 123       a3 (refl (T3 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)
 124                    a2 (refl (T2 a0 (refl T0 a0) a1 (refl (T1 a0 (refl T0 a0)) a1)) a2))
 125                    a3).
 126   ∀b0:T0.
 127   ∀e0:eq (T0 …) a0 b0.
 128   ∀b1: T1 b0 e0.
 129   ∀e1:eq (T1 …) (R1 T0 a0 T1 a1 b0 e0) b1.
 130   ∀b2: T2 b0 e0 b1 e1.
 131   ∀e2:eq (T2 …) (R2 T0 a0 T1 a1 T2 a2 b0 e0 b1 e1) b2.
 132   ∀b3: T3 b0 e0 b1 e1 b2 e2.
 133   ∀e3:eq (T3 …) (R3 T0 a0 T1 a1 T2 a2 T3 a3 b0 e0 b1 e1 b2 e2) b3.
 134   T4 b0 e0 b1 e1 b2 e2 b3 e3.
 135 #T0;#a0;#T1;#a1;#T2;#a2;#T3;#a3;#T4;#a4;#b0;#e0;#b1;#e1;#b2;#e2;#b3;#e3;
 136 napply (eq_rect_Type0 ????? e3);
 137 napply (R3 ????????? e0 ? e1 ? e2);
 138 napply a4;
 139 nqed.
 140
 141
 142 ninductive II : Type[0] ≝
 143 | kII1 : ∀x,y,z.∀w:I4 x y z.II
 144 | kII2 : ∀x,y,z.∀w:I4 x y z.II.
 145
 146 (* nlemma foo : ∀a,b,c,d,e,f,g,h. kII1 a b c d = kII2 e f g h → True.
 147 #a;#b;#c;#d;#e;#f;#g;#h;#H;
 148 ndiscriminate H;
 149 nqed. *)
 150
 151 nlemma faof : ∀a,b,c,d,e,f,g,h.∀Heq:kII1 a b c d = kII1 e f g h.
 152               ∀P:(∀a,b,c,d.kII1 a b c d = kII1 e f g h → Prop).
 153               P e f g h (refl ??) → P a b c d Heq.
 154 #a;#b;#c;#d;#e;#f;#g;#h;#Heq;#P;#HP;
 155 ndestruct;
 156 napply HP;
 157 nqed.