More updates to Fsub.

[helm.git] / helm / software / matita / contribs / POPLmark / Fsub / part1adb.ma

diff --git a/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma b/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma
index 3b0b677b77ebf348d259ff866d5961e2886b381d..019d55cc5567ed0d4a8623f71c563e6561e6f5f4 100644 (file)
--- a/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma
+++ b/helm/software/matita/contribs/POPLmark/Fsub/part1adb.ma
@@ -49,25 +49,23 @@ intros 4; elim H;
     elim b in H10;simplify in H10;destruct;exists [apply t2]
     reflexivity]
   |*:assumption]
- |simplify;apply SA_Arrow;autobatch width=4
+ |simplify;autobatch width=5 size=11
  |simplify;apply (SA_All ? ? ? ? ? (H2 ? H6 ?? H8 H9))
   [assumption
   |apply H4
-   [apply WFE_cons
-    [assumption
-    |lapply (H2 ? H6 ? H7);autobatch]
-   |change in ⊢ (???%) with (flift f 1);apply injective_flift;assumption
+   [autobatch depth=4 width=4 size=8
+   |change in ⊢ (???%) with (flift f 1);autobatch;
    |intro;cases n;simplify;intros;autobatch depth=4
-   |change in ⊢ (???%) with (flift f 1);apply incl_cons;assumption]]]
+   |change in ⊢ (???%) with (flift f 1);autobatch]]]
 qed.
 
 inverter JS_indinv for JSubtype (%?%).
 
 theorem narrowing:∀G,G1,U,P,M,N.
-  G1 ⊢ P ⊴ U → 
+  G1 ⊢ P ⊴ U →  
   (∀G2,S,T.
     G2@G1 ⊢ S ⊴ lift U (length ? G2) O →
-    G2@G1 ⊢ lift U (length ? G2) O ⊴ T \to 
+    G2@G1 ⊢ lift U (length ? G2) O ⊴ T → 
     G2@G1 ⊢ S ⊴ T) → 
   G ⊢ M ⊴ N →
   ∀l.G=l@(mk_bound true U::G1) → l@(mk_bound true P::G1) ⊢ M ⊴ N.
@@ -123,46 +121,32 @@ elim (decidable_eq_nat n (length ? l1))
  |apply H6;reflexivity]]
 qed.
 
-lemma JS_trans_prova: ∀T,G1.WFType G1 T →
-∀G,R,U,f.injective ?? f → length ? G1 ≤ length ? G → G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U.
-intros 3;elim H;clear H; try autobatch;
-  [simplify in H5;simplify in H6;elim H5 using JS_indinv;destruct;autobatch
-  |simplify in H4;inversion H4; intros; destruct; assumption
-  |simplify in H7;elim H7 using JS_indinv;intros;destruct;
+lemma JS_trans_prova: ∀T,G,R,U,f.G ⊢ R ⊴ perm T f → G ⊢ perm T f ⊴ U → G ⊢ R ⊴ U.
+intro;elim T;
+  [simplify in H;simplify in H1;elim H using JS_indinv;destruct;autobatch
+  |simplify in H1;inversion H1; intros; destruct; assumption
+  |simplify in H2;elim H2 using JS_indinv;intros;destruct;
    [autobatch
-   |simplify in H8;inversion H8;intros;destruct;
-    [apply SA_Top;autobatch;
-    |apply SA_Arrow
-     [apply (H2 ?????? H12 H);assumption
-     |apply (H4 ?????? H10 H14);assumption]]]
-  |simplify in H7;elim H7 using JS_indinv;intros;destruct;
+   |simplify in H3;inversion H3;intros;destruct;autobatch depth=4 size=7]
+  |simplify in H2;elim H2 using JS_indinv;intros;destruct;
    [autobatch
-   |simplify in H8;inversion H8;intros;destruct;
+   |simplify in H3;inversion H3;intros;destruct;
     [apply SA_Top;autobatch
     |apply SA_All
-     [apply (H2 ?????? H12 H);assumption
-     |apply H4
-      [3:simplify;apply le_S_S;assumption
-      |4:apply (narrowing (mk_bound true (perm t f)::G) G ???? H12 ? H10 [])
-       [intros;rewrite > lift_perm2 in H16;rewrite > lift_perm2 in H17;
-        rewrite > perm_compose in H16; rewrite > perm_compose in H17;
-        apply H2
-        [3:apply (trans_le ??? H6);rewrite > length_append;autobatch
-        |4:apply H16
-        |5:apply H17
-        |2:apply injective_compose;autobatch]
+     [apply (H ???? H8 H4);assumption
+     |apply H1
+      [2:apply (narrowing (mk_bound true (perm t f)::G) G ???? H8 ? H6 [])
+       [intros;rewrite > lift_perm2 in H12;rewrite > lift_perm2 in H13;
+        rewrite > perm_compose in H12; rewrite > perm_compose in H13;
+        apply H
+        [2,3:autobatch]
        |reflexivity]
-      |5:assumption
-      |2:change in ⊢ (???%) with (flift f 1);autobatch]]]]]
+      |3:assumption]]]]]
 qed.
 
 theorem JS_trans : ∀G,T,U,V.G ⊢ T ⊴ U → G ⊢ U ⊴ V → G ⊢ T ⊴ V.
 intros 4;rewrite > (perm_id ? 0) in ⊢ (???% → ??%? → ?);
-intros;apply (JS_trans_prova ????????? H H1)
-[apply G
-|rewrite < perm_id in H;autobatch
-|simplify;intros;assumption
-|apply le_n] 
+intros;autobatch;
 qed.
 
 theorem JS_narrow : ∀G1,G2,P,Q,T,U.
@@ -170,4 +154,4 @@ theorem JS_narrow : ∀G1,G2,P,Q,T,U.
                        (G2 @ (mk_bound true P :: G1)) ⊢ T ⊴ U.
 intros; apply (narrowing ? ? ? ? ? ? H1 ? H) [|autobatch]
 intros;autobatch;
-qed.
+qed.
\ No newline at end of file