Ssr.SystemF_SN

Strong Normalization of System F


Require Import mathcomp.ssreflect.ssreflect.
From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq.
Require Import AutosubstSsr ARS Context.

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Definitions


Inductive type : Type :=
| TyVar (x : var)
| Arr (A B : type)
| All (A : {bind type}).

Inductive term :=
| TeVar (x : var)
| Abs (A : type) (s : {bind term})
| App (s t : term)
| TAbs (s : {bind type in term})
| TApp (s : term) (A : type).

Substitution Lemmas


Instance Ids_type : Ids type. derive. Defined.
Instance Rename_type : Rename type. derive. Defined.
Instance Subst_type : Subst type. derive. Defined.

Instance SubstLemmas_type : SubstLemmas type. derive. Qed.

Instance HSubst_term : HSubst type term. derive. Defined.

Instance Ids_term : Ids term. derive. Defined.
Instance Rename_term : Rename term. derive. Defined.
Instance Subst_term : Subst term. derive. Defined.

Instance HSubstLemmas_term : HSubstLemmas type term. derive. Qed.
Instance SubstHSubstComp_type_term : SubstHSubstComp type term. derive. Qed.

Instance SubstLemmas_term : SubstLemmas term. derive. Qed.

One-Step Reduction


Inductive step : term -> term -> Prop :=
| step_beta (A : type) (s t : term) :
    step (App (Abs A s) t) s.[t/]
| step_inst (A : type) (s : term) :
    step (TApp (TAbs s) A) s.|[A/]
| step_appL s1 s2 t :
    step s1 s2 -> step (App s1 t) (App s2 t)
| step_appR s t1 t2 :
    step t1 t2 -> step (App s t1) (App s t2)
| step_abs A s1 s2 :
    step s1 s2 -> step (Abs A s1) (Abs A s2)
| step_tapp A s1 s2 :
    step s1 s2 -> step (TApp s1 A) (TApp s2 A)
| step_tabs s1 s2 :
    step s1 s2 -> step (TAbs s1) (TAbs s2).

Lemma step_ebeta A s t u : u = s.[t/] -> step (App (Abs A s) t) u.
Proof. move->. exact: step_beta. Qed.

Lemma step_einst A s t : t = s.|[A/] -> step (TApp (TAbs s) A) t.
Proof. move->. exact: step_inst. Qed.

Lemma step_substf theta sigma s t :
  step s t -> step s.|[theta].[sigma] t.|[theta].[sigma].
Proof.
  move=> st. elim: st sigma theta => {s t}; asimpl; eauto using step.
  - move=> A s t sigma theta. apply: step_ebeta. by autosubst.
  - move=> A s sigma theta. apply: step_einst. by autosubst.
Qed.

Lemma step_subst sigma s t : step s t -> step s.[sigma] t.[sigma].
Proof. move=> h. apply (step_substf ids sigma) in h. by asimpl in h. Qed.

Lemma step_hsubst theta s t : step s t -> step s.|[theta] t.|[theta].
Proof. move=> h. apply (step_substf theta ids) in h. by asimpl in h. Qed.

Many-Step Reduction


Definition red := star step.

Definition sred sigma tau :=
  forall x : var, red (sigma x) (tau x).

Lemma red_app s1 s2 t1 t2 :
  red s1 s2 -> red t1 t2 -> red (App s1 t1) (App s2 t2).
Proof.
  move=> A B. apply: (star_trans (App s2 t1)).
  - apply: (star_hom (App^~ t1)) A => x y. exact: step_appL.
  - apply: star_hom B => x y. exact: step_appR.
Qed.

Lemma red_abs A s1 s2 : red s1 s2 -> red (Abs A s1) (Abs A s2).
Proof. apply: star_hom => x y. exact: step_abs. Qed.

Lemma red_tapp A s1 s2 : red s1 s2 -> red (TApp s1 A) (TApp s2 A).
Proof. apply: (star_hom (TApp^~A)) => x y. exact: step_tapp. Qed.

Lemma red_tabs s1 s2 : red s1 s2 -> red (TAbs s1) (TAbs s2).
Proof. apply: star_hom => x y. exact: step_tabs. Qed.

Lemma red_subst sigma s t : red s t -> red s.[sigma] t.[sigma].
Proof. apply: star_hom => x y. exact: step_subst. Qed.

Lemma red_hsubst theta s t : red s t -> red s.|[theta] t.|[theta].
Proof. apply: star_hom => x y. exact: step_hsubst. Qed.

Lemma sred_up sigma tau : sred sigma tau -> sred (up sigma) (up tau).
Proof. move=> A [|n] //=. asimpl. apply/red_subst/A. Qed.

Lemma sred_hup sigma tau theta :
  sred sigma tau -> sred (sigma >>| theta) (tau >>| theta).
Proof. move=> A n /=. apply/red_hsubst/A. Qed.

Hint Resolve red_app red_abs red_tapp red_tabs sred_up sred_hup : red_congr.

Lemma red_compat sigma tau s :
  sred sigma tau -> red s.[sigma] s.[tau].
Proof.
  elim: s sigma tau; intros; asimpl; eauto with red_congr.
Qed.

Lemma red_beta s t1 t2 : step t1 t2 -> red s.[t1/] s.[t2/].
Proof. move=> h. apply: red_compat => -[|n]/=; [exact: star1|exact: starR]. Qed.

Syntactic typing


Definition ctx := seq type.
Local Notation "Gamma `_ i" := (get Gamma i).

Inductive has_type (Gamma : ctx) : term -> type -> Prop :=
| ty_var (x : var) :
    x < size Gamma -> has_type Gamma (TeVar x) Gamma`_x
| ty_abs (A B : type) (s : term) :
    has_type (A :: Gamma) s B ->
    has_type Gamma (Abs A s) (Arr A B)
| ty_app (A B : type) (s t : term) :
    has_type Gamma s (Arr A B) ->
    has_type Gamma t A ->
    has_type Gamma (App s t) B
| ty_tabs (A : type) (s : term) :
    has_type Gamma..[ren (+1)] s A ->
    has_type Gamma (TAbs s) (All A)
| ty_tapp (A B : type) (s : term) :
    has_type Gamma s (All A) ->
    has_type Gamma (TApp s B) A.[B/].

(* Strong Normalization *)

Notation sn := (sn step).

Lemma sn_closed t s : sn (App s t) -> sn s.
Proof. apply: (sn_preimage (h := App^~t)) => x y. exact: step_appL. Qed.

Lemma sn_tclosed A s : sn (TApp s A) -> sn s.
Proof. apply: (sn_preimage (h := TApp^~A)) => x y. exact: step_tapp. Qed.

Lemma sn_subst sigma s : sn s.[sigma] -> sn s.
Proof. apply: sn_preimage => x y. exact: step_subst. Qed.

Lemma sn_hsubst theta s : sn s.|[theta] -> sn s.
Proof. apply: sn_preimage => x y. exact: step_hsubst. Qed.

(* The Reducibility Candidates/Logical Predicate*)

Definition cand := term -> Prop.

Definition neutral (s : term) : bool :=
  match s with
    | Abs _ _ | TAbs _ => false
    | _ => true
  end.

Record reducible (P : cand) : 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
}.

Fixpoint L (T : type) (rho : nat -> cand) : cand :=
  match T with
    | TyVar x => rho x
    | Arr A B => fun s => forall t, L A rho t -> L B rho (App s t)
    | All A => fun s => forall P B, reducible P -> L A (P .: rho) (TApp s B)
  end.

Definition EL E (rho : nat -> cand) (sigma : var -> term) : Prop :=
  forall x, x < size E -> L E`_x rho (sigma x).

Definition admissible (rho : nat -> cand) :=
  forall x, reducible (rho x).

(* Facts about reducible sets. *)

Lemma reducible_sn : reducible sn.
Proof. constructor; eauto using ARS.sn. by move=> s t [f] /f. Qed.
Hint Resolve reducible_sn.

Lemma reducible_var P x : reducible P -> P (TeVar x).
Proof. move/p_nc. apply=> // t st. inv st. Qed.

Lemma ad_cons P rho :
  reducible P -> admissible rho -> admissible (P .: rho).
Proof. by move=> H1 H2 [|i] //=. Qed.

Lemma L_reducible T rho :
  admissible rho -> reducible (L T rho).
Proof with eauto using step.
  elim: T rho => /=[i|A ih1 B ih2|A ih] rho safe...
  - constructor.
    + move=> s h. apply: (@sn_closed (TeVar 0)). apply: (p_sn (P := L B rho))...
      eapply h. eapply reducible_var; eauto.
    + move=> s t h st u la. apply: (p_cl _ (s := App s u))...
    + move=> s ns h t la. have snt := p_sn (ih1 _ safe) la.
      elim: snt la => {t} t _ ih3 la. apply: p_nc... move=> v st. inv st=> //...
      apply: ih3 => //. exact: (p_cl (ih1 _ safe)) la _.
  - constructor.
    + move=> s /(_ sn (TyVar 0) 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. inv st => //...
Qed.

Corollary L_sn A rho s : admissible rho -> L A rho s -> sn s.
Proof. move=> /L_reducible/p_sn. apply. Qed.

Corollary L_cl T rho s t : admissible rho -> L T rho s -> step s t -> L T rho t.
Proof. move=> /L_reducible/p_cl. apply. Qed.

Corollary L_nc T rho s :
  admissible rho -> neutral s -> (forall t, step s t -> L T rho t) -> L T rho s.
Proof. move=> /L_reducible/p_nc. apply. Qed.

Corollary L_var T rho x : admissible rho -> L T rho (TeVar x).
Proof. move=> /L_nc. apply=> // t st. inv st. Qed.

Corollary L_cl_star T rho s t :
  admissible rho -> L T rho s -> red s t -> L T rho t.
Proof. move=> /L_cl cl H st. elim: st H; eauto. Qed.

(* Closure under beta expansion. *)

Lemma beta_expansion A B rho s t :
  admissible rho -> sn t -> L A rho s.[t/] ->
  L A rho (App (Abs B s) t).
Proof with eauto.
  move=> ad snt h. have sns := sn_subst (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_subst.
  - apply: ih2 => //. apply: L_cl_star ad h _. exact: red_beta.
Qed.

Lemma inst_expansion A B rho s :
  admissible rho -> L A rho s.|[B/] -> L A rho (TApp (TAbs s) B).
Proof.
  move=> ad h. have sns := sn_hsubst (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_hsubst.
Qed.

(* The type substitution lemma. *)

Lemma extend_ext (rho tau : nat -> cand) :
  (forall i s, rho i s <-> tau i s) ->
  (forall P i s, (P .: rho) i s <-> (P .: tau) i s).
Proof. by move=>h P[]/=. Qed.

Lemma L_ext T rho tau :
  (forall i s, rho i s <-> tau i s) -> (forall s, L T rho s <-> L T tau s).
Proof.
  elim: T rho tau => //=[T1 IH1 T2 IH2|T IH] rho tau E s.
  - split=> H1 t H2.
    + rewrite -(IH2 _ _ E). apply: H1. by rewrite (IH1 _ _ E).
    + rewrite (IH2 _ _ E). apply: H1. by rewrite -(IH1 _ _ E).
  - move: E => /extend_ext E. split=> H P B /H.
    + move=> /(_ B). by rewrite (IH _ _ (E P)).
    + move=> /(_ B). by rewrite -(IH _ _ (E P)).
Qed.

Lemma L_ren A rho xi s :
  L A.[ren xi] rho s <-> L A (xi >>> rho) s.
Proof with intuition.
  elim: A rho xi s => [x|A ih1 B ih2|A ih] rho xi s; asimpl => //.
  - split=> h1 t h2. rewrite -ih2. apply: h1. by rewrite ih1.
    rewrite ih2. apply: h1. by rewrite -ih1.
  - split=> h P B r. move: (h _ B r). rewrite ih. apply L_ext. by case.
    rewrite ih. asimpl. exact: h.
Qed.

Lemma L_weaken A P rho s : L A.[ren (+1)] (P .: rho) s <-> L A rho s.
Proof. exact: L_ren. Qed.

Lemma L_subst A rho sigma s :
  L A.[sigma] rho s <-> L A (fun i => L (sigma i) rho) s.
Proof.
  elim: A rho sigma s => [x|A ih1 B ih2|A ih] rho sigma s; asimpl=>//.
  - split=> h1 t h2. rewrite -ih2. apply: h1. by rewrite ih1.
    rewrite ih2. apply h1. by rewrite -ih1.
  - split=> h P B /(h _ B); rewrite ih; apply L_ext => -[|x] //= t; asimpl;
    by rewrite L_weaken.
Qed.

(* The fundamental theorem. *)

Theorem soundness Gamma s A :
  has_type Gamma s A -> forall rho theta sigma,
    admissible rho -> EL Gamma rho sigma -> L A rho s.|[theta].[sigma].
Proof with eauto using L_sn, ad_cons.
  elim=> {Gamma s A} [|Gamma A B s _ ih||Gamma A s _ ih|Gamma A B s _ /=ih]
    rho theta sigma ad el; asimpl...
  - move=> t h. apply: beta_expansion... asimpl. apply: ih... by case.
  - move=> P B h. apply: inst_expansion... asimpl. apply: ih... move=> x.
    rewrite size_map => lt. rewrite get_map // L_weaken...
  - rewrite L_subst. specialize (ih _ theta sigma ad el (L B rho) B.[theta]).
    have/ih: reducible (L B rho). exact: L_reducible. apply L_ext. by case.
Qed.

Lemma rho_id : admissible (fun _ => sn).
Proof. move=> x /=. exact: reducible_sn. Qed.

Corollary type_L E s T rho : has_type E s T -> admissible rho -> L T rho s.
Proof.
  move=> ty ad. move: (@soundness E s T ty rho) => h.
  specialize (h ids ids ad). asimpl in h. apply: h => x B. exact: L_var.
Qed.

Corollary strong_normalization E s T : has_type E s T -> sn s.
Proof. move=>/type_L/(_ rho_id)/L_sn. apply. exact: rho_id. Qed.

(* Local Variables: *)
(* coq-load-path: (("." "Ssr")) *)
(* End: *)