]> matita.cs.unibo.it Git - helm.git/commitdiff
Updated, proofs are now about 750 lines.
authorWilmer Ricciotti <ricciott@cs.unibo.it>
Wed, 12 Sep 2007 14:30:28 +0000 (14:30 +0000)
committerWilmer Ricciotti <ricciott@cs.unibo.it>
Wed, 12 Sep 2007 14:30:28 +0000 (14:30 +0000)
matita/library/Fsub/defn.ma
matita/library/Fsub/part1a.ma
matita/library/Fsub/util.ma

index 3264ed5aabbfc536db4df5fe0c0471beb13eb895..a56b38eafc977ebae26ff39dacbf04460925767b 100644 (file)
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/Fsub/defn".
-include "logic/equality.ma".
-include "nat/nat.ma".
-include "datatypes/bool.ma".
-include "nat/compare.ma".
-include "list/list.ma".
 include "Fsub/util.ma".
 
 (*** representation of Fsub types ***)  
@@ -27,16 +22,7 @@ inductive Typ : Set \def
   | Top : Typ                     (* maximum type *)
   | Arrow : Typ \to Typ \to Typ   (* functions *) 
   | Forall : Typ \to Typ \to Typ. (* universal type *)
-  
-(*** representation of Fsub terms ***)
-inductive Term : Set \def
-  | Var : nat \to Term            (* variable *)
-  | Free : nat \to Term          (* free name *)
-  | Abs : Typ \to Term \to Term   (* abstraction *)
-  | App : Term \to Term \to Term  (* function application *)
-  | TAbs : Typ \to Term \to Term  (* type abstraction *)
-  | TApp : Term \to Typ \to Term. (* type application *)
-  
+
 (* representation of bounds *)
 
 record bound : Set \def { 
@@ -45,14 +31,6 @@ record bound : Set \def {
                           btype  : Typ      (* type to which the name is bound *)
                         }.
                
-(* representation of Fsub typing environments *)
-(*definition Env \def (list bound).
-definition Empty \def (nil bound).
-definition Cons \def \lambda G,X,T.((mk_bound false X T) :: G).
-definition TCons \def \lambda G,X,T.((mk_bound true X T) :: G).
-
-definition env_append : Env \to Env \to Env \def \lambda G,H.(H @ G). *)
-  
 (*** Various kinds of substitution, not all will be used probably ***)
 
 (* substitutes i-th dangling index in type T with type U *)
@@ -66,49 +44,6 @@ let rec subst_type_nat T U i \def
     | (Arrow T1 T2) \Rightarrow (Arrow (subst_type_nat T1 U i) (subst_type_nat T2 U i))
     | (Forall T1 T2) \Rightarrow (Forall (subst_type_nat T1 U i) (subst_type_nat T2 U (S i))) ].
 
-(* substitutes 0-th dangling index in type T with type U *)
-(*let rec subst_type_O T U  \def subst_type_nat T U O.*) 
-
-(* substitutes 0-th dangling index in term t with term u *)
-(*let rec subst_term_O t u  \def
-  let rec aux t0 i \def
-    match t0 with
-    [ (Var n) \Rightarrow match (eqb n i) with
-      [ true \Rightarrow u
-      | false \Rightarrow t0]
-    | (Free X) \Rightarrow t0
-    | (Abs T1 t1) \Rightarrow (Abs T1 (aux t1 (S i)))
-    | (App t1 t2) \Rightarrow (App (aux t1 i) (aux t2 i))
-    | (TAbs T1 t1) \Rightarrow (TAbs T1 (aux t1 (S i)))
-    | (TApp t1 T1) \Rightarrow (TApp (aux t1 i) T1) ]
-  in aux t O.
-
-(* substitutes 0-th dangling index in term T, which shall be a TVar,
-   with type U *)
-let rec subst_term_tO t T  \def
-  let rec aux t0 i \def
-    match t0 with
-    [ (Var n) \Rightarrow t0 
-    | (Free X) \Rightarrow t0
-    | (Abs T1 t1) \Rightarrow (Abs (subst_type_nat T1 T i) (aux t1 (S i)))
-    | (App t1 t2) \Rightarrow (App (aux t1 i) (aux t2 i))
-    | (TAbs T1 t1) \Rightarrow (TAbs (subst_type_nat T1 T i) (aux t1 (S i)))
-    | (TApp t1 T1) \Rightarrow (TApp (aux t1 i) (subst_type_nat T1 T i)) ]
-  in aux t O.
-
-(* substitutes (TFree X) in type T with type U *)
-let rec subst_type_tfree_type T X U on T \def
-  match T with
-    [ (TVar n) \Rightarrow T
-    | (TFree Y) \Rightarrow match (eqb X Y) with
-      [ true \Rightarrow U
-      | false \Rightarrow T ]
-    | Top \Rightarrow T
-    | (Arrow T1 T2) \Rightarrow (Arrow (subst_type_tfree_type T1 X U) 
-                                       (subst_type_tfree_type T2 X U))
-    | (Forall T1 T2) \Rightarrow (Forall (subst_type_tfree_type T1 X U) 
-                                       (subst_type_tfree_type T2 X U)) ].*)
-            
 (*** height of T's syntactic tree ***)
 
 let rec t_len T \def
@@ -119,33 +54,12 @@ let rec t_len T \def
      |(Arrow T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))
      |(Forall T1 T2) \Rightarrow (S (max (t_len T1) (t_len T2)))].
 
-definition head \def
-  \lambda G:(list bound).match G with
-    [ nil \Rightarrow (mk_bound false O Top)
-    | (cons b H) \Rightarrow b].
-
-definition head_nat \def
-  \lambda G:(list nat).match G with
-    [ nil \Rightarrow O
-    | (cons n H) \Rightarrow n].
-
 (*** definitions about lists ***)
 
-(*(* var binding is in env judgement *)                
-definition var_bind_in_env : bound \to (list bound) \to Prop \def
-  \lambda b,G.(in_list bound b G).*)
-
 definition fv_env : (list bound) \to (list nat) \def
   \lambda G.(map ? ? (\lambda b.match b with
       [(mk_bound B X T) \Rightarrow X]) G).
 
-(*(* variable is in env judgement *)              
-definition var_in_env : nat \to (list bound) \to Prop \def
-  \lambda x,G.(in_list nat x (fv_env G)).
-  
-definition var_type_in_env : nat \to (list bound) \to Prop \def
-  \lambda x,G.\exists T.(var_bind_in_env (mk_bound true x T) G).*)
-
 let rec fv_type T \def
   match T with
     [(TVar n) \Rightarrow []
@@ -238,81 +152,33 @@ notation "hvbox(|T|)"
 interpretation "type length" 'tlen T =
   (cic:/matita/Fsub/defn/t_len.con T).  
 
-notation > "hvbox(x ∈ l)"
-  non associative with precedence 30 for @{ 'inlist $x $l }.
-notation < "hvbox(x \nbsp ∈ \nbsp l)"
-  non associative with precedence 30 for @{ 'inlist $x $l }.
-interpretation "item in list" 'inlist x l =
-  (cic:/matita/Fsub/util/in_list.ind#xpointer(1/1) _ x l).
-  
 notation "hvbox(!X ⊴ T)"
   non associative with precedence 60 for @{ 'subtypebound $X $T }.
 interpretation "subtyping bound" 'subtypebound X T =
   (cic:/matita/Fsub/defn/bound.ind#xpointer(1/1/1) true X T).  
 
-(*notation < "hvbox(e break ⊢ ta \nbsp 'V' \nbsp tb (= \above \alpha))" 
-  non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
-notation > "hvbox(e break ⊢ ta 'Fall' break tb)" 
-  non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
-notation "hvbox(e break ⊢ ta \lessdot break tb)" 
-  non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.*)  
-
 (****** PROOFS ********)
 
-(*lemma subst_O_nat : \forall T,U.((subst_type_O T U) = T[#O↦U]).
-intros;elim T;simplify;reflexivity;
-qed.*)
-
 (*** theorems about lists ***)
 
-(* FIXME: these definitions shouldn't be part of the poplmark challenge
-   - use destruct instead, when hopefully it will get fixed... *) 
-
-lemma inj_head : \forall h1,h2:bound.\forall t1,t2:(list bound).
-                 (h1::t1 = h2::t2) \to h1 = h2.
-intros.
-lapply (eq_f ? ? head ? ? H).simplify in Hletin.assumption.
-qed.
-
-lemma inj_head_nat : \forall h1,h2:nat.\forall t1,t2:(list nat).
-                 (h1::t1 = h2::t2) \to (h1 = h2).
-intros.
-lapply (eq_f ? ? head_nat ? ? H).simplify in Hletin.assumption.
-qed.
-
-lemma inj_tail : \forall A.\forall h1,h2:A.\forall t1,t2:(list A).
-                 ((h1::t1) = (h2::t2)) \to (t1 = t2).
-intros.lapply (eq_f ? ? (tail ?) ? ? H).simplify in Hletin.assumption.
-qed.
-
-(* end of fixme *) 
-
 lemma boundinenv_natinfv : \forall x,G.
                               (\exists B,T.(in_list ? (mk_bound B x T) G)) \to
                               (in_list ? x (fv_env G)).
 intros 2;elim G
   [elim H;elim H1;lapply (in_list_nil ? ? H2);elim Hletin
-  |elim H1;elim H2;inversion H3
-     [intros;rewrite < H4;simplify;apply in_Base
-     |intros;elim a3;simplify;apply in_Skip;
-      lapply (inj_tail ? ? ? ? ? H7);rewrite > Hletin in H;apply H;
-      apply ex_intro
-        [apply a
-        |apply ex_intro
-           [apply a1
-           |rewrite > H6;assumption]]]]
+  |elim H1;elim H2;elim (in_cons_case ? ? ? ? H3)
+     [rewrite < H4;simplify;apply in_Base
+     |elim H4;elim t;simplify;apply in_Skip2;apply H;apply (ex_intro ? ? a);
+      apply (ex_intro ? ? a1);assumption]]
 qed.
 
 lemma nat_in_list_case : \forall G,H,n.(in_list nat n (H @ G)) \to 
                                (in_list nat n G) \lor (in_list nat n H).
 intros 3.elim H
   [simplify in H1;left;assumption
-  |simplify in H2;inversion H2
-    [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite > Hletin;
-     right;apply in_Base
-    |intros;lapply (inj_tail ? ? ? ? ? H6);rewrite < Hletin in H3;
-     rewrite > H5 in H1;lapply (H1 H3);elim Hletin1
-       [left;assumption|right;apply in_Skip;assumption]]]
+  |simplify in H2;elim (in_cons_case ? ? ? ? H2)
+    [right;rewrite > H3;apply in_Base
+    |elim H3;elim (H1 H5) [left;assumption|right;apply in_Skip2;assumption]]]
 qed.
 
 lemma natinG_or_inH_to_natinGH : \forall G,H,n.
@@ -321,7 +187,7 @@ lemma natinG_or_inH_to_natinGH : \forall G,H,n.
 intros.elim H1
   [elim H
      [simplify;assumption
-     |simplify;apply in_Skip;assumption]
+     |simplify;apply in_Skip2;assumption]
   |generalize in match H2;elim H2
      [simplify;apply in_Base
      |lapply (H4 H3);simplify;apply in_Skip;assumption]]
@@ -331,19 +197,12 @@ lemma natinfv_boundinenv : \forall x,G.(in_list ? x (fv_env G)) \to
                               \exists B,T.(in_list ? (mk_bound B x T) G).
 intros 2;elim G 0
   [simplify;intro;lapply (in_list_nil ? ? H);elim Hletin
-  |intros 3;elim t;simplify in H1;inversion H1
-     [intros;rewrite < H2;simplify;apply ex_intro
-        [apply b
-        |apply ex_intro
-           [apply t1
-           |lapply (inj_head_nat ? ? ? ? H3);rewrite > H2;rewrite < Hletin;
-            apply in_Base]]
-     |intros;lapply (inj_tail ? ? ? ? ? H5);rewrite < Hletin in H2;
-      rewrite < H4 in H2;lapply (H H2);elim Hletin1;elim H6;apply ex_intro
-        [apply a2
-        |apply ex_intro
-           [apply a3
-           |apply in_Skip;rewrite < H4;assumption]]]]
+  |intros 3;elim t;simplify in H1;elim (in_cons_case ? ? ? ? H1)
+     [rewrite < H2;apply (ex_intro ? ? b);apply (ex_intro ? ? t1);apply in_Base
+     |elim H2;elim (H H4);elim H5;apply (ex_intro ? ? a);
+      apply (ex_intro ? ? a1);apply in_Skip
+        [assumption
+        |intro;destruct H7;elim (H3 Hcut1)]]]
 qed.
 
 theorem varinT_varinT_subst : \forall X,Y,T.
@@ -375,10 +234,8 @@ qed.
 
 lemma incl_nat_cons : \forall x,l1,l2.
                   (incl nat l1 l2) \to (incl nat (x :: l1) (x :: l2)).
-intros.unfold in H.unfold.intros.inversion H1
-  [intros;lapply (inj_head_nat ? ? ? ? H3);rewrite > Hletin;apply in_Base
-  |intros;apply in_Skip;apply H;lapply (inj_tail ? ? ? ? ? H5);rewrite > Hletin;
-   assumption]
+intros.unfold in H.unfold.intros.elim (in_cons_case ? ? ? ? H1)
+  [rewrite > H2;apply in_Base|elim H2;apply in_Skip2;apply (H ? H4)]
 qed.
 
 lemma WFT_env_incl : \forall G,T.(WFType G T) \to
@@ -389,9 +246,8 @@ intros 3.elim H
   |apply WFT_Arrow [apply (H2 ? H6)|apply (H4 ? H6)]
   |apply WFT_Forall 
      [apply (H2 ? H6)
-     |intros;apply H4
+     |intros;apply (H4 ? ? H8)
         [unfold;intro;apply H7;apply(H6 ? H9)
-        |assumption
         |simplify;apply (incl_nat_cons ? ? ? H6)]]]
 qed.
 
@@ -399,8 +255,7 @@ lemma fv_env_extends : \forall H,x,B,C,T,U,G.
                           (fv_env (H @ ((mk_bound B x T) :: G))) = 
                           (fv_env (H @ ((mk_bound C x U) :: G))).
 intros;elim H
-  [simplify;reflexivity
-  |elim t;simplify;rewrite > H1;reflexivity]
+  [simplify;reflexivity|elim t;simplify;rewrite > H1;reflexivity]
 qed.
 
 lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y.
@@ -408,26 +263,19 @@ lemma lookup_env_extends : \forall G,H,B,C,D,T,U,V,x,y.
             (y \neq x) \to
             (in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G))).
 intros 10;elim H
-  [simplify in H1;(*FIXME*)generalize in match H1;intro;inversion H1
-     [intros;lapply (inj_head ? ? ? ? H5);rewrite < H4 in Hletin;
-      destruct Hletin;absurd (y = x) [symmetry;assumption|assumption]
-     |intros;simplify;lapply (inj_tail ? ? ? ? ? H7);rewrite > Hletin;
-      apply in_Skip;assumption]
-  |(*FIXME*)generalize in match H2;intro;inversion H2
-     [intros;simplify in H6;lapply (inj_head ? ? ? ? H6);rewrite > Hletin;
-      simplify;apply in_Base
-     |simplify;intros;lapply (inj_tail ? ? ? ? ? H8);rewrite > Hletin in H1;
-      rewrite > H7 in H1;apply in_Skip;apply (H1 H5 H3)]]
+  [simplify in H1;elim (in_cons_case ? ? ? ? H1)
+     [destruct H3;elim (H2 Hcut1)
+     |simplify;elim H3;apply (in_Skip ? ? ? ? H5);intro;destruct H6;
+      apply (H2 Hcut1)] 
+  |simplify in H2;simplify;elim (in_cons_case ? ? ? ? H2)
+     [rewrite > H4;apply in_Base
+     |elim H4;apply (in_Skip ? ? ? ? (H1 H6 H3) H5)]]
 qed.
 
 lemma in_FV_subst : \forall x,T,U,n.(in_list ? x (fv_type T)) \to
                                 (in_list ? x (fv_type (subst_type_nat T U n))).
 intros 3;elim T
-  [simplify in H;inversion H
-     [intros;lapply (sym_eq ? ? ? H2);absurd (a::l = [])
-        [assumption|apply nil_cons]
-     |intros;lapply (sym_eq ? ? ? H4);absurd (a1::l = [])
-        [assumption|apply nil_cons]]
+  [simplify in H;elim (in_list_nil ? ? H)
   |2,3:simplify;simplify in H;assumption
   |*:simplify in H2;simplify;apply natinG_or_inH_to_natinGH;
    lapply (nat_in_list_case ? ? ? H2);elim Hletin
@@ -444,49 +292,24 @@ cut (\forall l:(list nat).\exists n.\forall m.
      [apply a
      |apply H;constructor 1]
   |intros;elim l
-    [apply ex_intro 
-       [apply O
-       |intros;unfold;intro;inversion H1
-          [intros;lapply (sym_eq ? ? ? H3);absurd (a::l1 = [])
-             [assumption|apply nil_cons]
-          |intros;lapply (sym_eq ? ? ? H5);absurd (a1::l1 = [])
-             [assumption|apply nil_cons]]]
-    |elim H;lapply (decidable_eq_nat a t);elim Hletin
-       [apply ex_intro
-          [apply (S a)
-          |intros;unfold;intro;inversion H4
-             [intros;lapply (inj_head_nat ? ? ? ? H6);rewrite < Hletin1 in H5;
-              rewrite < H2 in H5;rewrite > H5 in H3;
-              apply (not_le_Sn_n ? H3)
-             |intros;lapply (inj_tail ? ? ? ? ? H8);rewrite < Hletin1 in H5;
-              rewrite < H7 in H5;
-              apply (H1 m ? H5);lapply (le_S ? ? H3);
-              apply (le_S_S_to_le ? ? Hletin2)]]
+    [apply (ex_intro ? ? O);intros;unfold;intro;elim (in_list_nil ? ? H1)
+    |elim H;elim (decidable_eq_nat a t)
+       [apply (ex_intro ? ? (S a));intros;intro;elim (in_cons_case ? ? ? ? H4)
+          [rewrite < H5 in H2;rewrite < H2 in H3;apply (not_le_Sn_n ? H3)
+          |elim H5;elim (H1 m ? H7);apply (le_S_S_to_le ? ? (le_S ? ? H3))]
        |cut ((leb a t) = true \lor (leb a t) = false)
           [elim Hcut
-             [apply ex_intro
-                [apply (S t)
-                |intros;unfold;intro;inversion H5
-                   [intros;lapply (inj_head_nat ? ? ? ? H7);rewrite > H6 in H4;
-                    rewrite < Hletin1 in H4;apply (not_le_Sn_n ? H4)
-                   |intros;lapply (inj_tail ? ? ? ? ? H9);
-                    rewrite < Hletin1 in H6;lapply (H1 a1)
-                      [apply (Hletin2 H6)
-                      |lapply (leb_to_Prop a t);rewrite > H3 in Hletin2;
-                       simplify in Hletin2;rewrite < H8;
-                       apply (trans_le ? ? ? Hletin2);
-                       apply (trans_le ? ? ? ? H4);constructor 2;constructor 1]]]
-             |apply ex_intro
-                [apply a
-                |intros;lapply (leb_to_Prop a t);rewrite > H3 in Hletin1;
-                 simplify in Hletin1;lapply (not_le_to_lt ? ? Hletin1);
-                 unfold in Hletin2;unfold;intro;inversion H5
-                   [intros;lapply (inj_head_nat ? ? ? ? H7);
-                    rewrite < Hletin3 in H6;rewrite > H6 in H4;
-                    apply (Hletin1 H4)
-                   |intros;lapply (inj_tail ? ? ? ? ? H9);
-                    rewrite < Hletin3 in H6;rewrite < H8 in H6;
-                    apply (H1 ? H4 H6)]]]
+             [apply (ex_intro ? ? (S t));intros;intro;
+              elim (in_cons_case ? ? ? ? H5)
+                [rewrite > H6 in H4;apply (not_le_Sn_n ? H4)
+                |elim H6;elim (H1 m ? H8);apply (trans_le a t m)
+                   [lapply (leb_to_Prop a t);rewrite > H3 in Hletin;assumption
+                   |apply (le_S_S_to_le t m (le_S (S t) m H4))]]
+             |apply (ex_intro ? ? a);intros;intro;elim (in_cons_case ? ? ? ? H5)
+                [lapply (leb_to_Prop a t);rewrite > H3 in Hletin;
+                 simplify in Hletin;lapply (not_le_to_lt ? ? Hletin);
+                 unfold in Hletin1;rewrite < H6 in Hletin;apply (Hletin H4)
+                |elim H6;elim (H1 ? H4 H8)]]
           |elim (leb a t);autobatch]]]]
 qed.
 
@@ -495,38 +318,23 @@ qed.
 lemma fv_WFT : \forall T,x,G.(WFType G T) \to (in_list ? x (fv_type T)) \to
                   (in_list ? x (fv_env G)).
 intros 4.elim H
-  [simplify in H2;inversion H2
-     [intros;lapply (inj_head_nat ? ? ? ? H4);rewrite < Hletin;assumption
-     |intros;lapply (inj_tail ? ? ? ? ? H6);rewrite < Hletin in H3;
-      inversion H3
-        [intros;lapply (sym_eq ? ? ? H8);absurd (a2 :: l2 = []) 
-           [assumption|apply nil_cons]
-        |intros;lapply (sym_eq ? ? ? H10);
-            absurd (a3 :: l2 = []) [assumption|apply nil_cons]]]
-  |simplify in H1;lapply (in_list_nil ? x H1);elim Hletin
-  |simplify in H5;lapply (nat_in_list_case ? ? ? H5);elim Hletin
-     [apply (H4 H6)
-     |apply (H2 H6)]
-  |simplify in H5;lapply (nat_in_list_case ? ? ? H5);elim Hletin
-     [lapply (fresh_name ((fv_type t1) @ (fv_env l)));elim Hletin1;
-      cut ((\lnot (in_list ? a (fv_type t1))) \land
-           (\lnot (in_list ? a (fv_env l))))
+  [simplify in H2;elim (in_cons_case ? ? ? ? H2)
+     [rewrite > H3;assumption|elim H3;elim (in_list_nil ? ? H5)]
+  |simplify in H1;elim (in_list_nil ? x H1)
+  |simplify in H5;elim (nat_in_list_case ? ? ? H5);autobatch
+  |simplify in H5;elim (nat_in_list_case ? ? ? H5)
+     [elim (fresh_name ((fv_type t1) @ (fv_env l)));
+      cut ((¬ (in_list ? a (fv_type t1))) ∧
+           (¬ (in_list ? a (fv_env l))))
         [elim Hcut;lapply (H4 ? H9 H8)
-           [cut (x \neq a)
-              [simplify in Hletin2;
-               (* FIXME trick *);generalize in match Hletin2;intro;
-               inversion Hletin2
-                 [intros;lapply (inj_head_nat ? ? ? ? H12);
-                  rewrite < Hletin3 in H11;lapply (Hcut1 H11);elim Hletin4
-                 |intros;lapply (inj_tail ? ? ? ? ? H14);rewrite > Hletin3;
-                  assumption]
-              |unfold;intro;apply H8;rewrite < H10;assumption]
+           [cut (x ≠ a)
+              [simplify in Hletin;elim (in_cons_case ? ? ? ? Hletin)
+                 [elim (Hcut1 H10)|elim H10;assumption]
+              |intro;apply H8;rewrite < H10;assumption]
            |apply in_FV_subst;assumption]
         |split
-           [unfold;intro;apply H7;apply natinG_or_inH_to_natinGH;right;
-            assumption
-           |unfold;intro;apply H7;apply natinG_or_inH_to_natinGH;left;
-            assumption]]
+           [intro;apply H7;apply natinG_or_inH_to_natinGH;right;assumption
+           |intro;apply H7;apply natinG_or_inH_to_natinGH;left;assumption]]
      |apply (H2 H6)]]
 qed.
            
@@ -669,27 +477,20 @@ lemma WFE_Typ_subst : \forall H,x,B,C,T,U,G.
                       (WFEnv (H @ ((mk_bound B x T) :: G))) \to (WFType G U) \to
                       (WFEnv (H @ ((mk_bound C x U) :: G))).
 intros 7;elim H 0
-  [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1
-     [intros;lapply (nil_cons ? G (mk_bound B x T));lapply (Hletin H4);
-      elim Hletin1
-     |intros;lapply (inj_tail ? ? ? ? ? H8);lapply (inj_head ? ? ? ? H8);
-      destruct Hletin1;rewrite < Hletin in H6;rewrite < Hletin in H4;
-      rewrite < Hcut1 in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)]
+  [simplify;intros;(*FIXME*)generalize in match H1;intro;inversion H1;intros
+     [lapply (nil_cons ? G (mk_bound B x T));elim (Hletin H4)
+     |destruct H8;rewrite < Hcut2 in H6;rewrite < Hcut in H4;
+      rewrite < Hcut in H6;apply (WFE_cons ? ? ? ? H4 H6 H2)]
   |intros;simplify;generalize in match H2;elim t;simplify in H4;
-   inversion H4
-     [intros;absurd (mk_bound b n t1::l@(mk_bound B x T::G)=[])
-        [assumption
-        |apply nil_cons]
-     |intros;lapply (inj_tail ? ? ? ? ? H9);lapply (inj_head ? ? ? ? H9);
-      destruct Hletin1;apply WFE_cons
-        [apply H1
-           [rewrite > Hletin;assumption
-           |assumption]
-        |rewrite > Hcut1;generalize in match H7;rewrite < Hletin;
-         rewrite > (fv_env_extends ? x B C T U);intro;assumption
-        |rewrite < Hletin in H8;rewrite > Hcut2;
-         apply (WFT_env_incl ? ? H8);rewrite > (fv_env_extends ? x B C T U);
-         unfold;intros;assumption]]]
+   inversion H4;intros
+     [destruct H5
+     |destruct H9;apply WFE_cons
+        [rewrite < Hcut in H5;apply (H1 H5 H3)
+        |rewrite < (fv_env_extends ? x B C T U);rewrite > Hcut;rewrite > Hcut2;
+         assumption
+        |rewrite < Hcut3 in H8;rewrite > Hcut1;apply (WFT_env_incl ? ? H8);
+         rewrite < (fv_env_extends ? x B C T U);unfold;intros;
+         rewrite > Hcut;assumption]]]
 qed.
 
 lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to
@@ -697,25 +498,13 @@ lemma WFE_bound_bound : \forall B,x,T,U,G. (WFEnv G) \to
                                   (in_list ? (mk_bound B x U) G) \to T = U.
 intros 6;elim H
   [lapply (in_list_nil ? ? H1);elim Hletin
-  |inversion H6
-     [intros;rewrite < H7 in H8;lapply (inj_head ? ? ? ? H8);
-      rewrite > Hletin in H5;inversion H5
-        [intros;rewrite < H9 in H10;lapply (inj_head ? ? ? ? H10);
-         destruct Hletin1;symmetry;assumption
-        |intros;lapply (inj_tail ? ? ? ? ? H12);rewrite < Hletin1 in H9;
-         rewrite < H11 in H9;lapply (boundinenv_natinfv x l)
-           [destruct Hletin;rewrite < Hcut1 in Hletin2;lapply (H3 Hletin2);
-            elim Hletin3
-           |apply ex_intro
-              [apply B|apply ex_intro [apply T|assumption]]]]
-     |intros;lapply (inj_tail ? ? ? ? ? H10);rewrite < H9 in H7;
-      rewrite < Hletin in H7;(*FIXME*)generalize in match H5;intro;inversion H5
-        [intros;rewrite < H12 in H13;lapply (inj_head ? ? ? ? H13);
-         destruct Hletin1;rewrite < Hcut1 in H7;
-         lapply (boundinenv_natinfv n l)
-           [lapply (H3 Hletin2);elim Hletin3
-           |apply ex_intro
-              [apply B|apply ex_intro [apply U|assumption]]]
-        |intros;apply (H2 ? H7);rewrite > H14;lapply (inj_tail ? ? ? ? ? H15);
-         rewrite > Hletin1;assumption]]]
+  |elim (in_cons_case ? ? ? ? H6)
+     [destruct H7;subst;elim (in_cons_case ? ? ? ? H5)
+        [destruct H7;assumption
+        |elim H7;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? b);
+         apply (ex_intro ? ? T);assumption]
+     |elim H7;elim (in_cons_case ? ? ? ? H5)
+        [destruct H10;elim H3;apply boundinenv_natinfv;apply (ex_intro ? ? B);
+         apply (ex_intro ? ? U);rewrite < Hcut1;assumption
+        |elim H10;apply (H2 H12 H9)]]]
 qed.
index 0437f1e29f4f354b028296a150de833801392277..7fb8fed9c14c5433fc8cbd503a8f71e02aedb655 100644 (file)
 (**************************************************************************)
 
 set "baseuri" "cic:/matita/Fsub/part1a/".
-include "logic/equality.ma".
-include "nat/nat.ma".
-include "datatypes/bool.ma".
-include "nat/compare.ma".
-include "Fsub/util.ma".
 include "Fsub/defn.ma".
 
 (*** Lemma A.1 (Reflexivity) ***)
 
-theorem JS_Refl : \forall T,G.(WFType G T) \to (WFEnv G) \to (JSubtype G T T).
-apply Typ_len_ind;intro;elim U
-  [(* FIXME *) generalize in match H1;intro;inversion H1
-     [intros;destruct H6
-     |intros;destruct H5
-     |*:intros;destruct H9]
-  |apply (SA_Refl_TVar ? ? H2);(*FIXME*)generalize in match H1;intro;
-   inversion H1
-     [intros;destruct H6;rewrite > Hcut;assumption
-     |intros;destruct H5
-     |*:intros;destruct H9]
-  |apply (SA_Top ? ? H2 H1)
-  |cut ((WFType G t) \land (WFType G t1))
-     [elim Hcut;apply SA_Arrow
-        [apply H2
-           [apply t_len_arrow1
-           |*:assumption]
-        |apply H2
-           [apply t_len_arrow2
-           |*:assumption]]
-     |(* no shortcut? *)
-      (*FIXME*)generalize in match H3;intro;inversion H3
-        [intros;destruct H8
-        |intros;destruct H7
-        |intros;destruct H11;rewrite > Hcut;rewrite > Hcut1;split;assumption
-        |intros;destruct H11]]
-  |cut (WFType G t)
-     [lapply (H2 t ? ? Hcut H4)
-        [apply t_len_forall1
-        |apply (SA_All ? ? ? ? ? Hletin);intros;apply H2
-           [rewrite < eq_t_len_TFree_subst;
-            apply t_len_forall2
-           |generalize in match H3;intro;inversion H3
-              [intros;destruct H9
-              |intros;destruct H8
-              |intros;destruct H12
-              |intros;destruct H12;subst;apply H9
-                 [assumption
-                 |unfold;intro;apply H5;
-                  elim (fresh_name ((fv_env l)@(fv_type t3)));
-                  cut ((\lnot (in_list ? a (fv_env l))) \land
-                       (\lnot (in_list ? a (fv_type t3))))
-                    [elim Hcut1;lapply (H9 ? H13 H14);
-                     lapply (fv_WFT ? X ? Hletin1)
-                       [simplify in Hletin2;inversion Hletin2
-                          [intros;lapply (inj_head_nat ? ? ? ? H16);subst;
-                           elim (H14 H11)
-                          |intros;lapply (inj_tail ? ? ? ? ? H18);
-                           rewrite < Hletin3 in H15;assumption]
-                       |apply varinT_varinT_subst;
-                        assumption]
-                    |split;unfold;intro;apply H12;apply natinG_or_inH_to_natinGH
-                       [right;assumption
-                       |left;assumption]]]]
-           |apply WFE_cons;assumption]]
-     |(*FIXME*)generalize in match H3;intro;inversion H3
-        [intros;destruct H8
-        |intros;destruct H7
-        |intros;destruct H11
-        |intros;destruct H11;subst;assumption]]]
+theorem JS_Refl : ∀T,G.WFType G T → WFEnv G → G ⊢ T ⊴  T.
+intros 3;elim H
+  [apply (SA_Refl_TVar l n H2 H1);
+  |apply (SA_Top l Top H1 (WFT_Top l));
+  |apply (SA_Arrow l t t1 t t1 (H2 H5) (H4 H5))
+  |apply (SA_All ? ? ? ? ? (H2 H5));intros;apply (H4 X H6)
+     [intro;apply H6;apply (fv_WFT (Forall t t1) X l)
+        [apply (WFT_Forall ? ? ? H1 H3)
+        |simplify;autobatch]
+     |autobatch]]
 qed.
 
 (* 
@@ -106,12 +51,57 @@ intros 4;elim H
      |apply WFE_cons
         [1,2:assumption
         |apply (JS_to_WFT1 ? ? ? Hletin)]
-     |unfold;intros;inversion H9
-        [intros;lapply (inj_head ? ? ? ? H11);rewrite > Hletin1;apply in_Base
-        |intros;lapply (inj_tail ? ? ? ? ? H13);rewrite < Hletin1 in H10;
-         apply in_Skip;apply (H7 ? H10)]]]
+     |unfold;intros;elim (in_cons_case ? ? ? ? H9)
+        [rewrite > H10;apply in_Base
+        |elim H10;apply (in_Skip ? ? ? ? ? H11);apply (H7 ? H12)]]]
+qed.
+
+lemma decidable_eq_Typ : \forall S,T:Typ.(S = T) ∨ (S ≠ T).
+intro;elim S
+  [elim T
+     [elim (decidable_eq_nat n n1)
+        [rewrite > H;left;reflexivity
+        |right;intro;destruct H1;apply (H Hcut)]
+     |2,3:right;intro;destruct H
+     |*:right;intro;destruct H2]
+  |elim T
+     [2:elim (decidable_eq_nat n n1)
+        [rewrite > H;left;reflexivity
+        |right;intro;destruct H1;apply (H Hcut)]
+     |1,3:right;intro;destruct H
+     |*:right;intro;destruct H2]
+  |elim T
+     [3:left;reflexivity
+     |1,2:right;intro;destruct H
+     |*:right;intro;destruct H2]
+  |elim T
+     [1,2,3:right;intro;destruct H2
+     |elim (H t2)
+        [rewrite > H4;elim (H1 t3)
+           [rewrite > H5;left;reflexivity
+           |right;intro;apply H5;destruct H6;assumption]
+        |right;intro;apply H4;destruct H5;assumption]
+     |right;intro;destruct H4]
+  |elim T
+     [1,2,3:right;intro;destruct H2
+     |right;intro;destruct H4
+     |elim (H t2)
+        [rewrite > H4;elim (H1 t3)
+           [rewrite > H5;left;reflexivity
+           |right;intro;apply H5;destruct H6;assumption]
+        |right;intro;apply H4;destruct H5;assumption]]]
 qed.
 
+lemma decidable_eq_bound: ∀b1,b2:bound.(b1 = b2) ∨ (b1 ≠ b2).
+intros;elim b1;elim b2;elim (decidable_eq_nat n n1)
+  [rewrite < H;elim (decidable_eq_Typ t t1)
+     [rewrite < H1;elim (bool_to_decidable_eq b b3)
+        [rewrite > H2;left;reflexivity
+        |right;intro;destruct H3;apply (H2 Hcut)]
+     |right;intro;destruct H2;apply (H1 Hcut1)]
+  |right;intro;destruct H1;apply (H Hcut1)]
+qed.     
+
 (* Lemma A.3 (Transitivity and Narrowing) *)
 
 lemma JS_trans_narrow : \forall Q.
@@ -151,17 +141,28 @@ cut (\forall G,T,P.
                  [apply (SA_Trans_TVar ? ? ? P)
                     [rewrite < H10;elim l1
                       [simplify;constructor 1
-                      |simplify;constructor 2;assumption]
+                      |simplify;elim (decidable_eq_bound (mk_bound true X P) t2)
+                         [rewrite < H12;apply in_Base
+                         |apply (in_Skip ? ? ? ? ? H12);assumption]]
                    |apply H7
                       [lapply (H6 ? H7 H8 H9);lapply (JS_to_WFE ? ? ? Hletin);
                        apply (JS_weakening ? ? ? H3 ? Hletin1);unfold;intros;
-                       elim l1;simplify;constructor 2;assumption
+                       elim l1
+                         [simplify;
+                          elim (decidable_eq_bound x (mk_bound true X P))
+                            [rewrite < H12;apply in_Base
+                            |apply (in_Skip ? ? ? ? ? H12);assumption]
+                         |simplify;elim (decidable_eq_bound x t2)
+                            [rewrite < H13;apply in_Base
+                            |apply (in_Skip ? ? ? ? ? H13);assumption]]
                       |lapply (WFE_bound_bound true n t1 U ? ? H4)
                          [apply (JS_to_WFE ? ? ? H5)
                          |rewrite < Hletin;apply (H6 ? H7 H8 H9)
                          |rewrite > H9;rewrite > H10;elim l1;simplify
                             [constructor 1
-                            |constructor 2;assumption]]]]
+                            |elim (decidable_eq_bound (mk_bound true n U) t2)
+                               [rewrite > H12;apply in_Base
+                               |apply (in_Skip ? ? ? ? ? H12);assumption]]]]]
                 |apply (SA_Trans_TVar ? ? ? t1)
                    [rewrite > H9 in H4;
                     apply (lookup_env_extends ? ? ? ? ? ? ? ? ? ? H4);
index fa59484f5dd27e94b73bbdd9625badce717984a0..5a81f7ec576ca0eaa9cc4e0681feeac1333194a9 100644 (file)
@@ -24,11 +24,22 @@ let rec max m n \def
      [true \Rightarrow n
      |false \Rightarrow m]. 
 
-inductive in_list (A : Type) : A \to (list A) \to Prop \def
-  | in_Base : \forall x:A.\forall l:(list A).
-              (in_list A x (x :: l))
-  | in_Skip : \forall x,y:A.\forall l:(list A).
-              (in_list A x l) \to (in_list A x (y :: l)).
+inductive in_list (A:Type): A → (list A) → Prop ≝
+| in_Base : ∀ x,l.(in_list A x (x::l))
+| in_Skip : ∀ x,y,l.(in_list A x l) → (x ≠ y) → (in_list A x (y::l)).
+
+notation > "hvbox(x ∈ l)"
+  non associative with precedence 30 for @{ 'inlist $x $l }.
+notation < "hvbox(x \nbsp ∈ \nbsp l)"
+  non associative with precedence 30 for @{ 'inlist $x $l }.
+interpretation "item in list" 'inlist x l =
+  (cic:/matita/Fsub/util/in_list.ind#xpointer(1/1) _ x l).
+
+lemma in_Skip2 : ∀x,y,l.(in_list nat x l) → (in_list nat x (y::l)).
+intros;elim (decidable_eq_nat x y)
+  [rewrite > H1;apply in_Base
+  |apply (in_Skip ? ? ? ? H H1)]
+qed.
 
 definition incl : \forall A.(list A) \to (list A) \to Prop \def
   \lambda A,l,m.\forall x.(in_list A x l) \to (in_list A x m).               
@@ -43,10 +54,14 @@ definition map : \forall A,B,f.((list A) \to (list B)) \def
 
 lemma in_list_nil : \forall A,x.\lnot (in_list A x []).
 intros.unfold.intro.inversion H
-  [intros;lapply (sym_eq ? ? ? H2);absurd (a::l = [])
-     [assumption|apply nil_cons]
-  |intros;lapply (sym_eq ? ? ? H4);absurd (a1::l = [])
-     [assumption|apply nil_cons]]
+  [intros;lapply (sym_eq ? ? ? H2);destruct Hletin
+  |intros;destruct H5]
+qed.
+
+lemma in_cons_case : ∀A.∀x,h:A.∀t:list A.x ∈ h::t → x = h ∨ (x ≠ h ∧ (x ∈ t)).
+intros;inversion H;intros
+  [destruct H2;left;symmetry;assumption
+  |destruct H5;right;split [rewrite > Hcut|rewrite > Hcut1] assumption ]
 qed.
 
 lemma max_case : \forall m,n.(max m n) = match (leb m n) with