From b66e834a43982f874c35e4e774412aab4475cec9 Mon Sep 17 00:00:00 2001
From: Yannick Forster <yannick.forster@inria.fr>
Date: Thu, 29 Aug 2024 12:47:03 +0200
Subject: [PATCH] fix statement of wcbv standardization

---
 pcuic/theories/PCUICNormalization.v | 18 ++++++++++--------
 1 file changed, 10 insertions(+), 8 deletions(-)

diff --git a/pcuic/theories/PCUICNormalization.v b/pcuic/theories/PCUICNormalization.v
index f1594751b..8d8a5f656 100644
--- a/pcuic/theories/PCUICNormalization.v
+++ b/pcuic/theories/PCUICNormalization.v
@@ -100,7 +100,7 @@ Lemma ws_wcbv_standardization {cf:checker_flags} {no:normalizing_flags} {Σ} {no
   Σ ;;; [] |- t : T ->
   closed_red Σ [] t v ->
   ¬ { t' & Σ ;;; [] |- v ⇝ t'} ->
-  {v' & eval Σ t v' * (Σ ;;; [] ⊢ v' ⇝ v)}.
+  {v' & eval Σ t v' * (Σ ;;; [] |- v' ⇝* v)}.
 Proof.
   intros Hwf Hax Hty Hred Hirred.
   destruct (@wcbv_normalization _ no Σ normalization T t) as (v' & Hv'); eauto.
@@ -109,7 +109,8 @@ Proof.
   2:{ econstructor; eauto. eapply subject_is_open_term. eauto. }
   destruct v as [v Hv].
   assert (v = v'') as <- by (eapply irred_equal; eauto).
-  exists v'; split; eauto.
+  exists v'; split; eauto. cbn.
+  apply closed_red_red. assumption.
 Qed.
 
 Lemma ws_wcbv_standardization_fst {cf:checker_flags} {no:normalizing_flags} {Σ} {normalization:NormalizationIn Σ} {i u args mind} {t v : ws_term (fun _ => false)} : wf Σ -> axiom_free Σ ->
@@ -128,16 +129,17 @@ Proof.
     eapply eval_to_value. eauto.
   }
   enough (v' = v) as -> by eauto.
-  eapply irred_equal. eauto.
-  intros. eapply firstorder_value_irred; eauto.
-  Unshelve.
+  eapply irred_equal.
+  - eapply typing_closed_red. 2: eassumption.
+    eapply subject_reduction_eval; eauto.
+  - intros. eapply firstorder_value_irred; eauto.
 Qed.
 
 Lemma wcbv_standardization {cf:checker_flags} {no:normalizing_flags} {Σ} {normalization:NormalizationIn Σ} {T t v : term} : wf Σ -> axiom_free Σ ->
   Σ ;;; [] |- t : T ->
-  Σ ;;; [] |- t ⇝ v ->
-  ¬ { t' & Σ ;;; [] |- v ⇝ t'} ->
-  {v' & eval Σ t v' * (Σ ;;; [] ⊢ v' ⇝ v)}.
+  Σ ;;; [] |- t ⇝* v ->
+  ¬ { t' &  Σ ;;; [] |- v ⇝ t'} ->
+  {v' & eval Σ t v' * (Σ ;;; [] |- v' ⇝* v)}.
 Proof.
   intros Hwf Hax Hty Hred Hirred.
   unshelve eapply @ws_wcbv_standardization with (T := T) (t := (exist t _)) (v := (exist v _)).