Recipes_neutralization.Recipes_step_lemmas
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 My_tactics.
Require Import Recipes.
Require Import Recipes_SN.
Lemma normal_no_step s t :
step s t -> normal step s -> False.
Proof.
move=> h1 h2.
apply h2.
by exists t.
Qed.
Lemma unique_nf_antistep s t u :
nf step s u ->
step t s ->
nf step t u.
Proof.
move=> h. destruct h.
split; last by done.
apply (cr_star_normal church_rosser) => //.
apply star_conv in H.
have {}H1: star step t s by apply star1.
apply star_conv in H1.
exact: (conv_trans s).
Qed.
Lemma unique_nf_antistarstep s t u :
nf step s u ->
star step t s ->
nf step t u.
Proof.
move=> h. destruct h.
split; last by done.
apply (cr_star_normal church_rosser) => //.
apply star_conv in H.
apply star_conv in H1.
exact: (conv_trans s).
Qed.
Lemma unique_nf_step s t u :
nf step s u ->
step s t ->
nf step t u.
Proof.
move=> h. destruct h.
split; last by done.
apply (cr_star_normal church_rosser) => //.
apply star_conv in H.
have {}H1: star step s t by apply star1.
apply star_conv in H1.
apply conv_sym in H1.
exact: (conv_trans s).
Qed.
Lemma unique_nf_starstep s t u :
nf step s u ->
star step s t ->
nf step t u.
Proof.
move=> h. destruct h.
split; last by done.
apply (cr_star_normal church_rosser) => //.
apply star_conv in H.
apply star_conv in H1.
apply conv_sym in H1.
exact: (conv_trans s).
Qed.
Lemma red_and_inv s t u :
star step (And s t) u ->
exists ss tt,
u = And ss tt /\ star step s ss /\ star step t tt.
Proof.
elim.
{ by exists s, t. }
{ move=> v w hs [ss [tt [h1 [h2 h3]]]] vw.
subst.
inv vw.
+ exists t0, tt.
split;[|split] =>//.
apply star_trans with ss=>//.
by apply star1.
+ exists ss, t0.
split;[|split] =>//.
apply star_trans with tt=>//.
by apply star1. }
Qed.
Lemma red_imp_inv f s u :
star step (Imp f s) u ->
exists t,
u = Imp f t /\ star step s t.
Proof.
elim.
{ exists s. by split. }
{ move=> v w hs [x [hx1 hx2]] vw.
subst.
inv vw.
exists t.
split=>//.
apply star_trans with x=>//.
by apply star1. }
Qed.
Lemma red_tall_inv s u :
star step (TAll s) u ->
exists t, u = TAll t /\ star step s t.
Proof.
elim.
{ exists s.
by split. }
{ move=> v w hs [x [hx1 hx2]] vw.
subst.
inv vw.
exists t.
split=>//.
apply star_trans with x=>//.
by apply star1. }
Qed.
Lemma inv_lam_hsubst s s0 θ U :
Lam U s0 = s.|[θ] ->
exists s1, Lam U s1 = s.
Proof.
case: s; try by discriminate.
move=> V s /= h.
exists s.
congruence.
Qed.
Lemma inv_tlam_hsubst s s0 θ :
TLam s0 = s.|[θ] ->
exists s1, TLam s1 = s.
Proof.
case: s; try by discriminate.
move=> s h.
by exists s.
Qed.
Lemma inv_step_hsubst : forall s u θ,
step s.|[θ] u ->
exists u', u = u'.|[θ] /\ step s u'.
Proof with by constructor.
elim=>//=.
{ move=> ?? h. by inv h. }
{ move=> ??? h. by inv h. }
{ move=> s hs t ht u θ st.
inversion st.
{ subst.
have[s1 h]:= inv_lam_hsubst s s0 θ U H.
subst.
exists s1.[t, neu t/]; split; [|by constructor].
asimpl in H.
have->: s0 = s1.|[θ] by injection H.
asimpl.
by rewrite neutralize_comm_subst_corr_hsubst. }
{ clear st; subst.
have [u [-> hu]]:= hs _ _ H2.
exists (App u t).
split... }
{ clear st; subst.
have [u [-> hu]]:= ht _ _ H2.
exists (App s u).
split... }}
{ move=> s hs t ht u θ st.
inv st.
{ destruct (hs _ _ H2) as [sθ [h1 h2]].
subst.
exists (And sθ t).
split... }
{ destruct (ht _ _ H2) as [tθ [h1 h2]].
subst.
exists (And s tθ); asimpl.
split... }}
{ move=> s hs S u θ st.
inversion st.
{ subst.
have[s1 h]:= inv_tlam_hsubst s s0 θ H.
subst.
exists s1.|[S/]; split; [|by constructor].
asimpl in H.
have->: s0 = s1.|[up θ] by injection H.
autosubst. }
{ clear st; subst.
have [sθ [-> h]] := hs _ _ H2.
subst.
exists (TApp sθ S).
split... }}
{ move=> f s hs u θ st.
inv st.
have [sθ [-> h]] := hs _ _ H2.
exists (Imp f sθ).
split... }
{ move=> U s hs u θ st.
inv st.
have [sθ [-> h]] := hs _ _ H2.
exists (Lam U sθ).
split... }
{ move=> s hs u θ st.
inv st.
have [sθ [-> h]] := hs _ _ H0.
exists (TLam sθ).
split... }
{ move=> s hs u θ st.
inv st.
have [sθ [-> h]] := hs _ _ H0.
exists (TAll sθ).
split... }
Qed.
Lemma inv_star_hsubst s u θ :
star step s.|[θ] u ->
exists u', u = u'.|[θ] /\ star step s u'.
Proof.
elim.
{ by exists s. }
{ move=> t w st {u}[u [eq su]] uw.
subst.
have[r [hr1 hr2]]:= (inv_step_hsubst _ _ _ uw).
exists r; split=>//.
by apply (star_trans u), star1. }
Qed.
Lemma normal_top :
normal step Top.
Proof.
by move=> h; inv h; inv H.
Qed.
Lemma normal_var g :
normal step (Var g).
Proof.
by move=> h; inv h; inv H.
Qed.
Lemma nf_top_is_top s :
nf step Top s -> s = Top.
Proof.
move=>[] h _.
apply normal_star in h => //.
exact: normal_top.
Qed.
Lemma nf_var_is_var s x :
nf step (Var x) s -> s = Var x.
Proof.
move=>[] h _.
apply normal_star in h => //.
exact: normal_var.
Qed.
Lemma normande s t :
normal step (And s t) -> normal step s /\ normal step t.
Proof.
split; move=> [u hu]; apply H;
[exists (And u t)|exists (And s u)]; by constructor.
Qed.
Lemma normapp s t :
normal step (App s t) -> normal step s /\ normal step t.
Proof.
split; move=> [u hu]; apply H;
[exists (App u t)|exists (App s u)]; by constructor.
Qed.
Lemma normimp f s :
normal step (Imp f s) -> normal step s.
Proof.
move=> h [u hu].
apply h.
exists (Imp f u).
by constructor.
Qed.
Lemma normall s :
normal step (TAll s) -> normal step s.
Proof.
move=> h [u hu].
apply h.
exists (TAll u).
by constructor.
Qed.
Lemma normal_tlam s :
normal step (TLam s) -> normal step s.
Proof.
move=> h [u hu].
apply h.
exists (TLam u).
by constructor.
Qed.
Lemma normal_lam U s :
normal step (Lam U s) -> normal step s.
Proof.
move=> h [u hu].
apply h.
exists (Lam U u).
by constructor.
Qed.
Lemma normal_tapp T s :
normal step (TApp s T) -> normal step s.
Proof.
move=> h [u hu].
apply h.
exists (TApp u T).
by constructor.
Qed.
Lemma normal_hsubst s θ :
normal step s.|[θ] -> normal step s.
Ltac constructor_hsubst := constructor; apply step_hsubst.
Proof with by constructor_hsubst.
elim: s=> //=.
{ move=> s hs t ht h ctr.
apply h.
destruct ctr as [u hu].
inv hu; asimpl.
{ exists s0.|[θ].[t.|[θ], neu t.|[θ]/]. by constructor. }
{ exists (App t0.|[θ] t.|[θ])... }
{ exists (App s.|[θ] t0.|[θ])... }}
{ move=> s hs t ht h ctr.
destruct (normande _ _ h).
inversion ctr as [u hu].
inv hu.
{ apply hs=>//. by exists t0. }
{ apply ht=>//. by exists t0. } }
{ move=> s hs S h ctr.
inversion ctr as [u hu]. inv hu.
{ apply h. exists s0.|[S.[θ].: θ]. constructor. by autosubst. }
{ apply h. exists (TApp t.|[θ] S.[θ])... }}
{ move=> f s hs h ctr.
inversion ctr as [u hu]. inv hu.
apply h.
exists (Imp f t.|[θ])... }
{ move=> U s hs h ctr.
inversion ctr as [u hu]. inv hu.
apply h.
exists (Lam U t.|[θ])... }
{ move=> s hs h ctr.
inversion ctr as [u hu]. inv hu.
apply h.
exists (TLam t.|[up θ])... }
{ move=> s hs h ctr.
inversion ctr as [u hu]. inv hu.
apply h.
exists (TAll t.|[up θ])... }
Qed.
Lemma inv_nf_hsubst s u θ :
nf step s.|[θ] u ->
exists u', u = u'.|[θ] /\ nf step s u'.
Proof.
Ltac ccl u θ :=
subst; exists u; split=>//; split=>//;
by apply normal_hsubst with θ.
elim: s u θ=>//=.
{ move=> u θ hu.
destruct hu.
apply normal_star in H; last by apply normal_top.
subst.
by exists Top. }
{ move=> v u θ hu.
destruct hu.
apply normal_star in H; last by apply normal_var.
subst.
by exists (Var v). }
{ move=> s hs t ht u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (App s t) u θ h1.
by ccl u' θ. }
{ move=> s hs t ht u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (And s t) u θ h1.
by ccl u' θ. }
{ move=> s hs S u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (TApp s S) u θ h1.
by ccl u' θ. }
{ move=> f s hs u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (Imp f s) u θ h1.
by ccl u' θ. }
{ move=> U s hs u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (Lam U s) u θ h1.
by ccl u' θ. }
{ move=> s hs u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (TLam s) u θ h1.
by ccl u' θ. }
{ move=> s hs u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (TAll s) u θ h1.
by ccl u' θ. }
Qed.
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 My_tactics.
Require Import Recipes.
Require Import Recipes_SN.
Lemma normal_no_step s t :
step s t -> normal step s -> False.
Proof.
move=> h1 h2.
apply h2.
by exists t.
Qed.
Lemma unique_nf_antistep s t u :
nf step s u ->
step t s ->
nf step t u.
Proof.
move=> h. destruct h.
split; last by done.
apply (cr_star_normal church_rosser) => //.
apply star_conv in H.
have {}H1: star step t s by apply star1.
apply star_conv in H1.
exact: (conv_trans s).
Qed.
Lemma unique_nf_antistarstep s t u :
nf step s u ->
star step t s ->
nf step t u.
Proof.
move=> h. destruct h.
split; last by done.
apply (cr_star_normal church_rosser) => //.
apply star_conv in H.
apply star_conv in H1.
exact: (conv_trans s).
Qed.
Lemma unique_nf_step s t u :
nf step s u ->
step s t ->
nf step t u.
Proof.
move=> h. destruct h.
split; last by done.
apply (cr_star_normal church_rosser) => //.
apply star_conv in H.
have {}H1: star step s t by apply star1.
apply star_conv in H1.
apply conv_sym in H1.
exact: (conv_trans s).
Qed.
Lemma unique_nf_starstep s t u :
nf step s u ->
star step s t ->
nf step t u.
Proof.
move=> h. destruct h.
split; last by done.
apply (cr_star_normal church_rosser) => //.
apply star_conv in H.
apply star_conv in H1.
apply conv_sym in H1.
exact: (conv_trans s).
Qed.
Lemma red_and_inv s t u :
star step (And s t) u ->
exists ss tt,
u = And ss tt /\ star step s ss /\ star step t tt.
Proof.
elim.
{ by exists s, t. }
{ move=> v w hs [ss [tt [h1 [h2 h3]]]] vw.
subst.
inv vw.
+ exists t0, tt.
split;[|split] =>//.
apply star_trans with ss=>//.
by apply star1.
+ exists ss, t0.
split;[|split] =>//.
apply star_trans with tt=>//.
by apply star1. }
Qed.
Lemma red_imp_inv f s u :
star step (Imp f s) u ->
exists t,
u = Imp f t /\ star step s t.
Proof.
elim.
{ exists s. by split. }
{ move=> v w hs [x [hx1 hx2]] vw.
subst.
inv vw.
exists t.
split=>//.
apply star_trans with x=>//.
by apply star1. }
Qed.
Lemma red_tall_inv s u :
star step (TAll s) u ->
exists t, u = TAll t /\ star step s t.
Proof.
elim.
{ exists s.
by split. }
{ move=> v w hs [x [hx1 hx2]] vw.
subst.
inv vw.
exists t.
split=>//.
apply star_trans with x=>//.
by apply star1. }
Qed.
Lemma inv_lam_hsubst s s0 θ U :
Lam U s0 = s.|[θ] ->
exists s1, Lam U s1 = s.
Proof.
case: s; try by discriminate.
move=> V s /= h.
exists s.
congruence.
Qed.
Lemma inv_tlam_hsubst s s0 θ :
TLam s0 = s.|[θ] ->
exists s1, TLam s1 = s.
Proof.
case: s; try by discriminate.
move=> s h.
by exists s.
Qed.
Lemma inv_step_hsubst : forall s u θ,
step s.|[θ] u ->
exists u', u = u'.|[θ] /\ step s u'.
Proof with by constructor.
elim=>//=.
{ move=> ?? h. by inv h. }
{ move=> ??? h. by inv h. }
{ move=> s hs t ht u θ st.
inversion st.
{ subst.
have[s1 h]:= inv_lam_hsubst s s0 θ U H.
subst.
exists s1.[t, neu t/]; split; [|by constructor].
asimpl in H.
have->: s0 = s1.|[θ] by injection H.
asimpl.
by rewrite neutralize_comm_subst_corr_hsubst. }
{ clear st; subst.
have [u [-> hu]]:= hs _ _ H2.
exists (App u t).
split... }
{ clear st; subst.
have [u [-> hu]]:= ht _ _ H2.
exists (App s u).
split... }}
{ move=> s hs t ht u θ st.
inv st.
{ destruct (hs _ _ H2) as [sθ [h1 h2]].
subst.
exists (And sθ t).
split... }
{ destruct (ht _ _ H2) as [tθ [h1 h2]].
subst.
exists (And s tθ); asimpl.
split... }}
{ move=> s hs S u θ st.
inversion st.
{ subst.
have[s1 h]:= inv_tlam_hsubst s s0 θ H.
subst.
exists s1.|[S/]; split; [|by constructor].
asimpl in H.
have->: s0 = s1.|[up θ] by injection H.
autosubst. }
{ clear st; subst.
have [sθ [-> h]] := hs _ _ H2.
subst.
exists (TApp sθ S).
split... }}
{ move=> f s hs u θ st.
inv st.
have [sθ [-> h]] := hs _ _ H2.
exists (Imp f sθ).
split... }
{ move=> U s hs u θ st.
inv st.
have [sθ [-> h]] := hs _ _ H2.
exists (Lam U sθ).
split... }
{ move=> s hs u θ st.
inv st.
have [sθ [-> h]] := hs _ _ H0.
exists (TLam sθ).
split... }
{ move=> s hs u θ st.
inv st.
have [sθ [-> h]] := hs _ _ H0.
exists (TAll sθ).
split... }
Qed.
Lemma inv_star_hsubst s u θ :
star step s.|[θ] u ->
exists u', u = u'.|[θ] /\ star step s u'.
Proof.
elim.
{ by exists s. }
{ move=> t w st {u}[u [eq su]] uw.
subst.
have[r [hr1 hr2]]:= (inv_step_hsubst _ _ _ uw).
exists r; split=>//.
by apply (star_trans u), star1. }
Qed.
Lemma normal_top :
normal step Top.
Proof.
by move=> h; inv h; inv H.
Qed.
Lemma normal_var g :
normal step (Var g).
Proof.
by move=> h; inv h; inv H.
Qed.
Lemma nf_top_is_top s :
nf step Top s -> s = Top.
Proof.
move=>[] h _.
apply normal_star in h => //.
exact: normal_top.
Qed.
Lemma nf_var_is_var s x :
nf step (Var x) s -> s = Var x.
Proof.
move=>[] h _.
apply normal_star in h => //.
exact: normal_var.
Qed.
Lemma normande s t :
normal step (And s t) -> normal step s /\ normal step t.
Proof.
split; move=> [u hu]; apply H;
[exists (And u t)|exists (And s u)]; by constructor.
Qed.
Lemma normapp s t :
normal step (App s t) -> normal step s /\ normal step t.
Proof.
split; move=> [u hu]; apply H;
[exists (App u t)|exists (App s u)]; by constructor.
Qed.
Lemma normimp f s :
normal step (Imp f s) -> normal step s.
Proof.
move=> h [u hu].
apply h.
exists (Imp f u).
by constructor.
Qed.
Lemma normall s :
normal step (TAll s) -> normal step s.
Proof.
move=> h [u hu].
apply h.
exists (TAll u).
by constructor.
Qed.
Lemma normal_tlam s :
normal step (TLam s) -> normal step s.
Proof.
move=> h [u hu].
apply h.
exists (TLam u).
by constructor.
Qed.
Lemma normal_lam U s :
normal step (Lam U s) -> normal step s.
Proof.
move=> h [u hu].
apply h.
exists (Lam U u).
by constructor.
Qed.
Lemma normal_tapp T s :
normal step (TApp s T) -> normal step s.
Proof.
move=> h [u hu].
apply h.
exists (TApp u T).
by constructor.
Qed.
Lemma normal_hsubst s θ :
normal step s.|[θ] -> normal step s.
Ltac constructor_hsubst := constructor; apply step_hsubst.
Proof with by constructor_hsubst.
elim: s=> //=.
{ move=> s hs t ht h ctr.
apply h.
destruct ctr as [u hu].
inv hu; asimpl.
{ exists s0.|[θ].[t.|[θ], neu t.|[θ]/]. by constructor. }
{ exists (App t0.|[θ] t.|[θ])... }
{ exists (App s.|[θ] t0.|[θ])... }}
{ move=> s hs t ht h ctr.
destruct (normande _ _ h).
inversion ctr as [u hu].
inv hu.
{ apply hs=>//. by exists t0. }
{ apply ht=>//. by exists t0. } }
{ move=> s hs S h ctr.
inversion ctr as [u hu]. inv hu.
{ apply h. exists s0.|[S.[θ].: θ]. constructor. by autosubst. }
{ apply h. exists (TApp t.|[θ] S.[θ])... }}
{ move=> f s hs h ctr.
inversion ctr as [u hu]. inv hu.
apply h.
exists (Imp f t.|[θ])... }
{ move=> U s hs h ctr.
inversion ctr as [u hu]. inv hu.
apply h.
exists (Lam U t.|[θ])... }
{ move=> s hs h ctr.
inversion ctr as [u hu]. inv hu.
apply h.
exists (TLam t.|[up θ])... }
{ move=> s hs h ctr.
inversion ctr as [u hu]. inv hu.
apply h.
exists (TAll t.|[up θ])... }
Qed.
Lemma inv_nf_hsubst s u θ :
nf step s.|[θ] u ->
exists u', u = u'.|[θ] /\ nf step s u'.
Proof.
Ltac ccl u θ :=
subst; exists u; split=>//; split=>//;
by apply normal_hsubst with θ.
elim: s u θ=>//=.
{ move=> u θ hu.
destruct hu.
apply normal_star in H; last by apply normal_top.
subst.
by exists Top. }
{ move=> v u θ hu.
destruct hu.
apply normal_star in H; last by apply normal_var.
subst.
by exists (Var v). }
{ move=> s hs t ht u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (App s t) u θ h1.
by ccl u' θ. }
{ move=> s hs t ht u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (And s t) u θ h1.
by ccl u' θ. }
{ move=> s hs S u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (TApp s S) u θ h1.
by ccl u' θ. }
{ move=> f s hs u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (Imp f s) u θ h1.
by ccl u' θ. }
{ move=> U s hs u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (Lam U s) u θ h1.
by ccl u' θ. }
{ move=> s hs u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (TLam s) u θ h1.
by ccl u' θ. }
{ move=> s hs u θ []h1 h2.
have[u' [hu1 hu2]] := inv_star_hsubst (TAll s) u θ h1.
by ccl u' θ. }
Qed.