Recipes_neutralization.Recipes_SN
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.
Require Import Recipes.
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.
Require Import Recipes.
Strong Normalization
The inductive ARS.sn is isomorph to Coq.Init.Wf.Acc
where the relation R is in the opposite direction.
Lemma sn_closed s t : sn step (App s t) -> sn step s.
Proof. apply: (sn_preimage (h := App^~t)) => x y. exact: step_ctx_appl. Qed.
Lemma sn_tclosed s T : sn step (TApp s T) -> sn step s.
Proof. apply: (sn_preimage (h := TApp^~T)) => x y. exact: step_ctx_tapp. Qed.
Lemma sn_subst σ s : admissible_subst σ -> sn step s.[σ] -> sn step s.
Proof. move=> H. apply: sn_preimage => x y. by exact: step_subst. Qed.
Lemma sn_hsubst θ s : sn step s.|[θ] -> sn step s.
Proof. apply: sn_preimage => x y. exact: step_hsubst. Qed.
The Reducibility Candidates (cf. Girard 72).
A term which is not a Lambda is simple.
The idea is that when a simple term t is applied to u,
then the reduction step either happen in t or u but the
application does not reduce :
App t u → App t' u or App t u → App t u'.
Predicate over recipes.
Girard conditions known as CR1, CR2, CR3.
Record reducible (P : cand) : Prop := {
p_sn : forall s, P s -> sn step s;
p_cl : forall s t, P s -> step s t -> P t;
p_nc : forall s, simple s -> (forall t, step s t -> P t) -> P s
}.
p_sn : forall s, P s -> sn step s;
p_cl : forall s t, P s -> step s t -> P t;
p_nc : forall s, simple s -> (forall t, step s t -> P t) -> P s
}.
Logical relation.
Fixpoint RED U : cand :=
match U with
| Void => sn step
| Arr U V => fun s => forall t, RED U t -> RED U (neu t) -> RED V (App s t)
| TArr V => fun s => forall T, RED V (TApp s T)
end.
match U with
| Void => sn step
| Arr U V => fun s => forall t, RED U t -> RED U (neu t) -> RED V (App s t)
| TArr V => fun s => forall T, RED V (TApp s T)
end.
Logical relation generalized to a entire substitution.
Definition REDσ Γ (σ : var -> recipe) : Prop :=
forall x, RED (Γ x) (σ x).
Lemma reducible_sn : reducible (sn step).
Proof. constructor; eauto using sn. by move=> s t [f] /f. Qed.
Lemma reducible_var P x : reducible P -> P (Var x).
Proof. move/p_nc. apply=> // t st. inv st. Qed.
forall x, RED (Γ x) (σ x).
Lemma reducible_sn : reducible (sn step).
Proof. constructor; eauto using sn. by move=> s t [f] /f. Qed.
Lemma reducible_var P x : reducible P -> P (Var x).
Proof. move/p_nc. apply=> // t st. inv st. Qed.
Check that the logical relation respects Girard's conditions.
Lemma red_reducible U : reducible (RED U).
Proof with eauto using step.
elim: U => /=.
{ constructor.
+ done.
+ move=> s t H st.
by apply H.
+ move=> ?? H; split.
exact H. }
{ move=> U ih1 V ih2. constructor.
+ move=> ? h.
apply: (@sn_closed _ (Var 0)).
apply: (p_sn (RED V))...
apply: h.
exact: reducible_var.
have->: neu (Var 0) = Var 1 by rewrite /neu/=/ns.
exact: reducible_var.
+ move=> s t h st u redu rednu.
apply p_cl with (App s u)...
+ move=> ???? redt rednt.
have snt := p_sn _ ih1 _ redt.
elim: snt redt rednt => {} u _ ih3 redu rednu.
apply: p_nc => // v st.
inv st => //...
apply: (ih3 _ H2).
by apply p_cl with u.
apply: (p_cl _ ih1 (neu u) _ rednu).
exact: (step_subst admissible_neu H2). }
{ move=> U ih. constructor.
+ move=> ??.
apply: (@sn_tclosed _ (TNat 0)).
apply: (p_sn (RED U))...
+ move=> s t h st T.
apply p_cl with (TApp s T)...
+ move=> s ss h T.
apply p_nc...
move=> t st.
inv st.
by simpl in ss.
exact: h. }
Qed.
Corollary RED_sn U s :
RED U s -> sn step s.
Proof.
apply: p_sn. apply: red_reducible.
Qed.
Corollary RED_cl U s t :
RED U s -> step s t -> RED U t.
Proof.
apply: p_cl. apply: red_reducible.
Qed.
Corollary RED_nc U s :
simple s -> (forall t, step s t -> RED U t) -> RED U s.
Proof.
apply: p_nc. apply: red_reducible.
Qed.
Corollary RED_var U x : RED U (Var x).
Proof.
apply: RED_nc => //= t st.
by inv st.
Qed.
Corollary RED_cl_star U s t :
RED U s -> red s t -> RED U t.
Proof.
move=> cl st.
elim: st cl => //.
move=> u v ? H H2 ?.
apply: (RED_cl _ u v) => //.
exact: H.
Qed.
Proof with eauto using step.
elim: U => /=.
{ constructor.
+ done.
+ move=> s t H st.
by apply H.
+ move=> ?? H; split.
exact H. }
{ move=> U ih1 V ih2. constructor.
+ move=> ? h.
apply: (@sn_closed _ (Var 0)).
apply: (p_sn (RED V))...
apply: h.
exact: reducible_var.
have->: neu (Var 0) = Var 1 by rewrite /neu/=/ns.
exact: reducible_var.
+ move=> s t h st u redu rednu.
apply p_cl with (App s u)...
+ move=> ???? redt rednt.
have snt := p_sn _ ih1 _ redt.
elim: snt redt rednt => {} u _ ih3 redu rednu.
apply: p_nc => // v st.
inv st => //...
apply: (ih3 _ H2).
by apply p_cl with u.
apply: (p_cl _ ih1 (neu u) _ rednu).
exact: (step_subst admissible_neu H2). }
{ move=> U ih. constructor.
+ move=> ??.
apply: (@sn_tclosed _ (TNat 0)).
apply: (p_sn (RED U))...
+ move=> s t h st T.
apply p_cl with (TApp s T)...
+ move=> s ss h T.
apply p_nc...
move=> t st.
inv st.
by simpl in ss.
exact: h. }
Qed.
Corollary RED_sn U s :
RED U s -> sn step s.
Proof.
apply: p_sn. apply: red_reducible.
Qed.
Corollary RED_cl U s t :
RED U s -> step s t -> RED U t.
Proof.
apply: p_cl. apply: red_reducible.
Qed.
Corollary RED_nc U s :
simple s -> (forall t, step s t -> RED U t) -> RED U s.
Proof.
apply: p_nc. apply: red_reducible.
Qed.
Corollary RED_var U x : RED U (Var x).
Proof.
apply: RED_nc => //= t st.
by inv st.
Qed.
Corollary RED_cl_star U s t :
RED U s -> red s t -> RED U t.
Proof.
move=> cl st.
elim: st cl => //.
move=> u v ? H H2 ?.
apply: (RED_cl _ u v) => //.
exact: H.
Qed.
Closure under beta expansion.
Lemma beta_expansion U V s t :
sn step t -> RED U s.[t, neu t/] ->
RED U (App (Lam V s) t).
Proof with eauto.
move=> snt h.
have sns := sn_subst _ _ (admissible_subst_var01 t) (@RED_sn _ _ h).
elim: sns t snt h => {} s sns ih1 t.
elim=> {} t snt ih2 h.
apply: RED_nc => // u st.
inv st => //.
- inv H2.
apply: ih1 => //.
apply: RED_cl h _.
exact: (step_subst (admissible_subst_var01 t)).
- apply: ih2 => //.
apply: RED_cl_star h _.
exact: red_beta01.
Qed.
Lemma tbeta_expansion U T s :
RED U s.|[T/] -> RED U (TApp (TLam s) T).
Proof.
move=> h.
have sns : sn step s.
apply: (sn_hsubst (T .: ids) s).
by apply (RED_sn U).
elim: sns h => {} s _ ih h.
apply: RED_nc => // t st.
inv st => //.
inv H2 => //.
apply: ih => //.
apply: RED_cl h _.
exact: step_hsubst.
Qed.
Constructor expansion
Lemma imp_expansion s f :
RED Void s -> RED Void (Imp f s).
Proof.
move=> h.
have sns: sn step s by apply (RED_sn Void).
elim: sns h => {} s _ ih h.
apply: RED_nc; first by simpl.
move=> t st /=.
inv st.
apply: (ih _ H2).
by apply h.
Qed.
Lemma and_expansion s t :
RED Void s -> RED Void t -> RED Void (And s t).
Proof.
move=> hs ht.
have sns : sn step s by apply (RED_sn Void).
have snt : sn step t by apply (RED_sn Void).
elim: sns t snt hs ht => {} s sns ih1 t.
elim=> {} t snt ih2 hs ht.
apply: RED_nc; first by trivial.
move=> u stu.
inv stu.
{ apply: ih1.
+ done.
+ by apply ht.
+ by apply hs.
+ done. }
{ apply: ih2.
+ done.
+ by apply hs.
+ by apply ht. }
Qed.
Lemma tall_expansion s :
sn step s -> sn step (TAll s).
Proof with eauto using step.
elim => {} s _ ih.
split => t st.
inv st.
exact: (ih _ H0).
Qed.
Lemma sneu_idempotent : sneu >> sneu = sneu.
Proof.
f_ext=> x.
rewrite /sneu/ns/=.
case (boolP (odd x)) => [odd_x|nodd_x].
by rewrite ifT.
by rewrite ifT.
Qed.
The fundamental theorem.
Theorem soundness [Γ : ctx] [U : type] (s : recipe):
[ Γ ⊢ s :- U ] -> [ Γ ⊢ ] ->
forall τ σ, admissible_subst σ -> REDσ Γ σ ->
RED U s.|[τ].[σ].
Proof with eauto using RED_sn.
elim=> {Γ s U}
[Γ| Γ s ty_s /= ih
| Γ s U ty_s ih1
| Γ h U <-
| Γ s f ty_s ih1
| Γ s t ty_s ih1 ty_t ih2
| Γ s U V ty_s ih1
| Γ s t U V ty_s ih1 ty_t ih2
| Γ s T U ih1 ih2 ]
adΓ τ σ adσ el; asimpl...
{ split=> ? ih. by inv ih. }
{ apply: tall_expansion.
apply: (sn_hsubst (TVar 0 .: ids)).
asimpl.
exact: ih. }
{ move=> T.
apply: tbeta_expansion.
asimpl.
exact: ih1. }
{ apply: imp_expansion. exact: ih1. }
{ apply: and_expansion. exact: ih1. exact: ih2. }
{ move=> t h hneu.
apply: beta_expansion...
asimpl.
apply: ih1.
+ by apply: wf_ext.
+ rewrite /REDσ /= /admissible_subst.
move=>[]//[]//= n.
rewrite Bool.negb_involutive.
exact: adσ.
+ by move=>[]//=[]//=. }
{ simpl in ih1.
apply: ih1...
rewrite /neu.
asimpl.
apply: ih2...
* rewrite /admissible_subst => n oddsn.
rewrite /neu.
asimpl.
rewrite sneu_idempotent adσ.
have->: (neu (σ n)).[sneu] = neu (neu (σ n)) by asimpl.
by rewrite -neu_idempotent.
done.
* rewrite /REDσ => x.
case (boolP (odd x)) => [odd_x|nodd_x].
+ have->: (σ >> sneu) x = (σ x).
have->: σ x = neu (σ x).
have->: σ x = neu (σ x.-1).
have{1}->: x = x.-1.+1 by lia.
rewrite adσ => //=.
lia.
by apply neu_idempotent.
by asimpl.
by exact: el.
+ have->: (σ >> sneu) x = (σ x.+1).
have->: (σ >> sneu) x = neu (σ x) by autosubst.
by rewrite adσ.
have->: Γ x = Γ x.+1 by rewrite adΓ.
by apply el. }
{ simpl in ih2.
apply ih2... }
Qed.
Corollary type_L Γ s U :
[ Γ ⊢ ] ->
[ Γ ⊢ s :- U ] ->
RED U s.
Proof.
move=> wf ty.
specialize (soundness s ty wf ids ids).
asimpl.
apply.
exact: admissible_ids.
rewrite /REDσ => x.
exact: RED_var.
Qed.
Corollary strong_normalization [Γ U] s :
[ Γ ⊢ ] -> [ Γ ⊢ s :- U ] -> sn step s.
Proof.
move=>wf /type_L /RED_sn.
by apply.
Qed.
Corollary strong_normalization_plus s :
sn step s -> sn (plus step) s.
Proof.
elim=>{}s sns ih.
split=> y []{}y z sy yz.
have[r [sr []]]:= @invstarES _ _ z s y yz sy.
{ exact: ih. }
{ move=> u w ru uw.
have snpr: (sn (plus step)) r by exact: ih.
have plusrw: plus step r w by apply plusSE with u.
by apply snpr. }
Qed.
Corollary step_anti_refl [Γ U] s : [ Γ ⊢ ] -> [ Γ ⊢ s :- U ] -> ~ step s s.
Proof.
move=> wf wt.
have: sn step s by exact: (@strong_normalization Γ U s).
elim=> t _ ih tt.
exact: (ih t).
Qed.