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.
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.
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}).
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.
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.
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.
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.
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.
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.
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].
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].
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->: (neu (σ g.-1)).|[τ].[(+m.*2) >>> ids] =
(neu (σ g.-1)).[(+m.*2) >>> ids].|[τ]
by autosubst.
have->: (neu (σ g.-1)).|[τ].[(+m.*2) >>> upn m.*2 sneu >>| τ] =
(neu (σ g.-1)).[(+m.*2) >>> upn m.*2 sneu].|[τ] by autosubst.
f_equal.
have->: (neu (σ g.-1)).[(+m.*2) >>> upn m.*2 sneu] =
(rename (+m.*2) (neu (σ g.-1))).[upn m.*2 sneu] by autosubst.
have->: (neu (σ g.-1)).[(+m.*2) >>> ids] =
(rename (+m.*2) (neu (σ g.-1))) by autosubst.
have->: rename (+m.*2) (neu (σ g.-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.
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->: (neu (σ g.-1)).|[τ].[(+m.*2) >>> ids] =
(neu (σ g.-1)).[(+m.*2) >>> ids].|[τ]
by autosubst.
have->: (neu (σ g.-1)).|[τ].[(+m.*2) >>> upn m.*2 sneu >>| τ] =
(neu (σ g.-1)).[(+m.*2) >>> upn m.*2 sneu].|[τ] by autosubst.
f_equal.
have->: (neu (σ g.-1)).[(+m.*2) >>> upn m.*2 sneu] =
(rename (+m.*2) (neu (σ g.-1))).[upn m.*2 sneu] by autosubst.
have->: (neu (σ g.-1)).[(+m.*2) >>> ids] =
(rename (+m.*2) (neu (σ g.-1))) by autosubst.
have->: rename (+m.*2) (neu (σ g.-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.
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.
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.
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.
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.
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 ]").
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 ]").
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) U (σ n) (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.
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) U (σ n) (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.
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.
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.