Recipes_neutralization.Recipes_NF
Computing normal forms
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 Recipes_SN Recipes_step_lemmas.
From Coq Require Extraction.
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 Recipes_SN Recipes_step_lemmas.
From Coq Require Extraction.
Deterministic reduction strategy.
Fixpoint rho r : recipe :=
match r with
| Top => Top
| Var h => Var h
| App (Lam U s) t => s.[t, neu t/]
| TApp (TLam s) T => s.|[T/]
| App s t => App (rho s) (rho t)
| TApp s T => TApp (rho s) T
| And s t => And (rho s) (rho t)
| Imp f s => Imp f (rho s)
| TLam s => TLam (rho s)
| TAll s => TAll (rho s)
| Lam U s => Lam U (rho s)
end.
match r with
| Top => Top
| Var h => Var h
| App (Lam U s) t => s.[t, neu t/]
| TApp (TLam s) T => s.|[T/]
| App s t => App (rho s) (rho t)
| TApp s T => TApp (rho s) T
| And s t => And (rho s) (rho t)
| Imp f s => Imp f (rho s)
| TLam s => TLam (rho s)
| TAll s => TAll (rho s)
| Lam U s => Lam U (rho s)
end.
Deterministic normal form checking.
Fixpoint my_nf r :=
match r with
| Top | Var _ => true
| App (Lam _ _) _ | TApp (TLam _) _ => false
| App s t | And s t => andb (my_nf s) (my_nf t)
| Imp _ s | TLam s | TAll s | Lam _ s | TApp s _ => my_nf s
end.
Lemma nf_nf r : (my_nf r = false) <-> ARS.reducible step r.
Proof.
elim: r.
{ by have := normal_top. }
{ by move=>g; have := normal_var g. }
{ move=> s hs t ht /=.
have[[U [u hh]]| n]: decidable (exists x y, s = Lam x y).
{ case s; try by (move=>*; right => h; inv h; inv H; inv H0).
left. by exists U, s0. }
{ rewrite hh/=.
split=>// h2.
exists u.[t, neu t/].
by constructor. }
{ simpl in n.
have->:
match s with
| Lam _ _ => false
| _ => my_nf s && my_nf t
end = my_nf s && my_nf t.
case: s hs n; try by move=>*; ainv.
move=> U s ? h.
exfalso. apply h. by exists U, s.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ case (boolP (my_nf t)) => //= [hty|htn].
{ split; first by done.
move=> h.
inv h. inv H; exfalso.
+ by apply n; exists U, s0.
+ destruct hs.
have: ~ (ARS.reducible step s).
move=>reds.
apply H0 in reds.
by lia.
by apply; exists t0.
+ destruct ht.
have: ~ (ARS.reducible step t).
move=>redt.
apply H0 in redt.
by lia.
by apply; exists t0. }
{ split; last by trivial.
move=> _.
destruct ht.
have [y hy]: ARS.reducible step t. apply H. by lia.
exists (App s y).
by constructor. } }
{ split; last by trivial.
move=> _.
destruct hs.
have [y hy]: ARS.reducible step s. apply H. by lia.
exists (App y t).
by constructor. } } }
{ move=> s hs t ht.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ case (boolP (my_nf t)) => //= [hty|htn].
{ split; first by lia.
move=> h.
inv h. inv H; exfalso.
+ destruct hs.
have: ~ (ARS.reducible step s).
move=>reds.
apply H0 in reds.
by lia.
by apply; exists t0.
+ destruct ht.
have: ~ (ARS.reducible step t).
move=>redt.
apply H0 in redt.
by lia.
by apply; exists t0. }
{ split; last by lia.
move=> _.
destruct ht.
have [y hy]: ARS.reducible step t. apply H. by lia.
exists (And s y).
by constructor. } }
{ split; last by lia.
move=> _.
destruct hs.
have [y hy]: ARS.reducible step s. apply H. by lia.
exists (And y t).
by constructor. } }
{ move=> s hs S.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ split.
+ have h: decidable (exists t, s = TLam t).
case s; try by (move=>*; right => h; inv h).
by left; exists s0.
case h => [[t ->]|notlam].
* exists t.|[S/].
by constructor.
* have->: match s with | TLam _ => false | _ => my_nf s end = my_nf s.
case: s hs hsy h notlam; try by move=>*; ainv.
move=> s hs hsy dec h.
exfalso. apply h. by exists s.
by lia.
+ move=> h.
inv h. inv H.
done.
have->: my_nf s = false by apply hs; exists t.
by case s. }
{ split=> h.
+ destruct hs.
have [u hu]: ARS.reducible step s by apply H; lia.
exists (TApp u S).
by constructor.
+ case: s hs hsn h; try by lia. } }
{ move=> f s hs.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (Imp f u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. }
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (Imp f u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. } }
{ move=> U s hs.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (Lam U u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. }
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (Lam U u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. } }
{ move=> s hs.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (TLam u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. }
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (TLam u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. } }
{ move=> s hs.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (TAll u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. }
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (TAll u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. } }
Qed.
Corollary nf_nf_2 r :
(my_nf r = true) <-> ARS.normal step r.
Proof.
split.
+ move=> mynf h. apply nf_nf in h. by lia.
+ move=> h.
have: ~ (my_nf r = false); last by lia.
by apply/nf_nf.
Qed.
match r with
| Top | Var _ => true
| App (Lam _ _) _ | TApp (TLam _) _ => false
| App s t | And s t => andb (my_nf s) (my_nf t)
| Imp _ s | TLam s | TAll s | Lam _ s | TApp s _ => my_nf s
end.
Lemma nf_nf r : (my_nf r = false) <-> ARS.reducible step r.
Proof.
elim: r.
{ by have := normal_top. }
{ by move=>g; have := normal_var g. }
{ move=> s hs t ht /=.
have[[U [u hh]]| n]: decidable (exists x y, s = Lam x y).
{ case s; try by (move=>*; right => h; inv h; inv H; inv H0).
left. by exists U, s0. }
{ rewrite hh/=.
split=>// h2.
exists u.[t, neu t/].
by constructor. }
{ simpl in n.
have->:
match s with
| Lam _ _ => false
| _ => my_nf s && my_nf t
end = my_nf s && my_nf t.
case: s hs n; try by move=>*; ainv.
move=> U s ? h.
exfalso. apply h. by exists U, s.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ case (boolP (my_nf t)) => //= [hty|htn].
{ split; first by done.
move=> h.
inv h. inv H; exfalso.
+ by apply n; exists U, s0.
+ destruct hs.
have: ~ (ARS.reducible step s).
move=>reds.
apply H0 in reds.
by lia.
by apply; exists t0.
+ destruct ht.
have: ~ (ARS.reducible step t).
move=>redt.
apply H0 in redt.
by lia.
by apply; exists t0. }
{ split; last by trivial.
move=> _.
destruct ht.
have [y hy]: ARS.reducible step t. apply H. by lia.
exists (App s y).
by constructor. } }
{ split; last by trivial.
move=> _.
destruct hs.
have [y hy]: ARS.reducible step s. apply H. by lia.
exists (App y t).
by constructor. } } }
{ move=> s hs t ht.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ case (boolP (my_nf t)) => //= [hty|htn].
{ split; first by lia.
move=> h.
inv h. inv H; exfalso.
+ destruct hs.
have: ~ (ARS.reducible step s).
move=>reds.
apply H0 in reds.
by lia.
by apply; exists t0.
+ destruct ht.
have: ~ (ARS.reducible step t).
move=>redt.
apply H0 in redt.
by lia.
by apply; exists t0. }
{ split; last by lia.
move=> _.
destruct ht.
have [y hy]: ARS.reducible step t. apply H. by lia.
exists (And s y).
by constructor. } }
{ split; last by lia.
move=> _.
destruct hs.
have [y hy]: ARS.reducible step s. apply H. by lia.
exists (And y t).
by constructor. } }
{ move=> s hs S.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ split.
+ have h: decidable (exists t, s = TLam t).
case s; try by (move=>*; right => h; inv h).
by left; exists s0.
case h => [[t ->]|notlam].
* exists t.|[S/].
by constructor.
* have->: match s with | TLam _ => false | _ => my_nf s end = my_nf s.
case: s hs hsy h notlam; try by move=>*; ainv.
move=> s hs hsy dec h.
exfalso. apply h. by exists s.
by lia.
+ move=> h.
inv h. inv H.
done.
have->: my_nf s = false by apply hs; exists t.
by case s. }
{ split=> h.
+ destruct hs.
have [u hu]: ARS.reducible step s by apply H; lia.
exists (TApp u S).
by constructor.
+ case: s hs hsn h; try by lia. } }
{ move=> f s hs.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (Imp f u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. }
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (Imp f u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. } }
{ move=> U s hs.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (Lam U u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. }
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (Lam U u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. } }
{ move=> s hs.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (TLam u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. }
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (TLam u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. } }
{ move=> s hs.
case (boolP (my_nf s)) => //= [hsy|hsn].
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (TAll u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. }
{ split.
+ move=> h.
inv hs.
have[u hu]:= (H h).
exists (TAll u). by constructor.
+ move=> [u hu].
inv hs. apply H0. inv hu. by exists t. } }
Qed.
Corollary nf_nf_2 r :
(my_nf r = true) <-> ARS.normal step r.
Proof.
split.
+ move=> mynf h. apply nf_nf in h. by lia.
+ move=> h.
have: ~ (my_nf r = false); last by lia.
by apply/nf_nf.
Qed.
Lemma classical_step r :
{ARS.reducible step r} + {ARS.normal step r}.
Proof.
case (boolP (my_nf r)).
+ right => h.
apply nf_nf in h.
by lia.
+ left.
apply nf_nf.
by lia.
Qed.
{ARS.reducible step r} + {ARS.normal step r}.
Proof.
case (boolP (my_nf r)).
+ right => h.
apply nf_nf in h.
by lia.
+ left.
apply nf_nf.
by lia.
Qed.
Lemma sound_step s :
red s (rho s).
Proof with eauto using red_top, red_app, red_and, red_tapp, red_imp, red_lam, red_tlam, red_tall, red_subst, red_hsubst, sred_up, sred_hup.
elim: s => //=...
{ move=>?. exact: starR. }
{ case; try by move=> *; apply red_app.
move=> *.
apply star1.
by constructor. }
{ case; try by move=> *; apply red_tapp.
move=> *.
apply star1.
by constructor. }
Qed.
Lemma sound_step_n n s :
red s (iter n rho s).
Proof.
elim: n => //= n h.
apply: (star_trans (iter n rho s)).
done.
exact: sound_step.
Qed.
Lemma recipe_not_lam s t :
(forall U s₀, s <> Lam U s₀) ->
match s with
| Lam _ s0 => s0.[t,neu t/]
| _ => App (rho s) (rho t)
end = App (rho s) (rho t).
Proof.
destruct s; try by (move=>*; ainv).
move=> h.
by specialize (h U s).
Qed.
Lemma recipe_not_tlam s S :
(forall s₀, s <> TLam s₀) ->
match s with
| TLam s0 => s0.|[S/]
| _ => TApp (rho s) S
end = TApp (rho s) S.
Proof.
destruct s; try by (move=>*; ainv).
move=> h.
by specialize (h s).
Qed.
Lemma recipe_var_dec s :
{exists g, s = Var g} + {forall g, s <> Var g}.
Proof.
case s; try by (right=>*; discriminate).
left.
by exists h.
Qed.
Lemma recipe_lam_dec s :
{exists U s₀, s = Lam U s₀} + {forall U s₀, s <> Lam U s₀}.
Proof.
case s; try by (right=>*; discriminate).
left.
by exists U, s0.
Qed.
Lemma recipe_tlam_dec s :
{exists s₀, s = TLam s₀} + {forall s₀, s <> TLam s₀}.
Proof.
case s; try by (right=>*; discriminate).
left.
by exists s0.
Qed.
Section Plus_lemmas.
Lemma plus_and s₁ s₂ t₁ t₂ :
plus step s₁ s₂ -> plus step t₁ t₂ -> plus step (And s₁ t₁) (And s₂ t₂).
Proof.
move=> s t. apply: (plus_trans (y:=And s₂ t₁)).
- apply: (@plus_hom _ _ (And^~ t₁)) s => x y. exact: step_ctx_andl.
- apply: plus_hom t => x y. exact: step_ctx_andr.
Qed.
Lemma plus_andl s₁ s₂ t :
plus step s₁ s₂ -> plus step (And s₁ t) (And s₂ t).
Proof.
move=> s.
apply: (@plus_hom _ _ (And^~ t)) s => x y.
exact: step_ctx_andl.
Qed.
Lemma plus_andr s t₁ t₂ :
plus step t₁ t₂ -> plus step (And s t₁) (And s t₂).
Proof.
move=> t.
apply: (@plus_hom _ _ (And s)) t => x y.
exact: step_ctx_andr.
Qed.
Lemma plus_app s₁ s₂ t₁ t₂ :
plus step s₁ s₂ -> plus step t₁ t₂ -> plus step (App s₁ t₁) (App s₂ t₂).
Proof.
move=> s t. apply: (plus_trans (y:=App s₂ t₁)).
- apply: (@plus_hom _ _ (App^~ t₁)) s => x y. exact: step_ctx_appl.
- apply: plus_hom t => x y. exact: step_ctx_appr.
Qed.
Lemma plus_appl s₁ s₂ t :
plus step s₁ s₂ -> plus step (App s₁ t) (App s₂ t).
Proof.
move=> s.
apply: (@plus_hom _ _ (App^~ t)) s => x y.
exact: step_ctx_appl.
Qed.
Lemma plus_appr s t₁ t₂ :
plus step t₁ t₂ -> plus step (App s t₁) (App s t₂).
Proof.
move=> t.
apply: (@plus_hom _ _ (App s)) t => x y.
exact: step_ctx_appr.
Qed.
Lemma plus_tapp T s t :
plus step s t -> plus step (TApp s T) (TApp t T).
Proof.
apply: (@plus_hom _ _ (TApp^~T)) => x y.
exact: step_ctx_tapp.
Qed.
Lemma plus_imp f s t :
plus step s t -> plus step (Imp f s) (Imp f t).
Proof.
apply: (@plus_hom _ _ (Imp f)) => x y.
exact: step_ctx_imp.
Qed.
Lemma plus_lam s t π :
plus step s t -> plus step (Lam π s) (Lam π t).
Proof.
apply: plus_hom => x y.
exact: step_ctx_lam.
Qed.
Lemma plus_tlam s t :
plus step s t -> plus step (TLam s) (TLam t).
Proof.
apply: plus_hom => x y.
exact: step_ctx_tlam.
Qed.
Lemma plus_tall s t :
plus step s t -> plus step (TAll s) (TAll t).
Proof.
apply: plus_hom => x y.
exact: step_ctx_tall.
Qed.
End Plus_lemmas.
Lemma normal_rho_id s :
ARS.normal step s -> s = rho s.
Proof.
move=> h; apply nf_nf_2 in h; move: h.
elim: s => //=.
{ move=> s hs t ht m.
case (recipe_lam_dec s) => [[V [? u]]|fa].
by rewrite u in m.
have lemma: (forall U s₀, s <> Lam U s₀) ->
match s with
| Lam _ s0 => false
| _ => my_nf s && my_nf t
end = my_nf s && my_nf t
by destruct s; try by (move=>*; ainv).
rewrite (recipe_not_lam s t fa).
rewrite (lemma fa) in m => {lemma fa}.
move: m => /andP [] ns nt.
by rewrite {1}(hs ns) {1}(ht nt). }
{ move=> s hs t ht /andP [] ns nt.
by rewrite {1}(hs ns) {1}(ht nt). }
{ move=> s hs S m.
case (recipe_tlam_dec s) => [[? u]|fa].
by rewrite u in m.
have lemma: (forall s₀, s <> TLam s₀) ->
match s with
| TLam s0 => false
| _ => my_nf s
end = my_nf s
by destruct s; try by (move=>*; ainv).
rewrite (recipe_not_tlam s S fa).
rewrite (lemma fa) in m => {lemma fa}.
by rewrite {1}(hs m). }
{ move=> ? t ht nt. by rewrite {1}(ht nt). }
{ move=> ? t ht nt. by rewrite {1}(ht nt). }
{ move=> t ht nt. by rewrite {1}(ht nt). }
{ move=> t ht nt. by rewrite {1}(ht nt). }
Qed.
Lemma plus_s_rho_s [Γ : ctx] [U : type] s :
[ Γ ⊢ ] -> [ Γ ⊢ s :- U ] ->
ARS.reducible step s ->
plus step s (rho s).
Proof.
elim: s Γ U.
{ move=> ???? h. inv h. by inv H. }
{ move=> ????? h. inv h. by inv H. }
{ move=> s hs t ht Γ U wf wt h /=.
case (recipe_lam_dec s) => [[V [s₀ ->]]|fa].
exact/plus1/step_beta.
rewrite (recipe_not_lam s t fa).
inv wt.
specialize (hs Γ _ wf H1).
specialize (ht Γ _ wf H3).
inv h.
case (classical_step t); case (classical_step s).
{ move=> rs rt.
specialize (hs rs) => {rs}.
specialize (ht rt) => {rt}.
by apply plus_app. }
{ move=> ns rt.
specialize (ht rt) => {rt}.
rewrite {1}(normal_rho_id s ns).
exact: plus_appr. }
{ move=> rs nt.
specialize (hs rs) => {rs}.
rewrite {1}(normal_rho_id t nt).
exact: plus_appl. }
{ move=> ns nt.
inv H; exfalso.
{ exact: (fa U1 s0). }
{ by apply ns; exists t0. }
{ by apply nt; exists t0. } } }
{ move=> s hs t ht Γ U wf wt h /=.
inv wt.
specialize (hs Γ Void wf H1).
specialize (ht Γ Void wf H3).
inv h.
case (classical_step t); case (classical_step s).
{ move=> rs rt.
specialize (hs rs) => {rs}.
specialize (ht rt) => {rt}.
by apply plus_and. }
{ move=> ns rt.
specialize (ht rt) => {rt}.
rewrite {1}(normal_rho_id s ns).
exact: plus_andr. }
{ move=> rs nt.
specialize (hs rs) => {rs}.
rewrite {1}(normal_rho_id t nt).
exact: plus_andl. }
{ move=> ns nt.
inv H; exfalso.
{ by apply ns; exists t0. }
{ by apply nt; exists t0. } } }
{ move=> s hs T Γ U wf wt h /=.
inv wt. specialize (hs _ _ wf H2).
inv h. inv H.
+ exact/plus1/step_tbeta.
+ case (recipe_tlam_dec s) => [[s0 ->]| fa] /=.
* exact/plus1/step_tbeta.
rewrite (recipe_not_tlam s T fa).
apply/plus_tapp/hs.
by exists t. }
{ move=> f s hs Γ U wf wt h /=.
inv wt. specialize (hs _ _ wf H2).
inv h. inv H.
apply/plus_imp/hs.
by exists t. }
{ move=> V s hs Γ U wf wt h /=.
inv wt. inv h. inv H.
apply/plus_lam/(hs (V .: V .: Γ) V0) => //.
exact: wf_ext.
by exists t. }
{ move=> s hs Γ U wf wt h /=.
inv wt. inv h. inv H.
apply/plus_tlam/(hs Γ U0) => //.
by exists t. }
{ move=> s hs Γ U wf wt h /=.
inv wt. inv h. inv H.
apply/plus_tall/(hs Γ Void) => //.
by exists t. }
Qed.
Definition ppets := fun x y => plus step y x.
red s (rho s).
Proof with eauto using red_top, red_app, red_and, red_tapp, red_imp, red_lam, red_tlam, red_tall, red_subst, red_hsubst, sred_up, sred_hup.
elim: s => //=...
{ move=>?. exact: starR. }
{ case; try by move=> *; apply red_app.
move=> *.
apply star1.
by constructor. }
{ case; try by move=> *; apply red_tapp.
move=> *.
apply star1.
by constructor. }
Qed.
Lemma sound_step_n n s :
red s (iter n rho s).
Proof.
elim: n => //= n h.
apply: (star_trans (iter n rho s)).
done.
exact: sound_step.
Qed.
Lemma recipe_not_lam s t :
(forall U s₀, s <> Lam U s₀) ->
match s with
| Lam _ s0 => s0.[t,neu t/]
| _ => App (rho s) (rho t)
end = App (rho s) (rho t).
Proof.
destruct s; try by (move=>*; ainv).
move=> h.
by specialize (h U s).
Qed.
Lemma recipe_not_tlam s S :
(forall s₀, s <> TLam s₀) ->
match s with
| TLam s0 => s0.|[S/]
| _ => TApp (rho s) S
end = TApp (rho s) S.
Proof.
destruct s; try by (move=>*; ainv).
move=> h.
by specialize (h s).
Qed.
Lemma recipe_var_dec s :
{exists g, s = Var g} + {forall g, s <> Var g}.
Proof.
case s; try by (right=>*; discriminate).
left.
by exists h.
Qed.
Lemma recipe_lam_dec s :
{exists U s₀, s = Lam U s₀} + {forall U s₀, s <> Lam U s₀}.
Proof.
case s; try by (right=>*; discriminate).
left.
by exists U, s0.
Qed.
Lemma recipe_tlam_dec s :
{exists s₀, s = TLam s₀} + {forall s₀, s <> TLam s₀}.
Proof.
case s; try by (right=>*; discriminate).
left.
by exists s0.
Qed.
Section Plus_lemmas.
Lemma plus_and s₁ s₂ t₁ t₂ :
plus step s₁ s₂ -> plus step t₁ t₂ -> plus step (And s₁ t₁) (And s₂ t₂).
Proof.
move=> s t. apply: (plus_trans (y:=And s₂ t₁)).
- apply: (@plus_hom _ _ (And^~ t₁)) s => x y. exact: step_ctx_andl.
- apply: plus_hom t => x y. exact: step_ctx_andr.
Qed.
Lemma plus_andl s₁ s₂ t :
plus step s₁ s₂ -> plus step (And s₁ t) (And s₂ t).
Proof.
move=> s.
apply: (@plus_hom _ _ (And^~ t)) s => x y.
exact: step_ctx_andl.
Qed.
Lemma plus_andr s t₁ t₂ :
plus step t₁ t₂ -> plus step (And s t₁) (And s t₂).
Proof.
move=> t.
apply: (@plus_hom _ _ (And s)) t => x y.
exact: step_ctx_andr.
Qed.
Lemma plus_app s₁ s₂ t₁ t₂ :
plus step s₁ s₂ -> plus step t₁ t₂ -> plus step (App s₁ t₁) (App s₂ t₂).
Proof.
move=> s t. apply: (plus_trans (y:=App s₂ t₁)).
- apply: (@plus_hom _ _ (App^~ t₁)) s => x y. exact: step_ctx_appl.
- apply: plus_hom t => x y. exact: step_ctx_appr.
Qed.
Lemma plus_appl s₁ s₂ t :
plus step s₁ s₂ -> plus step (App s₁ t) (App s₂ t).
Proof.
move=> s.
apply: (@plus_hom _ _ (App^~ t)) s => x y.
exact: step_ctx_appl.
Qed.
Lemma plus_appr s t₁ t₂ :
plus step t₁ t₂ -> plus step (App s t₁) (App s t₂).
Proof.
move=> t.
apply: (@plus_hom _ _ (App s)) t => x y.
exact: step_ctx_appr.
Qed.
Lemma plus_tapp T s t :
plus step s t -> plus step (TApp s T) (TApp t T).
Proof.
apply: (@plus_hom _ _ (TApp^~T)) => x y.
exact: step_ctx_tapp.
Qed.
Lemma plus_imp f s t :
plus step s t -> plus step (Imp f s) (Imp f t).
Proof.
apply: (@plus_hom _ _ (Imp f)) => x y.
exact: step_ctx_imp.
Qed.
Lemma plus_lam s t π :
plus step s t -> plus step (Lam π s) (Lam π t).
Proof.
apply: plus_hom => x y.
exact: step_ctx_lam.
Qed.
Lemma plus_tlam s t :
plus step s t -> plus step (TLam s) (TLam t).
Proof.
apply: plus_hom => x y.
exact: step_ctx_tlam.
Qed.
Lemma plus_tall s t :
plus step s t -> plus step (TAll s) (TAll t).
Proof.
apply: plus_hom => x y.
exact: step_ctx_tall.
Qed.
End Plus_lemmas.
Lemma normal_rho_id s :
ARS.normal step s -> s = rho s.
Proof.
move=> h; apply nf_nf_2 in h; move: h.
elim: s => //=.
{ move=> s hs t ht m.
case (recipe_lam_dec s) => [[V [? u]]|fa].
by rewrite u in m.
have lemma: (forall U s₀, s <> Lam U s₀) ->
match s with
| Lam _ s0 => false
| _ => my_nf s && my_nf t
end = my_nf s && my_nf t
by destruct s; try by (move=>*; ainv).
rewrite (recipe_not_lam s t fa).
rewrite (lemma fa) in m => {lemma fa}.
move: m => /andP [] ns nt.
by rewrite {1}(hs ns) {1}(ht nt). }
{ move=> s hs t ht /andP [] ns nt.
by rewrite {1}(hs ns) {1}(ht nt). }
{ move=> s hs S m.
case (recipe_tlam_dec s) => [[? u]|fa].
by rewrite u in m.
have lemma: (forall s₀, s <> TLam s₀) ->
match s with
| TLam s0 => false
| _ => my_nf s
end = my_nf s
by destruct s; try by (move=>*; ainv).
rewrite (recipe_not_tlam s S fa).
rewrite (lemma fa) in m => {lemma fa}.
by rewrite {1}(hs m). }
{ move=> ? t ht nt. by rewrite {1}(ht nt). }
{ move=> ? t ht nt. by rewrite {1}(ht nt). }
{ move=> t ht nt. by rewrite {1}(ht nt). }
{ move=> t ht nt. by rewrite {1}(ht nt). }
Qed.
Lemma plus_s_rho_s [Γ : ctx] [U : type] s :
[ Γ ⊢ ] -> [ Γ ⊢ s :- U ] ->
ARS.reducible step s ->
plus step s (rho s).
Proof.
elim: s Γ U.
{ move=> ???? h. inv h. by inv H. }
{ move=> ????? h. inv h. by inv H. }
{ move=> s hs t ht Γ U wf wt h /=.
case (recipe_lam_dec s) => [[V [s₀ ->]]|fa].
exact/plus1/step_beta.
rewrite (recipe_not_lam s t fa).
inv wt.
specialize (hs Γ _ wf H1).
specialize (ht Γ _ wf H3).
inv h.
case (classical_step t); case (classical_step s).
{ move=> rs rt.
specialize (hs rs) => {rs}.
specialize (ht rt) => {rt}.
by apply plus_app. }
{ move=> ns rt.
specialize (ht rt) => {rt}.
rewrite {1}(normal_rho_id s ns).
exact: plus_appr. }
{ move=> rs nt.
specialize (hs rs) => {rs}.
rewrite {1}(normal_rho_id t nt).
exact: plus_appl. }
{ move=> ns nt.
inv H; exfalso.
{ exact: (fa U1 s0). }
{ by apply ns; exists t0. }
{ by apply nt; exists t0. } } }
{ move=> s hs t ht Γ U wf wt h /=.
inv wt.
specialize (hs Γ Void wf H1).
specialize (ht Γ Void wf H3).
inv h.
case (classical_step t); case (classical_step s).
{ move=> rs rt.
specialize (hs rs) => {rs}.
specialize (ht rt) => {rt}.
by apply plus_and. }
{ move=> ns rt.
specialize (ht rt) => {rt}.
rewrite {1}(normal_rho_id s ns).
exact: plus_andr. }
{ move=> rs nt.
specialize (hs rs) => {rs}.
rewrite {1}(normal_rho_id t nt).
exact: plus_andl. }
{ move=> ns nt.
inv H; exfalso.
{ by apply ns; exists t0. }
{ by apply nt; exists t0. } } }
{ move=> s hs T Γ U wf wt h /=.
inv wt. specialize (hs _ _ wf H2).
inv h. inv H.
+ exact/plus1/step_tbeta.
+ case (recipe_tlam_dec s) => [[s0 ->]| fa] /=.
* exact/plus1/step_tbeta.
rewrite (recipe_not_tlam s T fa).
apply/plus_tapp/hs.
by exists t. }
{ move=> f s hs Γ U wf wt h /=.
inv wt. specialize (hs _ _ wf H2).
inv h. inv H.
apply/plus_imp/hs.
by exists t. }
{ move=> V s hs Γ U wf wt h /=.
inv wt. inv h. inv H.
apply/plus_lam/(hs (V .: V .: Γ) V0) => //.
exact: wf_ext.
by exists t. }
{ move=> s hs Γ U wf wt h /=.
inv wt. inv h. inv H.
apply/plus_tlam/(hs Γ U0) => //.
by exists t. }
{ move=> s hs Γ U wf wt h /=.
inv wt. inv h. inv H.
apply/plus_tall/(hs Γ Void) => //.
by exists t. }
Qed.
Definition ppets := fun x y => plus step y x.
The inductive ARS.sn is isomorph to Coq.Init.Wf.Acc
where the relation R is in the opposite direction.
Lemma sn_is_acc [T : Type] (R : T -> T -> Prop) (s : T) :
ARS.sn R s <-> Acc (fun x y => R y x) s.
Proof.
by split; elim; split.
Qed.
Lemma wt_acc_plus [Γ : ctx] [U : type] s (wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :
Acc ppets s.
Proof.
apply sn_is_acc.
apply strong_normalization_plus.
exact: (@strong_normalization Γ U s).
Qed.
Definition rho_wt [Γ : ctx] [U : type] s (wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :
[ Γ ⊢ rho s :- U ].
Proof.
exact: (subject_reduction_red _ _ (sound_step _)).
Qed.
Corollary not_mynf_then_reducible r :
my_nf r = false -> ARS.reducible step r.
Proof.
by apply nf_nf.
Qed.
Record RNF s :=
{ dest : recipe; (* destination recipe : the normal form *)
dest_nf : my_nf dest = true; (* proof that it is the nf *)
path : star step s dest; (* path from source recipe to destination *)
rho_len : nat; (* number of rho-steps *)
eq_nrho : dest = iter rho_len rho s; (* proof *)
}.
Lemma iter_succ_rw x y n :
x = iter n rho (rho y) ->
x = iter n.+1 rho y.
Proof.
by rewrite iterSr.
Qed.
ARS.sn R s <-> Acc (fun x y => R y x) s.
Proof.
by split; elim; split.
Qed.
Lemma wt_acc_plus [Γ : ctx] [U : type] s (wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :
Acc ppets s.
Proof.
apply sn_is_acc.
apply strong_normalization_plus.
exact: (@strong_normalization Γ U s).
Qed.
Definition rho_wt [Γ : ctx] [U : type] s (wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :
[ Γ ⊢ rho s :- U ].
Proof.
exact: (subject_reduction_red _ _ (sound_step _)).
Qed.
Corollary not_mynf_then_reducible r :
my_nf r = false -> ARS.reducible step r.
Proof.
by apply nf_nf.
Qed.
Record RNF s :=
{ dest : recipe; (* destination recipe : the normal form *)
dest_nf : my_nf dest = true; (* proof that it is the nf *)
path : star step s dest; (* path from source recipe to destination *)
rho_len : nat; (* number of rho-steps *)
eq_nrho : dest = iter rho_len rho s; (* proof *)
}.
Lemma iter_succ_rw x y n :
x = iter n rho (rho y) ->
x = iter n.+1 rho y.
Proof.
by rewrite iterSr.
Qed.
Basically the function is doing, but the decreasing argument is non trivial.
Fixpoint eval s := if my_nf s then s else eval (rho s)
Fixpoint eval0 [Γ : ctx] [U : type] (s : recipe)
(wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) (H : Acc ppets s) : (RNF s) :=
match my_nf s as b return my_nf s = b -> _ with
| true => fun h => {| dest := s ; dest_nf := h; path := starR step s; rho_len := 0; eq_nrho := erefl |}
| false => fun hnf =>
match H with
| Acc_intro π =>
let wt' : [ Γ ⊢ rho s :- U ] := rho_wt s wf wt in
let h := not_mynf_then_reducible _ hnf in
let plus_s_rho_s : ppets (rho s) s := plus_s_rho_s s wf wt h in
let (to1, nf1, fromto1, n, hn) := eval0 (rho s) wf wt' (π (rho s) plus_s_rho_s) in
let h0 : star step (rho s) to1 := fromto1 in
let h1 : star step s (rho s) := sound_step s in
let h2 : star step s to1 := @star_trans recipe step (rho s) s to1 h1 h0 in
let hn : to1 = iter n rho (rho s) := hn in
let hsn : (to1 = iter n.+1 rho s) := iter_succ_rw to1 s n hn in
{|
dest := to1;
dest_nf := nf1;
path := h2;
rho_len := n.+1;
eq_nrho := hsn;
|}
end
end erefl.
Lemma norm_step [Γ : ctx] [U : type] (s : recipe)
(wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :
forall t : recipe, nf step s t ->
exists n : nat, t = iter n rho s.
Proof.
move=> t nf.
have [r nfr sr n hn] := eval0 s wf wt (wt_acc_plus s wf wt).
destruct nf.
have: t = r.
have h := confluence => {hn n wt wf U Γ}.
specialize (h s t r H sr).
apply (cr_conv_normal church_rosser).
{ inv h. inv H1 => {sr nfr H0 H s}.
{ elim: H2; first by apply convR.
move=> y z ry cyr yz.
have rz: star step r z by apply starSE with y.
by apply/conv_sym/star_conv. }
{ have {H3}ty: conv step t y by apply star_conv.
have {H4}yx: conv step y x by apply conv1.
have {ty yx}tx: conv step t x by apply conv_trans with y.
have {H2}rx: conv step r x by apply star_conv.
apply conv_sym in rx.
by apply conv_trans with x. } }
+ done.
+ by apply nf_nf_2.
move=> eq.
subst.
by exists n.
Qed.
Section MyComputationN.
Inductive my_accn (x : recipe) : Prop :=
| accnH : normal step x -> my_accn x
| accnL : my_accn (rho x) -> my_accn x.
Scheme accn_ind' := Induction for my_accn Sort Prop.
Lemma nf_accn [Γ U] x y :
[ Γ ⊢ ] -> [ Γ ⊢ x :- U ] -> nf step x y -> my_accn x.
Proof.
move=> wf wt A.
case: (@norm_step Γ U x wf wt y A) => n.
case: A => _. move/accnH.
elim: n y => [|n ih] y A /= B. by rewrite -B.
apply: (ih (iter n rho x)) => //. apply: accnL. by rewrite -B.
Qed.
Lemma wn_accn [Γ U] x :
[ Γ ⊢ ] -> [ Γ ⊢ x :- U ] -> wn step x -> my_accn x.
Proof.
move=> ??[y].
exact: (@nf_accn Γ U).
Qed.
Lemma sn_wn x :
sn step x -> wn step x.
Proof.
elim=> {} x _ ih. case (classical_step x) => [[y exy]|A].
- case: (ih _ exy) => z [A B]. exists z. split=> //. exact: starES A.
- exists x. by split.
Qed.
Lemma my_accn_inv x (H1 : my_accn x) (H2 : ARS.reducible step x) :
my_accn (rho x).
Proof.
by case: H1.
Defined.
(wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :
forall t : recipe, nf step s t ->
exists n : nat, t = iter n rho s.
Proof.
move=> t nf.
have [r nfr sr n hn] := eval0 s wf wt (wt_acc_plus s wf wt).
destruct nf.
have: t = r.
have h := confluence => {hn n wt wf U Γ}.
specialize (h s t r H sr).
apply (cr_conv_normal church_rosser).
{ inv h. inv H1 => {sr nfr H0 H s}.
{ elim: H2; first by apply convR.
move=> y z ry cyr yz.
have rz: star step r z by apply starSE with y.
by apply/conv_sym/star_conv. }
{ have {H3}ty: conv step t y by apply star_conv.
have {H4}yx: conv step y x by apply conv1.
have {ty yx}tx: conv step t x by apply conv_trans with y.
have {H2}rx: conv step r x by apply star_conv.
apply conv_sym in rx.
by apply conv_trans with x. } }
+ done.
+ by apply nf_nf_2.
move=> eq.
subst.
by exists n.
Qed.
Section MyComputationN.
Inductive my_accn (x : recipe) : Prop :=
| accnH : normal step x -> my_accn x
| accnL : my_accn (rho x) -> my_accn x.
Scheme accn_ind' := Induction for my_accn Sort Prop.
Lemma nf_accn [Γ U] x y :
[ Γ ⊢ ] -> [ Γ ⊢ x :- U ] -> nf step x y -> my_accn x.
Proof.
move=> wf wt A.
case: (@norm_step Γ U x wf wt y A) => n.
case: A => _. move/accnH.
elim: n y => [|n ih] y A /= B. by rewrite -B.
apply: (ih (iter n rho x)) => //. apply: accnL. by rewrite -B.
Qed.
Lemma wn_accn [Γ U] x :
[ Γ ⊢ ] -> [ Γ ⊢ x :- U ] -> wn step x -> my_accn x.
Proof.
move=> ??[y].
exact: (@nf_accn Γ U).
Qed.
Lemma sn_wn x :
sn step x -> wn step x.
Proof.
elim=> {} x _ ih. case (classical_step x) => [[y exy]|A].
- case: (ih _ exy) => z [A B]. exists z. split=> //. exact: starES A.
- exists x. by split.
Qed.
Lemma my_accn_inv x (H1 : my_accn x) (H2 : ARS.reducible step x) :
my_accn (rho x).
Proof.
by case: H1.
Defined.
Normalizing recipe evaluates to normal forms that exists.
Lemma my_evaln2 (x : recipe) (H : ARS.sn step x) :
exists r, nf step x r.
Proof.
elim: H.
move=> {}x h1 h2.
case (classical_step x).
{ move=> [] y hy.
destruct (h2 y hy).
exists x0.
destruct H.
split.
apply star_trans with y.
by apply star1.
done.
done. }
{ move=> h.
exists x.
split.
apply starR.
done. }
Qed.
Fixpoint my_evaln (x : recipe) (H : my_accn x) : recipe :=
match classical_step x with
| left a => my_evaln (rho x) (my_accn_inv x H a)
| right _ => x
end.
Lemma evaln_sound x (H : my_accn x) :
nf step x (my_evaln x H).
Proof.
move: x H. apply: accn_ind'.
- move=> x n /=. by case: (classical_step x).
- move=> x a [A B] /=. case: (classical_step x) => //= _.
split=>//. apply: star_trans A. exact: sound_step.
Defined.
Theorem evalnP [Γ U] x :
[ Γ ⊢ ] -> [ Γ ⊢ x :- U ] ->
ex (nf step x) -> sig (nf step x).
Proof.
move=> wf wt A.
exists (my_evaln x (wn_accn x wf wt A)).
exact: evaln_sound.
Defined.
Lemma acc_if_wt Γ U x :
[ Γ ⊢ ] -> [ Γ ⊢ x :- U ] ->
my_accn x.
Proof.
move=> wf wt.
apply: (@wn_accn Γ U x) => //.
apply sn_wn.
exact: (@strong_normalization Γ U x).
Defined.
Theorem wt2nf_ex [Γ U] x :
[ Γ ⊢ ] -> [ Γ ⊢ x :- U ] ->
ex (nf step x).
Proof.
move=> wf wt.
have H := acc_if_wt Γ U x wf wt.
exists (my_evaln x H).
by apply evaln_sound.
Defined.
Definition wt2nf_sig [Γ U] s :
[ Γ ⊢ ] -> [ Γ ⊢ s :- U ] ->
sig (nf step s).
Proof.
move=> wf wt.
have A : ex (nf step s) by exact: (@wt2nf_ex Γ U).
exists (my_evaln s (wn_accn s wf wt A)).
exact: evaln_sound.
Defined.
End MyComputationN.
Definition eval [Γ U] s (wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :=
my_evaln s (acc_if_wt Γ U s wf wt).
Lemma eval_sound [Γ U] s (wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) : nf step s (eval s wf wt).
Proof.
exact: evaln_sound.
Qed.
Corollary eval_nf_sound [Γ U] s (wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :
forall t, nf step s t -> t = eval s wf wt.
Proof.
move=> t nft.
destruct nft.
destruct (eval_sound s wf wt).
apply (cr_conv_normal church_rosser) => //.
have st: conv step s t by exact: star_conv.
have se: conv step s (eval s wf wt) by exact: star_conv.
apply conv_sym in st.
exact: (conv_trans s).
Qed.
Lemma eval_red [Γ U] s t
(wf : [ Γ ⊢ ]) (wts : [ Γ ⊢ s :- U ]) (wtt : [ Γ ⊢ t :- U ]) :
red s t -> (eval s wf wts) = eval t wf wtt.
Proof.
move=> h.
have [ss nfs] := eval_sound s wf wts.
have [st nft] := eval_sound t wf wtt.
apply: (cr_conv_normal church_rosser) => //.
apply conv_trans with s.
by apply/conv_sym/star_conv.
apply conv_trans with t.
by apply/star_conv.
by apply/star_conv.
Qed.
Lemma eval_ty [Γ U] s
(wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :
[Γ ⊢ (eval s wf wt) :- U].
Proof.
have [ss nfs] := eval_sound s wf wt.
by apply subject_reduction_red with s.
Qed.
(* Recursive Extraction eval. *)
(* Recursive Extraction my_evaln. *)
Definition eval_nf [Γ : ctx] [U : type] (s : recipe)
(wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :=
dest s (eval0 s wf wt (wt_acc_plus s wf wt)).
exists r, nf step x r.
Proof.
elim: H.
move=> {}x h1 h2.
case (classical_step x).
{ move=> [] y hy.
destruct (h2 y hy).
exists x0.
destruct H.
split.
apply star_trans with y.
by apply star1.
done.
done. }
{ move=> h.
exists x.
split.
apply starR.
done. }
Qed.
Fixpoint my_evaln (x : recipe) (H : my_accn x) : recipe :=
match classical_step x with
| left a => my_evaln (rho x) (my_accn_inv x H a)
| right _ => x
end.
Lemma evaln_sound x (H : my_accn x) :
nf step x (my_evaln x H).
Proof.
move: x H. apply: accn_ind'.
- move=> x n /=. by case: (classical_step x).
- move=> x a [A B] /=. case: (classical_step x) => //= _.
split=>//. apply: star_trans A. exact: sound_step.
Defined.
Theorem evalnP [Γ U] x :
[ Γ ⊢ ] -> [ Γ ⊢ x :- U ] ->
ex (nf step x) -> sig (nf step x).
Proof.
move=> wf wt A.
exists (my_evaln x (wn_accn x wf wt A)).
exact: evaln_sound.
Defined.
Lemma acc_if_wt Γ U x :
[ Γ ⊢ ] -> [ Γ ⊢ x :- U ] ->
my_accn x.
Proof.
move=> wf wt.
apply: (@wn_accn Γ U x) => //.
apply sn_wn.
exact: (@strong_normalization Γ U x).
Defined.
Theorem wt2nf_ex [Γ U] x :
[ Γ ⊢ ] -> [ Γ ⊢ x :- U ] ->
ex (nf step x).
Proof.
move=> wf wt.
have H := acc_if_wt Γ U x wf wt.
exists (my_evaln x H).
by apply evaln_sound.
Defined.
Definition wt2nf_sig [Γ U] s :
[ Γ ⊢ ] -> [ Γ ⊢ s :- U ] ->
sig (nf step s).
Proof.
move=> wf wt.
have A : ex (nf step s) by exact: (@wt2nf_ex Γ U).
exists (my_evaln s (wn_accn s wf wt A)).
exact: evaln_sound.
Defined.
End MyComputationN.
Definition eval [Γ U] s (wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :=
my_evaln s (acc_if_wt Γ U s wf wt).
Lemma eval_sound [Γ U] s (wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) : nf step s (eval s wf wt).
Proof.
exact: evaln_sound.
Qed.
Corollary eval_nf_sound [Γ U] s (wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :
forall t, nf step s t -> t = eval s wf wt.
Proof.
move=> t nft.
destruct nft.
destruct (eval_sound s wf wt).
apply (cr_conv_normal church_rosser) => //.
have st: conv step s t by exact: star_conv.
have se: conv step s (eval s wf wt) by exact: star_conv.
apply conv_sym in st.
exact: (conv_trans s).
Qed.
Lemma eval_red [Γ U] s t
(wf : [ Γ ⊢ ]) (wts : [ Γ ⊢ s :- U ]) (wtt : [ Γ ⊢ t :- U ]) :
red s t -> (eval s wf wts) = eval t wf wtt.
Proof.
move=> h.
have [ss nfs] := eval_sound s wf wts.
have [st nft] := eval_sound t wf wtt.
apply: (cr_conv_normal church_rosser) => //.
apply conv_trans with s.
by apply/conv_sym/star_conv.
apply conv_trans with t.
by apply/star_conv.
by apply/star_conv.
Qed.
Lemma eval_ty [Γ U] s
(wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :
[Γ ⊢ (eval s wf wt) :- U].
Proof.
have [ss nfs] := eval_sound s wf wt.
by apply subject_reduction_red with s.
Qed.
(* Recursive Extraction eval. *)
(* Recursive Extraction my_evaln. *)
Definition eval_nf [Γ : ctx] [U : type] (s : recipe)
(wf : [ Γ ⊢ ]) (wt : [ Γ ⊢ s :- U ]) :=
dest s (eval0 s wf wt (wt_acc_plus s wf wt)).