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 "../legacy/coq.ma".
  18
  19 theorem pippo: \forall (A,B:Prop). A \land B \to A.
  20  intros; decompose; assumption.
  21 qed.
  22
  23 inline procedural "cic:/matita/test/prova/pippo.con".
  24
  25 alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
  26 alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
  27 alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
  28 theorem plus_comm: \forall n:nat.\forall m:nat.eq nat (plus n m) (plus m n).
  29  intros; alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
  30 apply plus_comm.
  31 qed.
  32 (*
  33 include "LAMBDA-TYPES/LambdaDelta-1/preamble.ma".
  34 alias id "ty3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3.ind#xpointer(1/1)".
  35 alias id "pc3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs/pc3.con".
  36 alias id "THead" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1/3)".
  37 alias id "T" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1)".
  38 alias id "G" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs/G.ind#xpointer(1/1)".
  39 alias id "Flat" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1/2)".
  40 alias id "Cast" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1/2)".
  41 alias id "C" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs/C.ind#xpointer(1/1)".
  42 theorem ty3_gen_cast:
  43  (\forall g:G
  44  .\forall c:C
  45   .\forall t1:T
  46    .\forall t2:T
  47     .\forall x:T
  48      .ty3 g c (THead (Flat Cast) t2 t1) x
  49       \rarr pc3 c t2 x\land ty3 g c t1 t2)
  50 .
  51 (* tactics: 80 *)
  52 intros 6 (g c t1 t2 x H).
  53 apply insert_eq;(* 6 P P P C I I 3 0 *)
  54 [apply T(* dependent *)
  55 |apply (THead (Flat Cast) t2 t1)(* dependent *)
  56 |apply (\lambda t:T.ty3 g c t x)(* dependent *)
  57 |intros 2 (y H0).
  58 alias id "ty3_ind" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3_ind.con".
  59 elim H0 using ty3_ind names 0;(* 13 P C I I I I I I I C C C I 12 3 *)
  60 [intros 11 (c0 t0 t UNUSED UNUSED u t3 UNUSED H4 H5 H6).
  61 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 *)
  62 rewrite > H7 in H4:(%) as (H8).
  63 cut (pc3 c0 t2 t3\land ty3 g c0 t1 t2) as H10;
  64 [id
  65 |apply H8.(* 1 I *)
  66 apply refl_equal(* 2 C C *)
  67 ].
  68 elim H10 using and_ind names 0.(* 5 P P C I I 3 0 *)
  69 intros 2 (H11 H12).
  70 apply conj;(* 4 C C I I *)
  71 [alias id "pc3_t" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_t.con".
  72 apply pc3_t;(* 6 P C C I C I *)
  73 [apply t3(* dependent *)
  74 |apply H11(* assumption *)
  75 |apply H5(* assumption *)
  76 ]
  77 |apply H12(* assumption *)
  78 ]
  79 |intros 3 (c0 m H1).
  80 alias id "K" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1)".
  81 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
  82 [TSort (_:nat)\rArr True
  83 |TLRef (_:nat)\rArr False
  84 |THead (_:K) (_:T) (_:T)\rArr False] as H2;
  85 [id
  86 |rewrite < H1 in \vdash (%).
  87 apply I
  88 ].
  89 clearbody H2.
  90 change in H2:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
  91 [TSort (_:nat)\rArr True
  92 |TLRef (_:nat)\rArr False
  93 |THead (_:K) (_:T) (_:T)\rArr False].
  94 elim H2 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 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
 111 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 112 [TSort (_:nat)\rArr False
 113 |TLRef (_:nat)\rArr True
 114 |THead (_:K) (_:T) (_:T)\rArr False] as H5;
 115 [id
 116 |rewrite < H4 in \vdash (%).
 117 apply I
 118 ].
 119 clearbody H5.
 120 change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 121 [TSort (_:nat)\rArr False
 122 |TLRef (_:nat)\rArr True
 123 |THead (_:K) (_:T) (_:T)\rArr False].
 124 elim H5 using False_ind names 0(* 2 C I 2 0 *)
 125 |intros 14 (c0 u t UNUSED UNUSED b t0 t3 UNUSED UNUSED t4 UNUSED UNUSED H7).
 126 alias id "F" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1)".
 127 alias id "B" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/B.ind#xpointer(1/1)".
 128 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 129 [TSort (_:nat)\rArr False
 130 |TLRef (_:nat)\rArr False
 131 |THead (k:K) (_:T) (_:T)\rArr
 132  match k in K return \lambda _:K.Prop with
 133  [Bind (_:B)\rArr True|Flat (_:F)\rArr False]] as H8;
 134 [id
 135 |rewrite < H7 in \vdash (%).
 136 apply I
 137 ].
 138 clearbody H8.
 139 change in H8:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 140 [TSort (_:nat)\rArr False
 141 |TLRef (_:nat)\rArr False
 142 |THead (k:K) (_:T) (_:T)\rArr
 143  match k in K return \lambda _:K.Prop with
 144  [Bind (_:B)\rArr True|Flat (_:F)\rArr False]].
 145 elim H8 using False_ind names 0(* 2 C I 2 0 *)
 146 |intros 10 (c0 w u UNUSED UNUSED v t UNUSED UNUSED H5).
 147 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 148 [TSort (_:nat)\rArr False
 149 |TLRef (_:nat)\rArr False
 150 |THead (k:K) (_:T) (_:T)\rArr
 151  match k in K return \lambda _:K.Prop with
 152  [Bind (_:B)\rArr False
 153  |Flat (f:F)\rArr
 154   match f in F return \lambda _:F.Prop with
 155   [Appl\rArr True|Cast\rArr False]]] as H6;
 156 [id
 157 |rewrite < H5 in \vdash (%).
 158 apply I
 159 ].
 160 clearbody H6.
 161 change in H6:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
 162 [TSort (_:nat)\rArr False
 163 |TLRef (_:nat)\rArr False
 164 |THead (k:K) (_:T) (_:T)\rArr
 165  match k in K return \lambda _:K.Prop with
 166  [Bind (_:B)\rArr False
 167  |Flat (f:F)\rArr
 168   match f in F return \lambda _:F.Prop with
 169   [Appl\rArr True|Cast\rArr False]]].
 170 elim H6 using False_ind names 0(* 2 C I 2 0 *)
 171 |intros 9 (c0 t0 t3 H1 H2 t4 UNUSED UNUSED H5).
 172 letin H6 \def (f_equal T T
 173  (\lambda e:T
 174   .match e in T return \lambda _:T.T with
 175    [TSort (_:nat)\rArr t3
 176    |TLRef (_:nat)\rArr t3
 177    |THead (_:K) (t:T) (_:T)\rArr t]) (THead (Flat Cast) t3 t0)
 178  (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
 179 letin H7 \def (f_equal T T
 180  (\lambda e:T
 181   .match e 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]) (THead (Flat Cast) t3 t0)
 185  (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
 186 cut (t3=t2\rarr pc3 c0 t2 t3\land ty3 g c0 t1 t2) as DEFINED;
 187 [id
 188 |intros 1 (H8).
 189 rewrite > H8 in H2:(%) as (UNUSED).
 190 rewrite > H8 in H1:(%) as (H12).
 191 rewrite > H8 in \vdash (%).
 192 clearbody H7.
 193 change in H7:(%) with (match THead (Flat Cast) t3 t0 in T return \lambda _:T.T with
 194  [TSort (_:nat)\rArr t0
 195  |TLRef (_:nat)\rArr t0
 196  |THead (_:K) (_:T) (t:T)\rArr t]
 197  =match THead (Flat Cast) t2 t1 in T return \lambda _:T.T with
 198   [TSort (_:nat)\rArr t0
 199   |TLRef (_:nat)\rArr t0
 200   |THead (_:K) (_:T) (t:T)\rArr t]).
 201 rewrite > H7 in H12:(%) as (H14).
 202 apply conj;(* 4 C C I I *)
 203 [alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con".
 204 apply pc3_refl(* 2 C C *)
 205 |apply H14(* assumption *)
 206 ]
 207 ].
 208 apply DEFINED.(* 1 I *)
 209 apply H6(* assumption *)
 210 ]
 211 |apply H(* assumption *)
 212 ].
 213 qed.
 214 *)
 215 (*
 216 include "nat/orders.ma".
 217
 218 theorem le_inv:
 219  \forall P:nat \to Prop
 220  .\forall p2
 221   .\forall p1
 222    .p2 <= p1 \to
 223     (p1 = p2 \to P p2) \to
 224      (\forall n1
 225       .p2 <= n1 \to
 226       (p1 = n1 \to P n1) \to
 227       p1 = S n1 \to P (S n1)) \to
 228       P p1.
 229  intros 4; elim H names 0; clear H p1; intros;
 230  [ apply H; reflexivity
 231  | apply H3; clear H3; intros;
 232    [ apply H | apply H1; clear H1; intros; subst;
 233      [ apply H2; apply H3 | ]
 234    | reflexivity
 235  ]
 236 *)