Recipes_neutralization.Recipes

Set Warnings "-notation-overridden, -notation-overriden".
From mathcomp Require Import ssreflect ssrbool eqtype ssrnat seq zify.
From Coq Require Import ssrfun PeanoNat Lia Arith_base.
Set Warnings "notation-overridden, notation-overriden".

Require Import AutosubstSsr ARS.

Create HintDb red_congr.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

AST

Section AST.

Inductive term : Type :=
  | TVar (x : var)
  | TNat (n : nat)
  | TCons (S T : term).

Inductive fmla : Type :=
  | FEqu (S T : term)
  | FAll (f : {bind term in fmla})
  | FNot (f : fmla)
  | FAnd (f g : fmla)
  | FOr (f g : fmla).

  (* | FApp (n : nat) (ts : list term). *)

Inductive type : Type :=
  | Void
  | Arr (U : type) (V : type)
  | TArr (V : type).

Inductive recipe : Type :=
  | Top
  | Var (h : var)
  | App (s t : recipe)
  | And (s t : recipe)
  | TApp (s : recipe) (S : term)
  | Imp (f : fmla) (t : recipe)
  | Lam (U : type) (s : {bind 2 of recipe})
  | TLam (s : {bind term in recipe})
  | TAll (s : {bind term in recipe}).

The idea is to bind pairs of recipe variable at every Lam. When there is an application, App ((Lam U s) t) reduces to s.[t, (neu t)/]. Thus, every even index is the recipe and the odd following is its neutralization. Then, we can define neutralization as s substitution 2n -> 2n+1.

End AST.

Decidability lemmas
Section EqDec.

Lemma var_eq_dec (v1 v2 : var) : {v1 = v2} + {v1 <> v2}.
Proof.
  by decide equality.
Qed.

Lemma term_eq_dec (t1 t2 : term) : {t1 = t2} + {t1 <> t2}.
Proof.
  decide equality.
  exact: var_eq_dec.
  by decide equality.
Qed.

Lemma fmla_eq_dec (f1 f2 : fmla) : {f1 = f2} + {f1 <> f2}.
Proof.
  decide equality.
  exact: term_eq_dec.
  exact: term_eq_dec.
Qed.

Lemma type_eq_dec (t1 t2 : type) : {t1 = t2} + {t1 <> t2}.
Proof.
  by decide equality.
Qed.

Lemma recipe_eq_dec (s t : recipe) : {s = t} + {s <> t}.
Proof.
  decide equality.
  exact: var_eq_dec.
  exact: term_eq_dec.
  exact: fmla_eq_dec.
  exact: type_eq_dec.
Qed.

End EqDec.

Type classes instanciations
Term
Global Instance Ids_term : Ids term. derive. Defined.
Global Instance Rename_term : Rename term. derive. Defined.
Global Instance Subst_term : Subst term. derive. Defined.

Global Instance SubstLemmas_term : SubstLemmas term. derive. Qed.
Global Instance HSubst_t_fmla : HSubst term fmla. derive. Defined.
Global Instance HSubst_t_reci : HSubst term recipe. derive. Defined.

Formula
Global Instance Rename_flma : Rename fmla. derive. Defined.
Global Instance Subst_fmla : Subst fmla. derive. Defined.

Recipe
Global Instance Ids_reci : Ids recipe. derive. Defined.
Global Instance Rename_reci : Rename recipe. derive. Defined.
Global Instance Subst_reci : Subst recipe. derive. Defined.

Global Instance HSubstLemmas_term_reci : HSubstLemmas term recipe. derive. Qed.

Global Instance HSubst_reci_term : HSubst recipe term. derive. Defined.

Global Instance HSubstLemmas_reci_term : HSubstLemmas recipe term. derive. Qed.
Global Instance SubstHSubstComp_reci_term : SubstHSubstComp recipe term. derive. Qed.
Global Instance SubstHSubstComp_term_reci : SubstHSubstComp term recipe. derive. Qed.
Global Instance SubstLemmas_reci : SubstLemmas recipe. derive. Qed.

End AutosubstTypeClasses.

Section SubstLemmasP.

Lemma upnPh n σ h :
  upn n σ h =
    if h < n then TVar h else (σ (h - n)).[ren (+n)].
Proof.
  case: ifPn.
  - elim: h n =>[|h ih][|n]//=/ih e. rewrite iterate_S. asimpl. by rewrite e.
  - rewrite -leqNgt. elim: h n => [|h ih][|n]; try autosubst. by case: n.
    move=>/ih e. rewrite iterate_S. asimpl. rewrite e. autosubst.
Qed.

Lemma upnP n σ h :
  upn n σ h =
    if h < n then Var h else (σ (h - n)).[ren (+n)].
Proof.
  case: ifPn.
  - elim: h n =>[|h ih][|n]//=/ih e. rewrite iterate_S. asimpl. by rewrite e.
  - rewrite -leqNgt. elim: h n => [|h ih][|n]; try autosubst. by case: n.
    move=>/ih e. rewrite iterate_S. asimpl. rewrite e. autosubst.
Qed.

Lemma upnP_cond n σ h :
  h >= n ->
  upn n σ h = (σ (h - n)).[ren (+n)].
Proof.
  move=>H.
  by rewrite upnP ifF; [reflexivity|lia].
Qed.

Lemma upn2P n σ h :
  upn n σ h =
    if h < n then Var h else upn n σ h.
Proof.
  case: ifPn; rewrite upnP; case: ifPn => //=.
Qed.

End SubstLemmasP.

Neutralization definition

Section Neutralization.

Definition ns (n : var) : var := if odd n then n else n.+1.
Definition sneu : var -> recipe := ren ns.
Definition neu (s : recipe) : recipe := s.[sneu].

A substitution is admissible iff Var (2.*n.+1) is the neutralization of Var (2.*n)
Definition admissible_subst (σ: var -> recipe) : Prop :=
  forall n, (odd n.+1) -> σ n.+1 = neu (σ n).

(* equivalent definition and proof, but useless ? *)
Definition admissible_subst2 (σ: var -> recipe) : Prop :=
  forall n, neu (σ n.*2) = σ n.*2.+1.

Lemma admissible_subst_rw : forall σ, admissible_subst σ <-> admissible_subst2 σ.
Proof.
  rewrite /admissible_subst /admissible_subst2.
  split => H n.
  { have H2: (odd n.*2.+1) by rewrite oddS; apply/negbT/odd_double.
    by rewrite (H _ H2). }
  { move=> ?.
    have H2: ~~ (odd n) by rewrite -oddS.
    by rewrite -(even_halfK H2) H. }
Qed.

Lemma sn_eq_nsn_if_odd n : odd n.+1 -> n.+1 = ns n.
Proof.
  rewrite oddS => H.
  by rewrite /ns ifN.
Qed.

Lemma admissible_neu : admissible_subst sneu.
Proof.
  move=> n H.
  by rewrite sn_eq_nsn_if_odd.
Qed.

Lemma admissible_ids : admissible_subst ids.
Proof.
  move=> n H.
  by rewrite sn_eq_nsn_if_odd.
Qed.

Lemma admissible_subst_ext t σ : admissible_subst σ -> admissible_subst (t .: neu t .: σ).
Proof.
  move=> h.
  rewrite /admissible_subst => []/=[]//= n hn.
  have {}hn: odd n by lia.
  have {}hn2: n <> 0 by lia.
  have->: (neu t .: σ) n = σ n.-1 by destruct n.
  specialize (h n.-1).
  rewrite -h.
  by have->: n.-1.+1 = n by lia.
  by have->: n.-1.+1 = n by lia.
Qed.

Corollary admissible_subst_var01 s : admissible_subst (s .: neu s .: ids).
Proof.
  apply admissible_subst_ext.
  exact admissible_ids.
Qed.

Lemma neu_idempotent s : neu s = neu (neu s).
Proof.
  rewrite /neu /sneu /ns.
  asimpl.
  unfold ">>>".
  do! f_equal; f_ext.
  move=> x.
  case: ifPn => H.
    by rewrite ifT.
  by rewrite oddS ifT.
Qed.

Lemma neu_idempotent_upn s n : neu s = (neu s).[upn n.*2 sneu].
Proof.
  rewrite /neu /sneu /ns.
  asimpl.
  unfold ">>>".
  do! f_equal; f_ext.
    asimpl.
  move=> x.
  case: ifPn => H.
    rewrite upnP.
    case: ifPn => H1 //=.
    rewrite ifT; last by lia.
    have H2: x >= n.*2 by lia.
    by have->: (n.*2 + (x - n.*2))%coq_nat = x by lia.
  rewrite upnP.
  case: ifPn => H1 //=.
  rewrite ifT; last by lia.
  have H2: x.+1 >= n.*2 by lia.
  by have->: (n.*2 + (x.+1 - n.*2))%coq_nat = x.+1 by lia.
Qed.

Lemma admissible_subst_up2 σ :
  admissible_subst σ -> admissible_subst (upn 2 σ).
Proof.
  move=> H.
  rewrite /admissible_subst.
  do 2 (case; first by simpl).
  move=> n Hn.
  asimpl.
  rewrite H /neu; last by lia.
  asimpl.
  f_equal.
  unfold ">>", ">>>".
  f_ext => x.
  rewrite /sneu /ns.
  asimpl.
  by case: ifPn; simpl.
Qed.

Lemma admissible_hsubst σ θ :
  admissible_subst σ -> admissible_subst (σ >>| θ).
Proof.
  rewrite /admissible_subst => H n Hn.
  asimpl.
  rewrite H /neu; last by assumption.
  have->: (σ n).[sneu].|[θ] = (σ n).|[θ].[sneu >>| θ] by autosubst.
  by f_equal.
Qed.

Lemma neutralize_comm_subst s σ θ τ m :
  admissible_subst σ ->
  s.|[θ].[upn m.*2 σ >>| τ].[upn m.*2 sneu >>| τ] =
  s.[upn m.*2 sneu >>| τ].|[θ].[upn m.*2 σ >>| τ].
Proof.
  elim: s σ θ τ m => //.
  { move=> /= h σ θ τ m H.
    rewrite !upnP.
    case: ifPn => [lt| /ltP/not_lt/leP ge].
    + asimpl. by rewrite !upnP !ifT.
    + set g := (h - m.*2).
      case: (boolP (odd g)) => [Hodd|Heven].
      { have->: sneu g = Var g
           by rewrite /sneu /ns /= ifT.
        asimpl.
        have->: (upn m.*2 σ (m.*2 + g)) = ((σ ((m.*2 + g) - m.*2)).[ren (+m.*2)])
          by rewrite upnP ifF; [reflexivity|lia].
        have->: m.*2 + g - m.*2 = g by lia.
        asimpl.
        have->: subst (ren (+m.*2)) = subst ((+m.*2) >>> ids) by autosubst.
        have gpos: 0 < g by apply odd_gt0.
        rewrite /admissible_subst in H.
        move: (H g.-1).
        have->: (g.-1.+1 = g) by apply Nat.succ_pred; lia.
        move=> H1; move: (H1 Hodd) => {H1} ->.
        have->: (neug.-1)).|[τ].[(+m.*2) >>> ids] =
                (neug.-1)).[(+m.*2) >>> ids].|[τ]
                by autosubst.
        have->: (neug.-1)).|[τ].[(+m.*2) >>> upn m.*2 sneu >>| τ] =
                (neug.-1)).[(+m.*2) >>> upn m.*2 sneu].|[τ] by autosubst.
        f_equal.
        have->: (neug.-1)).[(+m.*2) >>> upn m.*2 sneu] =
                (rename (+m.*2) (neug.-1))).[upn m.*2 sneu] by autosubst.
        have->: (neug.-1)).[(+m.*2) >>> ids] =
                (rename (+m.*2) (neug.-1))) by autosubst.
        have->: rename (+m.*2) (neug.-1)) =
                neu (rename (+m.*2)g.-1)).
          rewrite /neu /sneu /ns.
          asimpl.
          f_equal. f_equal. f_ext=> x.
          simpl.
          case: ifP=>[tt|ff].
          + by rewrite ifT; lia.
          + by rewrite ifN; lia.
        asimpl.
        by rewrite -neu_idempotent_upn. }
      { have->: sneu g = Var g.+1
          by rewrite /sneu /ns /= ifN.
        asimpl.
        rewrite upnP ifF; last by lia.
        have->: ((m.*2 + g).+1 - m.*2) = g.+1 by lia.
        rewrite /admissible_subst in H.
        rewrite -oddS in Heven.
        rewrite (H g Heven).
        have->: (σ g).|[τ].[(+m.*2) >>> upn m.*2 sneu >>| τ] =
                (σ g).[(+m.*2) >>> upn m.*2 sneu].|[τ]
                by autosubst.
        f_equal.
        rewrite /neu.
        asimpl.
        f_equal.
        unfold ">>", ">>>".
        f_ext=> x.
        rewrite upnP ifF /=; last by lia.
        by have->: ((m.*2 + x)%coq_nat - m.*2)%N = x by lia. }
     }
  { move=> /= s H1 t H2 σ θ τ m H.
    move: (H1 σ θ τ m H) (H2 σ θ τ m H) => {}H1 {}H2.
    by rewrite /neu -H1 -H2. }
  { move=> /= s H1 t H2 σ θ τ m H.
    move: (H1 σ θ τ m H) (H2 σ θ τ m H) => {}H1 {}H2.
    by rewrite /neu -H1 -H2. }
  { move=> /= s H1 T σ θ τ m H.
    move: (H1 σ θ τ m H) => {H} H1.
    by rewrite /neu -H1. }
  { move=> /= f s H1 σ θ τ m H.
    move: (H1 σ θ τ m H) => {H} H1.
    by rewrite /neu -H1. }
  { move=> U s H1 σ θ τ m H.
    asimpl.
    f_equal.
    move: (H1 σ θ τ m.+1 H) => {}H1.
    asimpl in *.
    have->: ids 0 .: ids 1 .: upn m.*2 σ >>| τ >> (upn m.*2 sneu >>| τ >> ren (+2)) =
                       upn 2 (upn m.*2 σ >>| τ >> (upn m.*2 sneu >>| τ)) by autosubst.
    have->: ids 0 .: ids 1 .: upn m.*2 sneu >>| (τ >> θ) >> (upn m.*2 σ >>| τ >> ren (+2)) =
                       upn 2 (upn m.*2 sneu >>| (τ >> θ) >> (upn m.*2 σ >>| τ)) by autosubst.
    have lemma: forall x, upn m.+1.*2 x = upn 2 (upn m.*2 x).
      move=> x.
      have->: (m.+1.*2 = m.*2.+2) by lia.
      by asimpl.
    have->: upn 2 (upn m.*2 σ >>| τ >> (upn m.*2 sneu >>| τ)) =
                  (upn m.+1.*2 σ >>| τ >> (upn m.+1.*2 sneu >>| τ))
            by rewrite !lemma; autosubst.
    have->: upn 2 (upn m.*2 sneu >>| (τ >> θ) >> (upn m.*2 σ >>| τ)) =
                  (upn m.+1.*2 sneu >>| (τ >> θ) >> (upn m.+1.*2 σ >>| τ))
            by rewrite !lemma; autosubst.
    done. }
  { move=> s H1 σ θ τ m H /=.
    f_equal.
    pose (H1 σ (up θ) (τ >> ren(+1)) m H).
    asimpl in *.
    exact e. }
  { move=> s H1 σ θ τ m H /=.
    f_equal.
    pose (H1 σ (up θ) (τ >> ren(+1))m H).
    asimpl in *.
    exact e. }
Qed.

Corollary neutralize_comm_subst_corr s θ σ :
  admissible_subst σ -> s.|[θ].[σ].[sneu] = s.[sneu].|[θ].[σ].
Proof.
  move=>?.
  have: s.|[θ].[upn 0.*2 σ >>| ids].[upn 0.*2 sneu >>| ids] =
        s.[upn 0.*2 sneu >>| ids].|[θ].[upn 0.*2 σ >>| ids]
        by apply neutralize_comm_subst.
  autosubst.
Qed.

Corollary neutralize_comm_subst_corr2 s θ σ :
  admissible_subst σ -> neu s.|[θ].[σ] = (neu s).|[θ].[σ].
Proof.
  rewrite /neu.
  by apply neutralize_comm_subst_corr.
Qed.

Corollary neutralize_comm_subst_corr3 s σ :
  admissible_subst σ -> neu s.[σ] = (neu s).[σ].
Proof.
  have{1}->: s = s.|[ids] by autosubst.
  have{1}->: (neu s) = (neu s).|[ids] by autosubst.
  by apply neutralize_comm_subst_corr2.
Qed.

Lemma admissible_compose σ θ :
  admissible_subst σ -> admissible_subst θ -> admissible_subst (σ >> θ).
Proof.
  rewrite/admissible_subst.
  move=> h1 h2 n.
  asimpl=> non.
  have osn: odd n.+1 by lia.
  rewrite (h1 n osn).
  rewrite -neutralize_comm_subst_corr3 /neu.
  by asimpl.
  exact h2.
Qed.

End Neutralization.

Step relations between recipes.

Section Step.

Reserved Notation "s ===> t" (at level 80, no associativity).

Inductive step : recipe -> recipe -> Prop :=

| step_beta s t U : App (Lam U s) t ===> s.[t,neu t/]
| step_tbeta s S : TApp (TLam s) S ===> s.|[S/]

| step_ctx_andl s t u : step s t -> step (And s u) (And t u)
| step_ctx_andr s t u : step s t -> step (And u s) (And u t)
| step_ctx_appl s t u : step s t -> step (App s u) (App t u)
| step_ctx_appr s t u : step s t -> step (App u s) (App u t)
| step_ctx_tapp s t T : step s t -> step (TApp s T) (TApp t T)
| step_ctx_lam s t U : step s t -> step (Lam U s) (Lam U t)
| step_ctx_imp s t f : step s t -> step (Imp f s) (Imp f t)
| step_ctx_tlam s t : step s t -> step (TLam s) (TLam t)
| step_ctx_tall s t : step s t -> step (TAll s) (TAll t)

 where "s ===> t" := (forall u, t = u -> step s u).

Local Hint Constructors step : step.
Local Hint Extern 1 (_ = _) => autosubst : autosubst.

Lemma step_substf θ σ s t :
  step s t -> admissible_subst σ -> step s.|[θ].[σ] t.|[θ].[σ].
Proof.
  move=> st; elim: st σ θ => {s t};
    try (move=> *; subst; asimpl; eauto using step; econstructor; autosubst).
  { move=> ??? u<-{u} *.
    constructor. asimpl. by rewrite neutralize_comm_subst_corr2. }
  { move=> ???? H *.
    constructor.
    by apply/H/admissible_subst_up2. }
  { move=> ??? H *.
    constructor.
    by apply/H/admissible_hsubst. }
  { move=> ??? H *.
    constructor.
    by apply/H/admissible_hsubst. }
Qed.

Corollary neutralize_comm_subst_corr_hsubst s θ :
  neu s.|[θ] = (neu s).|[θ].
Proof.
  have->: s.|[θ] = s.|[θ].[ids] by autosubst.
  have->: (neu s).|[θ] = (neu s).|[θ].[ids] by autosubst.
  pose admissible_ids.
  exact: neutralize_comm_subst_corr.
Qed.

Lemma step_subst σ S T : admissible_subst σ -> step S T -> step S.[σ] T.[σ].
Proof.
  move=> H h.
  apply (@step_substf ids σ) in h; last by assumption.
  by asimpl in h.
Qed.

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

End Step.

Transitive+reflexive closure of step

Section StarStep.

Definition red := star step.

Definition sred σ τ :=
  forall x : var, red (σ x) (τ x).

Lemma red_top : red Top Top.
Proof. exact: starR. Qed.

Lemma red_app s₁ s₂ t₁ t₂ :
  red s₁ s₂ -> red t₁ t₂ -> red (App s₁ t₁) (App s₂ t₂).
Proof.
  move=> s t. apply: (star_trans (App s₂ t₁)).
  - apply: (star_hom (App^~ t₁)) s => x y. exact: step_ctx_appl.
  - apply: star_hom t => x y. exact: step_ctx_appr.
Qed.

Lemma red_and s₁ s₂ t₁ t₂ :
  red s₁ s₂ -> red t₁ t₂ -> red (And s₁ t₁) (And s₂ t₂).
Proof.
  move=> s t. apply: (star_trans (And s₂ t₁)).
  - apply: (star_hom (And^~ t₁)) s => x y. exact: step_ctx_andl.
  - apply: star_hom t => x y. exact: step_ctx_andr.
Qed.

Lemma red_tapp T s t : red s t -> red (TApp s T) (TApp t T).
Proof. apply: (star_hom (TApp^~T)) => x y. exact: step_ctx_tapp. Qed.

Lemma red_imp f s t : red s t -> red (Imp f s) (Imp f t).
Proof. apply: (star_hom (Imp f)) => x y. exact: step_ctx_imp. Qed.

Lemma red_lam s t π : red s t -> red (Lam π s) (Lam π t).
Proof. apply: star_hom => x y. exact: step_ctx_lam. Qed.

Lemma red_tlam s t : red s t -> red (TLam s) (TLam t).
Proof. apply: star_hom => x y. exact: step_ctx_tlam. Qed.

Lemma red_tall s t : red s t -> red (TAll s) (TAll t).
Proof. apply: star_hom => x y. exact: step_ctx_tall. Qed.

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

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

Lemma sred_up σ τ :
  sred σ τ -> sred (upn 2 σ) (upn 2 τ).
Proof.
  move=> s [|h] //.
  move: h => [|h] //.
  asimpl.
  apply/red_subst/s.
  rewrite /admissible_subst /neu /sneu /ns /= => n H.
  by rewrite ifN; [reflexivity|lia].
Qed.

Lemma sred_hup σ τ θ :
  sred σ τ -> sred (σ >>| θ) (τ >>| θ).
Proof. move=> s n /=. apply/red_hsubst/s. Qed.

Local Hint Resolve
  red_top red_app red_and red_tapp red_imp red_lam red_tlam red_tall
  red_subst red_hsubst sred_up sred_hup : red_congr.

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

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

Lemma red_beta01 s t₁ t₂ : step t₁ t₂ -> red s.[t₁, neu t₁/] s.[t₂, neu t₂/].
Proof.
  move=> h.
  apply red_compat => -[|[|n]]/=; [exact: star1| | exact: starR].
  apply red_subst.
    exact admissible_neu.
  exact: star1.
Qed.

The Tait, Martin-Löf, Takahashi confluence proof method.

(“parallel” step relations)
Section ChurchRosser.

Reserved Notation "s ===>> t" (at level 80, no associativity).

Inductive pstep : recipe -> recipe -> Prop :=
(* Identity *)
| pstep_var h : pstep (Var h) (Var h)
| pstep_top : pstep Top Top

(* Beta *)
| pstep_beta s₁ t₁ s₂ t₂ U : pstep s₁ t₁ -> pstep s₂ t₂ -> (App (Lam U s₁) s₂) ===>> t₁.[t₂, neu t₂/]
| pstep_tbeta s t T : pstep s t -> (TApp (TLam s) T) ===>> t.|[T/]

(* Context *)
| pstep_lam s t U : pstep s t -> (Lam U s) ===>> (Lam U t)
| pstep_tlam s t : pstep s t -> (TLam s) ===>> (TLam t)
| pstep_imp s t f : pstep s t -> (Imp f s) ===>> (Imp f t)
| pstep_tall s t : pstep s t -> (TAll s) ===>> (TAll t)
| pstep_tapp s t T : pstep s t -> (TApp s T) ===>> (TApp t T)
| pstep_app s₁ t₁ s₂ t₂ : pstep s₁ t₁ -> pstep s₂ t₂ -> (App s₁ s₂) ===>> (App t₁ t₂)
| pstep_and s₁ t₁ s₂ t₂ : pstep s₁ t₁ -> pstep s₂ t₂ -> (And s₁ s₂) ===>> (And t₁ t₂)

 where "x ===>> y" := (forall u, y = u -> pstep x u).

Definition psstep (σ τ : var -> recipe) :=
  forall x, pstep (σ x) (τ x).

Lemma pstep_refl s : pstep s s.
Proof. elim: s; eauto using pstep. Qed.
Hint Resolve pstep_refl : core.

Lemma step_pstep s t : step s t -> pstep s t.
Proof. elim; eauto using pstep. Qed.

Lemma pstep_red s t : pstep s t -> red s t.
Proof with eauto using step with red_congr.
  elim=> {s t} //=; intros ; subst ; try apply starR...
  { apply (star_trans (App (Lam U t₁) s₂)).
      apply/red_app... done.
    apply (star_trans (App (Lam U t₁) t₂)).
      by apply/red_app.
    apply star1... }
  { apply (star_trans (TApp (TLam t) T)).
      apply red_tapp...
    apply star1... }
Qed.

Lemma pstep_substf :
  forall s t, pstep s t ->
    forall σ, admissible_subst σ -> forall θ, pstep s.|[θ].[σ] t.|[θ].[σ].
Proof with eauto using pstep.
  move=> s t; elim => {s t}; try by (move => *; subst; asimpl;
    eauto using pstep; econstructor; autosubst).
  { move=> s₁ t₁ s₂ t₂ U ? H1 ? H2 u<-{u} σ ad θ.
    asimpl.
    apply (pstep_beta (t₁:=t₁.|[θ].[upn 2 σ]) (t₂:=t₂.|[θ].[σ])).
    + by apply/H1/admissible_subst_up2.
    + by apply/H2.
    + by rewrite neutralize_comm_subst_corr2; autosubst. }
  { move=> s t T ? H u<-{u} σ ad θ.
    asimpl.
    apply (pstep_tbeta (t:=t.|[up θ].[σ >>| ren (+1)])).
    + by apply/H/admissible_hsubst.
    + by autosubst. }
  { move=> s t U ? H u<-{u} σ ad θ.
    asimpl.
    apply (pstep_lam (t:=t.|[θ].[upn 2 σ])).
    + by apply/H/admissible_subst_up2.
    + by autosubst. }
  { move=> s t ? H u<-{u} σ ad θ.
    asimpl.
    apply (pstep_tlam (t:=t.|[up θ].[σ >>| ren (+1)])).
    + by apply/H/admissible_hsubst.
    + by autosubst. }
  { move=> s t ? H u<-{u} σ ad θ.
    asimpl.
    apply (pstep_tall (t:=t.|[up θ].[σ >>| ren (+1)])).
    + by apply/H/admissible_hsubst.
    + by autosubst. }
Qed.

Lemma pstep_subst σ s t :
  pstep s t -> admissible_subst σ -> pstep s.[σ] t.[σ].
Proof.
  have->: s.[σ] = s.|[ids].[σ] by autosubst.
  have->: t.[σ] = t.|[ids].[σ] by autosubst.
  move=> *.
  exact: pstep_substf.
Qed.

Lemma psstep_up σ τ :
  psstep σ τ -> psstep (upn 2 σ) (upn 2 τ).
Proof.
  move=> s.
  (do 2 elim=>//)=> nn ??.
  asimpl.
  apply pstep_subst.
    exact: s.
  move=> n H.
  rewrite /neu /sneu /ns.
  asimpl.
  by rewrite ifN; [|lia].
Qed.

Lemma psstep_hsubst σ τ θ :
  psstep σ τ -> psstep (σ >>| θ) (τ >>| θ).
Proof.
  move=> s n.
  have->: (σ >>| θ) n = (σ n).|[θ].[ids] by autosubst.
  have->: (τ >>| θ) n = (τ n).|[θ].[ids] by autosubst.
  apply pstep_substf.
    exact: s.
  exact: admissible_ids.
Qed.

Lemma pstep_compat θ σ τ s t :
  admissible_subst σ ->
  admissible_subst τ ->
  psstep σ τ -> pstep s t -> pstep s.|[θ].[σ] t.|[θ].[τ].
Proof with eauto using pstep, psstep_up, psstep_hsubst.
  move=> H₁ H₂ H₃ H₄; elim: H₄ θ σ τ H₁ H₂ H₃ => {s t}; asimpl;
    try by (move=> *; subst; eauto using pstep, psstep_up, psstep_hsubst).
  { move=> ? s₂ ? t₂ ?? HA ?? u<-{u} θ σ τ ???.
    apply: (@pstep_beta _ (s₂.|[θ].[upn 2 τ]) _ (t₂.|[θ].[τ]))...
    apply: HA; try apply admissible_subst_up2...
    asimpl.
    rewrite neutralize_comm_subst_corr2... }
  { move=> ? s₂ ?? ih u<-{u} θ σ τ ???.
    apply pstep_tbeta with s₂.|[up θ].[τ >>| ren (+1)]; last by autosubst.
    apply: ih...
    + exact: admissible_hsubst.
    + exact: admissible_hsubst. }
  { move=> s₁ s₂ ?? ih u<-{u} θ σ τ ???.
    asimpl.
    apply pstep_lam with s₂.|[θ].[upn 2 τ]; last by reflexivity.
    apply: ih...
    + exact: admissible_subst_up2.
    + exact: admissible_subst_up2. }
  { move=> s₁ s₂ ? ih u<-{u} θ σ τ ???.
    asimpl.
    apply pstep_tlam with s₂.|[up θ].[τ >>| ren (+1)]; last by reflexivity.
    apply: ih...
    + exact: admissible_hsubst.
    + exact: admissible_hsubst. }
  { move=> s₁ s₂ ? ih u<-{u} θ σ τ ???.
    asimpl.
    apply pstep_tall with s₂.|[up θ].[τ >>| ren (+1)]; last by reflexivity.
    apply: ih...
    + exact: admissible_hsubst.
    + exact: admissible_hsubst. }
Qed.

Lemma pstep_compat_tbeta s t T :
  pstep s t -> pstep s.|[T/] t.|[T/].
Proof.
  move=> H.
  have->: s.|[T/] = s.|[T/].[ids] by autosubst.
  have->: t.|[T/] = t.|[T/].[ids] by autosubst.
  apply: pstep_compat H.
  + exact: admissible_ids.
  + exact: admissible_ids.
  + by move=>?; apply pstep_refl.
Qed.

Lemma pstep_compat_beta0 s₁ s₂ t₁ t₂ :
  admissible_subst (t₁ .: ids) ->
  admissible_subst (t₂ .: ids) ->
  pstep s₁ s₂ -> pstep t₁ t₂ -> pstep s₁.[t₁/] s₂.[t₂/].
Proof.
  move=> H1 H2 s t.
  have->: s₁ = s₁.|[ids] by autosubst.
  have->: s₂ = s₂.|[ids] by autosubst.
  apply: pstep_compat s => //.
  by move=>[].
Qed.

Lemma pstep_compat_beta s₁ s₂ t₁ t₂ C₁ C₂ :
  admissible_subst (t₁ .: C₁ .: ids) ->
  admissible_subst (t₂ .: C₂ .: ids) ->
  pstep s₁ s₂ -> pstep t₁ t₂ -> pstep C₁ C₂ -> pstep s₁.[t₁,C₁/] s₂.[t₂,C₂/].
Proof.
  move=> ?? s ??.
  have->: s₁ = s₁.|[ids] by autosubst.
  have->: s₂ = s₂.|[ids] by autosubst.
  apply: pstep_compat s => //.
  by move=>[]//[]//.
Qed.

Deterministic strategy included in pstep relation.

Fixpoint rho (s : recipe) : recipe :=
  match s with
    | Top => Top
    | Var x => Var x

    | App (Lam U s) t => (rho s).[rho t, neu (rho t)/]
    | TApp (TLam s) T => (rho s).|[T/]

    | Imp f s => Imp f (rho s)
    | Lam U s => Lam U (rho s)
    | TAll s => TAll (rho s)
    | TLam s => TLam (rho s)
    | TApp s t => TApp (rho s) t
    | App s t => App (rho s) (rho t)
    | And s t => And (rho s) (rho t)
  end.

Lemma rho_triangle : triangle pstep rho.
Proof with eauto using pstep.
  move=> s t; elim=> {s t};
      try by (move=> *; subst; asimpl; eauto using pstep).
  { move=> *; subst; simpl.
    eapply pstep_compat_beta...
    + exact: admissible_subst_var01.
    + exact: admissible_subst_var01.
    + apply pstep_subst => //.
      exact: admissible_neu. }
  { move=> s₁ s₂ T ?? u<-{u} /=.
    have->: s₂.|[T/] = s₂.|[T/].[ids] by autosubst.
    have->: (rho s₁).|[T/] = (rho s₁).|[T/].[ids] by autosubst.
    apply pstep_compat.
    + exact: admissible_ids.
    + exact: admissible_ids.
    + move=>?; apply pstep_refl.
    + by assumption. }
  { move=> + s₂ T + + u<-{u}.
    case=> //= ...
    move=> s H1 H2.
    inv H1.
    apply pstep_tbeta with (rho s); last by [].
    inv H2.
    by congruence. }
  { move=> + s₂ t₁ t₂ + + ? ? u<-{u}.
    elim=> //= ...
    move=> ? s ? H2 H3.
    inv H2. inv H3.
    apply pstep_beta with (rho s) (rho t₁);
      by congruence. }
Qed.

Confluence of step

Theorem church_rosser :
  forall s t, conv step s t -> joinable red s t.
Proof.
  apply: (cr_method (e2 := pstep) (rho := rho)).
  + exact: step_pstep.
  + exact: pstep_red.
  + exact: rho_triangle.
Qed.

Corollary confluence :
  confluent step.
Proof.
  apply confluent_cr.
  exact church_rosser.
Qed.

End ChurchRosser.

End StarStep.

Reserved Notation "[ Γ ⊢ ]" (format "[ Γ ⊢ ]").
Reserved Notation "[ Γ ⊢ σ ]" (format "[ Γ ⊢ σ ]").
Reserved Notation "[ Γ ⊢ s :- U ]" (format "[ Γ ⊢ s :- U ]").

Typing

Section TypingDefinitions.

Definition ctx := var -> type.

Inductive has_type (Γ : ctx) : recipe -> type -> Prop :=
| ty_top : [ Γ Top :- Void ]
| ty_tall s : [ Γ s :- Void ] ->
              [ Γ TAll s :- Void ]
| ty_tlam s U : [ Γ s :- U ] ->
                [ Γ TLam s :- TArr U ]
| ty_var x U : Γ x = U ->
              [ Γ Var x :- U ]
| ty_imp s f :
              [ Γ s :- Void ] ->
              [ Γ Imp f s :- Void ]
| ty_and s t :
              [ Γ s :- Void ] ->
              [ Γ t :- Void ] ->
              [ Γ And s t :- Void ]
| ty_lam s U V :
    [ U .: U .: Γ s :- V ] ->
              [ Γ Lam U s :- Arr U V ]
| ty_app s t U V :
              [ Γ s :- Arr U V ] ->
              [ Γ t :- U ] ->
              [ Γ App s t :- V ]
| ty_tapp s T U :
              [ Γ s :- TArr U ] ->
              [ Γ TApp s T :- U ]
where "[ Γ ⊢ s :- U ]" := (has_type Γ s U).

Definition wf_ctx (Γ : ctx) :=
  forall i, odd i.+1 -> Γ i.+1 = Γ i.

Definition wf_subst (σ : var -> recipe) (Γ : ctx) := forall x, [ Γ σ x :- Γ x ].

End TypingDefinitions.

Notation "[ Γ ⊢ s :- U ]" := (has_type Γ s U).
Notation "[ Γ ⊢ ]" := (wf_ctx Γ).
Notation "[ Γ ⊢ σ ]" := (wf_subst σ Γ).

Section TypingLemmas.

Lemma wf_subst_neu Γ σ :
  [ Γ ] ->
  [ Γ σ ] ->
  admissible_subst σ ->
  [ Γ σ >> sneu ].
Proof.
  move=> wf wfσ ad v.
  have->: (σ >> sneu) v = neu (Var v).|[ids].[σ] by autosubst.
  rewrite (neutralize_comm_subst_corr2 _ _ ad).
  asimpl.
  rewrite /wf_subst in wfσ.
  rewrite /admissible_subst in ad.
  case: (boolP (odd v))=> [y|n].
  + have->: sneu v = Var v by rewrite/sneu/ns/= ifT.
    by apply wfσ.
  + have->/=: sneu v = Var v.+1 by rewrite/sneu/ns/= ifF; [done|lia].
    have->: Γ v = Γ v.+1 by rewrite wf.
    by apply wfσ.
Qed.

Lemma ty_ren [Γ U] s Δ ξ :
  (forall x, Γ (ξ x) = Δ x) ->
  [ Δ s :- U ] ->
  [ Γ s.[ren ξ] :- U ].
Proof with eauto using has_type.
  move=> H ty. elim: ty Γ ξ H => {Δ s U} /=...
  { move=> Γ s ty H1 Δ ξ H2.
    asimpl.
    by apply/ty_tall/H1. }
  { move=> Γ s U H1 H2 Δ ξ H3.
    apply ty_tlam. asimpl.
    by apply H2. }
  { move=> Γ x tx <- {tx} Δ ξ <-.
    have->: ids (ξ x) = Var (ξ x) by autosubst.
    exact: ty_var. }
  { move=> Γ U V s H1 ih Δ ξ H3.
    asimpl.
    apply: ty_lam.
    apply: ih.
    by do 2 (case => //=). }
Qed.

Lemma ty_weak [Γ U V] s :
  [ Γ s :- U ] -> [ V .: Γ s.[ren (+1)] :- U ].
Proof.
  exact: ty_ren.
Qed.

Lemma ty_weak2 [Γ U V] s :
  [ Γ s :- U ] -> [ V .: V .: Γ s.[ren (+2)] :- U ].
Proof.
  exact: ty_ren.
Qed.

Lemma wf_ext [Γ U] :
  [ Γ ] -> [ U .: U .: Γ ].
Proof.
  move=>H []//[]// n.
  asimpl.
  rewrite Bool.negb_involutive.
  exact: H.
Qed.

Lemma ty_hsubst [Γ U] s τ :
  [ Γ s :- U ] ->
  [ Γ s.|[τ] :- U ].
Proof with eauto using has_type.
  move=> H. elim: H τ; asimpl...
Qed.

Lemma ty_subst Γ Δ s U σ :
  (forall x, [ Δ σ x :- Γ x ]) ->
  [ Γ s :- U ] ->
  [ Δ s.[σ] :- U ].
Proof with eauto using has_type.
  move=> H ty. elim: ty Δ σ H => {Γ s U}/=...
  - move=> Γ s tyA ih Δ τ H /=.
    apply/ty_tall/ih.
    by case=>[|n]; asimpl; apply/ty_hsubst/H.
  - move=> Γ s tyA H1 ih Δ τ H /=.
    apply: ty_tlam.
    apply: ih.
    asimpl=> x.
    by apply ty_hsubst.
  - move=> Γ s tyA <- {tyA} Δ τ H /=. exact: H.
  - move=> Γ s U V tyA ih Δ σ H /=.
    apply: ty_lam.
    apply: ih.
    asimpl.
    have id_var: forall n, ids n = Var n by autosubst.
    case; first by asimpl; rewrite id_var; apply/ty_var.
    case; first by asimpl; rewrite id_var; apply/ty_var.
    move=> n.
    have Hn2 := (@ty_weak Δ (Γ n) Un) (H n)).
    have := (@ty_weak (U.:Δ) (Γ n) U (σ n).[ren(+1)] Hn2).
    by autosubst.
Qed.

Lemma ty_neu_m [Γ U] s m :
  [ Γ ] -> [ Γ s :- U ] -> [ Γ s.[upn m.*2 sneu] :- U ].
Proof with eauto using has_type.
  move=> H ty. elim: ty H m => {Γ s U}; asimpl; ainv...
  { asimpl.
    apply: ty_tall.
    rewrite /sneu.
    asimpl.
    apply ty_subst with Γ; last by assumption.
    move=> x.
    asimpl.
    rewrite upnP /ns.
    case: ifP => [lt|ge] /=...
    case: ifP=> [odd|even].
    have->: (m.*2 + (x - m.*2))%coq_nat = x by lia...
    have->: (m.*2 + (x - m.*2).+1)%coq_nat = x.+1 by lia.
    have oddSi: (odd x.+1) by lia.
    rewrite -H1... }
  { asimpl.
    apply ty_tlam.
    apply ty_subst with Γ.
      asimpl => x.
      apply ty_hsubst.
      rewrite upnP.
      case: ifP => [lt|ge]...
      simpl.
      rewrite /ns.
      case: ifP=> [odd|even].
      have->: (m.*2 + (x - m.*2))%coq_nat = x by lia...
      have->: (m.*2 + (x - m.*2).+1)%coq_nat = x.+1 by lia.
      have oddSx: (odd x.+1) by lia.
      rewrite -H1...
    done. }
  { rewrite upnP.
    case: ifP => [lt|ge]...
    rewrite /=/ns.
    case: ifP=> [odd|even].
    have->: (m.*2 + (x - m.*2))%coq_nat = x by lia...
    have->: (m.*2 + (x - m.*2).+1)%coq_nat = x.+1 by lia.
    have oddSx: (odd x.+1) by lia.
    rewrite -H0... }
  { apply ty_lam.
    rewrite -fold_up_up !fold_up_upn.
    have->: m.*2.+2 = m.+1.*2 by lia.
    by apply/H0/wf_ext. }
Qed.

Corollary ty_neu [Γ U] s :
  [ Γ ] -> [ Γ s :- U ] -> [ Γ neu s :- U ].
Proof.
  rewrite /neu.
  have->: sneu = upn 0.*2 sneu by rewrite -[0.*2]/0.
  exact: ty_neu_m.
Qed.

Subject Reduction

Section SubjectReduction.

Theorem subject_reduction [Γ U] s t :
  [ Γ ] -> [ Γ s :- U ] -> step s t -> [ Γ t :- U ].
Proof with eauto using has_type.
  move=> wf wt. elim: wt wf t => {s U}; asimpl; ainv...
  { inv H3; apply ty_and => //=.
    + exact: H0.
    + exact: H2. }
  { apply/ty_lam/H0.
    exact: wf_ext.
    done. }
  { inv H3.
    { inv H.
      apply ty_subst with (U .: U .: Γ0) => //.
      case=> //.
      case=> //=...
      exact: ty_neu. }
    { inv H... }
    { inv H... } }
  { inv H1. inv H.
    exact: ty_hsubst.
    exact/ty_tapp/H0. }
Qed.

Corollary subject_reduction_red [Γ U] s t :
  [ Γ ] -> [ Γ s :- U ] -> red s t -> [ Γ t :- U ].
Proof.
  move=> h1 h2.
  elim=> // {}t *.
  by apply subject_reduction with t.
Qed.

End SubjectReduction.
End TypingLemmas.