Rec.Examples.sysf_const_sn

Section 10 Case Study : Strong Normalisation of System F

This file contains the Coq code corresponding to chapter 10, showing strong normalisation of System F. It is based on the previous framework.

From mathcomp Require Import ssreflect.all_ssreflect.
Require Import Base.axioms Base.fintype Base.ARS.
Require Import Framework.graded Framework.sysf_types Framework.sysf_const_terms.
Set Implicit Arguments.
Unset Strict Implicit.

The tactic repeatedly rewrites with the lemmas established for traversals and models for the types and terms of System FCBV.

Local Ltac asimpl :=
repeat progress (cbn; fsimpl; gsimpl; ty_simpl; tm_simpl).

One-Step Reduction

Inductive step {m n} : tm m n -> tm m n -> Prop :=
| step_beta (A : ty m) (s : tm m n.+1) (t : tm m n) :
    step (Tm.app (Tm.lam A s) t) s .[Ty.var , t .: Tm.var ]%tm
| step_Beta (A : ty m) (s : tm m.+1 n) :
    step (Tm.App (Tm.Lam s) A) s .[A .: Ty.var , Tm.var ]%tm
| step_appL s1 s2 t :
    step s1 s2 -> step (Tm.app s1 t) (Tm.app s2 t)
| step_appR s t1 t2 :
    step t1 t2 -> step (Tm.app s t1) (Tm.app s t2)
| step_abs A s1 s2 :
    @step m n.+1 s1 s2 -> step (Tm.lam A s1) (Tm.lam A s2)
| step_tapp A s1 s2 :
    step s1 s2 -> step (Tm.App s1 A) (Tm.App s2 A)
| step_tabs s1 s2 :
    @step m.+1 n s1 s2 -> step (Tm.Lam s1) (Tm.Lam s2).

Lemma step_ebeta {m n} A s t (u : tm m n) :
  u = s .[Ty.var , t .: Tm.var ]%tm -> step (Tm.app (Tm.lam A s) t) u.
Proof. move->. exact: step_beta. Qed.

Lemma step_eBeta {m n} A s (t : tm m n) :
  t = s .[A .: Ty.var , Tm.var ]%tm -> step (Tm.App (Tm.Lam s) A) t.
Proof. move->. exact: step_Beta. Qed.

One-step reduction is compatible with substitution.

Lemma step_inst {m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau : fin n1 -> tm m2 n2) s t :
  step s t -> step s .[sigma ,tau ]%tm t .[sigma ,tau ]%tm.
Proof.
  move=> st. elim: st m2 n2 tau sigma => {m1 n1 s t}; asimpl; eauto using @step.
  - move=> m1 n1 A s t m2 n2 tau sigma. apply: step_ebeta. by asimpl.
  - move=> m1 n1 A s m2 n2 tau sigma. apply: step_eBeta. by asimpl.
Qed.

Many-Step Reduction

Definition red {m n} := star (@step m n).

Definition sred {m n k} (sigma tau : fin m -> tm n k) :=
forall x, @red n k (sigma x) (tau x).

Congruence and compatibility of many-step reduction. This is necessary to show that beta-reduction entails the correct behaviour (Lemma red_beta). The proofs are standard.

Lemma red_app {m n} (s1 s2 t1 t2 : tm m n) :
  red s1 s2 -> red t1 t2 -> red (Tm.app s1 t1) (Tm.app s2 t2).
Proof.
  move=> A B. apply: (star_trans (Tm.app s2 t1)).
  - apply: (star_hom (@Tm.app m n^~ t1)) A => x y. exact: step_appL.
  - apply: star_hom B => x y. exact: step_appR.
Qed.

Lemma red_abs {m n} A (s1 s2 : tm m n .+1) :
  red s1 s2 -> red (Tm.lam A s1) (Tm.lam A s2).
Proof. apply: star_hom => x y. exact: step_abs. Qed.

Lemma red_tapp {m n} A (s1 s2 : tm m n) :
  red s1 s2 -> red (Tm.App s1 A) (Tm.App s2 A).
Proof. apply: (star_hom (@Tm.App m n^~A)) => x y. exact: step_tapp. Qed.

Lemma red_tabs {m n} (s1 s2 : tm m .+1 n) :
  red s1 s2 -> red (Tm.Lam s1) (Tm.Lam s2).
Proof. apply: star_hom => x y. exact: step_tabs. Qed.

Lemma red_inst {m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau : fin n1 -> tm m2 n2) s t :
  red s t -> red s .[sigma ,tau ]%tm t .[sigma ,tau ]%tm.
Proof. apply: star_hom => x y. exact: step_inst. Qed.

Hint Resolve red_app red_abs red_tapp red_tabs : red_congr.

Lemma red_compat {m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau1 tau2 : fin n1 -> tm m2 n2) s :
  sred tau1 tau2 -> red s .[sigma ,tau1 ]%tm s .[sigma ,tau2 ]%tm.
Proof.
  elim: s m2 n2 sigma tau1 tau2; intros; asimpl; eauto with red_congr.
  - apply: red_abs. apply: H. hnf=>/=-[i|]//=. asimpl. rewrite Tm.embed [(_ ◁ (_,_))%tm]Tm.embed.
    apply: red_inst. exact: H0.
  - apply: red_tabs. apply: H. hnf=>/=i. asimpl. rewrite Tm.embed [(_ ◁ (_,_))%tm]Tm.embed.
    apply: red_inst. exact: H0.
  - exact: starR.
Qed.

Lemma red_beta {m n} s (t1 t2 : tm m n) :
  step t1 t2 -> red s .[Ty.var , t1 .: Tm.var ]%tm s .[Ty.var , t2 .: Tm.var ]%tm.
Proof. move=> h. apply: red_compat => /=-[i|]/=; [exact: starR|exact: star1]. Qed.

Syntactic typing

Definition ctx m n := fin n -> ty m.

Inductive has_type {m n} (Gamma : ctx m n) : tm m n -> ty m -> Prop :=
| ty_var (x : fin n) :
    has_type Gamma (Tm.var x) (Gamma x)
| ty_abs (A B : ty m) (s : tm m n.+1) :
    @has_type m n.+1 (A .: Gamma) s B ->
    has_type Gamma (Tm.lam A s) (Ty.arr A B)
| ty_app (A B : ty m) (s t : tm m n) :
    has_type Gamma s (Ty.arr A B) ->
    has_type Gamma t A ->
    has_type Gamma (Tm.app s t) B
| ty_tabs (A : ty m.+1) (s : tm m.+1 n) :
    @has_type m.+1 n (Gamma >> Ty.ren shift) s A ->
    has_type Gamma (Tm.Lam s) (Ty.all A)
| ty_tapp (A : ty m.+1) (B : ty m) (s : tm m n) :
    has_type Gamma s (Ty.all A) ->
    has_type Gamma (Tm.App s B) A .[B .: Ty.var ]%ty.

Strong Normalization

Definition and proof of closedness / compatibility with instantiation.

Notation sn := (sn (@step _ _)).

Lemma sn_closed {m n} (t s : tm m n) :
sn (Tm.app s t) -> sn s.
Proof. apply: (sn_preimage (h := @Tm.app m n^~t)) => x y. exact: step_appL. Qed.

Lemma sn_tclosed {m n} A (s : tm m n) : sn (Tm.App s A) -> sn s.
Proof. apply: (sn_preimage (h := @Tm.App m n^~A)) => x y. exact: step_tapp. Qed.

Lemma sn_inst {m1 m2 n1 n2} (sigma : fin m1 -> ty m2) (tau : fin n1 -> tm m2 n2) s :
sn s .[sigma ,tau ]%tm -> sn s.
Proof. apply: sn_preimage. exact: step_inst. Qed.

The Reducibility Candidates/Logical Predicate

Definition cand m n := tm m n -> Prop.

Neutral (Definition 10.1)

Definition neutral {m n} (s : tm m n) : bool :=
  match s with
    | Tm.lam _ _ | Tm.Lam _ => false
    | _ => true
  end.

Reducibility candidates (Definition 10.2)

Record reducible {m n} (P : cand m n) : Prop := {
  p_sn : forall s, P s -> sn s;
  p_cl : forall s t, P s -> step s t -> P t;
  p_nc : forall s, neutral s -> (forall t, step s t -> P t ) -> P s
}.

Definition admissibility.

Definition admissible {m n k} (rho : fin m -> cand n k) :=
forall i, reducible (rho i).

S-traversal (Definition 10.3) and S evaluation.

Definition S {m n} : Ty.smodel (cand m n) (cand m n).
Proof.
  apply: Ty.SModel.
  - exact id.
  - intros P Q f. refine (forall s, P s -> Q (Tm.app f s)).
  - intros F f. refine (forall P B, reducible P -> F P (Tm.App f B)).
Defined.
Notation E := (Ty.seval S).

Facts about reducible sets.

Lemma reducible_sn {m n} : reducible (sn : tm m n -> Prop).
Proof. constructor; eauto using ARS.sn. by move=> s t [sigma] /sigma. Qed.
Hint Resolve @reducible_sn.

Lemma reducible_const {m n} (P : cand m n) : reducible P -> P (Tm.const m n).
Proof. move/p_nc. apply=> // t st. by inversion st. Qed.

Lemma ad_cons {m n k} (P : cand n k) (rho : fin m -> cand n k) :
reducible P -> admissible rho -> admissible (P .: rho).
Proof. by move=> H1 H2 [i|] //=. Qed.

Lemma 10.4 and consequences.

Lemma L_reducible {m n k} (A : ty m) (rho : fin m -> cand n k) :
  admissible rho -> reducible (E rho A).
Proof with eauto using @step.
  elim: A n k rho => /={m}[m i|m A ih1 B ih2|m A ih] n k rho safe.
  - exact: safe.
  - constructor.
    + move=> s. asimpl=> h. apply (@sn_closed n k (Tm.const n k)).
      apply: (p_sn (P := E rho B))... apply: h. apply: reducible_const...
    + move=> s t h st u la. apply: (p_cl _ (s := Tm.app s u))...
    + move=> s ns. asimpl=> h t la. have snt := p_sn (ih1 _ _ _ safe) la.
      elim: snt la => {t} t _ ih3 la. apply: p_nc...
      move=> v st; inversion st; clear st; subst=>//...
      apply: ih3 => //. exact: (p_cl (ih1 _ _ _ safe)) la _.
  - cbn. constructor.
    + move=> s /(_ sn (Ty.all (Ty.var bound)) reducible_sn)/p_sn/sn_tclosed; apply.
      by apply/ih/ad_cons...
    + move=> s t h st P B rep. apply: p_cl (step_tapp B st)...
      by apply/ih/ad_cons.
    + move=> s ns h P B rep. apply ih... exact: ad_cons.
      move=> t st. inversion st; clear st; subst=> //. exact: h.
Qed.

Corollary L_sn {m n k} A (rho : fin m -> cand n k) s :
  admissible rho -> E rho A s -> sn s.
Proof. move/L_reducible/p_sn. apply. Qed.

Corollary L_cl {m n k} T (rho : fin m -> cand n k) s t :
  admissible rho -> E rho T s -> step s t -> E rho T t.
Proof. move/L_reducible/p_cl. apply. Qed.

Corollary L_nc {m n k} T (rho : fin m -> cand n k) s :
  admissible rho -> neutral s -> (forall t, step s t -> E rho T t ) -> E rho T s.
Proof. move/L_reducible/p_nc. apply. Qed.

Corollary L_var {m n k} T (rho : fin m -> cand n k) x :
  admissible rho -> E rho T (Tm.var x).
Proof. move/L_nc. apply=> // t st. by inversion st. Qed.

Corollary L_const {m n k} T (rho : fin m -> cand n k) :
  admissible rho -> E rho T (Tm.const n k).
Proof. move/L_nc. apply=> // t st. by inversion st. Qed.

Corollary L_cl_star {m n k} T (rho : fin m -> cand n k) s t :
  admissible rho -> E rho T s -> red s t -> E rho T t.
Proof. move=> /L_cl cl H st. elim: st H; eauto. Qed.

Semantic typing (Definition 10.5)

Definition tm_sty {m n} (Gamma : fin n -> ty m) (s : tm m n) (A : ty m) : Prop :=
forall k1 k2 (rho : fin m -> cand k1 k2) theta sigma,
admissible rho -> (forall i, E rho (Gamma i) (sigma i)) -> E rho A s .[theta ,sigma ]%tm.

The fundamental theorem

Closure under beta expansion and Beta expansion. Special cases for the fundamental theorem.

Ltac inv H := inversion H; clear H; subst.

Lemma beta_expansion {m n k} A B (rho : fin m -> cand n k) s t :
  admissible rho -> sn t -> E rho A s .[Ty.var , t .: Tm.var ]%tm ->
  E rho A (Tm.app (Tm.lam B s) t).
Proof with eauto.
  move=> ad snt h. have sns := sn_inst (L_sn ad h).
  elim: sns t snt h => {s} s sns ih1 t. elim=> {t} t snt ih2 h.
  apply: L_nc => // u st. inv st => //.
  - inv H2. apply: ih1 => //. apply: L_cl ad h _. exact: step_inst.
  - apply: ih2 => //. apply: L_cl_star ad h _. exact: red_beta.
Qed.

Lemma inst_expansion {m n k} A B (rho : fin m -> cand n k) s :
  admissible rho -> E rho A s .[B .: Ty.var , Tm.var ]%tm ->
  E rho A (Tm.App (Tm.Lam s) B).
Proof.
  move=> ad h. have sns := sn_inst (L_sn ad h). elim: sns h.
  move=> {s} s _ ih h. apply: L_nc => // t st. inv st => //.
  inv H2 => //. apply: ih => //. apply: L_cl ad h _. exact: step_inst.
Qed.

The fundamental theorem (Theorem 10.6).

Syntactic typing implies semantic typing.

Theorem soundness {m n} (Gamma : fin n -> ty m) s A :
  has_type Gamma s A -> tm_sty Gamma s A.
Proof with eauto using L_sn, ad_cons.
  elim=> {Gamma s A m n}[m n|m n Gamma A B s _ ih|m n Gamma A B s t _ ih1 _ ih2|m n Gamma A s _ ih|m n Gamma A B s _ /=ih]
    k1 k2 rho theta sigma ad el; asimpl...
  - move=> t h. apply: beta_expansion... asimpl. apply: ih... by case.
  - move: ih1. asimpl. apply=>//. exact: ih2.
  - move=> P B h. apply: inst_expansion... asimpl. apply: ih... move=> x.
    asimpl. exact: el.
  - apply: ih... apply: L_reducible...
Qed.

Strong normalisation

Lemma rho_id {m n k} : admissible (fun _ : fin m => sn : tm n k -> Prop).
Proof. move=> x /=. exact: reducible_sn. Qed.

Corollary type_E {m n} Gamma (s : tm m n) A (rho : fin m -> cand m n) :
  has_type Gamma s A -> admissible rho -> E rho A s.
Proof.
  move=> ty ad. move: (@soundness _ _ Gamma s A ty _ _ rho) => h.
  specialize (h Ty.var Tm.var ad). move: h. asimpl. apply=> x /=. exact: L_var.
Qed.

Corollary 10.7

Corollary strong_normalisation {m n} E (s : tm m n) A :
has_type E s A -> sn s.
Proof. move=>/type_E/(_ rho_id)/L_sn. apply. exact: rho_id. Qed.