Ltac sets H E :=
set (H := E); clearbody H.
Ltac poses H :=
let N := fresh "HU" in sets N H.
Ltac asserts H E :=
assert (H : E).
Ltac splits :=
repeat split.
Ltac destructs H :=
let H1 := fresh "H" in let H2 := fresh "H" in first
[ destruct H as [H1 H2]; destructs H1 ; destructs H2 | idtac ].
Ltac inversions H :=
inversion H; subst.
Ltac injections H :=
injection H; clear H; intros; subst.
Ltac contradictions :=
assert False; [ idtac | contradiction ].
Ltac decide_equality :=
match goal with |- {?X = ?Y} + {?X <> ?Y}
=> decide equality X Y end.
Ltac func_equal := match goal with
| [ |- (?F _ = ?F _ ) ] => apply (f_equal F)
| [ |- (?F _ _ = ?F _ _) ] => apply (f_equal2 F)
| [ |- (?F _ _ _ = ?F _ _ _) ] => apply (f_equal3 F)
| [ |- (?F _ _ _ _ = ?F _ _ _ _) ] => apply (f_equal4 F)
| _ => idtac
end.
Ltac generalize_equality expr name := let equa := fresh in
(set (name := expr); assert (equa : name = expr);
[ trivial | generalize name equa; clear name equa ]).
Require Import Omega.
Tactic Notation "change_maths" constr(H1) "with" constr(H2) :=
replace H1 with H2; [ idtac | omega ].
Tactic Notation "absurd_maths" :=
assert False; [ omega | contradiction ].
Tactic Notation "auto" "*" :=
try solve [ auto | intuition (eauto 7) ].
Tactic Notation "asserts" "*" ident(H) constr(E) :=
assert (H : E); [ auto* | idtac ].
Tactic Notation "apply" "*" constr(H) :=
first [ apply H | eapply H ]; auto*.
Tactic Notation "splits" "*" :=
splits; auto*.
Tactic Notation "inversion" "*" constr(H) :=
inversion H; auto*.
Tactic Notation "induction" "*" constr(H) :=
induction H; auto*.
Tactic Notation "inversions" "*" constr(H) :=
inversions H; auto*.
Tactic Notation "contradictions" "*" :=
contradictions; auto*.
Tactic Notation "rewrite" "*" constr(H) :=
rewrite H; auto*.
Tactic Notation "rewrite" "*" "<-" constr(H) :=
rewrite <- H; auto*.
Tactic Notation "simpl" "*" :=
simpl; auto*.
Tactic Notation "destruct" "*" constr(H) :=
destruct H; auto*.
Tactic Notation "func_equal" "*" :=
func_equal; auto*.
Ltac use expr :=
poses expr; auto*.
Ltac use2 expr1 expr2 :=
poses expr1; use expr2.
Ltac use3 expr1 expr2 expr3 :=
poses expr1; poses expr2; use expr3.
Set Implicit Arguments.
Require Import List.
Definition var := nat.
Lemma eq_var_dec : forall (x y : var), {x = y} + {x <> y}.
decide equality.
Qed.
Notation "x 'notin' L" := (~ (In x L)) (at level 68).
Lemma fresh_sum_plus_one : forall x L,
In x L -> fold_right (fun r y => S (y + r)) 1 L > x.
induction L; simpl; intros; destruct H.
subst. omega. poses (IHL H). omega.
Qed.
Lemma fresh_exists : forall L, exists x : var, x notin L.
intros. set (x := fold_right (fun r y => S (y + r)) 1 L).
exists x. intro H. sets HX (fresh_sum_plus_one x L H).
unfold x in HX. omega.
Qed.
Notation "x == y" := (eq_var_dec x y) (at level 67).
Notation "i === j" := (eq_nat_dec i j) (at level 67).
Definition atm := nat.
Inductive typ : Set :=
| typvar : atm -> typ
| arrow : typ -> typ -> typ.
Inductive trm : Set :=
| bvar : nat -> trm
| fvar : var -> trm
| app : trm -> trm -> trm
| abs : typ -> trm -> trm.
Fixpoint substb (k : nat) (u : trm) (t : trm) {struct t} : trm :=
match t with
| bvar i => if k === i then u else (bvar i)
| fvar x => fvar x
| app t1 t2 => app (substb k u t1) (substb k u t2)
| abs U t1 => abs U (substb (S k) u t1)
end.
Notation "{ k ~> u } t" := (substb k u t) (at level 67).
Notation "t ^^ u" := (substb 0 u t) (at level 67).
Notation "t ^ x" := (substb 0 (fvar x) t).
Fixpoint substf (z : var) (u : trm) (t : trm) {struct t} : trm :=
match t with
| bvar i => bvar i
| fvar x => if x == z then u else (fvar x)
| app t1 t2 => app (substf z u t1) (substf z u t2)
| abs U t1 => abs U (substf z u t1)
end.
Notation "[ z ~> u ] t" := (substf z u t) (at level 68).
Inductive env : Set :=
| env_empty : env
| env_push : env -> var -> typ -> env.
Notation "¤" := (env_empty).
Notation "E & x ~: T" := (env_push E x T) (at level 68).
Inductive env_has : env -> var -> typ -> Prop :=
| env_has_init : forall E x T,
env_has (E & x ~: T) x T
| env_has_push : forall E x y T U,
env_has E x T -> env_has (E & y ~: U) x T.
Notation "E 'has' x ~: T" := (env_has E x T) (at level 68).
Fixpoint dom (E : env) : list var :=
match E with
| ¤ => nil
| E & x ~: U => x :: (dom E)
end.
Notation "x '#' E" := (x notin (dom E)) (at level 68).
Reserved Notation "E 'wf' T" (at level 68).
Inductive wfin : env -> trm -> Prop :=
| wfin_fvar : forall E x T,
E has x ~: T -> E wf (fvar x)
| wfin_app : forall E t1 t2,
E wf t1 -> E wf t2 -> E wf (app t1 t2)
| wfin_abs : forall L E U t1,
(forall x, x notin L -> (E & x ~: U) wf (t1 ^ x)) ->
E wf (abs U t1)
where "E 'wf' t" := (wfin E t).
Inductive ok : env -> Prop :=
| ok_empty :
ok env_empty
| ok_push : forall E x T, ok E -> x # E -> ok (E & x ~: T).
Notation "E 'oks' t" := (ok E /\ E wf t) (at level 68).
Reserved Notation "E |- t ~: T" (at level 69).
Inductive typing : env -> trm -> typ -> Prop :=
| T_var : forall E x T, E oks (fvar x) ->
E has x ~: T -> E |- (fvar x) ~: T
| T_app : forall E S T t1 t2, E oks (app t1 t2) ->
E |- t1 ~: (arrow S T) -> E |- t2 ~: S ->
E |- (app t1 t2) ~: T
| T_abs : forall L E U T t1, E oks (abs U t1) ->
(forall x, x notin L -> (E & x ~: U) |- t1 ^ x ~: T) ->
E |- (abs U t1) ~: (arrow U T)
where "E |- t ~: T" := (typing E t T).
Inductive value : trm -> Prop :=
| value_abs : forall U t1, value (abs U t1).
Inductive red : trm -> trm -> Prop :=
| red_abs : forall U t1 t2,
value t2 -> red (app (abs U t1) t2) (t1 ^^ t2)
| red_app_1 : forall t1 t1' t2,
red t1 t1' -> red (app t1 t2) (app t1' t2)
| red_app_2 : forall t1 t2 t2',
value t1 -> red t2 t2' -> red (app t1 t2) (app t1 t2').
Notation "t --> t'" := (red t t') (at level 68).
Hint Constructors env_has wfin ok typing value red.
Ltac case_var :=
let destr x y := destruct (x == y); [try subst x | idtac] in
match goal with
| |- context [?x == ?y] => destr x y
| H: context [?x == ?y] |- _ => destr x y
end.
Tactic Notation "case_var" "*" := case_var; auto*.
Lemma fresh_cons : forall (x:var) y L,
x notin y :: L -> x <> y /\ x notin L.
splits; intro; apply H; simpl*.
Qed.
Lemma fresh_append : forall (x:var) K L,
x notin K ++ L -> x notin K /\ x notin L.
splits; use in_or_app.
Qed.
Ltac simpl_fresh H :=
let H1 := fresh "H" in let H2 := fresh "H" in
let recurse :=
clear H; try (simpl_fresh H1); try (simpl_fresh H2) in
match type of H with
| _ notin _ :: _ => destruct (fresh_cons H) as [H1 H2]; recurse
| ?x notin ?K ++ ?L =>
destruct (fresh_append x K L H) as [H1 H2]; recurse
end.
Tactic Notation "pick" ident(x) "notin" constr(L) :=
let H := fresh "H" in
(destruct (fresh_exists L) as [x H]; try simpl_fresh H).
Ltac apply_T_abs x L :=
let Fr := fresh "Fr" in (eapply (@T_abs L);
[ auto* | intros x Fr; simpl_fresh Fr ]).
Lemma has_to_not_fresh : forall E x U,
x # E -> E has x ~: U -> False.
intros. induction E. inversion H0.
simpl in H. inversions* H0.
Qed.
Lemma env_functional : forall x U V E,
ok E -> E has x ~: U -> E has x ~: V -> U = V.
intros x U V E. induction E; intros; inversion H;
inversion H0; inversion H1; subst; try solve
[ auto | contradictions; apply* has_to_not_fresh ].
Qed.
Fixpoint infv (x : var) (t : trm) {struct t} : Prop :=
match t with
| bvar i => False
| fvar y => x = y
| app t1 t2 => infv x t1 \/ infv x t2
| abs U t1 => infv x t1
end.
Lemma infv_pass_binder : forall x y t k,
infv x t -> infv x ({k ~> fvar y}t).
induction t; simpl*.
Qed.
Lemma fresh_wf_to_not_infv : forall x E T,
x # E -> E wf T -> ~(infv x T).
intros x E T Fr WT. induction WT; simpl*.
intro. subst x. apply* has_to_not_fresh.
intro C. pick y notin (x :: (dom E) ++ L).
assert (x # (E & y ~: U)). simpl*.
use infv_pass_binder.
Qed.
Lemma var_intro_infv : forall x u t k, ~(infv x t) ->
{k ~> u}t = [x ~> u]{k ~> fvar x}t.
induction t; simpl; intros; func_equal*.
destruct (k === n); simpl. case_var*. auto*.
case_var*.
Qed.
Lemma var_intro : forall x E U t, x # E -> E wf (abs U t) ->
forall u, t ^^ u = [x ~> u](t ^x).
intros. apply var_intro_infv. use fresh_wf_to_not_infv.
Qed.
Lemma substb_cross : forall u v t i j, i <> j ->
{i ~> u}({j ~> v}t) = {j ~> v}t -> {i ~> u}t = t.
induction t; intros; simpl in *; inversion H0; func_equal*.
destruct* (j === n). destruct* (i === n). absurd_maths.
Qed.
Lemma substb_on_wf : forall E t u,
E wf t -> forall k, {k ~> u}t = t.
intros E T u WF. induction WF; intros; simpl; func_equal*.
pick x notin L. eapply substb_cross with (j := 0). omega. auto*.
Qed.
Lemma subst_permutation_ind : forall E x y u t,
y <> x -> E wf u -> forall k,
{k ~> fvar y} ([x ~> u]t) = [x ~> u] ({k ~> fvar y} t).
induction t; intros; simpl; func_equal*.
destruct* (k === n). simpl. case_var*.
case_var*. apply* substb_on_wf.
Qed.
Lemma subst_permutation : forall E x y u t, y <> x -> E wf u ->
([x ~> u]t) ^ y = [x ~> u] (t ^ y).
use subst_permutation_ind.
Qed.
Definition extends E F :=
forall x U, E has x ~: U -> F has x ~: U.
Notation "E 'inc' F" := (extends E F) (at level 68).
Hint Unfold extends.
Lemma extends_push : forall E F x T,
E inc F -> (E & x ~: T) inc (F & x ~: T).
unfold extends. intros. inversion* H0.
Qed.
Definition env_subst z E F :=
forall x U, E has x ~: U -> x <> z -> F has x ~: U.
Notation "E '\' z 'incl' F" := (env_subst z E F) (at level 67).
Lemma env_subst_init : forall E z S, (E & z ~: S) \ z incl E.
unfold env_subst. intros. inversions* H.
Qed.
Lemma env_subst_push : forall z E F x U, x <> z ->
E \ z incl F -> (E & x ~: U) \ z incl (F & x ~: U).
unfold env_subst. intros. inversions* H1.
Qed.
Lemma typing_to_ok : forall E t T, E |- t ~: T -> ok E.
intros. inversion* H.
Qed.
Lemma typing_to_wf : forall E t T, E |- t ~: T -> E wf t.
intros. inversion* H.
Qed.
Lemma extends_wf : forall E t, E wf t ->
forall F, E inc F -> F wf t.
intros E t H. induction* H. use extends_push.
Qed.
Lemma subst_wf : forall t z u E, E wf t ->
forall F, E \ z incl F -> F wf u -> F wf ([z ~> u]t).
intros t z u E H. induction H; intros F Incl Wu; simpl.
case_var*. auto*. apply* (@wfin_abs (z::L)).
intros x Fr. simpl_fresh Fr. rewrite* (@subst_permutation F).
use2 extends_wf env_subst_push.
Qed.
Hint Resolve typing_to_ok typing_to_wf extends_wf.
Lemma extends_typing : forall E t T,
E |- t ~: T -> forall F, E inc F -> ok F -> F |- t ~: T.
intros E r T Typt. induction* Typt.
intros. apply_T_abs x (L ++ dom F). use extends_push.
Qed.
Lemma subst_typing : forall E z u U t T,
E has z ~: U -> E |- t ~: T ->
forall F, E \ z incl F -> F |- u ~: U ->
F |- [z ~> u]t ~: T.
intros E z u U t T Has Typt.
induction Typt; intros F Incl Typu; simpl*.
case_var*. rewrite* (@env_functional z T U E).
apply* T_app.
sets WF (@subst_wf (abs U0 t1)). simpl in WF.
apply_T_abs x (z :: dom F ++ dom E ++ L).
rewrite* (@subst_permutation F). apply* H1.
apply* env_subst_push. apply* extends_typing.
Qed.
Lemma preservation_ind : forall t t', t --> t' ->
forall E T, E |- t ~: T -> E |- t' ~: T.
intros t t' Red. induction Red; intros E T Typ; inversions Typ.
inversions H4. pick x notin (L ++ dom E).
rewrite* (@var_intro x E S).
apply* subst_typing. apply* env_subst_init.
apply* T_app. apply* T_app.
Qed.
Lemma progress_ind : forall t T E, E |- t ~: T ->
E = env_empty -> value t \/ exists t' : trm, t --> t'.
intros t T E Typ. induction Typ; intros EQ; subst.
inversion H0. destruct* (IHTyp1). destruct* (IHTyp2).
inversion* H0. destruct* H1. destruct* H0. auto*.
Qed.
Theorem preservation : forall E t t' T,
t --> t' -> E |- t ~: T -> E |- t' ~: T.
use preservation_ind.
Qed.
Theorem progress : forall t T, ¤ |- t ~: T ->
value t \/ exists t' : trm, t --> t'.
use progress_ind.
Qed.