matita/contribs/prova.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 set "baseuri" "cic:/matita/test/prova".
  16
  17 include "LAMBDA-TYPES/LambdaDelta-1/preamble.ma".
  18 alias id "ty3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3.ind#xpointer(1/1)".
  19 alias id "pc3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs/pc3.con".
  20 alias id "THead" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1/3)".
  21 alias id "T" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1)".
  22 alias id "G" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs/G.ind#xpointer(1/1)".
  23 alias id "Flat" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1/2)".
  24 alias id "Cast" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1/2)".
  25 alias id "C" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs/C.ind#xpointer(1/1)".
  26 theorem ty3_gen_cast:
  27  (\forall g:G
  28  .\forall c:C
  29   .\forall t1:T
  30    .\forall t2:T
  31     .\forall x:T
  32      .ty3 g c (THead (Flat Cast) t2 t1) x
  33       \rarr pc3 c t2 x\land ty3 g c t1 t2)
  34 .
  35 (* tactics: 68 *)
  36 intros 6 (g c t1 t2 x H).
  37 apply insert_eq;(* 6 P P P C I I 3 0 *)
  38 [apply T(* dependent *)
  39 |apply (THead (Flat Cast) t2 t1)(* dependent *)
  40 |apply (\lambda t:T.ty3 g c t x)(* dependent *)
  41 |intros 2 (y H0).
  42 alias id "ty3_ind" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3_ind.con".
  43 elim H0 using ty3_ind names 0;(* 13 P C I I I I I I I C C C I 12 3 *)
  44 [intros 11 (c0 t0 t UNUSED UNUSED u t3 UNUSED H4 H5 H6).
  45 letin H7 \def (f_equal T T (\lambda e:T.e) u (THead (Flat Cast) t2 t1) H6).(* 6 C C C C C I *)
  46 clearbody H7.
  47 rewrite > H7 in H4:(%) as (H8).
  48 cut (pc3 c0 t2 t3\land ty3 g c0 t1 t2) as H10;
  49 [id
  50 |apply H8.(* 1 I *)
  51 apply refl_equal(* 2 C C *)
  52 ].
  53 elim H10 using and_ind names 0.(* 5 P P C I I 3 0 *)
  54 intros 2 (H11 H12).
  55 apply conj;(* 4 C C I I *)
  56 [alias id "pc3_t" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_t.con".
  57 apply pc3_t;(* 6 P C C I C I *)
  58 [apply t3(* dependent *)
  59 |apply H11(* assumption *)
  60 |apply H5(* assumption *)
  61 ]
  62 |apply H12(* assumption *)
  63 ]
  64 |intros 3 (c0 m H1).
  65 alias id "K" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1)".
  66 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
  67 [TSort (_:nat)\rArr True
  68 |TLRef (_:nat)\rArr False
  69 |THead (_:K) (_:T) (_:T)\rArr False] as H2;
  70 [id
  71 |rewrite < H1 in \vdash (%).
  72 apply I
  73 ].
  74 clearbody H2.
  75 change in H2:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
  76 [TSort (_:nat)\rArr True
  77 |TLRef (_:nat)\rArr False
  78 |THead (_:K) (_:T) (_:T)\rArr False].
  79 elim H2 using False_ind names 0(* 2 C I 2 0 *)
  80 |intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
  81 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
  82 [TSort (_:nat)\rArr False
  83 |TLRef (_:nat)\rArr True
  84 |THead (_:K) (_:T) (_:T)\rArr False] as H5;
  85 [id
  86 |rewrite < H4 in \vdash (%).
  87 apply I
  88 ].
  89 clearbody H5.
  90 change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
  91 [TSort (_:nat)\rArr False
  92 |TLRef (_:nat)\rArr True
  93 |THead (_:K) (_:T) (_:T)\rArr False].
  94 elim H5 using False_ind names 0(* 2 C I 2 0 *)
  95 |intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
  96 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
  97 [TSort (_:nat)\rArr False
  98 |TLRef (_:nat)\rArr True
  99 |THead (_:K) (_:T) (_:T)\rArr False] as H5;
 100 [id
 101 |rewrite < H4 in \vdash (%).
 102 apply I
 103 ].
 104 clearbody H5.
 105 change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 106 [TSort (_:nat)\rArr False
 107 |TLRef (_:nat)\rArr True
 108 |THead (_:K) (_:T) (_:T)\rArr False].
 109 elim H5 using False_ind names 0(* 2 C I 2 0 *)
 110 |intros 14 (c0 u t UNUSED UNUSED b t0 t3 UNUSED UNUSED t4 UNUSED UNUSED H7).
 111 alias id "F" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1)".
 112 alias id "B" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/B.ind#xpointer(1/1)".
 113 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 114 [TSort (_:nat)\rArr False
 115 |TLRef (_:nat)\rArr False
 116 |THead (k:K) (_:T) (_:T)\rArr
 117  match k in K return \lambda _:K.Prop with
 118  [Bind (_:B)\rArr True|Flat (_:F)\rArr False]] as H8;
 119 [id
 120 |rewrite < H7 in \vdash (%).
 121 apply I
 122 ].
 123 clearbody H8.
 124 change in H8:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 125 [TSort (_:nat)\rArr False
 126 |TLRef (_:nat)\rArr False
 127 |THead (k:K) (_:T) (_:T)\rArr
 128  match k in K return \lambda _:K.Prop with
 129  [Bind (_:B)\rArr True|Flat (_:F)\rArr False]].
 130 elim H8 using False_ind names 0(* 2 C I 2 0 *)
 131 |intros 10 (c0 w u UNUSED UNUSED v t UNUSED UNUSED H5).
 132 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 133 [TSort (_:nat)\rArr False
 134 |TLRef (_:nat)\rArr False
 135 |THead (k:K) (_:T) (_:T)\rArr
 136  match k in K return \lambda _:K.Prop with
 137  [Bind (_:B)\rArr False
 138  |Flat (f:F)\rArr
 139   match f in F return \lambda _:F.Prop with
 140   [Appl\rArr True|Cast\rArr False]]] as H6;
 141 [id
 142 |rewrite < H5 in \vdash (%).
 143 apply I
 144 ].
 145 clearbody H6.
 146 change in H6:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 147 [TSort (_:nat)\rArr False
 148 |TLRef (_:nat)\rArr False
 149 |THead (k:K) (_:T) (_:T)\rArr
 150  match k in K return \lambda _:K.Prop with
 151  [Bind (_:B)\rArr False
 152  |Flat (f:F)\rArr
 153   match f in F return \lambda _:F.Prop with
 154   [Appl\rArr True|Cast\rArr False]]].
 155 elim H6 using False_ind names 0(* 2 C I 2 0 *)
 156 |intros 9 (c0 t0 t3 H1 H2 t4 UNUSED UNUSED H5).
 157 letin H6 \def (f_equal T T
 158  (\lambda e:T
 159   .match e in T return \lambda _:T.T with
 160    [TSort (_:nat)\rArr t3
 161    |TLRef (_:nat)\rArr t3
 162    |THead (_:K) (t:T) (_:T)\rArr t]) (THead (Flat Cast) t3 t0)
 163  (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
 164 alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con".
 165 letin DEFINED \def (let H7 \def
 166         f_equal T T
 167         (\lambda e:T
 168          .match e in T return \lambda _:T.T with
 169           [TSort (_:nat)\rArr t0
 170           |TLRef (_:nat)\rArr t0
 171           |THead (_:K) (_:T) (t:T)\rArr t])
 172         (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5
 173  in
 174  \lambda H8:t3=t2
 175  .(let H11 \def
 176           eq_ind T t3
 177           (\lambda t:T
 178            .t0=THead (Flat Cast) t2 t1
 179             \rarr pc3 c0 t2 t\land ty3 g c0 t1 t2) H2 t2 H8
 180    in
 181    let H12 \def eq_ind T t3 (\lambda t:T.ty3 g c0 t0 t) H1 t2 H8 in
 182    eq_ind_r T t2 (\lambda t:T.pc3 c0 t2 t\land ty3 g c0 t1 t2)
 183    (let H14 \def eq_ind T t0 (\lambda t:T.ty3 g c0 t t2) H12 t1 H7 in
 184     conj (pc3 c0 t2 t2) (ty3 g c0 t1 t2) (pc3_refl c0 t2) H14) t3
 185    H8)).
 186 apply DEFINED.(* 1 I *)
 187 apply H6(* assumption *)
 188 ]
 189 |apply H(* assumption *)
 190 ].
 191 qed.
 192