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