X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2Fprova.ma;h=a0cab98679b4c713b6857a62b473e7ef8d997c5b;hb=fdda444a05fe4c68c925cd94e4e3a38c93d0c35f;hp=b975eaffbb360e8cf325df22bf4f9671d281beb1;hpb=e63beeff229680e6f6933fc7095e0910dbb56209;p=helm.git

diff --git a/helm/software/matita/contribs/prova.ma b/helm/software/matita/contribs/prova.ma
index b975eaffb..a0cab9867 100644
--- a/helm/software/matita/contribs/prova.ma
+++ b/helm/software/matita/contribs/prova.ma
@@ -14,6 +14,22 @@
 
 set "baseuri" "cic:/matita/test/prova".
 
+include "../legacy/coq.ma".
+
+theorem pippo: \forall (A,B:Prop). A \land B \to A.
+ intros; decompose; assumption.
+qed.  
+
+inline procedural "cic:/matita/test/prova/pippo.con".
+
+alias id "plus" = "cic:/Coq/Init/Peano/plus.con".
+alias id "nat" = "cic:/Coq/Init/Datatypes/nat.ind#xpointer(1/1)".
+alias id "eq" = "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1)".
+theorem plus_comm: \forall n:nat.\forall m:nat.eq nat (plus n m) (plus m n).
+ intros; alias id "plus_comm" = "cic:/Coq/Arith/Plus/plus_comm.con".
+apply plus_comm.
+qed.
+(*
 include "LAMBDA-TYPES/LambdaDelta-1/preamble.ma".
 alias id "ty3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3.ind#xpointer(1/1)".
 alias id "pc3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs/pc3.con".
@@ -32,7 +48,7 @@ theorem ty3_gen_cast:
      .ty3 g c (THead (Flat Cast) t2 t1) x
       \rarr pc3 c t2 x\land ty3 g c t1 t2)
 .
-(* tactics: 68 *)
+(* tactics: 80 *)
 intros 6 (g c t1 t2 x H).
 apply insert_eq;(* 6 P P P C I I 3 0 *)
 [apply T(* dependent *)
@@ -43,7 +59,6 @@ alias id "ty3_ind" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3_ind.co
 elim H0 using ty3_ind names 0;(* 13 P C I I I I I I I C C C I 12 3 *)
 [intros 11 (c0 t0 t UNUSED UNUSED u t3 UNUSED H4 H5 H6).
 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 *)
-clearbody H7.
 rewrite > H7 in H4:(%) as (H8).
 cut (pc3 c0 t2 t3\land ty3 g c0 t1 t2) as H10;
 [id
@@ -161,32 +176,61 @@ letin H6 \def (f_equal T T
    |TLRef (_:nat)\rArr t3
    |THead (_:K) (t:T) (_:T)\rArr t]) (THead (Flat Cast) t3 t0)
  (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
-alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con".
-letin DEFINED \def (let H7 \def 
-        f_equal T T
-        (\lambda e:T
-         .match e in T return \lambda _:T.T with 
-          [TSort (_:nat)\rArr t0
-          |TLRef (_:nat)\rArr t0
-          |THead (_:K) (_:T) (t:T)\rArr t])
-        (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5
- in
- \lambda H8:t3=t2
- .(let H11 \def 
-          eq_ind T t3
-          (\lambda t:T
-           .t0=THead (Flat Cast) t2 t1
-            \rarr pc3 c0 t2 t\land ty3 g c0 t1 t2) H2 t2 H8
-   in
-   let H12 \def eq_ind T t3 (\lambda t:T.ty3 g c0 t0 t) H1 t2 H8 in
-   eq_ind_r T t2 (\lambda t:T.pc3 c0 t2 t\land ty3 g c0 t1 t2)
-   (let H14 \def eq_ind T t0 (\lambda t:T.ty3 g c0 t t2) H12 t1 H7 in
-    conj (pc3 c0 t2 t2) (ty3 g c0 t1 t2) (pc3_refl c0 t2) H14) t3
-   H8)).
+letin H7 \def (f_equal T T
+ (\lambda e:T
+  .match e in T return \lambda _:T.T with 
+   [TSort (_:nat)\rArr t0
+   |TLRef (_:nat)\rArr t0
+   |THead (_:K) (_:T) (t:T)\rArr t]) (THead (Flat Cast) t3 t0)
+ (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
+cut (t3=t2\rarr pc3 c0 t2 t3\land ty3 g c0 t1 t2) as DEFINED;
+[id
+|intros 1 (H8).
+rewrite > H8 in H2:(%) as (UNUSED).
+rewrite > H8 in H1:(%) as (H12).
+rewrite > H8 in \vdash (%).
+clearbody H7.
+change in H7:(%) with (match THead (Flat Cast) t3 t0 in T return \lambda _:T.T with 
+ [TSort (_:nat)\rArr t0
+ |TLRef (_:nat)\rArr t0
+ |THead (_:K) (_:T) (t:T)\rArr t]
+ =match THead (Flat Cast) t2 t1 in T return \lambda _:T.T with 
+  [TSort (_:nat)\rArr t0
+  |TLRef (_:nat)\rArr t0
+  |THead (_:K) (_:T) (t:T)\rArr t]).
+rewrite > H7 in H12:(%) as (H14).
+apply conj;(* 4 C C I I *)
+[alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con".
+apply pc3_refl(* 2 C C *)
+|apply H14(* assumption *)
+]
+].
 apply DEFINED.(* 1 I *)
 apply H6(* assumption *)
 ]
 |apply H(* assumption *)
 ].
 qed.
+*)
+(*
+include "nat/orders.ma".
 
+theorem le_inv:
+ \forall P:nat \to Prop
+ .\forall p2
+  .\forall p1
+   .p2 <= p1 \to
+    (p1 = p2 \to P p2) \to 
+     (\forall n1
+      .p2 <= n1 \to 
+      (p1 = n1 \to P n1) \to 
+      p1 = S n1 \to P (S n1)) \to 
+      P p1.
+ intros 4; elim H names 0; clear H p1; intros;
+ [ apply H; reflexivity
+ | apply H3; clear H3; intros;
+   [ apply H | apply H1; clear H1; intros; subst;
+     [ apply H2; apply H3 | ]
+   | reflexivity
+ ]
+*)