[Poplmark] Pure Fsub
Jerome Vouillon
Jerome.Vouillon at pps.jussieu.fr
Sat Mar 19 21:20:58 EST 2005
For a start, here are some proofs of transitivity of subtyping
and type safety for pure Fsub.
They are written in Coq using de Bruijn indices. I used the
v7 syntax as I have not yet learned the new syntax. They can
be compiled with the latest version of Coq by "coqc -v7 Fsub.v"
and translated to the new syntax using "coqc -translate Fsub.v".
-- Jerome
-------------- next part --------------
Implicit Arguments On.
Require Arith.
Require Omega.
(****)
Inductive typ : Set :=
tvar : nat -> typ
| top : typ
| arrow : typ -> typ -> typ
| all : typ -> typ -> typ.
Inductive term : Set :=
var : nat -> term
| abs : typ -> term -> term
| app : term -> term -> term
| tabs : typ -> term -> term
| tapp : term -> typ -> term.
(****)
Fixpoint tshift [n0 : nat; n : nat; t : typ] : typ :=
Cases t of
(tvar x) => (tvar if (le_gt_dec n0 x) then [_](plus n x) else [_]x)
| top => top
| (arrow t1 t2) => (arrow (tshift n0 n t1) (tshift n0 n t2))
| (all t1 t2) => (all (tshift n0 n t1) (tshift (S n0) n t2))
end.
Fixpoint shift [n0 : nat; n : nat; t : term] : term :=
Cases t of
(var x) => (var if (le_gt_dec n0 x) then [_](plus n x) else [_]x)
| (abs t1 t2) => (abs (tshift n0 n t1) (shift (S n0) n t2))
| (app t1 t2) => (app (shift n0 n t1) (shift n0 n t2))
| (tabs t1 t2) => (tabs (tshift n0 n t1) (shift (S n0) n t2))
| (tapp t1 t2) => (tapp (shift n0 n t1) (tshift n0 n t2))
end.
(****)
(*
We use the same set of indices for type and term variables and do
not use any well-formedness condition in this part of the proofs.
Hence, these substitutions do strange things when the same index is
used both as a term variable and as a type variable. This still
allows us to prove the preservation and progress theorems.
Later, we use a well-formedness condition ("well_formed" predicate)
to prevent this issue.
*)
(*
Parameter dummy_type : typ.
Parameter dummy_term : term.
*)
Definition dummy_type := top.
Definition dummy_term := (var O).
Fixpoint tsubst [t : typ] : nat -> typ -> typ :=
[x; t']
Cases t of
(tvar x') =>
Cases (lt_eq_lt_dec x' x) of
(inleft (left _)) => (tvar x')
| (inleft (right _)) => (tshift (0) x t')
| (inright _) => (tvar (pred x'))
end
| top => top
| (arrow t1 t2) => (arrow (tsubst t1 x t') (tsubst t2 x t'))
| (all t1 t2) => (all (tsubst t1 x t') (tsubst t2 (S x) t'))
end.
Fixpoint subst [e : term] : nat -> term -> term :=
[x; e']
Cases e of
(var x') =>
Cases (lt_eq_lt_dec x' x) of
(inleft (left _)) => (var x')
| (inleft (right _)) => (shift (0) x e')
| (inright _) => (var (pred x'))
end
| (abs t1 e1) => (abs (tsubst t1 x dummy_type) (subst e1 (S x) e'))
| (app e1 e2) => (app (subst e1 x e') (subst e2 x e'))
| (tabs t1 e1) => (tabs (tsubst t1 x dummy_type) (subst e1 (S x) e'))
| (tapp e1 t2) => (tapp (subst e1 x e') (tsubst t2 x dummy_type))
end.
Fixpoint subst_typ [e : term] : nat -> typ -> term :=
[x; t]
Cases e of
(var x') =>
Cases (lt_eq_lt_dec x' x) of
(inleft (left _)) => (var x')
| (inleft (right _)) => dummy_term
| (inright _) => (var (pred x'))
end
| (abs t1 e1) => (abs (tsubst t1 x t) (subst_typ e1 (S x) t))
| (app e1 e2) => (app (subst_typ e1 x t) (subst_typ e2 x t))
| (tabs t1 e1) => (tabs (tsubst t1 x t) (subst_typ e1 (S x) t))
| (tapp e1 t2) => (tapp (subst_typ e1 x t) (tsubst t2 x t))
end.
(****)
Lemma tshift_0_prop : (n : nat) (t : typ) (tshift n O t) = t.
Intros n t; Generalize n; Clear n; NewInduction t;
[ Intro n'; Simpl; Case (le_gt_dec n' n); Trivial
| Trivial
| Intro n; Simpl; Rewrite IHt1; Rewrite IHt2; Trivial
| Intro n; Simpl; Rewrite IHt1; Rewrite IHt2; Trivial ].
Qed.
Lemma tshift_tshift_prop_1 :
(n1, n2, n3, n4 : nat) (t : typ)
(le n3 n1) -> (le n1 (plus n3 n4)) ->
(tshift n1 n2 (tshift n3 n4 t)) = (tshift n3 (plus n2 n4) t).
Intros n1 n2 n3 n4 t; Generalize n1 n2 n3 n4; Clear n1 n2 n3 n4;
NewInduction t;
[ Intros n1 n2 n3 n4 H1 H2; Simpl; Case (le_gt_dec n3 n); Intro H3;
[ Case (le_gt_dec n1 (plus n4 n)); Intro H4;
[ Rewrite plus_assoc_r; Trivial
| Assert False; [ Omega | Contradiction ] ]
| Case (le_gt_dec n1 n); Intro H4;
[ Assert False; [ Omega | Contradiction ]
| Trivial ] ]
| Trivial
| Intros n1 n2 n3 n4 H1 H2; Simpl;
Rewrite IHt1; Trivial; Rewrite IHt2; Trivial
| Intros n1 n2 n3 n4 H1 H2; Simpl;
Rewrite IHt1; Trivial; Rewrite IHt2; Try Omega; Trivial ].
Qed.
Lemma tshift_tshift_prop_2 :
(t : typ) (n1, n2, n3, n4 : nat)
(le n1 n3) ->
(tshift n1 n2 (tshift n3 n4 t)) = (tshift (plus n3 n2) n4 (tshift n1 n2 t)).
NewInduction t;
[ Intros n1 n2 n3 n4 H1; Simpl; Case (le_gt_dec n1 n); Intro H2;
[ Case (le_gt_dec n3 n); Intro H3;
[ Case (le_gt_dec n1 (plus n4 n)); Intro H4;
[ Case (le_gt_dec (plus n3 n2) (plus n2 n)); Intro H5;
[ Rewrite plus_permute; Trivial
| Assert False; [ Omega | Contradiction ] ]
| Assert False; [ Omega | Contradiction ] ]
| Case (le_gt_dec n1 n); Intro H4;
[ Case (le_gt_dec (plus n3 n2) (plus n2 n)); Intro H5;
[ Assert False; [ Omega | Contradiction ]
| Trivial ]
| Assert False; [ Omega | Contradiction ] ] ]
| Case (le_gt_dec n3 n); Intro H3;
[ Assert False; [ Omega | Contradiction ]
| Case (le_gt_dec n1 n); Intro H4;
[ Assert False; [ Omega | Contradiction ]
| Case (le_gt_dec (plus n3 n2) n); Intro H5;
[ Assert False; [ Omega | Contradiction ]
| Trivial ] ] ] ]
| Trivial
| Intros n1 n2 n3 n4 H1; Simpl; Rewrite IHt1; Trivial; Rewrite IHt2; Trivial
| Intros n1 n2 n3 n4 H1; Simpl; Rewrite IHt1; Trivial;
Rewrite IHt2; Try Omega; Trivial ].
Qed.
Lemma tshift_tshift_prop :
(n, n', n'' : nat) (t : typ)
(tshift n n' (tshift n n'' t)) = (tshift n (plus n' n'') t).
Intros n n' n'' t; Rewrite tshift_tshift_prop_1; Try Omega; Trivial.
Qed.
Lemma tsubst_tshift_prop_1 :
(t, t' : typ) (n, n', n'' : nat)
(le n n'') -> (le n'' (plus n n')) ->
(tsubst (tshift n (S n') t) n'' t') = (tshift n n' t).
NewInduction t;
[ Intros t n1 n2 n3 H1 H2; Simpl; Case (le_gt_dec n1 n); Intro H3;
[ Case (lt_eq_lt_dec (S (plus n2 n)) n3);
[ Intros s; Case s; Clear s; Intro H4;
[ Assert False; [ Omega | Contradiction ]
| Assert False; [ Omega | Contradiction ] ]
| Trivial ]
| Case (lt_eq_lt_dec n n3);
[ Intros s; Case s; Clear s; Intro H4;
[ Trivial
| Assert False; [ Omega | Contradiction ] ]
| Intro H4; Assert False; [ Omega | Contradiction ] ] ]
| Trivial
| Intros n1 n2 n3 n4 H1 H2; Simpl;
Rewrite IHt1; Trivial; Rewrite IHt2; Trivial
| Intros n1 n2 n3 n4 H1 H2; Simpl;
Rewrite IHt1; Trivial; Rewrite IHt2; Try Omega; Trivial ].
Qed.
Lemma tsubst_tshift_prop :
(n, n' : nat) (t, t' : typ)
(tsubst (tshift n (S n') t) n t') = (tshift n n' t).
Intros n n' t t'; Rewrite tsubst_tshift_prop_1; Try Omega; Trivial.
Qed.
Lemma tshift_tsubst_prop_1 :
(n, n', n'' : nat) (t0, t : typ)
(tshift n n' (tsubst t0 (plus n n'') t)) =
(tsubst (tshift n n' t0) (plus n' (plus n n'')) t).
Intros n n' n'' t; Generalize n n' n''; Clear n n' n''; NewInduction t;
[ Simpl; Intros n1 n2 n3 t; Case (le_gt_dec n1 n); Intro H1;
[ Case (lt_eq_lt_dec n (plus n1 n3));
[ Intros s; Case s; Clear s; Intro H2;
[ Case (lt_eq_lt_dec (plus n2 n) (plus n2 (plus n1 n3)));
[ Intros s; Case s; Clear s; Intro H3;
[ Simpl; Case (le_gt_dec n1 n); Intro H4;
[ Trivial
| Assert False; [ Omega | Contradiction ] ]
| Assert False; [ Omega | Contradiction ] ]
| Intro H3; Assert False; [ Omega | Contradiction ] ]
| Case (lt_eq_lt_dec (plus n2 n) (plus n2 (plus n1 n3)));
[ Intros s; Case s; Clear s; Intro H3;
[ Assert False; [ Omega | Contradiction ]
| Rewrite tshift_tshift_prop_1; Try Omega; Trivial ]
| Intro H3; Assert False; [ Omega | Contradiction ] ] ]
| Intro H2; Case (lt_eq_lt_dec (plus n2 n) (plus n2 (plus n1 n3)));
[ Intros s; Case s; Clear s; Intro H3;
[ Assert False; [ Omega | Contradiction ]
| Assert False; [ Omega | Contradiction ] ]
| Intro H3; Simpl; Case (le_gt_dec n1 (pred n)); Intro H4;
[ Assert H5 : (plus n2 (pred n)) = (pred (plus n2 n));
[ Omega
| Rewrite H5; Trivial ]
| Assert False; [ Omega | Contradiction ] ] ] ]
| Case (lt_eq_lt_dec n (plus n1 n3));
[ Intros s; Case s; Clear s; Intro H2;
[ Case (lt_eq_lt_dec n (plus n2 (plus n1 n3)));
[ Intros s; Case s; Clear s; Intro H3;
[ Simpl; Case (le_gt_dec n1 n); Intro H4;
[ Assert False; [ Omega | Contradiction ]
| Trivial ]
| Assert False; [ Omega | Contradiction ] ]
| Intro H3; Assert False; [ Omega | Contradiction ] ]
| Assert False; [ Omega | Contradiction ] ]
| Intro H2; Assert False; [ Omega | Contradiction ] ] ]
| Trivial
| Intros n n' n'' u; Simpl; Rewrite IHt1; Rewrite IHt2; Trivial
| Intros n n' n'' u; Simpl;
Rewrite IHt1; Rewrite (IHt2 (S n) n' n'');
Simpl; Rewrite <- plus_Snm_nSm; Trivial ].
Qed.
Lemma tshift_tsubst_prop_2 :
(n, n', n'' : nat) (t, u : typ)
(tshift (plus n'' n) n' (tsubst t n'' u)) =
(tsubst (tshift (S (plus n'' n)) n' t) n'' (tshift n n' u)).
Intros n n' n'' t; Generalize n n' n''; Clear n n' n''; NewInduction t;
[ Unfold tshift; Fold tshift;
Intros n1 n2 n3 u; Case (le_gt_dec (S (plus n3 n1)) n); Intro H2; Simpl;
[ Case (lt_eq_lt_dec n n3);
[ Intros s; Case s; Clear s; Intro H3;
[ Assert False; [ Omega | Contradiction ]
| Assert False; [ Omega | Contradiction ] ]
| Intro H3; Case (lt_eq_lt_dec (plus n2 n) n3);
[ Intros s; Case s; Clear s; Intro H4;
[ Assert False; [ Omega | Contradiction ]
| Assert False; [ Omega | Contradiction ] ]
| Intro H4; Simpl;
Case (le_gt_dec (plus n3 n1) (pred n)); Intro H5;
[ Assert H6 : (plus n2 (pred n)) = (pred (plus n2 n));
Try Omega;
Rewrite H6; Trivial
| Assert False; [ Omega | Contradiction ] ] ] ]
| Case (lt_eq_lt_dec n n3);
[ Intros s; Case s; Clear s; Intro H3;
[ Simpl; Case (le_gt_dec (plus n3 n1) n); Intro H4;
[ Assert False; [ Omega | Contradiction ]
| Trivial ]
| Rewrite (!tshift_tshift_prop_2 u (0) n3 n1 n2); Try Omega;
Rewrite plus_sym; Trivial ]
| Intro H3; Simpl; Case (le_gt_dec (plus n3 n1) (pred n)); Intro H4;
[ Assert False; [ Omega | Contradiction ]
| Trivial ] ] ]
| Trivial
| Intros n n' n'' u; Simpl; Rewrite IHt1; Rewrite IHt2; Trivial
| Intros n n' n'' u; Simpl;
Rewrite IHt1; Rewrite (IHt2 n n' (S n'')); Trivial ].
Qed.
Lemma tshift_injective :
(t, t' : typ) (n, n' : nat) (tshift n n' t) = (tshift n n' t') -> t = t'.
NewInduction t;
[ Intro t'; Case t'; Try (Intros; Discriminate);
Simpl; Intros n1 n2 n3 E; Assert H : n = n1;
[ Generalize E; Clear E;
Case (le_gt_dec n2 n);
[ Case (le_gt_dec n2 n1);
[ Intros H1 H2 E; Injection E; Intros E'; Omega
| Intros H1 H2 E; Injection E; Intros E'; Omega ]
| Case (le_gt_dec n2 n1);
[ Intros H1 H2 E; Injection E; Intros E'; Omega
| Intros H1 H2 E; Injection E; Intros E'; Omega ] ]
| Rewrite H; Trivial ]
| Intro t'; Case t'; Try (Intros; Discriminate); Trivial
| Intro t'; Case t'; Try (Intros; Discriminate);
Simpl; Intros t3 t4 n n' E; Injection E; Intros E1 E2;
Rewrite (IHt1 ? ? ? E2); Rewrite (IHt2 ? ? ? E1); Trivial
| Intro t'; Case t'; Try (Intros; Discriminate);
Simpl; Intros t3 t4 n n' E; Injection E; Intros E1 E2;
Rewrite (IHt1 ? ? ? E2); Rewrite (IHt2 ? ? ? E1); Trivial ].
Qed.
Lemma tsubst_tsubst_prop :
(n, n' : nat) (t, u, v : typ)
(tsubst (tsubst t n u) (plus n n') v) =
(tsubst (tsubst t (S (plus n n')) v) n (tsubst u n' v)).
Intros n n' t; Generalize n n'; Clear n n'; NewInduction t;
[ Simpl; Intros n1 n2 u v; Case (lt_eq_lt_dec n (S (plus n1 n2)));
[ Intros s; Case s; Clear s; Intro H1;
[ Simpl; Case (lt_eq_lt_dec n n1);
[ Intros s; Case s; Clear s; Intro H2;
[ Simpl; Case (lt_eq_lt_dec n (plus n1 n2));
[ Intros s; Case s; Clear s; Intro H3;
[ Trivial
| Assert False; [ Omega | Contradiction ] ]
| Intro H3; Assert False; [ Omega | Contradiction ] ]
| Generalize (!tshift_tsubst_prop_1 (0) n1 n2 u v);
Simpl; Intro E; Rewrite E; Trivial ]
| Intro H2; Simpl; Case (lt_eq_lt_dec (pred n) (plus n1 n2));
[ Intros s; Case s; Clear s; Intro H3;
[ Trivial
| Assert False; [ Omega | Contradiction ] ]
| Intro H3; Assert False; [ Omega | Contradiction ] ] ]
| Case (lt_eq_lt_dec n n1);
[ Intros s; Case s; Clear s; Intro H2;
[ Assert False; [ Omega | Contradiction ]
| Assert False; [ Omega | Contradiction ] ]
| Intro H2; Simpl; Case (lt_eq_lt_dec (pred n) (plus n1 n2));
[ Intros s; Case s; Clear s; Intro H3;
[ Assert False; [ Omega | Contradiction ]
| Rewrite tsubst_tshift_prop_1; Try Omega; Trivial ]
| Intro H3; Assert False; [ Omega | Contradiction ] ] ] ]
| Intro H1; Simpl; Case (lt_eq_lt_dec (pred n) n1);
[ Intros s; Case s; Clear s; Intro H2;
[ Assert False; [ Omega | Contradiction ]
| Assert False; [ Omega | Contradiction ] ]
| Intro H2; Case (lt_eq_lt_dec n n1);
[ Intros s; Case s; Clear s; Intro H3;
[ Assert False; [ Omega | Contradiction ]
| Assert False; [ Omega | Contradiction ] ]
| Intro H3; Simpl; Case (lt_eq_lt_dec (pred n) (plus n1 n2));
[ Intros s; Case s; Clear s; Intro H4;
[ Assert False; [ Omega | Contradiction ]
| Assert False; [ Omega | Contradiction ] ]
| Trivial ] ] ] ]
| Trivial
| Simpl; Intros n1 n2 u v; Rewrite IHt1; Rewrite IHt2; Trivial
| Simpl; Intros n1 n2 u v; Rewrite IHt1; Rewrite (IHt2 (S n1) n2); Trivial ].
Qed.
(****)
Lemma shift_0_prop : (n : nat) (t : term) (shift n O t) = t.
Intros n t; Generalize n; Clear n; NewInduction t;
[ Intros n'; Simpl; Case (le_gt_dec n' n); Trivial
| Intros n; Simpl; Rewrite IHt; Rewrite tshift_0_prop; Trivial
| Intros n; Simpl; Rewrite IHt1; Rewrite IHt2; Trivial
| Intros n; Simpl; Rewrite IHt; Rewrite tshift_0_prop; Trivial
| Intros n; Simpl; Rewrite IHt; Rewrite tshift_0_prop; Trivial ].
Qed.
Lemma shift_shift_prop :
(n, n', n'' : nat) (t : term)
(shift n n' (shift n n'' t)) = (shift n (plus n' n'') t).
Intros n n' n'' t; Generalize n n' n''; Clear n n' n''; NewInduction t;
[ Simpl; Intros n1 n2 n3; Case (le_gt_dec n1 n); Intro H1;
[ Case (le_gt_dec n1 (plus n3 n)); Intro H2;
[ Rewrite plus_assoc_r; Trivial
| Assert False; [ Omega | Contradiction ] ]
| Case (le_gt_dec n1 n); Intro H2;
[ Assert False; [ Omega | Contradiction ]
| Trivial ] ]
| Intros n1 n2 n3; Simpl; Rewrite IHt; Rewrite tshift_tshift_prop; Trivial
| Intros n1 n2 n3; Simpl; Rewrite IHt1; Rewrite IHt2; Trivial
| Intros n1 n2 n3; Simpl; Rewrite IHt; Rewrite tshift_tshift_prop; Trivial
| Intros n1 n2 n3; Simpl; Rewrite IHt; Rewrite tshift_tshift_prop; Trivial ].
Qed.
(****)
Inductive binding : Set :=
evar : typ -> binding
| ebound : typ -> binding.
Definition bshift [n0, n : nat; b : binding] :=
Cases b of
(evar t) => (evar (tshift n0 n t))
| (ebound t) => (ebound (tshift n0 n t))
end.
Definition bsubst [b : binding; n : nat; t : typ] :=
Cases b of
(evar t') => (evar (tsubst t' n t))
| (ebound t') => (ebound (tsubst t' n t))
end.
Inductive env : Set :=
empty : env
| econs : binding -> env -> env.
Definition opt_map [A, B : Set; f : A -> B; x : (option A)] :=
Cases x of
(Some x) => (Some ? (f x))
| None => (None ?)
end.
Definition opt_bind [A, B : Set; f : A -> (option B); x : (option A)] :=
Cases x of
(Some x) => (f x)
| None => (None ?)
end.
Fixpoint esubst [e : env] : nat -> typ -> env :=
[n; t]
Cases n e of
O (econs _ e) => e
| (S n) (econs b e) => (econs (bsubst b n t) (esubst e n t))
| _ empty => empty
end.
Fixpoint get [e : env; n : nat] : (option binding) :=
Cases n e of
O (econs b e) => (Some ? b)
| (S n) (econs _ e) => (get e n)
| _ empty => (None ?)
end.
Definition get_var [e : env; n : nat] :=
(opt_bind
[b]
Cases b of
(evar t) => (Some ? (tshift (0) (S n) t))
| _ => (None ?)
end
(get e n)).
Definition get_bound [e : env; n : nat] :=
(opt_bind
[b]
Cases b of
(ebound t) => (Some ? (tshift (0) (S n) t))
| _ => (None ?)
end
(get e n)).
Definition add_var [e : env; t : typ] := (econs (evar t) e).
Definition add_bound [e : env; t : typ] := (econs (ebound t) e).
Lemma get_var_extend :
(e : env) (b : binding) (n : nat)
(get_var (econs b e) (S n)) =
(opt_map [t](tshift (0) (1) t) (get_var e n)).
Intros e b n; Unfold get_var; Simpl; Case (get e n); Simpl;
[ Intro b'; Case b'; Simpl;
[ Intro t; Rewrite tshift_tshift_prop; Trivial
| Trivial ]
| Trivial ].
Qed.
Lemma get_bound_extend :
(e : env) (b : binding) (n : nat)
(get_bound (econs b e) (S n)) =
(opt_map [t](tshift (0) (1) t) (get_bound e n)).
Intros e b n; Unfold get_bound; Simpl; Case (get e n); Simpl;
[ Intro b'; Case b'; Simpl;
[ Trivial
| Intro t; Rewrite tshift_tshift_prop; Trivial ]
| Trivial ].
Qed.
Lemma get_var_shape :
(e : env) (n : nat) (t : typ)
(get_var e n) = (Some ? t) -> (EX t' | t = (tshift (0) (S n) t')).
Intros e n t; Unfold get_var; Case (get e n);
[ Intro b; Case b;
[ Simpl; Intros t' E; Injection E; Intro E';
Rewrite <- E'; Exists t'; Trivial
| Intros; Discriminate ]
| Intros; Discriminate ].
Qed.
Lemma get_bound_shape :
(e : env) (n : nat) (t : typ)
(get_bound e n) = (Some ? t) -> (EX t' | t = (tshift (0) (S n) t')).
Intros e n t; Unfold get_bound; Case (get e n);
[ Intro b; Case b;
[ Intros; Discriminate
| Simpl; Intros t' E; Injection E; Intro E';
Rewrite <- E'; Exists t'; Trivial ]
| Intros; Discriminate ].
Qed.
Lemma get_subst_lt :
(n, n' : nat) (e : env) (t : typ)
(lt n n') ->
(get (esubst e n' t) n) =
(opt_map [b](bsubst b (minus n' (S n)) t) (get e n)).
NewInduction n;
[ NewInduction n';
[ Intros e t H; Case (lt_n_O ? H)
| NewInduction e; Trivial;
Intros t H; Simpl; Rewrite <- minus_n_O; Trivial ]
| NewInduction n';
[ Intros e t H; Case (lt_n_O ? H)
| NewInduction e;
[ Trivial
| Simpl; Intros t H; Apply IHn; Apply lt_S_n; Trivial ] ] ].
Qed.
Lemma get_var_subst_lt :
(n, n' : nat) (e : env) (t : typ)
(lt n n') ->
(get_var (esubst e n' t) n) = (opt_map [t'](tsubst t' n' t) (get_var e n)).
Intros n n' e t H; Unfold get_var; Rewrite get_subst_lt with 1 := H;
Case (get e n);
[ Intro b; Case b;
[ Intro t'; Simpl;
Generalize (!tshift_tsubst_prop_1 (0) (S n) (minus n' (S n)) t' t);
Simpl; Intro E; Rewrite E;
Assert H1 : (S (plus n (minus n' (S n)))) = n';
[ Omega
| Rewrite H1; Trivial ]
| Trivial ]
| Trivial ].
Qed.
Lemma get_bound_subst_lt :
(n, n' : nat) (e : env) (t : typ)
(lt n n') ->
(get_bound (esubst e n' t) n) =
(opt_map [t'](tsubst t' n' t) (get_bound e n)).
Intros n n' e t H; Unfold get_bound; Rewrite get_subst_lt with 1 := H;
Case (get e n);
[ Intro b; Case b;
[ Trivial
| Intro t'; Simpl;
Generalize (!tshift_tsubst_prop_1 (0) (S n) (minus n' (S n)) t' t);
Simpl; Intro E; Rewrite E;
Assert H1 : (S (plus n (minus n' (S n)))) = n';
[ Omega
| Rewrite H1; Trivial ] ]
| Trivial ].
Qed.
Lemma get_subst_ge :
(n, n' : nat) (e : env) (t : typ)
(ge n n') ->
(get (esubst e n' t) n) =
(get e (S n)).
NewInduction n;
[ Intro n'; Case n';
[ Intros e t _; Case e; Trivial
| Intros n e t H; Assert False; [ Omega | Contradiction ] ]
| Intros n' e t; Case e;
[ Case n'; Trivial
| Case n';
[ Trivial
| Simpl; Intros n'' _ e' H; Rewrite IHn; Trivial; Omega ] ] ].
Qed.
Lemma get_var_subst_ge :
(n, n' : nat) (e : env) (t : typ)
(ge n n') ->
(get_var (esubst e n' t) n) =
(opt_map [t'](tsubst t' n' t) (get_var e (S n))).
Intros n n' e t H; Unfold get_var; Rewrite get_subst_ge with 1 := H;
Case e; Trivial;
Simpl; Intros _ e'; Case (get e' n); Trivial;
Intro b; Case b; Trivial;
Intro t'; Simpl; Rewrite tsubst_tshift_prop_1; Trivial; Omega.
Qed.
(* XXX KILL *)
Lemma get_bound_subst_ge :
(n, n' : nat) (e : env) (t : typ)
(ge n n') ->
(get_bound e (S n)) =
(opt_map [t'](tshift (0) (1) t') (get_bound (esubst e n' t) n)).
Intros n n' e t H; Unfold get_bound; Rewrite get_subst_ge; Trivial;
Case (get e (S n));
[ Intro b; Case b;
[ Trivial
| Simpl; Intro t'; Rewrite tshift_tshift_prop; Trivial ]
| Trivial ].
Qed.
Lemma get_bound_subst_ge_2 :
(n, n' : nat) (e : env) (t : typ)
(ge n n') ->
(get_bound (esubst e n' t) n) =
(opt_map [t'](tsubst t' n' t) (get_bound e (S n))).
Intros n n' e t H; Unfold get_bound; Rewrite get_subst_ge with 1 := H;
Case e; Trivial;
Simpl; Intros _ e'; Case (get e' n); Trivial;
Intro b; Case b; Trivial;
Intro t'; Simpl; Rewrite tsubst_tshift_prop_1; Trivial; Omega.
Qed.
Lemma get_var_or_bound :
(n : nat) (e : env) (t, t' : typ)
(get_var e n) = (Some ? t) -> ~(get_bound e n) = (Some ? t').
Unfold get_var get_bound; Intros n e t t'; Case (get e n);
[ Intro b; Case b; Intros; Discriminate
| Intros; Discriminate ].
Qed.
Lemma get_var_or_bound_2 :
(n : nat; e : env) ~(get_var e n) = (None ?) -> (get_bound e n) = (None ?).
Unfold get_var get_bound; Intros n e; Case (get e n);
[ Intro b; Case b;
[ Trivial
| Intros t H; Case H; Trivial ]
| Trivial ].
Qed.
(****)
Definition env_free [e : env; n : nat] :=
(n' : nat) (t : typ)
(lt n' n) -> (get_bound e n') = (Some ? t) \/ (get_var e n') = (Some ? t) ->
(EX t' | t = (tshift n (1) t')).
Lemma env_free_0 : (e : env) (env_free e O).
Intros e n' t H; Assert False; [ Omega | Contradiction ].
Qed.
Lemma env_free_extend :
(e : env) (n : nat) (b : binding)
(env_free e n) -> (env_free (econs (bshift n (1) b) e) (S n)).
Intros e n b H1 n'; NewInduction n';
[ Intros t H2 [E | E];
[ NewInduction b; Try Discriminate;
Injection E; Rewrite tshift_tshift_prop_2; Try Omega;
Rewrite plus_sym; Simpl; Intro E2; Rewrite <- E2;
Exists (tshift (0) (1) t0); Trivial
| NewInduction b; Try Discriminate;
Injection E; Rewrite tshift_tshift_prop_2; Try Omega;
Rewrite plus_sym; Simpl; Intro E2; Rewrite <- E2;
Exists (tshift (0) (1) t0); Trivial ]
| Intros t H2 H3;
Rewrite get_bound_extend in H3; Rewrite get_var_extend in H3;
Case H3; Clear H3; Intro E1;
[ Cut (EX t' : typ | (get_bound e n') = (Some ? t'));
[ Intros (t', E2); Case (H1 n' t');
[ Omega
| Auto
| Intros t'' E3; Rewrite E3 in E2; Rewrite E2 in E1;
Injection E1; Intro E4;
Rewrite tshift_tshift_prop_2 in E4; Try Omega;
Rewrite plus_sym in E4; Rewrite <- E4;
Exists (tshift (0) (1) t''); Trivial ]
| NewInduction (get_bound e n'); Try Discriminate;
Exists a; Trivial ]
| Cut (EX w' : typ | (get_var e n') = (Some ? w'));
[ Intros (w', E2); Case (H1 n' w');
[ Omega
| Auto
| Intros w'' E3; Rewrite E3 in E2; Rewrite E2 in E1;
Injection E1; Intro E4;
Rewrite tshift_tshift_prop_2 in E4; Try Omega;
Rewrite plus_sym in E4; Rewrite <- E4;
Exists (tshift (0) (1) w''); Trivial ]
| NewInduction (get_var e n'); Try Discriminate;
Exists a; Trivial ] ] ].
Qed.
(****)
Inductive sub : env -> typ -> typ -> Prop :=
SA_Top :
(e : env) (s : typ) (sub e s top)
| SA_Refl_TVar :
(e : env) (x : nat) (sub e (tvar x) (tvar x))
| SA_Trans_TVar :
(e : env) (x : nat) (t, u : typ)
(get_bound e x) = (Some ? u) -> (sub e u t) -> (sub e (tvar x) t)
| SA_Arrow :
(e : env) (t1, t2, s1, s2 : typ)
(sub e t1 s1) -> (sub e s2 t2) -> (sub e (arrow s1 s2) (arrow t1 t2))
| SA_All :
(e : env) (t1, t2, s1, s2 : typ)
(sub e t1 s1) -> (sub (add_bound e t1) s2 t2) ->
(sub e (all s1 s2) (all t1 t2)).
(****)
Lemma sub_reflexivity : (e : env) (t : typ) (sub e t t).
Intros e t; Generalize e; Clear e; NewInduction t; Intro e;
[ Apply SA_Refl_TVar
| Apply SA_Top
| Apply SA_Arrow; Trivial
| Apply SA_All; Trivial ].
Qed.
Lemma sub_weakening_ind :
(e : env) (n : nat) (t, u, v : typ)
(sub (esubst e n t) u v) -> (env_free e n) ->
(sub e (tshift n (1) u) (tshift n (1) v)).
Intros e n t u v H; Cut (EX e' | e' = (esubst e n t));
[ Intros (e', E); Rewrite <- E in H;
Generalize e n E; Clear e n E; NewInduction H;
[ Intros e' n E H; Apply SA_Top
| Intros e' n E H; Apply sub_reflexivity
| Intros e' n E H5; Simpl; Case (le_gt_dec n x); Intro H1;
[ Apply SA_Trans_TVar with 2 := (IHsub ? ? E H5);
Rewrite (get_bound_subst_ge e' t H1);
Rewrite <- E; Rewrite H; Simpl;
Generalize (get_bound_shape H); Intros (v, E1);
Rewrite E1; Rewrite tshift_tshift_prop_1; Try Omega;
Rewrite tshift_tshift_prop_1; Try Omega; Trivial
| Apply SA_Trans_TVar with 2 := (IHsub ? ? E H5);
Rewrite E in H; Rewrite (get_bound_subst_lt e' t H1) in H;
Cut (EX t' | (get_bound e' x) = (Some ? t'));
[ Intros (t', E1);
Generalize (H5 ? ? H1 (or_introl ? ? E1)); Intros (v, E2);
Rewrite E2 in E1; Clear E2;
Rewrite E1 in H; Simpl in H;
Rewrite tsubst_tshift_prop in H;
Injection H; Intro E2; Rewrite <- E2;
Rewrite tshift_0_prop; Trivial
| NewInduction (get_bound e' x); Try Discriminate;
Exists a; Trivial ] ]
| Intros e' n E H2; Simpl; Apply SA_Arrow; Auto
| Intros e' n E H2; Simpl; Apply SA_All; Auto;
Apply IHsub2;
[ Rewrite E; Simpl; Rewrite tsubst_tshift_prop;
Rewrite tshift_0_prop; Trivial
| Exact (env_free_extend 3!(ebound t1) H2) ] ]
| Exists (esubst e n t); Trivial ].
Qed.
Lemma sub_weakening :
(e : env) (b : binding) (t, u : typ)
(sub e t u) -> (sub (econs b e) (tshift (0) (1) t) (tshift (0) (1) u)).
Intros e b t u H; Apply sub_weakening_ind with t := top; Trivial;
Apply env_free_0.
Qed.
Fixpoint size [t : typ] : nat :=
Cases t of
(tvar _) => (0)
| top => (0)
| (arrow t1 t2) => (S (plus (size t1) (size t2)))
| (all t1 t2) => (S (plus (size t1) (size t2)))
end.
Lemma shift_preserves_size :
(t : typ) (n0, n : nat) (size (tshift n0 n t)) = (size t).
NewInduction t;
[ Trivial
| Trivial
| Simpl; Intros n0 n; Rewrite IHt1; Rewrite IHt2; Trivial
| Simpl; Intros n0 n; Rewrite IHt1; Rewrite IHt2; Trivial ].
Qed.
Definition transitivity_prop [q : typ] :=
(e : env) (s, t : typ) (sub e s q) -> (sub e q t) -> (sub e s t).
Definition narrow_rel [e, e' : env; t, t' : typ; n : nat] :=
((n' : nat) (~ n' = n) -> (get e n') = (get e' n')) /\
(get e n) = (Some ? (ebound t)) /\ (get e' n) = (Some ? (ebound t')) /\
(sub e' (tshift (0) (S n) t') (tshift (0) (S n) t)).
Lemma narrow_rel_0 :
(e : env) (t, t' : typ)
(sub e t' t) ->
(narrow_rel (add_bound e t) (add_bound e t') t t' (0)).
Intros e t t' H; Repeat Split;
[ Intros n'; Case n';
[ Intro H1; Case H1; Trivial
| Trivial ]
| Unfold add_bound; Apply sub_weakening; Trivial ].
Qed.
Lemma narrow_rel_extend :
(e, e' : env) (t, t' : typ) (b : binding) (n : nat)
(narrow_rel e e' t t' n) ->
(narrow_rel (econs b e) (econs b e') t t' (S n)).
Intros e e' t t' b n (H1, (H2, (H3, H4))); Repeat Split;
[ Intros n' H5; NewInduction n'; Simpl; Auto
| Trivial
| Trivial
| Generalize (sub_weakening b H4);
Rewrite tshift_tshift_prop; Rewrite tshift_tshift_prop; Trivial ].
Qed.
Definition narrowing_prop [q : typ] :=
(e, e' : env) (n : nat) (p, s, t : typ)
(narrow_rel e e' q p n) -> (sub e s t) -> (sub e' s t).
Lemma transitivity_case :
(q : typ)
((q' : typ) (lt (size q') (size q)) ->
(transitivity_prop q') /\ (narrowing_prop q')) ->
(transitivity_prop q).
Intros q H e s t H1 H2; NewInduction H1;
[ Inversion_clear H2; Apply SA_Top
| Trivial
| Exact (SA_Trans_TVar H0 (IHsub H H2))
| Inversion_clear H2;
[ Apply SA_Top
| Apply SA_Arrow;
[ Assert H5 : (lt (size t1) (size (arrow t1 t2)));
[ Simpl; Omega
| Generalize (H ? H5); Intros (H6, _);
Exact (H6 ? ? ? H3 H1) ]
| Assert H5 : (lt (size t2) (size (arrow t1 t2)));
[ Simpl; Omega
| Generalize (H ? H5); Intros (H6, _);
Exact (H6 ? ? ? H0 H4) ] ] ]
| Inversion_clear H2;
[ Apply SA_Top
| Assert H5 : (lt (size t1) (size (all t1 t2)));
[ Simpl; Omega
| Generalize (H ? H5); Clear H5; Intros (H5, H6);
Apply SA_All;
[ Exact (H5 ? ? ? H3 H1)
| Assert H7 := (narrow_rel_0 H3);
Assert H8 := (H6 ? ? ? ? ? ? H7 H0);
Assert H9 : (lt (size t2) (size (all t1 t2)));
[ Simpl; Omega
| Assert G1 := (proj1 ? ? (H ? H9));
Exact (G1 (add_bound e t0) ? ? H8 H4) ] ] ] ] ].
Qed.
Lemma narrowing_case :
(q : typ)
((q' : typ) (size q') = (size q) -> (transitivity_prop q')) ->
(narrowing_prop q).
Intros q H2 e e' n t1 t2 t3 H3 H4; Generalize e' n H3; Clear e' n H3;
NewInduction H4; Intros e' n H3;
[ Apply SA_Top
| Apply SA_Refl_TVar
| Generalize H3; Intros (H5, (H6, (H7, H8)));
Case (eq_nat_dec x n);
[ Intro E; Rewrite E in H; Rewrite E; Clear x E;
Assert H4' := (IHsub ? ? H3); Clear H4 IHsub;
Unfold get_bound in H; Rewrite H6 in H; Simpl in H;
Injection H; Intros E; Rewrite <- E in H4'; Clear u H E;
Apply (H2 ? (shift_preserves_size ? (0) (S n))) with 2 := H4';
Apply SA_Trans_TVar with 2 := H8;
Unfold get_bound; Rewrite H7; Trivial
| Intro H9; Apply SA_Trans_TVar with 2 := (IHsub ? ? H3);
Unfold get_bound; Rewrite <- (H5 ? H9); Trivial ]
| Apply SA_Arrow; EAuto
| Apply SA_All;
[ EAuto
| EApply IHsub2; Unfold add_bound;
Apply narrow_rel_extend with 1 := H3 ] ].
Qed.
Lemma transitivity_and_narrowing :
(q : typ) (transitivity_prop q) /\ (narrowing_prop q).
Assert H :
(n : nat) (q : typ) (lt (size q) n) ->
(transitivity_prop q) /\ (narrowing_prop q);
[ NewInduction n;
[ Intros q H; Assert False; [ Omega | Contradiction ]
| Intros q H; Case (le_lt_or_eq ? ? H);
[ Intro H'; Apply IHn; Omega
| Intro E; Injection E; Clear E; Intro E; Rewrite <- E in IHn;
Assert H1 :
(q' : typ) (size q') = (size q) -> (transitivity_prop q');
[ Intros q' E1; Rewrite <- E1 in IHn;
Apply transitivity_case; Trivial
| Split;
[ Apply H1; Trivial
| Apply narrowing_case; Trivial ] ] ] ]
| Intro q; Apply (H (S (size q))); Omega ].
Qed.
Lemma sub_transitivity :
(e : env) (t, u, v : typ) (sub e t u) -> (sub e u v) -> (sub e t v).
Intros e t u v H1 H2;
Generalize (transitivity_and_narrowing u); Intros (H3, _); Apply H3; Trivial.
Qed.
Lemma sub_narrowing_ind :
(e, e' : env) (n : nat) (p, q, s, t : typ)
(narrow_rel e e' q p n) -> (sub e s t) -> (sub e' s t).
Intros e e' n p q s t H1 H2;
Generalize (transitivity_and_narrowing q); Intros (_, H3);
Apply H3 with 1 := H1 2 := H2.
Qed.
(****)
Lemma tsubst_preserves_subtyping_ind :
(e : env) (n : nat) (t, u, v : typ)
(sub e u v) ->
((t' : typ) (get_bound e n) = (Some ? (tshift (0) (S n) t')) ->
(sub (esubst e n t) (tshift (0) n t) (tshift (0) n t'))) ->
(sub (esubst e n t) (tsubst u n t) (tsubst v n t)).
Intros e n t u v H; Generalize n; Clear n; NewInduction H;
[ Intros n H1; Apply SA_Top
| Intros n H1; Apply sub_reflexivity
| Intros n H1; Simpl; Case (lt_eq_lt_dec x n);
[ Intros s; Case s; Clear s;
[ Intro H2; Apply SA_Trans_TVar with u := (tsubst u n t);
[ Rewrite get_bound_subst_lt with 1 := H2; Rewrite H; Trivial
| Apply IHsub; Trivial ]
| Intro E; Rewrite E in H; Clear x E;
Apply sub_transitivity with 2 := (IHsub ? H1);
Generalize (get_bound_shape H);
Intros (v, E); Rewrite E in H; Rewrite E;
Rewrite tsubst_tshift_prop_1; Try Omega; Auto ]
| Intro H2; Apply SA_Trans_TVar with u := (tsubst u n t);
[ Rewrite get_bound_subst_ge_2; Try Omega;
NewInduction x;
[ Assert False; [ Omega | Contradiction ]
| Simpl; Rewrite H; Trivial ]
| Apply IHsub; Trivial ] ]
| Intros n H2; Simpl; Apply SA_Arrow; Auto
| Intros n H2; Simpl; Apply SA_All; Auto;
Apply (IHsub2 (S n)); Intros t' H3;
Assert H4 : (ge n (0));
[ Omega
| Generalize (!get_bound_subst_ge_2 n (0) (add_bound e t1) top H4);
Simpl; Rewrite H3; Simpl; Rewrite tsubst_tshift_prop;
Intro H5;
Generalize (sub_weakening (ebound (tsubst t1 n t)) (H2 ? H5));
Rewrite tshift_tshift_prop; Rewrite tshift_tshift_prop;
Trivial ] ].
Qed.
(****)
Inductive typing : env -> term -> typ -> Prop :=
t_var :
(e : env) (n : nat) (t : typ)
(get_var e n) = (Some ? t) -> (typing e (var n) t)
| t_abs :
(e : env) (t : term) (t1, t2 : typ)
(typing (add_var e t1) t (tshift (0) (1) t2)) ->
(typing e (abs t1 t) (arrow t1 t2))
| t_app :
(e : env) (t1, t2 : term) (t11, t12 : typ)
(typing e t1 (arrow t11 t12)) -> (typing e t2 t11) ->
(typing e (app t1 t2) t12)
| t_tabs :
(e : env) (t : term) (t1, t2 : typ)
(typing (add_bound e t1) t t2) ->
(typing e (tabs t1 t) (all t1 t2))
| t_tapp :
(e : env) (t1 : term) (t11, t12, t2 : typ)
(typing e t1 (all t11 t12)) -> (sub e t2 t11) ->
(typing e (tapp t1 t2) (tsubst t12 (0) t2))
| t_sub :
(e : env) (t : term) (t1, t2 : typ)
(typing e t t1) -> (sub e t1 t2) -> (typing e t t2).
(****)
Lemma subst_typ_preserves_typing_ind :
(e : env) (t : term) (u, p, q : typ) (n : nat)
(typing e t u) ->
(get_bound e n) = (Some ? (tshift (0) (S n) q)) ->
(sub (esubst e n p) (tshift (0) n p) (tshift (0) n q)) ->
(typing (esubst e n p) (subst_typ t n p) (tsubst u n p)).
Intros e t u p q n H; Generalize n; Clear n; NewInduction H;
[ Intros n' H1 H2; Simpl; Case (lt_eq_lt_dec n n');
[ Intro s; Case s; Clear s;
[ Intro H3; Apply t_var;
Rewrite (get_var_subst_lt e p H3); Rewrite H; Trivial
| Intros E; Rewrite E in H; Case (get_var_or_bound H H1) ]
| Intro H3; Apply t_var; NewInduction n;
[ Assert False; [ Omega | Contradiction ]
| Simpl; Assert H4 : (ge n n');
[ Omega
| Rewrite (get_var_subst_ge e p H4); Rewrite H; Trivial ] ] ]
| Intros n E H1; Simpl; Apply t_abs;
Assert H2 :
(get_bound (add_var e t1) (S n)) = (Some typ (tshift (0) (S (S n)) q));
[ Unfold add_var; Rewrite get_bound_extend; Rewrite E;
Simpl; Rewrite tshift_tshift_prop; Trivial
| Generalize (!tshift_tsubst_prop_1 (0) (1) n t2 p); Simpl;
Intro E1; Rewrite E1; Apply IHtyping with 1 := H2; Simpl;
Generalize (sub_weakening (evar (tsubst t1 n p)) H1);
Rewrite tshift_tshift_prop; Rewrite tshift_tshift_prop; Trivial ]
| Intros n E H2; Simpl; Assert H3 := (IHtyping1 ? E H2);
Assert H4 := (IHtyping2 ? E H2); Simpl in H3;
Exact (t_app H3 H4)
| Intros n E H2; Simpl; Apply t_tabs; Apply (IHtyping (S n));
[ Unfold add_bound; Rewrite get_bound_extend; Rewrite E;
Simpl; Rewrite tshift_tshift_prop; Trivial
| Generalize (sub_weakening (ebound (tsubst t1 n p)) H2);
Rewrite tshift_tshift_prop; Rewrite tshift_tshift_prop;
Trivial ]
| Intros n E H1; Simpl; Assert H2 := (IHtyping ? E H1); Simpl in H2;
Rewrite (!tsubst_tsubst_prop (0) n); Apply t_tapp with 1 := H2;
Apply tsubst_preserves_subtyping_ind with 1 := H0;
Intros t' E1; Rewrite E1 in E; Injection E; Intro E2;
Rewrite (tshift_injective E2); Trivial
| Intros n E H1; Apply t_sub with 1 := (IHtyping ? E H1);
(* XXX We could factorize with the previous case *)
Apply tsubst_preserves_subtyping_ind with 1 := H0;
Intros t' E1; Rewrite E1 in E; Injection E; Intro E2;
Rewrite (tshift_injective E2); Trivial ].
Qed.
Lemma typing_weakening_ind :
(e : env) (n : nat) (t : term) (u, v : typ)
(typing (esubst e n v) t u) -> (env_free e n) ->
(typing e (shift n (1) t) (tshift n (1) u)).
Intros e n t u v H; Cut (EX e' | e' = (esubst e n v));
[ Intros (e', E); Rewrite <- E in H; Generalize e n v E; Clear e n v E;
NewInduction H;
[ Intros e' n' v E H1; Simpl; Case (le_gt_dec n' n); Intro H2;
[ Apply t_var; Rewrite E in H;
Rewrite (get_var_subst_ge e' v H2) in H;
Cut (EX t' | (get_var e' (S n)) = (Some ? t'));
[ Intros (t', E1);
Generalize (get_var_shape E1); Intros (t'', E2);
Rewrite E2 in E1; Rewrite E1 in H;
Simpl in H; Injection H; Intro E3; Rewrite <- E3;
Simpl; Rewrite E1; Rewrite tsubst_tshift_prop_1; Try Omega;
Rewrite tshift_tshift_prop_1; Try Omega; Trivial
| NewInduction (get_var e' (S n)); Try Discriminate;
Exists a; Trivial ]
| Apply t_var; Rewrite E in H;
Rewrite (get_var_subst_lt e' v H2) in H;
Cut (EX t' | (get_var e' n) = (Some ? t'));
[ Intros (t', E1); Generalize (H1 ? t' H2 (or_intror ? ? E1));
Intros (t'', E2); Rewrite E2 in E1; Rewrite E1 in H;
Simpl in H; Injection H; Intro E3; Rewrite <- E3;
Rewrite E1; Rewrite tsubst_tshift_prop_1; Try Omega;
Rewrite tshift_tshift_prop_1; Try Omega; Trivial
| NewInduction (get_var e' n); Try Discriminate;
Exists a; Trivial ] ]
| Intros e' n v E H1; Simpl; Apply t_abs;
Rewrite tshift_tshift_prop_2; Try Omega; Rewrite plus_sym;
Apply IHtyping with v := v;
[ Simpl; Rewrite E; Rewrite tsubst_tshift_prop_1; Try Omega;
Rewrite tshift_0_prop; Trivial
| Exact (env_free_extend 3! (evar t1) H1) ]
| Intros e' n v E H2;
Assert H3 := (IHtyping1 ? ? ? E H2);
Assert H4 := (IHtyping2 ? ? ? E H2);
Exact (t_app H3 H4)
| Intros e' n v E H1; Simpl; Apply t_tabs;
Apply IHtyping with v := v;
[ Simpl; Rewrite E; Rewrite tsubst_tshift_prop;
Rewrite tshift_0_prop; Trivial
| Exact (env_free_extend 3! (ebound t1) H1) ]
| Intros e' n v E H1;
Assert H2 := (IHtyping ? ? ? E H1); Simpl in H2;
Rewrite E in H0; Rewrite (tshift_tsubst_prop_2 n (1) (0));
Exact (t_tapp H2 (sub_weakening_ind H0 H1))
| Intros e' n v E H1; Rewrite E in H0; Rewrite E in H;
Apply t_sub with 2 := (sub_weakening_ind H0 H1);
Exact (IHtyping ? ? ? E H1) ]
| Exists (esubst e n v); Trivial ].
Qed.
Lemma typing_weakening :
(e : env) (b : binding) (t : term) (u : typ)
(typing e t u) -> (typing (econs b e) (shift (0) (1) t) (tshift (0) (1) u)).
Intros e b t u H; Apply typing_weakening_ind with v := top; Trivial;
Apply env_free_0.
Qed.
Lemma subst_preserves_typing_ind :
(e : env) (t, t' : term) (u, p : typ) (n : nat)
(typing e t u) ->
(get_var e n) = (Some ? (tshift (0) (S n) p)) ->
(typing (esubst e n dummy_type) (shift (0) n t') (tshift (0) n p)) ->
(typing (esubst e n dummy_type) (subst t n t') (tsubst u n dummy_type)).
Intros e t t' u p n H; Generalize n; Clear n; NewInduction H;
[ Intros n' E H1; Simpl; Case (lt_eq_lt_dec n n');
[ Intro s; Case s; Clear s;
[ Intro H2; Apply t_var; Rewrite (get_var_subst_lt e dummy_type H2);
Rewrite H; Trivial
| Intro E1; Rewrite E1 in H; Rewrite H in E; Injection E;
Intro E2; Rewrite E2; Rewrite tsubst_tshift_prop_1; Try Omega;
Trivial ]
| Intro H2; Apply t_var; Assert H3 : (ge (pred n) n');
[ Omega
| Rewrite (get_var_subst_ge e dummy_type H3);
Assert E1 : (S (pred n)) = n;
[ Omega
| Rewrite E1; Rewrite H; Trivial ] ] ]
| Intros n E H1; Simpl; Apply t_abs; Generalize (IHtyping (S n));
Generalize (tshift_tsubst_prop_1 (0) (1) n t2 dummy_type); Simpl;
Intro E1; Rewrite <- E1; Intro H2; Apply H2;
[ Unfold add_var; Rewrite get_var_extend; Rewrite E; Simpl;
Rewrite tshift_tshift_prop; Trivial
| Generalize (typing_weakening (evar (tsubst t1 n dummy_type)) H1);
Rewrite tshift_tshift_prop; Rewrite shift_shift_prop; Trivial ]
| Intros n E H2;
Assert H3 := (IHtyping1 ? E H2); Assert H4 := (IHtyping2 ? E H2);
Exact (t_app H3 H4)
| Intros n E H1; Simpl; Apply t_tabs; Apply (IHtyping (S n));
[ Unfold add_bound; Rewrite get_var_extend; Rewrite E; Simpl;
Rewrite tshift_tshift_prop; Trivial
| Generalize (typing_weakening (ebound (tsubst t1 n dummy_type)) H1);
Rewrite tshift_tshift_prop; Rewrite shift_shift_prop; Trivial ]
| Intros n E H1; Assert H2 := (IHtyping ? E H1); Simpl in H2;
Assert H3 :
(sub (esubst e n dummy_type)
(tsubst t2 n dummy_type) (tsubst t11 n dummy_type));
[ Apply tsubst_preserves_subtyping_ind with 1 := H0;
Intros t'' E1; Case (get_var_or_bound E E1)
| Rewrite (tsubst_tsubst_prop (0) n); Exact (t_tapp H2 H3) ]
| Intros n E H1; Apply t_sub with 1 := (IHtyping ? E H1);
Apply tsubst_preserves_subtyping_ind with 1 := H0;
Intros t'' E1; Case (get_var_or_bound E E1) ].
Qed.
Lemma typing_narrowing_ind :
(e, e' : env) (n : nat) (t : term) (u, v1, v2 : typ)
(narrow_rel e e' v1 v2 n) ->
(typing e t u) -> (typing e' t u).
Intros e e' n t u v1 v2 H1 H2; Generalize e' n H1; Clear e' n H1;
NewInduction H2; Intros e' n1 H1;
[ Generalize H1; Intros (H2, (H3, (H4, H5)));
Case (eq_nat_dec n n1);
[ Intro E; Rewrite E in H; Unfold get_var in H;
Rewrite H3 in H; Discriminate
| Intro H6; Apply t_var; Unfold get_var; Rewrite <- (H2 ? H6); Trivial ]
| Apply t_abs; Apply IHtyping with n := (S n1);
Unfold add_var; Apply narrow_rel_extend; Trivial
| EApply t_app; EAuto
| Apply t_tabs; Apply IHtyping with n := (S n1);
Unfold add_bound; Apply narrow_rel_extend; Trivial
| EApply t_tapp; EAuto;
Exact (sub_narrowing_ind H1 H)
| Apply t_sub with 1 := (IHtyping ? ? H1); Exact (sub_narrowing_ind H1 H) ].
Qed.
Lemma typing_narrowing :
(e : env) (t : term) (u, v1, v2 : typ)
(typing (add_bound e v1) t u) ->
(sub e v2 v1) ->
(typing (add_bound e v2) t u).
Intros e t u v1 v2 H1 H2; Exact (typing_narrowing_ind (narrow_rel_0 H2) H1).
Qed.
(****)
Definition value [t : term] :=
Cases t of
(abs _ _) => True
| (tabs _ _) => True
| _ => False
end.
Inductive red : term -> term -> Prop :=
appabs :
(t11 : typ) (t12, t2 : term) (value t2) ->
(red (app (abs t11 t12) t2) (subst t12 (0) t2))
| tapptabs :
(t11, t2 : typ) (t12 : term)
(red (tapp (tabs t11 t12) t2) (subst_typ t12 (0) t2))
| appfun :
(t1, t1', t2 : term) (red t1 t1') -> (red (app t1 t2) (app t1' t2))
| apparg :
(t1, t2, t2' : term)
(value t1) -> (red t2 t2') -> (red (app t1 t2) (app t1 t2'))
| typefun :
(t1, t1' : term) (t2 : typ)
(red t1 t1') -> (red (tapp t1 t2) (tapp t1' t2)).
(****)
Lemma t_abs_inversion :
(e : env) (t : term) (t0, t1, t2, t3 : typ)
(typing e (abs t1 t) t0) ->
(sub e t0 (arrow t2 t3)) ->
(sub e t2 t1) /\
(EX t4 | (sub e t4 t3) /\ (typing (add_var e t1) t (tshift (0) (1) t4))).
Intros e t t0 t1 t2 t3 H; Cut (EX t' | t' = (abs t1 t));
[ Intros (t', E1); Rewrite <- E1 in H;
Generalize t t1 t2 t3 E1; Clear t t1 t2 t3 E1;
NewInduction H; Intros; Try Discriminate;
[ Injection E1; Intros E2 E3; Rewrite <- E2; Rewrite <- E3;
Inversion_clear H0; Split;
[ Trivial
| Exists t2; Split; Trivial ]
| Apply IHtyping with 1 := E1 2 := (sub_transitivity H0 H1) ]
| Exists (abs t1 t); Trivial ].
Qed.
Lemma t_tabs_inversion :
(e : env) (t : term) (t0, t1, t2, t3 : typ)
(typing e (tabs t1 t) t0) ->
(sub e t0 (all t2 t3)) ->
(sub e t2 t1) /\
(EX t4 | (sub (add_bound e t2) t4 t3) /\ (typing (add_bound e t2) t t4)).
Intros e t t0 t1 t2 t3 H; Cut (EX t' | t' = (tabs t1 t));
[ Intros (t', E1); Rewrite <- E1 in H;
Generalize t t1 t2 t3 E1; Clear t t1 t2 t3 E1;
NewInduction H; Intros; Try Discriminate;
[ Injection E1; Intros E2 E3; Rewrite <- E2; Rewrite <- E3;
Inversion_clear H0; Split;
[ Trivial
| Exists t2; Split; Trivial;
Exact (typing_narrowing H H1) ]
| Apply IHtyping with 1 := E1 2 := (sub_transitivity H0 H1) ]
| Exists (tabs t1 t); Trivial ].
Qed.
Theorem preservation :
(e : env) (t, t' : term) (u : typ)
(typing e t u) -> (red t t') -> (typing e t' u).
Intros e t t' u H1; Generalize t'; Clear t'; NewInduction H1;
[ Intros t' H1; Inversion_clear H1
| Intros t' H2; Inversion_clear H2
| Intros t' H2; Generalize H1 IHtyping1; Clear H1 IHtyping1;
Inversion_clear H2;
[ Intros H1 IHtyping1;
Generalize (t_abs_inversion H1 (sub_reflexivity ? ?));
Intros (H2, (t4, (H4, H5)));
Apply t_sub with 2 := H4;
Generalize (!subst_preserves_typing_ind ? ? t2 ? t0 (0) H5);
Simpl; Rewrite tsubst_tshift_prop;
Rewrite tshift_0_prop; Rewrite tshift_0_prop;
Rewrite shift_0_prop; Intros H6; Apply H6;
[ Trivial
| Exact (t_sub H0 H2) ]
| Intros H1 IHtyping1; Apply t_app with 1 := (IHtyping1 ? H); Trivial
| Intros H2 IHtyping1; Apply t_app with 2 := (IHtyping2 ? H1); Trivial ]
| Intros t' H2; Inversion_clear H2
| Intros t' H2; Generalize H1 IHtyping; Clear H1 IHtyping;
Inversion_clear H2; Intros H1 IHtyping;
[ Generalize (t_tabs_inversion H1 (sub_reflexivity ? ?));
Intros (H2, (t3, (H4, H5)));
Assert H6 := (t_sub H5 H4);
Apply (!subst_typ_preserves_typing_ind ? ? ? t2 t11 (0) H6);
[ Trivial
| Rewrite tshift_0_prop; Rewrite tshift_0_prop; Trivial ]
| Apply t_tapp with 1 := (IHtyping ? H0); Trivial ]
| Intros t' H2; EApply t_sub; Auto ].
Qed.
(****)
Lemma fun_value :
(t : term) (t1, t2 : typ)
(value t) -> (typing empty t (arrow t1 t2)) ->
(EX t' | (EX t1' | t = (abs t1' t'))).
Intros t t1 t2 H1 H; Cut (EX e | e = empty);
[ Intros (e, E1); Rewrite <- E1 in H;
Cut (EX t0 | t0 = (arrow t1 t2));
[ Intros (t0, E2); Rewrite <- E2 in H;
Generalize t1 t2 E2; Clear t1 t2 E2;
NewInduction H; Try Contradiction;
[ Intros t3 t4 E; Exists t; Exists t1; Trivial
| Intros; Discriminate
| Intros t3 t4 E2; Rewrite E2 in H0;
Inversion H0;
[ Rewrite E1 in H2; NewInduction x; Discriminate
| Exact (IHtyping H1 E1 ? ? (sym_eq ? ? ? H5)) ] ]
| Exists (arrow t1 t2); Trivial ]
| Exists empty; Trivial ].
Qed.
Lemma typefun_value :
(t : term) (t1, t2 : typ)
(value t) -> (typing empty t (all t1 t2)) ->
(EX t' | (EX t1' | t = (tabs t1' t'))).
Intros t t1 t2 H1 H; Cut (EX e | e = empty);
[ Intros (e, E1); Rewrite <- E1 in H;
Cut (EX t0 | t0 = (all t1 t2));
[ Intros (t0, E2); Rewrite <- E2 in H;
Generalize t1 t2 E2; Clear t1 t2 E2;
NewInduction H; Try Contradiction;
[ Intros; Discriminate
| Intros t3 t4 E; Exists t; Exists t1; Trivial
| Intros t3 t4 E2; Rewrite E2 in H0;
Inversion H0;
[ Rewrite E1 in H2; NewInduction x; Discriminate
| Exact (IHtyping H1 E1 ? ? (sym_eq ? ? ? H5)) ] ]
| Exists (all t1 t2); Trivial ]
| Exists empty; Trivial ].
Qed.
Theorem progress :
(t : term) (u : typ) (typing empty t u) -> (value t) \/ (EX t' | (red t t')).
Intros t u H; Cut (EX e | e = empty);
[ Intros (e, E); Rewrite <- E in H; NewInduction H;
[ Rewrite E in H; NewInduction n; Discriminate
| Simpl; Auto
| Right; Case (IHtyping1 E);
[ Intro H2; Case (IHtyping2 E);
[ Intro H3; Rewrite E in H;
Generalize (fun_value H2 H); Intros (t', (t1', E1));
Rewrite E1; Exists (subst t' (0) t2); Apply appabs; Trivial
| Intros (t2', H3); Exists (app t1 t2'); Apply apparg; Trivial ]
| Intros (t1', H2); Exists (app t1' t2); Apply appfun; Trivial ]
| Simpl; Auto
| Right; Case (IHtyping E);
[ Intro H1; Rewrite E in H;
Generalize (typefun_value H1 H); Intros (t', (t1', E1));
Rewrite E1; Exists (subst_typ t' (0) t2); Apply tapptabs; Trivial
| Intros (t1', H1); Exists (tapp t1' t2); Apply typefun; Trivial ]
| Auto ]
| Exists empty; Trivial ].
Qed.
(****************************************************************************)
Fixpoint wf_typ [e : env; t : typ] : Prop :=
Cases t of
(tvar x) => ~ (get_bound e x) = (None ?)
| top => True
| (arrow t1 t2) => (wf_typ e t1) /\ (wf_typ e t2)
| (all t1 t2) => (wf_typ e t1) /\ (wf_typ (add_bound e top) t2)
end.
Fixpoint wf_term [e : env; t : term] : Prop :=
Cases t of
(var x) => ~ (get_var e x) = (None ?)
| (abs t1 e1) => (wf_typ e t1) /\ (wf_term (add_var e top) e1)
| (app e1 e2) => (wf_term e e1) /\ (wf_term e e2)
| (tabs t1 e1) => (wf_typ e t1) /\ (wf_term (add_bound e top) e1)
| (tapp e1 t2) => (wf_term e e1) /\ (wf_typ e t2)
end.
Definition well_formed [t : term] := (EX e | (wf_term e t)).
Lemma wf_typ_weakening :
(e : env) (n, n' : nat) (t, u : typ)
(wf_typ (esubst e n t) (tshift n n' u)) -> (env_free e n) ->
(wf_typ e (tshift n (S n') u)).
Intros e n n' t u; Generalize e n; Clear e n; NewInduction u;
[ Simpl; Intros e n''; Case (le_gt_dec n'' n); Intros H1 H2 H3;
[ Assert H4 : (ge (plus n' n) n''); Try Omega;
Rewrite (get_bound_subst_ge_2 e t H4) in H2;
NewInduction (get_bound e (S (plus n' n))); Trivial; Discriminate
| Rewrite (get_bound_subst_lt e t H1) in H2;
NewInduction (get_bound e n); Trivial; Discriminate ]
| Trivial
| Simpl; Intros e n (H1, H2); Auto
| Simpl; Intros e n (H1, H2) H3; Split; Auto;
Apply IHu2; Trivial;
Exact (env_free_extend 3!(ebound top) H3) ].
Qed.
Lemma tsubst_preserves_wf :
(e : env) (n : nat) (t, u : typ)
(wf_typ e u) ->
(~(get_bound e n) = (None ?) -> (wf_typ (esubst e n t) (tshift (0) n t))) ->
(wf_typ (esubst e n t) (tsubst u n t)).
Intros e n t u; Generalize e n; Clear e n; NewInduction u;
[ Simpl; Intros e n' E1 H1; Case (lt_eq_lt_dec n n');
[ Intros s; Case s; Clear s; Intro H2;
[ Simpl; Rewrite (get_bound_subst_lt e t H2);
NewInduction (get_bound e n); Try Discriminate; Case E1; Trivial
| Rewrite H2 in E1; Auto ]
| Intro H2; Simpl; Assert H3 : (ge (pred n) n');
[ Omega
| Rewrite (get_bound_subst_ge_2 e t H3);
Replace (S (pred n)) with n;
[ NewInduction (get_bound e n);
[ Discriminate
| Case E1; Trivial ]
| Omega ] ] ]
| Trivial
| Simpl; Intros e n (H1, H2); Auto
| Simpl; Intros e n (H1, H2) H3; Split;
[ Auto
| Apply (IHu2 ? (S n) H2); Intro H4; Unfold add_bound in H4;
Rewrite get_bound_extend in H4;
Apply wf_typ_weakening with t := top;
[ Apply H3; NewInduction (get_bound e n); Try Discriminate;
Case H4; Trivial
| Apply env_free_0 ] ] ].
Qed.
Lemma wf_term_weakening :
(e : env) (n, n' : nat) (t : term) (u : typ)
(wf_term (esubst e n u) (shift n n' t)) -> (env_free e n) ->
(wf_term e (shift n (S n') t)).
Intros e n n' t; Generalize e n; Clear e n; NewInduction t;
[ Simpl; Intros e n'' u; Case (le_gt_dec n'' n); Intros H1 H2 H3;
[ Assert H4 : (ge (plus n' n) n''); Try Omega;
Rewrite (get_var_subst_ge e u H4) in H2;
NewInduction (get_var e (S (plus n' n))); Try Discriminate;
Case H2; Trivial
| Rewrite (get_var_subst_lt e u H1) in H2;
NewInduction (get_var e n); Trivial; Discriminate ]
| Simpl; Intros e n u (H1, H2) H3; Split;
[ Apply wf_typ_weakening with 1 := H1 2 := H3
| Apply (IHt (add_var e top) (S n) u H2);
Exact (env_free_extend 3!(evar top) H3) ]
| Simpl; Intros e n u (H1, H2); EAuto
| Simpl; Intros e n u (H1, H2) H3; Split;
[ Apply wf_typ_weakening with 1 := H1 2 := H3
| Apply (IHt (add_bound e top) (S n) u H2);
Exact (env_free_extend 3!(ebound top) H3) ]
| Simpl; Intros e n u (H1, H2) H3; Split;
[ EAuto
| Apply wf_typ_weakening with 1 := H2 2 := H3 ] ].
Qed.
Lemma subst_preserves_wf :
(e : env) (t, t' : term) (n : nat)
(wf_term e t) -> ~ (get_var e n) = (None ?) ->
(wf_term (esubst e n dummy_type) (shift (0) n t')) ->
(wf_term (esubst e n dummy_type) (subst t n t')).
Intros e t; Generalize e; Clear e; NewInduction t;
[ Simpl; Intros e t' n' H1 H2 H3; Case (lt_eq_lt_dec n n');
[ Intro s; Case s; Clear s; Intro H4;
[ Simpl; Rewrite (get_var_subst_lt e dummy_type H4);
NewInduction (get_var e n); Try Discriminate;
Case H1; Trivial
| Trivial ]
| Intro H4; Simpl; Assert H5 : (ge (pred n) n'); Try Omega;
Rewrite get_var_subst_ge with 1 := H5;
Replace (S (pred n)) with n; Try Omega;
NewInduction (get_var e n); Try Discriminate;
Case H1; Trivial ]
| Simpl; Intros e t' n (H1, H2) H3 H4; Split;
[ Apply tsubst_preserves_wf with 1 := H1; Intro H5;
Case (H5 (get_var_or_bound_2 H3))
| Apply IHt with n := (S n) 1 := H2;
[ Unfold add_var; Rewrite get_var_extend;
NewInduction (get_var e n); Try Discriminate; Case H3; Trivial
| Apply wf_term_weakening with u := top; Trivial;
Apply env_free_0 ] ]
| Simpl; Intros e t' n (H1, H2); Auto
| Simpl; Intros e t' n (H1, H2) H3 H4; Split;
[ Apply tsubst_preserves_wf with 1 := H1; Intro H5;
Case (H5 (get_var_or_bound_2 H3))
| Apply IHt with n := (S n) 1 := H2;
[ Unfold add_bound; Rewrite get_var_extend;
NewInduction (get_var e n); Try Discriminate; Case H3; Trivial
| Apply wf_term_weakening with u := top; Trivial;
Apply env_free_0 ] ]
| Simpl; Intros e t' n (H1, H2) H3 H4; Split; Auto;
Apply tsubst_preserves_wf with 1 := H2; Intro H5;
Case (H5 (get_var_or_bound_2 H3)) ].
Qed.
Lemma subst_typ_preserves_wf :
(e : env) (t : term) (p : typ) (n : nat)
(wf_term e t) -> ~(get_bound e n) = (None ?) ->
(wf_typ (esubst e n p) (tshift (0) n p)) ->
(wf_term (esubst e n p) (subst_typ t n p)).
Intros e t; Generalize e; Clear e; NewInduction t;
[ Simpl; Intros e p n' H1 H2 H3; Case (lt_eq_lt_dec n n');
[ Intro s; Case s; Clear s; Intro H4;
[ Simpl; Rewrite (get_var_subst_lt e p H4);
NewInduction (get_var e n); Try Discriminate;
Case H1; Trivial
| Rewrite H4 in H1; Case (H2 (get_var_or_bound_2 H1)) ]
| Intro H4; Simpl; Assert H5 : (ge (pred n) n'); Try Omega;
Rewrite get_var_subst_ge with 1 := H5;
Replace (S (pred n)) with n; Try Omega;
NewInduction (get_var e n); Try Discriminate;
Case H1; Trivial ]
| Simpl; Intros e t' n (H1, H2) H3 H4; Split;
[ Apply tsubst_preserves_wf with 1 := H1; Trivial
| Apply (IHt (add_var e top) t' (S n)) with 1 := H2;
[ Unfold add_var; Rewrite get_bound_extend;
NewInduction (get_bound e n); Try Discriminate; Case H3; Trivial
| Apply wf_typ_weakening with t := top; Trivial;
Apply env_free_0 ] ]
| Simpl; Intros e t' n (H1, H2); Auto
| Simpl; Intros e t' n (H1, H2) H3 H4; Split;
[ Apply tsubst_preserves_wf with 1 := H1; Trivial
| Apply (IHt (add_bound e top) t' (S n)) with 1 := H2;
[ Unfold add_bound; Rewrite get_bound_extend;
NewInduction (get_bound e n); Try Discriminate; Case H3; Trivial
| Apply wf_typ_weakening with t := top; Trivial;
Apply env_free_0 ] ]
| Simpl; Intros e t' n (H1, H2) H3 H4; Split; Auto;
Apply tsubst_preserves_wf with 1 := H2; Trivial ].
Qed.
(****)
Fixpoint no_ref [in_typ : bool; n : nat; t : typ] : Prop :=
Cases t of
(tvar x) => if in_typ then ~(x = n) else True
| top => True
| (arrow t1 t2) => (no_ref in_typ n t1) /\ (no_ref in_typ n t2)
| (all t1 t2) => (no_ref in_typ n t1) /\ (no_ref in_typ (S n) t2)
end.
Fixpoint trm_no_ref [in_typ : bool; n : nat; t : term] : Prop :=
Cases t of
(var x) => if in_typ then True else ~(x = n)
| (abs t1 e1) => (no_ref in_typ n t1) /\ (trm_no_ref in_typ (S n) e1)
| (app e1 e2) => (trm_no_ref in_typ n e1) /\ (trm_no_ref in_typ n e2)
| (tabs t1 e1) => (no_ref in_typ n t1) /\ (trm_no_ref in_typ (S n) e1)
| (tapp e1 t2) => (trm_no_ref in_typ n e1) /\ (no_ref in_typ n t2)
end.
Lemma wf_implies_no_ref :
(t : typ) (e : env) (n : nat)
(wf_typ e t) -> (get_bound e n) = (None ?) ->
(no_ref true n t).
NewInduction t;
[ Simpl; Intros e n0 H E E'; Rewrite E' in H; Exact (H E)
| Trivial
| Simpl; Intros e n (H1, H2); EAuto
| Simpl; Intros e n (H1, H2); Split; EAuto;
Apply (IHt2 (add_bound e top)); Trivial;
Unfold add_bound; Rewrite get_bound_extend; Rewrite H; Trivial ].
Qed.
Lemma wf_implies_no_type_ref :
(t : term) (e : env) (n : nat)
(wf_term e t) -> (get_bound e n) = (None ?) ->
(trm_no_ref true n t).
NewInduction t;
[ Simpl; Trivial
| Simpl; Intros e n (H1, H2) E; Split;
[ Exact (wf_implies_no_ref H1 E)
| Apply IHt with 1 := H2; Unfold add_var;
Rewrite get_bound_extend; Rewrite E; Trivial ]
| Simpl; Intros e n (H1, H2) E; EAuto
| Simpl; Intros e n (H1, H2) E; Split;
[ Exact (wf_implies_no_ref H1 E)
| Apply IHt with 1 := H2; Unfold add_bound;
Rewrite get_bound_extend; Rewrite E; Trivial ]
| Simpl; Intros e n (H1, H2) E; Split; EAuto;
Exact (wf_implies_no_ref H2 E) ].
Qed.
Lemma no_term_var_in_typ :
(t : typ) (n : nat) (no_ref false n t).
NewInduction t; Simpl; Auto.
Qed.
Lemma wf_implies_no_term_ref :
(t : term) (e : env) (n : nat)
(wf_term e t) -> (get_var e n) = (None ?) ->
(trm_no_ref false n t).
NewInduction t;
[ Simpl; Intros e n0 H E E'; Rewrite E' in H; Exact (H E)
| Simpl; Intros e n (H1, H2) E; Split;
[ Apply no_term_var_in_typ
| Apply IHt with 1 := H2; Unfold add_var;
Rewrite get_var_extend; Rewrite E; Trivial ]
| Simpl; Intros e n (H1, H2) E; EAuto
| Simpl; Intros e n (H1, H2) E; Split;
[ Apply no_term_var_in_typ
| Apply IHt with 1 := H2; Unfold add_bound;
Rewrite get_var_extend; Rewrite E; Trivial ]
| Simpl; Intros e n (H1, H2) E; Split; EAuto;
Apply no_term_var_in_typ ].
Qed.
(****)
Fixpoint tlower [t : typ] : (n : nat) (no_ref true n t) -> typ :=
[x]
<[t:typ](no_ref true x t) -> typ>
Cases t of
(tvar x') =>
Cases (lt_eq_lt_dec x' x) of
(inleft (left _)) => [H](tvar x')
| (inleft (right G)) => [H](False_rec ? (H G))
| (inright _) => [H](tvar (pred x'))
end
| top => [H]top
| (arrow t1 t2) => [H](arrow (tlower (proj1 ? ? H)) (tlower (proj2 ? ? H)))
| (all t1 t2) => [H](all (tlower (proj1 ? ? H)) (tlower (proj2 ? ? H)))
end.
Fixpoint subst' [e : term] : (n : nat) term -> (trm_no_ref true n e) -> term :=
[x; e']
<[t:term](trm_no_ref true x t) -> term>
Cases e of
(var x') =>
[H]
Cases (lt_eq_lt_dec x' x) of
(inleft (left _)) => (var x')
| (inleft (right _)) => (shift (0) x e')
| (inright _) => (var (pred x'))
end
| (abs t1 e1) =>
[H](abs (tlower (proj1 ? ? H)) (subst' e' (proj2 ? ? H)))
| (app e1 e2) =>
[H](app (subst' e' (proj1 ? ? H)) (subst' e' (proj2 ? ? H)))
| (tabs t1 e1) =>
[H](tabs (tlower (proj1 ? ? H)) (subst' e' (proj2 ? ? H)))
| (tapp e1 t2) =>
[H](tapp (subst' e' (proj1 ? ? H)) (tlower (proj2 ? ? H)))
end.
Fixpoint subst_typ' [e : term] :
(n : nat) typ -> (trm_no_ref false n e) -> term :=
[x; t]
<[t:term](trm_no_ref false x t) -> term>
Cases e of
(var x') =>
[H]
Cases (lt_eq_lt_dec x' x) of
(inleft (left _)) => (var x')
| (inleft (right G)) => (False_rec ? (H G))
| (inright _) => (var (pred x'))
end
| (abs t1 e1) =>
[H](abs (tsubst t1 x t) (subst_typ' t (proj2 ? ? H)))
| (app e1 e2) =>
[H](app (subst_typ' t (proj1 ? ? H)) (subst_typ' t (proj2 ? ? H)))
| (tabs t1 e1) =>
[H](tabs (tsubst t1 x t) (subst_typ' t (proj2 ? ? H)))
| (tapp e1 t2) =>
[H](tapp (subst_typ' t (proj1 ? ? H)) (tsubst t2 x t))
end.
Lemma subst_equiv_lower :
(t : typ) (n : nat) (H : (no_ref true n t))
(tsubst t n dummy_type) = (tlower H).
NewInduction t;
[ Intros n' H; Simpl; Case (lt_eq_lt_dec n n');
[ Intros s; Case s; Clear s; Intro H1;
[ Trivial
| Case (H H1) ]
| Trivial ]
| Trivial
| Simpl; Fold no_ref; Intros n H;
Rewrite (IHt1 ? (proj1 ? ? H)); Rewrite (IHt2 ? (proj2 ? ? H)); Trivial
| Simpl; Fold no_ref; Intros n H;
Rewrite (IHt1 ? (proj1 ? ? H)); Rewrite (IHt2 ? (proj2 ? ? H)); Trivial ].
Qed.
Lemma subst_equiv_subst' :
(t, t' : term) (n : nat) (H : (trm_no_ref true n t))
(subst t n t') = (subst' t' H).
NewInduction t;
[ Trivial
| Simpl; Fold trm_no_ref; Intros t' n H;
Rewrite (subst_equiv_lower (proj1 ? ? H));
Rewrite (IHt t' ? (proj2 ? ? H)); Trivial
| Simpl; Fold trm_no_ref; Intros t' n H;
Rewrite (IHt1 t' ? (proj1 ? ? H));
Rewrite (IHt2 t' ? (proj2 ? ? H)); Trivial
| Simpl; Fold trm_no_ref; Intros t' n H;
Rewrite (subst_equiv_lower (proj1 ? ? H));
Rewrite (IHt t' ? (proj2 ? ? H)); Trivial
| Simpl; Fold trm_no_ref; Intros t' n H;
Rewrite (IHt t' ? (proj1 ? ? H));
Rewrite (subst_equiv_lower (proj2 ? ? H)); Trivial ].
Qed.
Lemma subst_typ_equiv_subst_typ' :
(t : term) (u : typ) (n : nat) (H : (trm_no_ref false n t))
(subst_typ t n u) = (subst_typ' u H).
NewInduction t;
[ Simpl; Intros _ n' H; Case (lt_eq_lt_dec n n');
[ Intro s; Case s; Clear s; Intro H1;
[ Trivial
| Case (H H1) ]
| Trivial ]
| Simpl; Fold trm_no_ref; Intros t' n H;
Rewrite (IHt t' ? (proj2 ? ? H)); Trivial
| Simpl; Fold trm_no_ref; Intros t' n H;
Rewrite (IHt1 t' ? (proj1 ? ? H));
Rewrite (IHt2 t' ? (proj2 ? ? H)); Trivial
| Simpl; Fold trm_no_ref; Intros t' n H;
Rewrite (IHt t' ? (proj2 ? ? H)); Trivial
| Simpl; Fold trm_no_ref; Intros t' n H;
Rewrite (IHt t' ? (proj1 ? ? H)); Trivial ].
Qed.
(****)
Inductive red' : term -> term -> Prop :=
appabs' :
(t11 : typ) (t12, t2 : term)
(value t2) -> (H : (trm_no_ref true (0) t12))
(red' (app (abs t11 t12) t2) (subst' t2 H))
| tapptabs' :
(t11, t2 : typ) (t12 : term) (H : (trm_no_ref false (0) t12))
(red' (tapp (tabs t11 t12) t2) (subst_typ' t2 H))
| appfun' :
(t1, t1', t2 : term) (red' t1 t1') -> (red' (app t1 t2) (app t1' t2))
| apparg' :
(t1, t2, t2' : term)
(value t1) -> (red' t2 t2') -> (red' (app t1 t2) (app t1 t2'))
| typefun' :
(t1, t1' : term) (t2 : typ)
(red' t1 t1') -> (red' (tapp t1 t2) (tapp t1' t2)).
Lemma red'_implies_red : (t, t' : term) (red' t t') -> (red t t').
Intros t t' H; NewInduction H;
[ Rewrite <- subst_equiv_subst'; Apply appabs; Trivial
| Rewrite <- subst_typ_equiv_subst_typ'; Apply tapptabs; Trivial
| Apply appfun; Trivial
| Apply apparg; Trivial
| Apply typefun; Trivial ].
Qed.
Theorem typing_preservation :
(e : env) (t, t' : term) (u : typ)
(typing e t u) -> (red' t t') -> (typing e t' u).
Intros e t t' u H1 H2; Apply preservation with 1 := H1;
Apply red'_implies_red; Trivial.
Qed.
Theorem wf_preservation :
(t, t' : term) (well_formed t) -> (red' t t') -> (well_formed t').
Intros t t' (e, H1) H2; Exists e; NewInduction H2;
[ Rewrite <- subst_equiv_subst';
Simpl in H1; Generalize H1; Clear H1; Intros ((H1, H2), H3);
Apply (!subst_preserves_wf ? ? t2 (0) H2);
[ Discriminate
| Rewrite shift_0_prop; Trivial ]
| Rewrite <- subst_typ_equiv_subst_typ';
Simpl in H1; Generalize H1; Clear H1; Intros ((H1, H2), H3);
Apply (!subst_typ_preserves_wf ? ? t2 (0) H2);
[ Discriminate
| Rewrite tshift_0_prop; Trivial ]
| Simpl in H1; Simpl; Case H1; Auto
| Simpl in H1; Simpl; Case H1; Auto
| Simpl in H1; Simpl; Case H1; Auto ].
Qed.
Theorem progress' :
(t : term) (u : typ) (well_formed t) -> (typing empty t u) ->
(value t) \/ (EX t' | (red' t t')).
Intros t u (e0, H0) H; Cut (EX e | e = empty);
[ Intros (e, E); Rewrite <- E in H; NewInduction H;
[ Rewrite E in H; NewInduction n; Discriminate
| Simpl; Auto
| Right; Simpl in H0; Case H0; Clear H0; Intros H0 H0';
Case (IHtyping1 H0 E);
[ Intro H2; Case (IHtyping2 H0' E);
[ Intro H3; Rewrite E in H;
Generalize (fun_value H2 H); Intros (t', (t1', E1));
Rewrite E1; Rewrite E1 in H0;
Simpl in H0; Case H0; Clear H0; Intros H4 H5;
Assert H6 :=
(wf_implies_no_type_ref 3!(0) H5 (refl_equal ? ?));
Exists (subst' t2 H6); Apply appabs'; Trivial
| Intros (t2', H3); Exists (app t1 t2'); Apply apparg'; Trivial ]
| Intros (t1', H2); Exists (app t1' t2); Apply appfun'; Trivial ]
| Simpl; Auto
| Right; Simpl in H0; Case H0; Clear H0; Intros H0 H0';
Case (IHtyping H0 E);
[ Intro H2; Rewrite E in H;
Generalize (typefun_value H2 H); Intros (t', (t1', E1));
Rewrite E1; Rewrite E1 in H0;
Simpl in H0; Case H0; Clear H0; Intros H4 H5;
Assert H6 :=
(wf_implies_no_term_ref 3!(0) H5 (refl_equal ? ?));
Exists (subst_typ' t2 H6); Apply tapptabs'; Trivial
| Intros (t1', H2); Exists (tapp t1' t2); Apply typefun'; Trivial ]
| Auto ]
| Exists empty; Trivial ].
Qed.
More information about the Poplmark
mailing list