# Library Stlc.Lec2

Require Import Metalib.Metatheory.

Require Import Stlc.Definitions.

Import StlcNotations.

Require Import Stlc.Lemmas.

Require Import Stlc.Lec1.

# Typing contexts

Lemma append_assoc_demo : ∀ (E0 E1 E2 E3:ctx),

E0 ++ (E1 ++ E2) ++ E3 = E0 ++ E1 ++ E2 ++ E3.

Proof.

intros.

auto. simpl_env.

reflexivity.

Qed.

To make contexts easy to read, instead of building them from
nil and cons, we prefer to build them from the following
components:
The simpl_env tactic actually puts lists built from only nil, one
and ++ into a "normal form". This process reassociates all appends
to the right, removes extraneous nils and converts cons to singleton
lists with an append.

- nil: The empty list.
- one: Lists consisting of exactly one item.
- ++: List append.

Lemma simpl_env_demo : ∀ (x y:atom) (T1 T2:typ) (E F:ctx),

([(x, T1)] ++ nil) ++ (y,T2) :: (nil ++ E) ++ F =

[(x,T1)] ++ [(y, T2)] ++ E ++ F.

Proof.

intros.

simpl_env.

reflexivity.

Qed.

Context operations.
The ternary predicate binds holds when a given binding is
present somewhere in an context.

The function dom computes the domain of an context,
returning a finite set of atoms. Note that we cannot use Coq's
equality for finite sets, we must instead use a defined relation
= for atom set equality.

The unary predicate uniq holds when each atom is bound at most
once in an context.

# Typing relation and cofinite quantification

typing_abs : forall (L : atoms) (G : ctx) (T1 : typ) (e : exp) (T2 : typ), (forall x : atom, x `notin` L -> typing ([(x, T1)] ++ G) (open e (var_f x)) T2) -> typing G (abs e) (typ_arrow T1 T2)

Inductive typing_e : ctx → exp → typ → Prop :=

| typing_e_var : ∀ E (x : atom) T,

uniq E →

binds x T E →

typing_e E (var_f x) T

| typing_e_abs : ∀ x E e T1 T2,

x `notin` dom E \u fv_exp e →

typing_e ([(x, T1)] ++ E) (e ^ x) T2 →

typing_e E (abs e) (typ_arrow T1 T2)

| typing_e_app : ∀ E e1 e2 T1 T2,

typing_e E e1 (typ_arrow T1 T2) →

typing_e E e2 T1 →

typing_e E (app e1 e2) T2.

Hint Constructors typing_e.

## Weakening

Lemma typing_weakening_0 : ∀ E F e T,

typing_e E e T →

uniq (F ++ E) →

typing_e (F ++ E) e T.

Proof.

intros E F e T H J.

induction H; auto.

Case "typing_abs".

apply (typing_e_abs x).

Abort.

We are stuck in the typing_abs case because the induction
hypothesis IHtyping_e applies only when we weaken the context at its
head. In this case, however, we need to weaken the context in
the middle; compare the conclusion at the point where we're stuck
to the hypothesis H, which comes from the given typing derivation.
We can obtain a more useful induction hypothesis by changing the
statement to insert new bindings into the middle of the
context, instead of at the head. However, the proof still
gets stuck, as can be seen by examining each of the cases in
the proof below.
Note: To view subgoal n in a proof, use the command "Show n".
To work on subgoal n instead of the first one, use the command
"Focus n".

Lemma typing_weakening_strengthened_0 : ∀ (E F G : ctx) e T,

typing_e (G ++ E) e T →

uniq (G ++ F ++ E) →

typing_e (G ++ F ++ E) e T.

Proof.

intros E F G e T H J.

induction H.

Case "typing_var".

Focus 2.

Case "typing_abs".

Abort.

The hypotheses in the typing_var case include an context
G0 that that has no relation to what we need to prove. The
missing fact we need is that G0 = (G ++ E).
The problem here arises from the fact that Coq's induction
tactic lets us only prove something about all typing derivations.
While it's clear to us that weakening applies to all typing
derivations, it's not clear to Coq, because the context is
written using concatenation. The induction tactic expects that
all arguments to a judgement are variables. So we see E0 in the
proof instead of (G ++ E).
The solution is to restate the lemma. For example, we can prove
The equality gets around the problem with Coq's induction
tactic. The placement of the (∀ G) quantifier gives us a
sufficiently strong induction hypothesis in the typing_abs case.
However, we prefer not to state the lemma in the way shown above,
since it is not as readable as the original statement. Instead,
we use a tactic to introduce the equality within the proof itself.
The tactic (remember t as t') replaces an object t with the
identifier t' everywhere in the goal and introduces an equality
t' = t into the context. It is often combined with generalize
dependent, as illustrated below.

forall E F E' e T, typing E' e T -> forall G, E' = G ++ E -> uniq (G ++ F ++ E) -> typing (G ++ F ++ E) e T.

Lemma typing_weakening_strengthened_1 : ∀ (E F G : ctx) e T,

typing_e (G ++ E) e T →

uniq (G ++ F ++ E) →

typing_e (G ++ F ++ E) e T.

Proof.

intros E F G e T H.

remember (G ++ E) as E'.

generalize dependent G.

induction H; intros G0 Eq Uniq; subst.

- Case "typing_var". auto.

- Case "typing_abs".

eapply (typing_e_abs x).

Abort.

Print typing_abs.

At this point, we are very close. However, there is still one issue. We
cannot show that x is fresh for the weakened context F.
This is the difficulty with the definition of typing_e. As in the local
closure judgement, the induction hypotheses is not strong enough in the
abs case.
However, this time, we take a slightly different solution, with the
cofinite quantification of the typing_abs rule.
>>
The advantage of this definition is that it is easier to derive
the "exists-fresh" version of the rule
typing_e_abs as a lemma, than the version we used in lc_exp.
(See below, we prove this lemma after we show substitution.) At the same
time, this version of the rule is sufficiently expressive to complete
the proof of weakening.
Complete the proof below, using the typing relation from Definitions.v.
HINTS:

| typing_abs : forall (L : atoms) (G : ctx) (T1 : typ) (e : exp) (T2 : typ), (forall x, x `notin` L -> typing ([(x, T1)] ++ G) (e ^ x) T2) -> typing (abs e) (typ_arrow T1 T2)

### Exercise typing_weakening_strengthened

- The typing_var case follows from binds_weaken, the
weakening lemma for the binds relation.
- The typing_abs case follows from the induction
hypothesis, but the apply tactic may be unable to unify
things as you might expect.
- - You'll need to specify the set to avoid with
(L := dom (G0 ++ F ++ E) \u L)).
- - In order to apply the induction hypothesis, use
rewrite_env to reassociate the list operations.
- - After applying the induction hypothesis, use
simpl_env to use uniq_push.
- - Here, use auto to solve facts about finite sets of
atoms, since it will simplify the dom function behind
the scenes. fsetdec does not work with the dom
function.

- - You'll need to specify the set to avoid with
(L := dom (G0 ++ F ++ E) \u L)).
- The typing_app case follows directly from the induction hypotheses.

Lemma typing_weakening_strengthened : ∀ (E F G : ctx) e T,

typing (G ++ E) e T →

uniq (G ++ F ++ E) →

typing (G ++ F ++ E) e T.

Proof.

intros E F G e T H.

remember (G ++ E) as E'.

generalize dependent G.

induction H; intros G0 Eq Uniq; subst.

Admitted.

### Demo typing_weakening

Lemma typing_weakening : ∀ (E F : ctx) e T,

typing E e T →

uniq (F ++ E) →

typing (F ++ E) e T.

Proof.

intros E F e T H J.

rewrite_env (nil ++ F ++ E).

apply typing_weakening_strengthened; auto.

Qed.

## Substitution

typing_subst_simple : forall E e u S T z, typing ([(z,S)] ++ E) e T -> typing E u S -> typing E ([z ~> u] e) T typing_subst : forall E F e u S T z, typing (F ++ [(z,S)] ++ E) e T -> typing E u S -> typing (F ++ E) ([z ~> u] e) T

### Exercise typing_subst_var_case

- If (x = z), then we need to show (typing (F ++ E) u T).
This follows from the given typing derivation for u by
weakening and the fact that T must equal S.
- If (x ≠ z), then we need to show (typing (F ++ E) x T). This follows by the typing rule for variables.

Lemma typing_subst_var_case : ∀ (E F : ctx) u S T (z x : atom),

binds x T (F ++ [(z,S)] ++ E) →

uniq (F ++ [(z,S)] ++ E) →

typing E u S →

typing (F ++ E) ([z ~> u] (var_f x)) T.

Proof.

intros E F u S T z x H J K.

simpl.

Admitted.

### Exercise typing_subst

- Use the lemma proved above for the typing_var case.
- The typing_abs case follows from the induction hypothesis.
- - Use simpl to simplify the substitution.
- - In order to use the induction hypothesis, use subst_var
to push the substitution under the opening operation.
- - Recall the lemma typing_to_lc_c and the rewrite_env
and simpl_env tactics.

- - Use simpl to simplify the substitution.
- The typing_app case follows from the induction hypotheses. Use simpl to simplify the substitution.

Lemma typing_subst : ∀ (E F : ctx) e u S T (z : atom),

typing (F ++ [(z,S)] ++ E) e T →

typing E u S →

typing (F ++ E) ([z ~> u] e) T.

Proof.

Admitted.

### Exercise typing_subst_simpl

Lemma typing_subst_simple : ∀ (E : ctx) e u S T (z : atom),

typing ([(z,S)] ++ E) e T →

typing E u S →

typing E ([z ~> u] e) T.

Proof.

Admitted.

# Type soundness

## Preservation

### Recommended Exercise preservation

- typing_var case: Variables don't step.
- typing_abs case: Abstractions don't step.
- typing_app case: By case analysis on how e steps. The step_beta case is interesting, since it follows by the substitution lemma. The others follow directly from the induction hypotheses.

Lemma preservation : ∀ (E : ctx) e e' T,

typing E e T →

step e e' →

typing E e' T.

Proof.

intros E e e' T H.

generalize dependent e'.

induction H; intros e' J.

Admitted.

## Progress

### Exercise progress

- typing_var case: Can't happen; the empty context doesn't
bind anything.
- typing_abs case: Abstractions are values.
- typing_app case: Applications reduce. The result follows from an exhaustive case analysis on whether the two components of the application step or are values and the fact that a value must be an abstraction.

Lemma progress : ∀ e T,

typing nil e T →

is_value e ∨ ∃ e', step e e'.

Proof.

intros e T H.

assert (typing nil e T); auto.

remember (@nil (atom × typ)) as E.

induction H; subst.

Admitted.

# Tactic support

Ltac gather_atoms ::=

let A := gather_atoms_with (fun x : atoms ⇒ x) in

let B := gather_atoms_with (fun x : atom ⇒ singleton x) in

let C := gather_atoms_with (fun x : list (var × typ) ⇒ dom x) in

let D := gather_atoms_with (fun x : exp ⇒ fv_exp x) in

constr:(A `union` B `union` C `union` D).

A number of other, useful tactics are defined by the Metatheory
library, and each depends on gather_atoms. By redefining
gather_atoms, denoted by the ::= in its definition below, we
automatically update these tactics so that they use the proper
notion of "all atoms in the context."
For example, the tactic (pick fresh x) chooses an atom fresh for
"everything" in the context. It is the same as (pick fresh x for
L), except where L has been computed by gather_atoms.
Substitution and weakening together give us a property we call
renaming: (see typing_rename below that we can change the name
of the variable used to open an expression in a typing
derivation. In practice, this means that if a variable is not
"fresh enough" during a proof, we can use this lemma to rename it
to one with additional freshness constraints.
Renaming is used below to show the correspondence between the
exists-fresh version of the rules with the cofinite version, and
also to show that typechecking is decidable.
However, before we prove renaming, we need an auxiliary lemma about
typing judgments which says that terms are well-typed only in
unique contexts.

# Renaming

Lemma typing_uniq : ∀ E e T,

typing E e T → uniq E.

Proof.

intros E e T H.

induction H; auto.

- Case "typing_abs".

pick fresh x.

assert (uniq ([(x, T1)] ++ G)); auto.

solve_uniq.

Qed.

Demo: the proof of renaming.
Note that this proof does not proceed by induction: even if we add
new typing rules to the language, as long as the weakening and
substution properties hold we can use this proof.

Lemma typing_rename : ∀ (x y : atom) E e T1 T2,

x `notin` fv_exp e →

y `notin` dom E →

typing ([(x, T1)] ++ E) (e ^ x) T2 →

typing ([(y, T1)] ++ E) (e ^ y) T2.

Proof.

intros x y E e T1 T2 Fr1 Fr2 H.

destruct (x == y).

- Case "x = y".

subst; eauto.

- Case "x <> y".

assert (J : uniq ([(x, T1)] ++ E)).

eapply typing_uniq; eauto.

assert (J' : uniq E).

inversion J; eauto.

rewrite (@subst_exp_intro x); eauto.

rewrite_env (nil ++ [(y, T1)] ++ E).

apply typing_subst with (S := T1).

simpl_env.

+ SCase "(open x s) is well-typed".

apply typing_weakening_strengthened. eauto. auto.

+ SCase "y is well-typed".

eapply typing_var; eauto.

Qed.

x `notin` fv_exp e →

y `notin` dom E →

typing ([(x, T1)] ++ E) (e ^ x) T2 →

typing ([(y, T1)] ++ E) (e ^ y) T2.

Proof.

intros x y E e T1 T2 Fr1 Fr2 H.

destruct (x == y).

- Case "x = y".

subst; eauto.

- Case "x <> y".

assert (J : uniq ([(x, T1)] ++ E)).

eapply typing_uniq; eauto.

assert (J' : uniq E).

inversion J; eauto.

rewrite (@subst_exp_intro x); eauto.

rewrite_env (nil ++ [(y, T1)] ++ E).

apply typing_subst with (S := T1).

simpl_env.

+ SCase "(open x s) is well-typed".

apply typing_weakening_strengthened. eauto. auto.

+ SCase "y is well-typed".

eapply typing_var; eauto.

Qed.

## Exists-Fresh Definition

Lemma typing_abs_exists : ∀ E e T1 T2 (x : atom),

x `notin` dom E \u fv_exp e →

typing ([(x,T1)] ++ E) (e ^ x) T2 →

typing E (abs e) (typ_arrow T1 T2).

Proof.

intros.

apply typing_abs with (L := dom E \u fv_exp e).

intros y Fr.

apply typing_rename with (x:=x); auto.

Qed.