-
(**************************************************************************)
(* ___ *)
(* ||M|| *)
nbtype : NTyp
}.
-inductive option (A:Type) : Set \def
-| Some : A \to option A
-| None : option A.
-
-definition swap : nat → nat → nat → nat ≝
- λu,v,x.match (eqb x u) with
- [true ⇒ v
- |false ⇒ match (eqb x v) with
- [true ⇒ u
- |false ⇒ x]].
-
-lemma swap_left : ∀x,y.(swap x y x) = y.
-intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
-qed.
-
-lemma swap_right : ∀x,y.(swap x y y) = x.
-intros;unfold swap;rewrite > eqb_n_n;apply (eqb_elim y x);intro;autobatch;
-qed.
-
-lemma swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
-intros;unfold swap;apply (eqb_elim z x);intro;simplify
- [elim H;assumption
- |rewrite > not_eq_to_eqb_false;autobatch]
-qed.
-
-lemma swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
-intros;unfold in match (swap u v x);apply (eqb_elim x u);intro;simplify
- [autobatch paramodulation
- |apply (eqb_elim x v);intro;simplify
- [autobatch paramodulation
- |apply swap_other;assumption]]
-qed.
-
-lemma swap_inj : ∀u,v,x,y.swap u v x = swap u v y → x = y.
-intros 4;unfold swap;apply (eqb_elim x u);simplify;intro
- [apply (eqb_elim y u);simplify;intro
- [intro;autobatch paramodulation
- |apply (eqb_elim y v);simplify;intros
- [autobatch paramodulation
- |elim H2;symmetry;assumption]]
- |apply (eqb_elim y u);simplify;intro
- [apply (eqb_elim x v);simplify;intros;
- [autobatch paramodulation
- |elim H2;assumption]
- |apply (eqb_elim x v);simplify;intro
- [apply (eqb_elim y v);simplify;intros
- [autobatch paramodulation
- |elim H1;symmetry;assumption]
- |apply (eqb_elim y v);simplify;intros
- [elim H;assumption
- |assumption]]]]
-qed.
+let rec encodetype T vars on T ≝
+ match T with
+ [ (TName n) ⇒ match (lookup n vars) with
+ [ true ⇒ (TVar (posn vars n))
+ | false ⇒ (TFree n)]
+ | NTop ⇒ Top
+ | (NArrow T1 T2) ⇒ Arrow (encodetype T1 vars) (encodetype T2 vars)
+ | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars)
+ (encodetype T2 (n2::vars))].
let rec swap_NTyp u v T on T ≝
match T with
|(Arrow T1 T2) ⇒ (Arrow (swap_Typ u v T1) (swap_Typ u v T2))
|(Forall T1 T2) ⇒ (Forall (swap_Typ u v T1) (swap_Typ u v T2))].
-definition swap_list : nat \to nat \to (list nat) \to (list nat) ≝
- \lambda u,v,l.(map ? ? (swap u v) l).
-
let rec var_NTyp (T:NTyp):list nat\def
match T with
[TName x ⇒ [x]
|NArrow U V ⇒ (var_NTyp U)@(var_NTyp V)
|NForall X U V ⇒ X::(var_NTyp U)@(var_NTyp V)].
-inductive alpha_eq : NTyp \to NTyp \to Prop \def
-| A_refl : \forall T.(alpha_eq T T)
-| A_arrow : \forall T1,T2,U1,U2.(alpha_eq T1 U1) \to (alpha_eq T2 U2) \to
- (alpha_eq (NArrow T1 T2) (NArrow U1 U2))
-| A_forall : \forall T1,T2,U1,U2,X,Y.
- (alpha_eq T1 U1) \to
- (\forall Z.
- \lnot (in_list nat Z (X::Y::((var_NTyp T2)@(var_NTyp U2))))
- \to (alpha_eq (swap_NTyp Z X T2) (swap_NTyp Z Y U2))) \to
- (alpha_eq (NForall X T1 T2) (NForall Y U1 U2)).
-
-let rec posn l x on l ≝
- match l with
- [ nil ⇒ O
- | (cons (y:nat) l2) ⇒
- match (eqb x y) with
- [ true ⇒ O
- | false ⇒ S (posn l2 x)]].
-
-let rec length A l on l ≝
- match l with
- [ nil ⇒ O
- | (cons (y:A) l2) ⇒ S (length A l2)].
-
-let rec lookup n l on l ≝
- match l with
- [ nil ⇒ false
- | cons (x:nat) l1 ⇒ match (eqb n x) with
- [true ⇒ true
- |false ⇒ (lookup n l1)]].
-
-let rec encodetype T vars on T ≝
- match T with
- [ (TName n) ⇒ match (lookup n vars) with
- [ true ⇒ (TVar (posn vars n))
- | false ⇒ (TFree n)]
- | NTop ⇒ Top
- | (NArrow T1 T2) ⇒ Arrow (encodetype T1 vars) (encodetype T2 vars)
- | (NForall n2 T1 T2) ⇒ Forall (encodetype T1 vars)
- (encodetype T2 (n2::vars))].
-
-let rec head (A:Type) l on l ≝
- match l with
- [ nil ⇒ None A
- | (cons (x:A) l2) ⇒ Some A x].
-
-let rec nth n l on n ≝
- match n with
- [ O ⇒ match l with
- [ nil ⇒ O
- | (cons x l2) ⇒ x]
- | (S n2) ⇒ (nth n2 (tail ? l))].
-
-definition max_list : (list nat) \to nat \def
- \lambda l.let rec aux l0 m on l0 \def
- match l0 with
- [ nil ⇒ m
- | (cons n l2) ⇒ (aux l2 (max m n))]
- in aux l O.
-
-let rec decodetype T vars C on T \def
- match T with
- [ TVar n ⇒ TName (nth n vars)
- | TFree x ⇒ TName x
- | Top ⇒ NTop
- | Arrow T1 T2 ⇒ NArrow (decodetype T1 vars C) (decodetype T2 vars C)
- | Forall T1 T2 ⇒ NForall (S (max_list (vars@C))) (decodetype T1 vars C)
- (decodetype T2 ((S (max_list (vars@C)))::vars) C)].
-
-definition sublist: \forall A:Type.(list A) \to (list A) \to Prop \def
- \lambda A,l1,l2.\forall x.(in_list ? x l1) \to (in_list ? x l2).
-
-let rec remove_nat (x:nat) (l:list nat) on l \def
- match l with
- [ nil ⇒ (nil nat)
- | (cons y l2) ⇒ match (eqb x y) with
- [ true ⇒ (remove_nat x l2)
- | false ⇒ (y :: (remove_nat x l2)) ]].
let rec fv_NTyp (T:NTyp):list nat\def
match T with
| false ⇒ (NForall Z (subst_NTyp_var U X Y)
(subst_NTyp_var V X Y))]].
+definition filter_ntypes : list nbound → list nbound ≝
+ λG.(filter ? G (λB.match B with [mk_nbound B X T ⇒ B])).
+
definition fv_Nenv : list nbound → list nat ≝
- map nbound nat
+ λG.map nbound nat
(λb.match b with
- [mk_nbound (B:bool) (X:nat) (T:NTyp) ⇒ X]).
+ [mk_nbound (B:bool) (X:nat) (T:NTyp) ⇒ X]) (filter_ntypes G).
inductive NWFType : (list nbound) → NTyp → Prop ≝
- | NWFT_TName : ∀X,G.(in_list ? X (fv_Nenv G))
+ | NWFT_TName : ∀X,G.(X ∈ (fv_Nenv G))
→ (NWFType G (TName X))
| NWFT_Top : ∀G.(NWFType G NTop)
| NWFT_Arrow : ∀G,T,U.(NWFType G T) → (NWFType G U) →
(NWFType G (NArrow T U))
| NWFT_Forall : ∀G,X,T,U.(NWFType G T) →
- (∀Y.¬(in_list ? Y (fv_Nenv G)) →
- (Y = X ∨ ¬(in_list ? Y (fv_NTyp U))) →
+ (∀Y.Y ∉ (fv_Nenv G) →
+ (Y = X ∨ Y ∉ (fv_NTyp U)) →
(NWFType ((mk_nbound true Y T) :: G) (swap_NTyp Y X U))) →
(NWFType G (NForall X T U)).
inductive NWFEnv : (list nbound) → Prop ≝
| NWFE_Empty : (NWFEnv (nil ?))
| NWFE_cons : ∀B,X,T,G.(NWFEnv G) →
- ¬(in_list ? X (fv_Nenv G)) →
+ X ∉ (fv_Nenv G) →
(NWFType G T) → (NWFEnv ((mk_nbound B X T) :: G)).
inductive NJSubtype : (list nbound) → NTyp → NTyp → Prop ≝
| NSA_Top : ∀G,T.(NWFEnv G) → (NWFType G T) → (NJSubtype G T NTop)
| NSA_Refl_TVar : ∀G,X.(NWFEnv G)
- → (in_list ? X (fv_Nenv G))
+ → X ∈ (fv_Nenv G)
→ (NJSubtype G (TName X) (TName X))
| NSA_Trans_TVar : ∀G,X,T,U.
- (in_list ? (mk_nbound true X U) G) →
+ (mk_nbound true X U) ∈ G →
(NJSubtype G U T) → (NJSubtype G (TName X) T)
| NSA_Arrow : ∀G,S1,S2,T1,T2.
(NJSubtype G T1 S1) → (NJSubtype G S2 T2) →
(NJSubtype G (NArrow S1 S2) (NArrow T1 T2))
| NSA_All : ∀G,X,Y,S1,S2,T1,T2.
- (NWFType G (NForall X S1 S2)) \to
- (NWFType G (NForall Y T1 T2)) \to
+ (NWFType G (NForall X S1 S2)) →
+ (NWFType G (NForall Y T1 T2)) →
(NJSubtype G T1 S1) →
- (∀Z.¬(in_list ? Z (fv_Nenv G)) →
- (Z = X \lor \lnot in_list ? Z (fv_NTyp S2)) \to
- (Z = Y \lor \lnot in_list ? Z (fv_NTyp T2)) \to
+ (∀Z.Z ∉ (fv_Nenv G) →
+ (Z = X ∨ Z ∉ (fv_NTyp S2)) →
+ (Z = Y ∨ Z ∉ (fv_NTyp T2)) →
(NJSubtype ((mk_nbound true Z T1) :: G)
(swap_NTyp Z X S2) (swap_NTyp Z Y T2))) →
- (NJSubtype G (NForall X S1 S2) (NForall Y T1 T2))
- | NSA_alpha : ∀G,T1,T2,U1,U2.(NJSubtype G T1 U1) →
- (alpha_eq T1 T2) →
- (alpha_eq U1 U2) →
- (NJSubtype G T2 U2).
+ (NJSubtype G (NForall X S1 S2) (NForall Y T1 T2)).
-let rec nt_len T \def
+let rec nt_len T ≝
match T with
[ TName X ⇒ O
| NTop ⇒ O
lemma eq_fv_Nenv_fv_env : ∀G. fv_Nenv G = fv_env (encodeenv G).
intro;elim G;simplify
[reflexivity
- |rewrite < H;elim a;simplify;reflexivity]
+ |elim a;elim b;simplify;rewrite < H;reflexivity]
qed.
lemma decidable_eq_Typ : ∀T,U:Typ.decidable (T = U).
|right;intro;destruct H1;elim H;reflexivity]
qed.
-lemma in_Nenv_to_in_env: ∀l,n,n2.in_list ? (mk_nbound true n n2) l →
- in_list ? (mk_bound true n (encodetype n2 [])) (encodeenv l).
+lemma in_Nenv_to_in_env: ∀l,n,n2.(mk_nbound true n n2) ∈ l →
+ (mk_bound true n (encodetype n2 [])) ∈ (encodeenv l).
intros 3;elim l
[elim (not_in_list_nil ? ? H)
|inversion H1;intros;destruct;
|elim a;simplify;apply in_list_cons;apply H;assumption]]
qed.
-lemma in_lookup : \forall x,l.(in_list ? x l) \to (lookup x l = true).
-intros;elim H;simplify
- [rewrite > eqb_n_n;reflexivity
- |rewrite > H2;elim (eqb a a1);reflexivity]
-qed.
-
-lemma lookup_in : \forall x,l.(lookup x l = true) \to (in_list ? x l).
-intros 2;elim l
- [simplify in H;destruct H
- |generalize in match H1;simplify;elim (decidable_eq_nat x a)
- [applyS in_list_head
- |apply in_list_cons;apply H;
- rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;assumption]]
-qed.
-
-lemma posn_length : \forall x,vars.(in_list ? x vars) \to
- (posn vars x) < (length ? vars).
-intros 2;elim vars
- [elim (not_in_list_nil ? ? H)
- |inversion H1;intros;destruct;simplify
- [rewrite > eqb_n_n;simplify;
- apply lt_O_S
- |elim (eqb x a);simplify
- [apply lt_O_S
- |apply le_S_S;apply H;assumption]]]
-qed.
-
-lemma in_remove : \forall a,b,l.(a \neq b) \to (in_list ? a l) \to
- (in_list ? a (remove_nat b l)).
-intros 4;elim l
- [elim (not_in_list_nil ? ? H1)
- |inversion H2;intros;destruct;simplify
- [rewrite > not_eq_to_eqb_false
- [simplify;apply in_list_head
- |intro;apply H;symmetry;assumption]
- |elim (eqb b a1);simplify
- [apply H1;assumption
- |apply in_list_cons;apply H1;assumption]]]
-qed.
-
lemma NTyp_len_ind : \forall P:NTyp \to Prop.
(\forall U.(\forall V.((nt_len V) < (nt_len U)) \to (P V))
\to (P U))
|*:autobatch paramodulation]
qed.
-lemma swap_same : \forall x,y.swap x x y = y.
-intros;elim (decidable_eq_nat y x)
- [autobatch paramodulation
- |rewrite > swap_other;autobatch]
-qed.
-
-lemma not_nat_in_to_lookup_false : ∀l,X.¬(in_list ? X l) → lookup X l = false.
-intros 2;elim l;simplify
- [reflexivity
- |elim (decidable_eq_nat X a)
- [elim H1;rewrite > H2;apply in_list_head
- |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
- apply (in_list_cons ? ? ? ? H3);]]
-qed.
-
lemma fv_encode : ∀T,l1,l2.
- (∀x.(in_list ? x (fv_NTyp T)) →
+ (∀x.x ∈ (fv_NTyp T) →
(lookup x l1 = lookup x l2 ∧
(lookup x l1 = true → posn l1 x = posn l2 x))) →
(encodetype T l1 = encodetype T l2).
intro;elim T
[simplify in H;elim (H n)
- [simplify;rewrite < H1;generalize in match H2;elim (lookup n l1);simplify
- [rewrite > H3;autobatch
+ [simplify;rewrite < H1;elim (lookup n l1) in H2;simplify
+ [rewrite > H2;autobatch
|reflexivity]
|apply in_list_head]
|simplify;reflexivity
|intros;apply H2;simplify;apply in_list_to_in_list_append_l;autobatch]]
qed.
-lemma lookup_swap : ∀a,b,x,vars.
- lookup (swap a b x) (swap_list a b vars) =
- lookup x vars.
-intros 4;elim vars;simplify
- [reflexivity
- |elim (decidable_eq_nat x a1)
- [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
- |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
- [rewrite > H;rewrite > H2;rewrite > swap_left;
- elim (decidable_eq_nat b a1)
- [rewrite < H3;rewrite > swap_right;
- rewrite > (not_eq_to_eqb_false b a)
- [reflexivity
- |intro;autobatch]
- |rewrite > (swap_other a b a1)
- [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
- |*:intro;autobatch]]
- |elim (decidable_eq_nat x b)
- [rewrite > H;rewrite > H3;rewrite > swap_right;
- elim (decidable_eq_nat a1 a)
- [rewrite > H4;rewrite > swap_left;
- rewrite > (not_eq_to_eqb_false a b)
- [reflexivity
- |intro;autobatch]
- |rewrite > (swap_other a b a1)
- [rewrite > (not_eq_to_eqb_false a a1)
- [reflexivity
- |intro;autobatch]
- |assumption
- |intro;autobatch]]
- |rewrite > H;rewrite > (swap_other a b x)
- [elim (decidable_eq_nat a a1)
- [rewrite > H4;rewrite > swap_left;
- rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
- |elim (decidable_eq_nat b a1)
- [rewrite > H5;rewrite > swap_right;
- rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
- |rewrite > (swap_other a b a1)
- [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
- |*:intro;autobatch]]]
- |*:assumption]]]]]
-qed.
-
-lemma posn_swap : ∀a,b,x,vars.
- posn vars x = posn (swap_list a b vars) (swap a b x).
-intros 4;elim vars;simplify
- [reflexivity
- |rewrite < H;elim (decidable_eq_nat x a1)
- [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
- |elim (decidable_eq_nat (swap a b x) (swap a b a1))
- [elim H1;autobatch
- |rewrite > (not_eq_to_eqb_false ? ? H1);
- rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
-qed.
-
theorem encode_swap : ∀a,x,T,vars.
- ((in_list ? a (fv_NTyp T)) → (in_list ? a vars)) →
- (in_list ? x vars) →
+ (a ∈ (fv_NTyp T) → a ∈ vars) →
+ x ∈ vars →
encodetype T vars =
encodetype (swap_NTyp a x T) (swap_list a x vars).
intros 3;elim T
qed.
lemma encode_swap2 : ∀a:nat.∀x:nat.∀T:NTyp.
- ¬(in_list ? a (fv_NTyp T)) →
- ∀vars.in_list ? x vars
- →encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
+ a ∉ (fv_NTyp T) →
+ ∀vars.x ∈ vars
+ → encodetype T vars=encodetype (swap_NTyp a x T) (swap_list a x vars).
intros;apply (encode_swap ? ? ? ? ? H1);intro;elim (H H2);
qed.
-lemma remove_inlist : \forall x,y,l.(in_list ? x (remove_nat y l)) \to
- (in_list ? x l) \land x \neq y.
-intros 3;elim l 0;simplify;intro
- [elim (not_in_list_nil ? ? H)
- |elim (decidable_eq_nat y a)
- [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
- rewrite > H in H1;elim (H1 H2);rewrite > H;split
- [apply in_list_cons;assumption
- |assumption]
- |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
- inversion H2;intros;destruct;
- [split;autobatch
- |elim (H1 H3);split;autobatch]]]
-qed.
-
-lemma inlist_remove : ∀x,y,l.(in_list ? x l → x \neq y →
- (in_list ? x (remove_nat y l))).
-intros 3;elim l
- [elim (not_in_list_nil ? ? H);
- |simplify;elim (decidable_eq_nat y a)
- [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
- [inversion H1;intros;destruct;
- [elim H2;reflexivity
- |assumption]
- |assumption]
- |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
- inversion H1;intros;destruct;autobatch]]
-qed.
-
-lemma incl_fv_var : \forall T.(incl ? (fv_NTyp T) (var_NTyp T)).
+lemma incl_fv_var : \forall T.(fv_NTyp T) ⊆ (var_NTyp T).
intro;elim T;simplify;unfold;intros
[1,2:assumption
|elim (in_list_append_to_or_in_list ? ? ? ? H2);autobatch
qed.
lemma fv_encode2 : ∀T,l1,l2.
- (∀x.(in_list ? x (fv_NTyp T)) →
+ (∀x.x ∈ (fv_NTyp T) →
(lookup x l1 = lookup x l2 ∧
posn l1 x = posn l2 x)) →
(encodetype T l1 = encodetype T l2).
[assumption|intro;assumption]
qed.
-lemma alpha_sym : \forall S,T.(alpha_eq S T) \to (alpha_eq T S).
-intros;elim H
- [apply A_refl
- |apply A_arrow;assumption
- |apply A_forall
- [assumption
- |intros;apply H4;intro;apply H5;elim (decidable_eq_nat Z n5)
- [rewrite > H7;apply in_list_head
- |apply in_list_cons;inversion H6;intros;destruct;
- [apply in_list_head
- |apply in_list_cons;inversion H8;intros;destruct;
- [elim H7;reflexivity
- |elim (in_list_append_to_or_in_list ? ? ? ? H10);autobatch]]]]]
-qed.
-
-(*legacy*)
-lemma nat_in_list_case :∀G,H,n.in_list nat n (H@G) →
- in_list nat n G ∨ in_list nat n H.
-intros;elim (in_list_append_to_or_in_list ???? H1)
-[right;assumption
-|left;assumption]
-qed.
-
lemma inlist_fv_swap : ∀x,y,b,T.
- (¬ in_list ? b (y::var_NTyp T)) →
- in_list ? x (fv_NTyp (swap_NTyp b y T)) →
- x ≠ y ∧ (x = b ∨ (in_list ? x (fv_NTyp T))).
+ b ∉ (y::var_NTyp T) →
+ x ∈ (fv_NTyp (swap_NTyp b y T)) →
+ x ≠ y ∧ (x = b ∨ x ∈ (fv_NTyp T)).
intros 4;elim T
[simplify in H;simplify;simplify in H1;elim (decidable_eq_nat y n)
[rewrite > H2 in H1;rewrite > swap_right in H1;inversion H1;intros;destruct;
|elim H6
[left;assumption
|right;apply in_list_to_in_list_append_r;assumption]]
- |intro;apply H2;elim (nat_in_list_case (var_NTyp n1) [y] ? H5)
- [apply (in_list_to_in_list_append_r ? ? (y::var_NTyp n) (var_NTyp n1));
- assumption
- |inversion H6;intros;destruct;
- [apply in_list_head
- |elim (not_in_list_nil ? ? H7)]]
+ |intro;apply H2;elim (in_list_append_to_or_in_list ?? [y] (var_NTyp n1) H5)
+ [lapply (in_list_singleton_to_eq ??? H6);applyS in_list_head
+ |autobatch]
|assumption]]
|simplify;simplify in H3;simplify in H2;elim (in_list_append_to_or_in_list ? ? ? ? H3)
[elim H
qed.
lemma inlist_fv_swap_r : ∀x,y,b,T.
- (¬(in_list ? b (y::var_NTyp T))) →
- ((x = b ∧ (in_list ? y (fv_NTyp T))) ∨
- (x \neq y ∧ (in_list ? x (fv_NTyp T)))) →
- (in_list ? x (fv_NTyp (swap_NTyp b y T))).
+ (b ∉ (y::var_NTyp T)) →
+ ((x = b ∧ y ∈ (fv_NTyp T)) ∨
+ (x ≠ y ∧ x ∈ (fv_NTyp T))) →
+ x ∈ (fv_NTyp (swap_NTyp b y T)).
intros 4;elim T
[simplify;simplify in H;simplify in H1;cut (b ≠ n)
[elim H1
|change in ⊢ (???%) with ((y::n::var_NTyp n1)@var_NTyp n2);autobatch]]
|intro;apply H2;inversion H4;simplify;intros;destruct;autobatch depth=4]]
qed.
-
-lemma fv_alpha : ∀S,T.alpha_eq S T → incl ? (fv_NTyp S) (fv_NTyp T).
-intros;elim H;simplify;unfold;intros
- [assumption
- |elim (in_list_append_to_or_in_list ? ? ? ? H5);autobatch
- |elim (in_list_append_to_or_in_list ? ? ? ? H5)
- [autobatch
- |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
- apply in_list_to_in_list_append_r;
- lapply (H4 ? H7);
- elim (remove_inlist ? ? ? H6);apply inlist_remove
- [lapply (inlist_fv_swap_r x n4 a n1)
- [elim (inlist_fv_swap x n5 a n3)
- [elim H11
- [rewrite < H12 in H7;elim H7;autobatch depth=5;
- |assumption]
- |intro;apply H7;inversion H10;intros;destruct;autobatch depth=4
- |autobatch]
- |intro;apply H7;inversion H10;intros;destruct;autobatch depth=4
- |right;split;assumption]
- |intros;intro;lapply (inlist_fv_swap_r x n4 a n1)
- [lapply (Hletin ? Hletin1);elim (inlist_fv_swap x n5 a n3 ? Hletin2)
- [apply (H11 H10)
- |intro;apply H7;elim (decidable_eq_nat a n4)
- [rewrite > H12;apply in_list_head
- |apply in_list_cons;inversion H11;intros;destruct;autobatch]]
- |intro;apply H7;inversion H11;intros;destruct;autobatch depth=4
- |right;split;assumption]]]]
-qed.
-
-theorem alpha_to_encode : ∀S,T.alpha_eq S T →
- ∀vars.encodetype S vars = encodetype T vars.
-intros 3;elim H
-[reflexivity
-|simplify;rewrite > H2;rewrite > H4;reflexivity
-|simplify;rewrite > H2;
- cut (encodetype n1 (n4::vars) = encodetype n3 (n5::vars))
- [rewrite > Hcut;reflexivity
- |elim (fresh_name (n4::n5::var_NTyp n1@var_NTyp n3));
- lapply (encode_swap2 a n4 n1 ? (n4::vars))
- [intro;apply H5;autobatch depth=5
- |lapply (encode_swap2 a n5 n3 ? (n5::vars))
- [intro;autobatch depth=5
- |rewrite > Hletin;rewrite > Hletin1;simplify;rewrite > swap_right;
- rewrite > swap_right;rewrite > (H4 a H5 (a::swap_list a n4 vars));
- rewrite > (fv_encode2 ? ? (a::swap_list a n5 vars))
- [reflexivity
- |intros;elim (decidable_eq_nat n4 n5)
- [autobatch
- |cut ((x ≠ n4) ∧ (x ≠ n5))
- [elim Hcut;elim (decidable_eq_nat x a);simplify
- [rewrite > (eq_to_eqb_true ? ? H10);simplify;autobatch
- |rewrite > (not_eq_to_eqb_false ? ? H10);simplify;elim vars;simplify
- [autobatch
- |elim H11;rewrite < H12;rewrite > H13;elim (decidable_eq_nat a a1)
- [rewrite > H14;do 2 rewrite > swap_left;
- rewrite > (not_eq_to_eqb_false ? ? H8);
- rewrite > (not_eq_to_eqb_false ? ? H9);simplify;autobatch
- |elim (decidable_eq_nat n4 a1)
- [rewrite > H15;rewrite > swap_right;rewrite > (swap_other a n5 a1)
- [rewrite > (not_eq_to_eqb_false ? ? H10);rewrite < H15;
- rewrite > (not_eq_to_eqb_false ? ? H8);autobatch
- |intro;autobatch
- |intro;autobatch]
- |rewrite > (swap_other a n4 a1);elim (decidable_eq_nat n5 a1)
- [rewrite < H16;rewrite > swap_right;
- rewrite > (not_eq_to_eqb_false ? ? H9);
- rewrite > (not_eq_to_eqb_false ? ? H10);autobatch
- |rewrite > (swap_other a n5 a1);try intro;autobatch
- |*:intro;autobatch]]]]]
- |split
- [lapply (H3 ? H5);lapply (alpha_sym ? ? Hletin2);
- lapply (fv_alpha ? ? Hletin3);lapply (Hletin4 ? H6);
- elim (inlist_fv_swap ? ? ? ? ? Hletin5)
- [assumption
- |intro;apply H5;inversion H8;intros;destruct;autobatch depth=4]
- |elim (inlist_fv_swap ? ? ? ? ? H6)
- [assumption
- |intro;apply H5;elim (decidable_eq_nat a n4)
- [applyS in_list_head
- |apply in_list_cons;inversion H8;intros;destruct;autobatch]]]]]]
- |apply in_list_head]
- |apply in_list_head]]]
-qed.
lemma encode_append : ∀T,U,n,l.length ? l ≤ n →
subst_type_nat (encodetype T l) U n = encodetype T l.
|intro;rewrite > H2 in Hletin1;unfold in Hletin1;autobatch]
|cut (lookup n l = false)
[rewrite > Hcut;reflexivity
- |generalize in match H1;elim (lookup n l);
- [elim H2;reflexivity|reflexivity]]]
+ |elim (lookup n l) in H1;
+ [elim H1;reflexivity|reflexivity]]]
|reflexivity
|autobatch
|rewrite > (H ? ? H2);rewrite > H1;
encodetype T l = subst_type_nat (encodetype T (l@[X])) (TFree X) (length ? l).
intros 2;elim T;simplify
[cut (lookup n l = true → posn l n = posn (l@[X]) n)
- [generalize in match Hcut;elim (bool_to_decidable_eq (lookup n l) true)
+ [elim (bool_to_decidable_eq (lookup n l) true) in Hcut
[cut (lookup n (l@[X]) = true)
- [rewrite > H;rewrite > Hcut1;simplify;
+ [rewrite > H;rewrite > Hcut;simplify;
cut (eqb (posn (l@[X]) n) (length nat l) = false)
- [rewrite > Hcut2;simplify;rewrite < (H1 H);reflexivity
- |generalize in match H;elim l 0
- [simplify;intro;destruct H2
+ [rewrite > Hcut1;simplify;rewrite < (H1 H);reflexivity
+ |elim l in H 0
+ [simplify;intro;destruct
|intros 2;simplify;elim (eqb n a);simplify
[reflexivity
- |simplify in H3;apply (H2 H3)]]]
- |generalize in match H;elim l
- [simplify in H2;destruct H2
- |generalize in match H3;simplify;elim (eqb n a) 0;simplify;intro
+ |simplify in H3;apply (H H2)]]]
+ |elim l in H
+ [simplify in H;destruct
+ |generalize in match H2;simplify;elim (eqb n a) 0;simplify;intro
[reflexivity
- |apply (H2 H4)]]]
+ |apply (H H3)]]]
|cut (lookup n l = false)
[elim (decidable_eq_nat n X)
- [rewrite > Hcut1;rewrite > H2;cut (lookup X (l@[X]) = true)
- [rewrite > Hcut2;simplify;cut (eqb (posn (l@[X]) X) (length nat l) = true)
- [rewrite > Hcut3;simplify;reflexivity
- |generalize in match Hcut1;elim l 0
+ [rewrite > Hcut;rewrite > H2;cut (lookup X (l@[X]) = true)
+ [rewrite > Hcut1;simplify;cut (eqb (posn (l@[X]) X) (length nat l) = true)
+ [rewrite > Hcut2;simplify;reflexivity
+ |elim l in Hcut 0
[intros;simplify;rewrite > eqb_n_n;simplify;reflexivity
|simplify;intros 2;rewrite > H2;elim (eqb X a);simplify in H4
- [destruct H4
+ [destruct
|apply (H3 H4)]]]
|elim l;simplify
[rewrite > eqb_n_n;reflexivity
[reflexivity
|assumption]]]
|cut (lookup n l = lookup n (l@[X]))
- [rewrite < Hcut2;rewrite > Hcut1;simplify;reflexivity
+ [rewrite < Hcut1;rewrite > Hcut;simplify;reflexivity
|elim l;simplify
[rewrite > (not_eq_to_eqb_false ? ? H2);simplify;reflexivity
|elim (eqb n a);simplify
[reflexivity
|assumption]]]]
- |generalize in match H;elim (lookup n l);
- [elim H2;reflexivity|reflexivity]]]
+ |elim (lookup n l) in H
+ [elim H;reflexivity|reflexivity]]]
|elim l 0
- [intro;simplify in H;destruct H
+ [intro;simplify in H;destruct
|simplify;intros 2;elim (eqb n a);simplify
[reflexivity
|simplify in H1;rewrite < (H H1);reflexivity]]]
rewrite < (H1 ([n]@l));reflexivity]
qed.
-lemma encode_subst : ∀T,X,Y,l.¬(in_list ? X l) → ¬(in_list ? Y l) →
- (in_list ? X (fv_NTyp T) → X = Y) →
+lemma encode_subst : ∀T,X,Y,l.X ∉ l → Y ∉ l →
+ (X ∈ (fv_NTyp T) → X = Y) →
encodetype (swap_NTyp X Y T) l =
subst_type_nat (encodetype T (l@[Y])) (TFree X) (length ? l).
apply NTyp_len_ind;intro;elim U
[simplify;rewrite > Hcut;rewrite > (not_nat_in_to_lookup_false ? ? H2);
simplify;cut (posn (l@[Y]) Y = length ? l)
[rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
- |generalize in match H2;elim l;simplify
+ |elim l in H2;simplify
[rewrite > eqb_n_n;reflexivity
|elim (decidable_eq_nat Y a)
- [elim H6;rewrite > H7;apply in_list_head
- |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;rewrite < H5
+ [elim H5;rewrite > H6;apply in_list_head
+ |rewrite > (not_eq_to_eqb_false ? ? H6);simplify;rewrite < H2
[reflexivity
|intro;autobatch]]]]
|elim l;simplify
cut (lookup Y (l@[Y]) = true)
[rewrite > Hcut;simplify;cut (posn (l@[Y]) Y = length ? l)
[rewrite > Hcut1;rewrite > eqb_n_n;reflexivity
- |generalize in match H2;elim l;simplify
+ |elim l in H2;simplify
[rewrite > eqb_n_n;reflexivity
|elim (decidable_eq_nat Y a)
- [elim H7;rewrite > H8;apply in_list_head
- |rewrite > (not_eq_to_eqb_false ? ? H8);simplify;rewrite < H6
+ [elim H6;applyS in_list_head
+ |rewrite > (not_eq_to_eqb_false ? ? H7);simplify;rewrite < H2
[reflexivity
|intro;autobatch]]]]
|elim l;simplify
|simplify;rewrite > (swap_other X Y n)
[cut (lookup n l = lookup n (l@[Y]) ∧
(lookup n l = true → posn l n = posn (l@[Y]) n))
- [elim Hcut;rewrite > H6;generalize in match H7;
- generalize in match H6;elim (lookup n (l@[Y]));simplify;
- [rewrite < H9;generalize in match H8;elim l
- [simplify in H10;destruct H10;
+ [elim Hcut;rewrite > H6;elim (lookup n (l@[Y])) in H7 H6;simplify;
+ [rewrite < H7;elim l in H6
+ [simplify in H6;destruct
|elim (decidable_eq_nat n a);simplify
- [rewrite > (eq_to_eqb_true ? ? H12);reflexivity
- |rewrite > (not_eq_to_eqb_false ? ? H12);
- simplify;generalize in match H10;elim (eqb (posn l1 n) (length nat l1))
- [simplify in H13;simplify in H11;
- rewrite > (not_eq_to_eqb_false ? ? H12) in H11;
- simplify in H11;lapply (H13 H11);destruct Hletin
+ [rewrite > (eq_to_eqb_true ? ? H9);reflexivity
+ |rewrite > (not_eq_to_eqb_false ? ? H9);
+ simplify;elim (eqb (posn l1 n) (length nat l1)) in H6
+ [simplify in H8;simplify in H6;
+ rewrite > (not_eq_to_eqb_false ? ? H9) in H8;
+ simplify in H8;lapply (H6 H8);destruct
|reflexivity]]
|*:assumption]
|reflexivity]
|intro;apply H5;simplify;autobatch]
|simplify;rewrite < (H2 n1 ? ? ? ? H3 H4)
[cut (l = swap_list X Y l)
- [|generalize in match H3;generalize in match H4;elim l;simplify
+ [|elim l in H3 H4;simplify
[reflexivity
|elim (decidable_eq_nat a X)
- [elim H8;rewrite > H9;apply in_list_head
+ [elim H4;applyS in_list_head
|elim (decidable_eq_nat a Y)
- [elim H7;rewrite > H10;apply in_list_head
+ [elim H6;applyS in_list_head
|rewrite > (swap_other X Y a)
- [rewrite < H6
+ [rewrite < H3
[reflexivity
|*:intro;autobatch]
|*:assumption]]]]]
|intro;apply H5;simplify;autobatch]]
qed.
-lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
-intros;unfold in match swap;simplify;elim (eqb x u);simplify
- [autobatch
- |elim (eqb x v);simplify;autobatch]
-qed.
-
-lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (incl ? (fv_NTyp T) (fv_Nenv G)).
+lemma in_fvNTyp_in_fvNenv : ∀G,T.(NWFType G T) → (fv_NTyp T) ⊆ (fv_Nenv G).
intros;elim H;simplify;unfold;intros;
[inversion H2;intros;destruct;
[assumption
autobatch depth=5
|apply (in_remove ? ? ? H15 H16)]]
|simplify;simplify in H13;elim (remove_inlist ? ? ? H13);
- elim (nat_in_list_case ? ? ? H14);
- [apply in_list_to_in_list_append_r;apply in_remove;
+ elim (in_list_append_to_or_in_list ???? H14)
+ [apply in_list_to_in_list_append_l;apply H10;
+ [rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n4));
+ intro;apply H12;simplify;
+ rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
+ elim (in_list_append_to_or_in_list ???? H17);autobatch depth=4
+ |autobatch]
+ |apply in_list_to_in_list_append_r;apply in_remove;
[elim (remove_inlist ? ? ? H16);intro;apply H18;
elim (swap_case a n n3)
[elim H20
[rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n5));
intro;apply H12;simplify;
rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4 @ var_NTyp n5));
- elim (nat_in_list_case ? ? ? H17);autobatch depth=4
- |elim (remove_inlist ? ? ? H16);autobatch]]
- |apply in_list_to_in_list_append_l;apply H10;
- [rewrite < (associative_append ? [x] (fv_Nenv l) (var_NTyp n4));
- intro;apply H12;simplify;
- rewrite < (associative_append ? [x] (fv_Nenv l) (n3::var_NTyp n4@var_NTyp n5));
- elim (nat_in_list_case ? ? ? H17);autobatch depth=4
- |autobatch]]]]
+ elim (in_list_append_to_or_in_list ???? H17);autobatch depth=4
+ |elim (remove_inlist ? ? ? H16);autobatch]]]]]
|split
[intro;apply H7;rewrite > H8;apply in_list_head
|elim (remove_inlist ? ? ? H6);assumption]]
|right;intro;autobatch depth=5]]]
qed.
-lemma fv_NTyp_fv_Typ : ∀T,X,l.(in_list ? X (fv_NTyp T)) → ¬(in_list ? X l) →
- (in_list ? X (fv_type (encodetype T l))).
+lemma fv_NTyp_fv_Typ : ∀T,X,l.X ∈ (fv_NTyp T) → X ∉ l →
+ X ∈ (fv_type (encodetype T l)).
intros 2;elim T;simplify
[simplify in H;cut (X = n)
[rewrite < Hcut;generalize in match (lookup_in X l);elim (lookup X l)
|*:apply not_in_list_nil]]]
qed.
-lemma not_in_list_encodetype : \forall T,l,x.in_list ? x l \to
- \lnot (in_list ? x (fv_type (encodetype T l))).
+lemma not_in_list_encodetype : \forall T,l,x.x ∈ l \to
+ \lnot x ∈ (fv_type (encodetype T l)).
intro;elim T;simplify
[apply (bool_elim ? (lookup n l));intro;simplify
[apply not_in_list_nil
[rewrite > (in_lookup ? ? H) in H1;destruct H1
|apply (not_in_list_nil ? ? H3)]]
|apply not_in_list_nil
- |intro;elim (nat_in_list_case ? ? ? H3);autobatch
- |intro;elim (nat_in_list_case ? ? ? H3);
- [apply (H1 (n::l) x ? H4);apply in_list_cons;assumption
- |autobatch]]
+ |intro;elim (in_list_append_to_or_in_list ???? H3);autobatch
+ |intro;elim (in_list_append_to_or_in_list ???? H3);
+ [autobatch
+ |apply (H1 (n::l) x ? H4);apply in_list_cons;assumption]]
qed.
-lemma incl_fv_encode_fv : \forall T,l.incl ? (fv_type (encodetype T l)) (fv_NTyp T).
+lemma incl_fv_encode_fv : \forall T,l.(fv_type (encodetype T l)) ⊆ (fv_NTyp T).
intro;elim T;simplify;unfold;
[intro;elim (lookup n l);simplify in H
[elim (not_in_list_nil ? ? H)
intros;elim H;simplify;autobatch;
qed.
-lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.incl ? (fv_Nenv G) (fv_Nenv H)
+lemma NWFT_env_incl : ∀G,T.NWFType G T → ∀H.(fv_Nenv G) ⊆ (fv_Nenv H)
→ NWFType H T.
intros 3;elim H
[4:apply NWFT_Forall
|intros;apply (H4 ? ? H8);
[intro;apply H7;apply (H6 ? H9)
|unfold;intros;simplify;simplify in H9;inversion H9;intros;
- destruct;autobatch]]
+ destruct;simplify;
+ [autobatch
+ |apply in_list_cons;apply H6;apply H10]]]
|*:autobatch]
qed.
[elim (not_in_list_nil ? ? H1)
|inversion H6;intros;destruct;
[simplify;autobatch
- |elim a;simplify;autobatch]]
+ |elim a;simplify;elim b;simplify;try apply in_list_cons;
+ apply H1;apply H7]]
|assumption]
|elim H2;elim H4;split;autobatch
- |split;assumption
- |elim H2;split
- [lapply (adeq_WFT ? ? H5);autobatch;
- |lapply (adeq_WFT ? ? H6);autobatch]]
+ |split;assumption]
qed.
theorem adequacy : ∀G,T,U.NJSubtype G T U →
apply (H6 ? H7)
[elim (decidable_eq_nat X n)
[left;assumption
- |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7;
- autobatch]
+ |right;intro;autobatch depth=5]
|elim (decidable_eq_nat X n1)
[left;assumption
- |right;intro;lapply (in_remove ? ? ? H10 H11);elim H7;
- autobatch]]
- |2,3:apply not_in_list_nil
+ |right;intro;autobatch depth=5]]
+ |2,3:autobatch
|intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);
lapply (in_fvNTyp_in_fvNenv ? ? H10);simplify in Hletin1;
elim (decidable_eq_nat X n1)
[assumption
- |lapply (in_remove ? ? ? H11 H8);elim H7;autobatch]]
+ |elim H7;autobatch depth=4]]
|2,3:autobatch
|intro;elim (NJSubtype_to_NWFT ? ? ? Hletin);lapply (in_fvNTyp_in_fvNenv ? ? H9);
simplify in Hletin1;elim (decidable_eq_nat X n)
[assumption
- |lapply (in_remove ? ? ? H11 H8);elim H7;autobatch]]]
- |rewrite < (alpha_to_encode ? ? H3);rewrite < (alpha_to_encode ? ? H4);
- assumption]
+ |elim H7;autobatch depth=4]]]]
qed.
let rec closed_type T n ≝
| Arrow T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 n
| Forall T1 T2 ⇒ closed_type T1 n ∧ closed_type T2 (S n)].
-alias id "nth" = "cic:/matita/list/list/nth.con".
-alias id "length" = "cic:/matita/list/list/length.con".
-definition distinct_list ≝
-λl.∀n,m.n < length ? l → m < length ? l → n ≠ m → nth ? l O n ≠ nth ? l O m.
-
-lemma posn_nth: ∀l,n.distinct_list l → n < length ? l →
- posn l (nth ? l O n) = n.
-intro;elim l
- [simplify in H1;elim (not_le_Sn_O ? H1)
- |simplify in H2;generalize in match H2;elim n
- [simplify;rewrite > eqb_n_n;simplify;reflexivity
- |simplify;cut (nth ? (a::l1) O (S n1) ≠ nth ? (a::l1) O O)
- [simplify in Hcut;rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
- rewrite > (H n1)
- [reflexivity
- |unfold;intros;unfold in H1;lapply (H1 (S n2) (S m));
- [simplify in Hletin;assumption
- |2,3:simplify;autobatch
- |intro;apply H7;destruct H8;reflexivity]
- |autobatch]
- |intro;apply H1;
- [6:apply H5
- |skip
- |skip
- |(*** *:autobatch; *)
- apply H4
- |simplify;autobatch
- |intro;elim (not_eq_O_S n1);symmetry;assumption]]]]
-qed.
-
-lemma nth_in_list : ∀l,n. n < length ? l → in_list ? (nth ? l O n) l.
-intro;elim l
- [simplify in H;elim (not_le_Sn_O ? H)
- |generalize in match H1;elim n;simplify
- [apply in_list_head
- |apply in_list_cons;apply H;simplify in H3;apply (le_S_S_to_le ? ? H3)]]
-qed.
-
-lemma lookup_nth : \forall l,n.n < length ? l \to
- lookup (nth nat l O n) l = true.
-intro;elim l
- [elim (not_le_Sn_O ? H);
- |generalize in match H1;elim n;simplify
- [rewrite > eqb_n_n;reflexivity
- |elim (eqb (nth nat l1 O n1) a);simplify;
- [reflexivity
- |apply H;apply le_S_S_to_le;assumption]]]
-qed.
-
lemma decoder : ∀T,n.closed_type T n →
∀l.length ? l = n → distinct_list l →
- (\forall x. in_list ? x (fv_type T) \to \lnot in_list ? x l) \to
+ (\forall x. x ∈ (fv_type T) \to x ∉ l) \to
∃U.T = encodetype U l.
intro;elim T
[simplify in H;apply (ex_intro ? ? (TName (nth ? l O n)));simplify;
|elim a in H6;simplify in H6;destruct H6;apply NWFE_cons;autobatch]]
qed.
-lemma xxx : \forall b,X,T,l.
+lemma in_list_encodeenv : \forall b,X,T,l.
in_list ? (mk_bound b X (encodetype T [])) (encodeenv l) \to
\exists U.encodetype U [] = encodetype T [] \land
- in_list ? (mk_nbound b X U) l.
+ (mk_nbound b X U) ∈ l.
intros 4;elim l
[simplify in H;elim (not_in_list_nil ? ? H)
|simplify in H1;inversion H1;elim a 0;simplify;intros;destruct;
qed.
lemma eq_swap_NTyp_to_case :
- \forall X,Y,Z,T.\lnot in_list ? Y (X::var_NTyp T) \to
+ \forall X,Y,Z,T. Y ∉ (X::var_NTyp T) \to
swap_NTyp Z Y (swap_NTyp Y X T) = swap_NTyp Z X T \to
- Z = X \lor \lnot in_list ? Z (fv_NTyp T).
+ Z = X \lor Z ∉ (fv_NTyp T).
intros 4;elim T
[simplify in H;simplify in H1;elim (decidable_eq_nat X n)
[rewrite > H2;simplify;elim (decidable_eq_nat Z n)
|rewrite > H3 in H2;rewrite < eq_fv_Nenv_fv_env in H2;assumption]
|intros;cut (T2 = TName n)
[|elim T2 in H5 0;simplify;intros;destruct;reflexivity]
- rewrite > Hcut;
- elim (decoder t1 O ? []);
- [rewrite > H4 in H1;rewrite > H7 in H1;elim (xxx ? ? ? ? H1);elim H8;
- autobatch
+ rewrite > Hcut;elim (decoder t1 O ? []);
+ [rewrite > H4 in H1;rewrite > H7 in H1;elim (in_list_encodeenv ???? H1);
+ elim H8;autobatch
|4:unfold;intros;simplify in H7;elim (not_le_Sn_O ? H7)
|*:autobatch]
|intros;cut (∃u,u1,u2,u3.T2 = NArrow u u1 ∧ U2 = NArrow u2 u3)
(*** definitions about lists ***)
+definition filter_types : list bound → list bound ≝
+ λG.(filter ? G (λB.match B with [mk_bound B X T ⇒ B])).
+
definition fv_env : list bound → list nat ≝
- λG.(map ? ? (λb.match b with [mk_bound B X T ⇒ X]) G).
+ λG.(map ? ? (λb.match b with [mk_bound B X T ⇒ X]) (filter_types G)).
let rec fv_type T ≝
match T with
(subst_type_nat S2 (TFree X) O) (subst_type_nat T2 (TFree X) O)) →
JSubtype G (Forall S1 S2) (Forall T1 T2).
-notation "hvbox(e ⊢ break ta ⊴ break tb)"
+notation "mstyle color #007f00 (hvbox(e ⊢ break ta ⊴ break tb))"
non associative with precedence 30 for @{ 'subjudg $e $ta $tb }.
interpretation "Fsub subtype judgement" 'subjudg e ta tb = (JSubtype e ta tb).
-notation > "hvbox(\Forall S.T)"
+notation "mstyle color #007f00 (hvbox(e ⊢ ♦))"
+ non associative with precedence 30 for @{ 'wfejudg $e }.
+interpretation "Fsub WF env judgement" 'wfejudg e = (WFEnv e).
+
+notation "mstyle color #007f00 (hvbox(e ⊢ break t))"
+ non associative with precedence 30 for @{ 'wftjudg $e $t }.
+interpretation "Fsub WF type judgement" 'wftjudg e t = (WFType e t).
+
+notation > "\Forall S.T"
non associative with precedence 60 for @{ 'forall $S $T}.
-notation < "hvbox('All' \sub S. break T)"
+notation < "hvbox(⊓ \sub S. break T)"
non associative with precedence 60 for @{ 'forall $S $T}.
interpretation "universal type" 'forall S T = (Forall S T).
right associative with precedence 55 for @{ 'arrow $s $t }.
interpretation "arrow type" 'arrow S T = (Arrow S T).
-notation "hvbox(S [# n ↦ T])"
+notation "hvbox(S [#n ↦ T])"
non associative with precedence 80 for @{ 'substvar $S $T $n }.
interpretation "subst bound var" 'substvar S T n = (subst_type_nat S T n).
(*** theorems about lists ***)
-lemma boundinenv_natinfv : ∀x,G.(∃B,T.in_list ? (mk_bound B x T) G) →
- in_list ? x (fv_env G).
+lemma boundinenv_natinfv : ∀x,G.(∃T.!x ⊴ T ∈ G) → x ∈ (fv_env G).
intros 2;elim G;decompose
- [elim (not_in_list_nil ? ? H)
- |elim (in_list_cons_case ? ? ? ? H1)
- [rewrite < H2;simplify;apply in_list_head
- |simplify;apply in_list_cons;apply H;autobatch]]
+ [elim (not_in_list_nil ? ? H1)
+ |elim (in_list_cons_case ? ? ? ? H2)
+ [rewrite < H1;simplify;apply in_list_head
+ |elim a;apply (bool_elim ? b);intro;simplify;try apply in_list_cons;
+ apply H;autobatch]]
qed.
-lemma natinfv_boundinenv : ∀x,G.in_list ? x (fv_env G) →
- ∃B,T.in_list ? (mk_bound B x T) G.
+lemma natinfv_boundinenv : ∀x,G.x ∈ (fv_env G) → ∃T.!x ⊴ T ∈ G.
intros 2;elim G 0
[simplify;intro;lapply (not_in_list_nil ? ? H);elim Hletin
|intros 3;
- elim a;simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
+ elim a;simplify in H1;elim b in H1;simplify in H1
+ [elim (in_list_cons_case ? ? ? ? H1)
[rewrite < H2;autobatch
- |elim (H H2);elim H3;apply ex_intro[apply a1];autobatch]]
+ |elim (H H2);autobatch]
+ |elim (H H1);autobatch]]
qed.
-lemma incl_bound_fv : ∀l1,l2.incl ? l1 l2 → incl ? (fv_env l1) (fv_env l2).
+lemma incl_bound_fv : ∀l1,l2.l1 ⊆ l2 → (fv_env l1) ⊆ (fv_env l2).
intros;unfold in H;unfold;intros;apply boundinenv_natinfv;
lapply (natinfv_boundinenv ? ? H1);decompose;autobatch depth=4;
qed.
-lemma incl_cons : ∀x,l1,l2.incl ? l1 l2 → incl nat (x :: l1) (x :: l2).
-intros.unfold in H.unfold.intros.elim (in_list_cons_case ? ? ? ? H1)
- [applyS in_list_head|autobatch]
-qed.
-
-lemma WFT_env_incl : ∀G,T.WFType G T →
- ∀H.incl ? (fv_env G) (fv_env H) → WFType H T.
+lemma WFT_env_incl : ∀G,T.(G ⊢ T) → ∀H.fv_env G ⊆ fv_env H → (H ⊢ T).
intros 3.elim H
[apply WFT_TFree;unfold in H3;apply (H3 ? H1)
|apply WFT_Top
[apply (H2 ? H6)
|intros;apply (H4 ? ? H8)
[unfold;intro;autobatch
- |simplify;apply (incl_cons ? ? ? H6)]]]
+ |simplify;apply (incl_cons ???? H6)]]]
qed.
-lemma fv_env_extends : ∀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
- [reflexivity|elim a;simplify;rewrite > H1;reflexivity]
+lemma fv_env_extends : ∀H,x,T,U,G,B.
+ fv_env (H @ mk_bound B x T :: G) =
+ fv_env (H @ mk_bound B x U :: G).
+intros 5;elim H;elim B
+ [1,2:reflexivity
+ |*:elim a;elim b;simplify;lapply (H1 true);lapply (H1 false);
+ try rewrite > Hletin;try rewrite > Hletin1;reflexivity]
qed.
lemma lookup_env_extends : ∀G,H,B,C,D,T,U,V,x,y.
- in_list ? (mk_bound D y V) (H @ ((mk_bound C x U) :: G)) → y ≠ x →
- in_list ? (mk_bound D y V) (H @ ((mk_bound B x T) :: G)).
+ mk_bound D y V ∈ H @ mk_bound C x U :: G → y ≠ x →
+ mk_bound D y V ∈ H @ mk_bound B x T :: G.
intros 10;elim H
[simplify in H1;elim (in_list_cons_case ? ? ? ? H1)
[destruct H3;elim H2;reflexivity
|apply (in_list_cons ? ? ? ? (H1 H4 H3))]]
qed.
-lemma in_FV_subst : ∀x,T,U,n.in_list ? x (fv_type T) →
- in_list ? x (fv_type (subst_type_nat T U n)).
+lemma in_FV_subst : ∀x,T,U,n.x ∈ fv_type T → x ∈ fv_type (subst_type_nat T U n).
intros 3;elim T
[simplify in H;elim (not_in_list_nil ? ? H)
|2,3:simplify;simplify in H;assumption
(*** lemma on fresh names ***)
-lemma fresh_name : ∀l:list nat.∃n.¬in_list ? n l.
+lemma fresh_name : ∀l:list nat.∃n.n ∉ l.
cut (∀l:list nat.∃n.∀m.n ≤ m → ¬ in_list ? m l);intros
[lapply (Hcut l);elim Hletin;apply ex_intro;autobatch
|elim l
(*** lemmata on well-formedness ***)
-lemma fv_WFT : ∀T,x,G.WFType G T → in_list ? x (fv_type T) →
- in_list ? x (fv_env G).
+lemma fv_WFT : ∀T,x,G.(G ⊢ T) → x ∈ fv_type T → x ∈ fv_env G.
intros 4.elim H
[simplify in H2;elim (in_list_cons_case ? ? ? ? H2)
[applyS H1|elim (not_in_list_nil ? ? H3)]
(*** lemmata relating subtyping and well-formedness ***)
-lemma JS_to_WFE : ∀G,T,U.G ⊢ T ⊴ U → WFEnv G.
+lemma JS_to_WFE : ∀G,T,U.G ⊢ T ⊴ U → G ⊢ ♦.
intros;elim H;assumption.
qed.
-lemma JS_to_WFT : ∀G,T,U.G ⊢ T ⊴ U → WFType G T ∧ WFType G U.
+lemma JS_to_WFT : ∀G,T,U.G ⊢ T ⊴ U → (G ⊢ T) ∧ (G ⊢ U).
intros;elim H
[1,2:autobatch
|split
apply (WFT_env_incl ? ? H10);simplify;unfold;intros;assumption]]
qed.
-lemma JS_to_WFT1 : ∀G,T,U.G ⊢ T ⊴ U → WFType G T.
+lemma JS_to_WFT1 : ∀G,T,U.G ⊢ T ⊴ U → G ⊢ T.
intros;elim (JS_to_WFT ? ? ? H);assumption;
qed.
-lemma JS_to_WFT2 : ∀G,T,U.G ⊢ T ⊴ U → WFType G U.
+lemma JS_to_WFT2 : ∀G,T,U.G ⊢ T ⊴ U → G ⊢ U.
intros;elim (JS_to_WFT ? ? ? H);assumption;
qed.
-lemma WFE_Typ_subst : ∀H,x,B,C,T,U,G.
- WFEnv (H @ ((mk_bound B x T) :: G)) → WFType G U →
- WFEnv (H @ ((mk_bound C x U) :: G)).
-intros 7;elim H 0
+lemma WFE_Typ_subst : ∀H,x,B,T,U,G.
+ H @ mk_bound B x T :: G ⊢ ♦ → (G ⊢ U) →
+ H @ mk_bound B x U :: G ⊢ ♦.
+intros 6;elim H 0
[simplify;intros;inversion H1;intros
[elim (nil_cons ? G (mk_bound B x T) H3)
|destruct H7;autobatch]
[destruct H5
|destruct H9;apply WFE_cons
[apply (H1 H5 H3)
- |rewrite < (fv_env_extends ? x B C T U); assumption
+ |rewrite < (fv_env_extends ? x T U); assumption
|apply (WFT_env_incl ? ? H8);
- rewrite < (fv_env_extends ? x B C T U);unfold;intros;
+ rewrite < (fv_env_extends ? x T U);unfold;intros;
assumption]]]
qed.
-lemma WFE_bound_bound : ∀B,x,T,U,G.WFEnv G → in_list ? (mk_bound B x T) G →
- in_list ? (mk_bound B x U) G → T = U.
-intros 6;elim H
+lemma WFE_bound_bound : ∀x,T,U,G.G ⊢ ♦ → !x ⊴ T ∈ G → !x ⊴ U ∈ G → T = U.
+intros 5;elim H
[lapply (not_in_list_nil ? ? H1);elim Hletin
|elim (in_list_cons_case ? ? ? ? H6)
[destruct H7;destruct;elim (in_list_cons_case ? ? ? ? H5)
|apply (H2 H8 H7)]]]
qed.
-lemma WFT_to_incl: ∀G,T,U.(∀X.¬in_list ? X (fv_env G) → ¬in_list ? X (fv_type U) →
- WFType (mk_bound true X T::G) (subst_type_nat U (TFree X) O))
- → incl ? (fv_type U) (fv_env G).
+lemma WFT_to_incl: ∀G,T,U.(∀X.X ∉ fv_env G → X ∉ fv_type U →
+ (mk_bound true X T::G ⊢ (subst_type_nat U (TFree X) O))) →
+ fv_type U ⊆ fv_env G.
intros;elim (fresh_name (fv_type U@fv_env G));lapply(H a)
[unfold;intros;lapply (fv_WFT ? x ? Hletin)
[simplify in Hletin1;inversion Hletin1;intros
qed.
lemma incl_fv_env: ∀X,G,G1,U,P.
- incl ? (fv_env (G1@(mk_bound true X U::G)))
- (fv_env (G1@(mk_bound true X P::G))).
+ fv_env (G1@ !X ⊴ U::G) ⊆ fv_env (G1@ !X ⊴ P::G).
intros.rewrite < fv_env_extends.apply incl_A_A.
qed.
lemma fv_append : ∀G,H.fv_env (G @ H) = fv_env G @ fv_env H.
-intro;elim G;simplify;autobatch paramodulation;
+intro;elim G;simplify;
+[reflexivity
+|elim a;simplify;elim b;simplify;lapply (H H1);rewrite > Hletin;reflexivity]
qed.
\ No newline at end of file
]
qed.
-(*
-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" 'mem x l = (in_list ? x l).
-
lemma max_case : \forall m,n.(max m n) = match (leb m n) with
[ true \Rightarrow n
| false \Rightarrow m ].
intros;elim m;simplify;reflexivity;
qed.
+
+definition swap : nat → nat → nat → nat ≝
+ λu,v,x.match (eqb x u) with
+ [true ⇒ v
+ |false ⇒ match (eqb x v) with
+ [true ⇒ u
+ |false ⇒ x]].
+
+lemma swap_left : ∀x,y.(swap x y x) = y.
+intros;unfold swap;rewrite > eqb_n_n;simplify;reflexivity;
+qed.
+
+lemma swap_right : ∀x,y.(swap x y y) = x.
+intros;unfold swap;rewrite > eqb_n_n;apply (eqb_elim y x);intro;autobatch;
+qed.
+
+lemma swap_other : \forall x,y,z.(z \neq x) \to (z \neq y) \to (swap x y z) = z.
+intros;unfold swap;apply (eqb_elim z x);intro;simplify
+ [elim H;assumption
+ |rewrite > not_eq_to_eqb_false;autobatch]
+qed.
+
+lemma swap_inv : \forall u,v,x.(swap u v (swap u v x)) = x.
+intros;unfold in match (swap u v x);apply (eqb_elim x u);intro;simplify
+ [autobatch paramodulation
+ |apply (eqb_elim x v);intro;simplify
+ [autobatch paramodulation
+ |apply swap_other;assumption]]
+qed.
+
+lemma swap_inj : ∀u,v,x,y.swap u v x = swap u v y → x = y.
+intros 4;unfold swap;apply (eqb_elim x u);simplify;intro
+ [apply (eqb_elim y u);simplify;intro
+ [intro;autobatch paramodulation
+ |apply (eqb_elim y v);simplify;intros
+ [autobatch paramodulation
+ |elim H2;symmetry;assumption]]
+ |apply (eqb_elim y u);simplify;intro
+ [apply (eqb_elim x v);simplify;intros;
+ [autobatch paramodulation
+ |elim H2;assumption]
+ |apply (eqb_elim x v);simplify;intro
+ [apply (eqb_elim y v);simplify;intros
+ [autobatch paramodulation
+ |elim H1;symmetry;assumption]
+ |apply (eqb_elim y v);simplify;intros
+ [elim H;assumption
+ |assumption]]]]
+qed.
+
+definition swap_list : nat \to nat \to (list nat) \to (list nat) ≝
+ \lambda u,v,l.(map ? ? (swap u v) l).
+
+let rec posn l x on l ≝
+ match l with
+ [ nil ⇒ O
+ | (cons (y:nat) l2) ⇒
+ match (eqb x y) with
+ [ true ⇒ O
+ | false ⇒ S (posn l2 x)]].
+
+let rec lookup n l on l ≝
+ match l with
+ [ nil ⇒ false
+ | cons (x:nat) l1 ⇒ match (eqb n x) with
+ [true ⇒ true
+ |false ⇒ (lookup n l1)]].
+
+let rec head (A:Type) l on l ≝
+ match l with
+ [ nil ⇒ None A
+ | (cons (x:A) l2) ⇒ Some A x].
+
+definition max_list : (list nat) \to nat \def
+ \lambda l.let rec aux l0 m on l0 \def
+ match l0 with
+ [ nil ⇒ m
+ | (cons n l2) ⇒ (aux l2 (max m n))]
+ in aux l O.
+
+let rec remove_nat (x:nat) (l:list nat) on l \def
+ match l with
+ [ nil ⇒ (nil nat)
+ | (cons y l2) ⇒ match (eqb x y) with
+ [ true ⇒ (remove_nat x l2)
+ | false ⇒ (y :: (remove_nat x l2)) ]].
+
+lemma in_lookup : \forall x,l.x ∈ l \to (lookup x l = true).
+intros;elim H;simplify
+ [rewrite > eqb_n_n;reflexivity
+ |rewrite > H2;elim (eqb a a1);reflexivity]
+qed.
+
+lemma lookup_in : \forall x,l.(lookup x l = true) \to x ∈ l.
+intros 2;elim l
+ [simplify in H;destruct H
+ |generalize in match H1;simplify;elim (decidable_eq_nat x a)
+ [applyS in_list_head
+ |apply in_list_cons;apply H;
+ rewrite > (not_eq_to_eqb_false ? ? H2) in H3;simplify in H3;assumption]]
+qed.
+
+lemma posn_length : \forall x,vars.x ∈ vars →
+ (posn vars x) < (length ? vars).
+intros 2;elim vars
+ [elim (not_in_list_nil ? ? H)
+ |inversion H1;intros;destruct;simplify
+ [rewrite > eqb_n_n;simplify;
+ apply lt_O_S
+ |elim (eqb x a);simplify
+ [apply lt_O_S
+ |apply le_S_S;apply H;assumption]]]
+qed.
+
+lemma in_remove : \forall a,b,l.(a ≠ b) \to a ∈ l \to
+ a ∈ (remove_nat b l).
+intros 4;elim l
+ [elim (not_in_list_nil ? ? H1)
+ |inversion H2;intros;destruct;simplify
+ [rewrite > not_eq_to_eqb_false
+ [simplify;apply in_list_head
+ |intro;apply H;symmetry;assumption]
+ |elim (eqb b a1);simplify
+ [apply H1;assumption
+ |apply in_list_cons;apply H1;assumption]]]
+qed.
+
+lemma swap_same : \forall x,y.swap x x y = y.
+intros;elim (decidable_eq_nat y x)
+ [autobatch paramodulation
+ |rewrite > swap_other;autobatch]
+qed.
+
+lemma not_nat_in_to_lookup_false : ∀l,X. X ∉ l → lookup X l = false.
+intros 2;elim l;simplify
+ [reflexivity
+ |elim (decidable_eq_nat X a)
+ [elim H1;rewrite > H2;apply in_list_head
+ |rewrite > (not_eq_to_eqb_false ? ? H2);simplify;apply H;intro;apply H1;
+ apply (in_list_cons ? ? ? ? H3);]]
+qed.
+
+lemma lookup_swap : ∀a,b,x,vars.
+ lookup (swap a b x) (swap_list a b vars) =
+ lookup x vars.
+intros 4;elim vars;simplify
+ [reflexivity
+ |elim (decidable_eq_nat x a1)
+ [rewrite > H1;rewrite > eqb_n_n;rewrite > eqb_n_n;simplify;reflexivity
+ |rewrite > (not_eq_to_eqb_false ? ? H1);elim (decidable_eq_nat x a)
+ [rewrite > H;rewrite > H2;rewrite > swap_left;
+ elim (decidable_eq_nat b a1)
+ [rewrite < H3;rewrite > swap_right;
+ rewrite > (not_eq_to_eqb_false b a)
+ [reflexivity
+ |intro;autobatch]
+ |rewrite > (swap_other a b a1)
+ [rewrite > (not_eq_to_eqb_false ? ? H3);simplify;reflexivity
+ |*:intro;autobatch]]
+ |elim (decidable_eq_nat x b)
+ [rewrite > H;rewrite > H3;rewrite > swap_right;
+ elim (decidable_eq_nat a1 a)
+ [rewrite > H4;rewrite > swap_left;
+ rewrite > (not_eq_to_eqb_false a b)
+ [reflexivity
+ |intro;autobatch]
+ |rewrite > (swap_other a b a1)
+ [rewrite > (not_eq_to_eqb_false a a1)
+ [reflexivity
+ |intro;autobatch]
+ |assumption
+ |intro;autobatch]]
+ |rewrite > H;rewrite > (swap_other a b x)
+ [elim (decidable_eq_nat a a1)
+ [rewrite > H4;rewrite > swap_left;
+ rewrite > (not_eq_to_eqb_false ? ? H3);reflexivity
+ |elim (decidable_eq_nat b a1)
+ [rewrite > H5;rewrite > swap_right;
+ rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity
+ |rewrite > (swap_other a b a1)
+ [rewrite > (not_eq_to_eqb_false ? ? H1);reflexivity
+ |*:intro;autobatch]]]
+ |*:assumption]]]]]
+qed.
+
+lemma posn_swap : ∀a,b,x,vars.
+ posn vars x = posn (swap_list a b vars) (swap a b x).
+intros 4;elim vars;simplify
+ [reflexivity
+ |rewrite < H;elim (decidable_eq_nat x a1)
+ [rewrite > H1;do 2 rewrite > eqb_n_n;reflexivity
+ |elim (decidable_eq_nat (swap a b x) (swap a b a1))
+ [elim H1;autobatch
+ |rewrite > (not_eq_to_eqb_false ? ? H1);
+ rewrite > (not_eq_to_eqb_false ? ? H2);reflexivity]]]
+qed.
+
+lemma remove_inlist : \forall x,y,l.x ∈ (remove_nat y l) → x ∈ l \land x ≠ y.
+intros 3;elim l 0;simplify;intro
+ [elim (not_in_list_nil ? ? H)
+ |elim (decidable_eq_nat y a)
+ [rewrite > H in H2;rewrite > eqb_n_n in H2;simplify in H2;
+ rewrite > H in H1;elim (H1 H2);rewrite > H;split
+ [apply in_list_cons;assumption
+ |assumption]
+ |rewrite > (not_eq_to_eqb_false ? ? H) in H2;simplify in H2;
+ inversion H2;intros;destruct;
+ [split;autobatch
+ |elim (H1 H3);split;autobatch]]]
+qed.
+
+lemma inlist_remove : ∀x,y,l.x ∈ l → x ≠ y → x ∈ (remove_nat y l).
+intros 3;elim l
+ [elim (not_in_list_nil ? ? H);
+ |simplify;elim (decidable_eq_nat y a)
+ [rewrite > (eq_to_eqb_true ? ? H3);simplify;apply H
+ [inversion H1;intros;destruct;
+ [elim H2;reflexivity
+ |assumption]
+ |assumption]
+ |rewrite > (not_eq_to_eqb_false ? ? H3);simplify;
+ inversion H1;intros;destruct;autobatch]]
+qed.
+
+lemma swap_case: ∀u,v,x.(swap u v x) = u ∨ (swap u v x) = v ∨ (swap u v x = x).
+intros;unfold in match swap;simplify;elim (eqb x u);simplify
+ [autobatch
+ |elim (eqb x v);simplify;autobatch]
+qed.
+
+definition distinct_list ≝
+λl.∀n,m.n < length ? l → m < length ? l → n ≠ m → nth ? l O n ≠ nth ? l O m.
+
+lemma posn_nth: ∀l,n.distinct_list l → n < length ? l →
+ posn l (nth ? l O n) = n.
+intro;elim l
+ [simplify in H1;elim (not_le_Sn_O ? H1)
+ |simplify in H2;generalize in match H2;elim n
+ [simplify;rewrite > eqb_n_n;simplify;reflexivity
+ |simplify;cut (nth ? (a::l1) O (S n1) ≠ nth ? (a::l1) O O)
+ [simplify in Hcut;rewrite > (not_eq_to_eqb_false ? ? Hcut);simplify;
+ rewrite > (H n1)
+ [reflexivity
+ |unfold;intros;unfold in H1;lapply (H1 (S n2) (S m));
+ [simplify in Hletin;assumption
+ |2,3:simplify;autobatch
+ |intro;apply H7;destruct H8;reflexivity]
+ |autobatch]
+ |intro;apply H1;
+ [6:apply H5
+ |skip
+ |skip
+ |(*** *:autobatch; *)
+ apply H4
+ |simplify;autobatch
+ |intro;elim (not_eq_O_S n1);symmetry;assumption]]]]
+qed.
+
+lemma nth_in_list : ∀l,n. n < length ? l → (nth ? l O n) ∈ l.
+intro;elim l
+ [simplify in H;elim (not_le_Sn_O ? H)
+ |generalize in match H1;elim n;simplify
+ [apply in_list_head
+ |apply in_list_cons;apply H;simplify in H3;apply (le_S_S_to_le ? ? H3)]]
+qed.
+
+lemma lookup_nth : \forall l,n.n < length ? l \to
+ lookup (nth nat l O n) l = true.
+intro;elim l
+ [elim (not_le_Sn_O ? H);
+ |generalize in match H1;elim n;simplify
+ [rewrite > eqb_n_n;reflexivity
+ |elim (eqb (nth nat l1 O n1) a);simplify;
+ [reflexivity
+ |apply H;apply le_S_S_to_le;assumption]]]
+qed.
\ No newline at end of file
projects / helm.git / commitdiff