Remove wcbv evaluation of axioms in PCUIC

In PCUIC we treated axioms as values, but we did not consistently treat
eg. fixpoints and cases stuck on axioms as values. This removes the
evaluation of axioms in PCUIC and gets rid of the axiom_free assumption
that was needed for erasure because of it.

Author: jakobbotsch

erasure/theories/EArities.v

@@ -548,7 +548,6 @@ Qed.
 
 Lemma Is_type_eval (Σ : global_env_ext) t v:
   wf Σ ->
-  axiom_free Σ ->
   eval Σ t v ->
   isErasable Σ [] t ->
   isErasable Σ [] v.
@@ -563,13 +562,12 @@ Qed.
 
 Lemma Is_type_eval_inv (Σ : global_env_ext) t v:
   wf_ext Σ ->
-  axiom_free Σ ->
   PCUICSafeLemmata.welltyped Σ [] t ->
   PCUICWcbvEval.eval Σ t v ->
   isErasable Σ [] v ->
   ∥ isErasable Σ [] t ∥.
 Proof.
-  intros wfΣ axfree [T HT] ev [vt [Ht Hp]].
+  intros wfΣ [T HT] ev [vt [Ht Hp]].
   eapply wcbeval_red in ev; eauto.
   pose proof (subject_reduction _ _ _ _ _ wfΣ.1 HT ev).
   pose proof (common_typing _ wfΣ Ht X) as [P [Pvt [Pt vP]]].

erasure/theories/EOptimizePropDiscr.v

@@ -232,27 +232,25 @@ Proof.
 Qed.
 
 Lemma erasable_tBox_value (wfl := Ee.default_wcbv_flags) (Σ : global_env_ext) (wfΣ : wf_ext Σ) t T v :
-  axiom_free Σ.1 ->
   forall wt : Σ ;;; [] |- t : T,
   Σ |-p t ▷ v -> erases Σ [] v tBox -> ∥ isErasable Σ [] t ∥.
 Proof.
   intros.
-  depind H0.
+  depind H.
   eapply Is_type_eval_inv; eauto. eexists; eauto.
 Qed.
 
 Lemma erase_eval_to_box (wfl := Ee.default_wcbv_flags) {Σ : global_env_ext}  {wfΣ : wf_ext Σ} {t v Σ' t' deps} :
-  axiom_free Σ.1 ->
   forall wt : welltyped Σ [] t,
   erase Σ (sq wfΣ) [] t wt = t' ->
   KernameSet.subset (term_global_deps t') deps ->
   erase_global deps Σ (sq wfΣ.1) = Σ' ->
   PCUICWcbvEval.eval Σ t v ->
   @Ee.eval Ee.default_wcbv_flags Σ' t' tBox -> ∥ isErasable Σ [] t ∥.
 Proof.
-  intros axiomfree [T wt].
+  intros [T wt].
   intros.
-  destruct (erase_correct Σ wfΣ _ _ _ _ _ axiomfree _ H H0 H1 X) as [ev [eg [eg']]].
+  destruct (erase_correct Σ wfΣ _ _ _ _ _ _ H H0 H1 X) as [ev [eg [eg']]].
   pose proof (Ee.eval_deterministic H2 eg'). subst.
   eapply erasable_tBox_value; eauto.
 Qed.
@@ -457,18 +455,16 @@ Proof.
 Qed.
 
 Lemma erase_opt_correct (wfl := Ee.default_wcbv_flags) (Σ : global_env_ext) (wfΣ : wf_ext Σ) t v Σ' t' :
-  axiom_free Σ.1 ->
   forall wt : welltyped Σ [] t,
   erase Σ (sq wfΣ) [] t wt = t' ->
   erase_global (term_global_deps t') Σ (sq wfΣ.1) = Σ' ->
   PCUICWcbvEval.eval Σ t v ->
   ∃ v' : term, Σ;;; [] |- v ⇝ℇ v' ∧ 
   ∥ @Ee.eval Ee.opt_wcbv_flags (optimize_env Σ') (optimize Σ' t') (optimize Σ' v') ∥.
 Proof.
-  intros axiomfree wt.
+  intros wt.
   generalize (sq wfΣ.1) as swfΣ.
   intros swfΣ HΣ' Ht' ev.
-  assert (extraction_pre Σ) by now constructor.
   pose proof (erases_erase (wfΣ := sq wfΣ) wt); eauto.
   rewrite HΣ' in H.
   destruct wt as [T wt].
@@ -485,5 +481,3 @@ Proof.
   eapply KernameSet.subset_spec.
   intros x hin; auto.
 Qed.
-
-Print Assumptions erase_opt_correct.

erasure/theories/ErasureCorrectness.v

@@ -429,14 +429,7 @@ Qed.
 
 (** ** The correctness proof  *)
 
-Record extraction_pre (Σ : global_env_ext) : Type
-  := Build_extraction_pre
-  { extr_env_axiom_free' : axiom_free (fst Σ);
-    extr_env_wf' : wf_ext Σ }.
-
 Hint Constructors PCUICWcbvEval.eval erases : core.
-Arguments extr_env_wf' {Σ}.
-Arguments extr_env_axiom_free' {Σ}.
 
 Definition EisConstruct_app :=
   fun t => match (EAstUtils.decompose_app t).1 with
@@ -682,16 +675,16 @@ Proof.
 Qed.
 
 Lemma erases_correct (wfl := default_wcbv_flags) Σ t T t' v Σ' :
-  extraction_pre Σ ->
+  wf_ext Σ ->
   Σ;;; [] |- t : T ->
   Σ;;; [] |- t ⇝ℇ t' ->  
   erases_deps Σ Σ' t' ->
   Σ |-p t ▷ v ->
   exists v', Σ;;; [] |- v ⇝ℇ v' /\ ∥ Σ' ⊢ t' ▷ v' ∥.
 Proof.
-  intros pre Hty He Hed H.
+  intros wfΣ Hty He Hed H.
   revert T Hty t' He Hed.
-  induction H; intros T Hty t' He Hed; destruct pre as [axfree wfΣ].
+  induction H; intros T Hty t' He Hed.
   - assert (Hty' := Hty).
     assert (eval Σ (PCUICAst.tApp f a) res) by eauto.
     eapply inversion_App in Hty as (? & ? & ? & ? & ? & ?).
@@ -805,10 +798,6 @@ Proof.
     + exists EAst.tBox. split. econstructor.
       eapply Is_type_eval. 3: eassumption. eauto. eauto. eauto. constructor. econstructor. eauto.
 
-  - destruct Σ as (Σ, univs).
-    cbn in *.
-    eapply axfree in isdecl. congruence.
-
   - assert (Hty' := Hty).
     assert (Σ |-p tCase (ind, pars) p discr brs ▷ res) by eauto.
     eapply inversion_Case in Hty' as [u' [args' [mdecl [idecl [ps [pty [btys 
@@ -906,7 +895,7 @@ Proof.
         eapply subject_reduction. eauto. exact Hty.
         etransitivity.
         eapply PCUICReduction.red_case_c. eapply wcbeval_red. eauto.
-        now eapply PCUICClosed.subject_closed in t0. eauto. eauto.
+        eauto. eauto.
 
         etransitivity. constructor. constructor.
         unfold iota_red. rewrite <- nth_default_eq. unfold nth_default.
@@ -949,7 +938,7 @@ Proof.
            eapply subject_reduction. eauto. exact Hty.
            etransitivity.
            eapply PCUICReduction.red_case_c. eapply wcbeval_red. eauto.
-           now eapply PCUICClosed.subject_closed in t0; eauto. eauto. eauto.
+           eauto. eauto.
            etransitivity. constructor. constructor.
            unfold iota_red. rewrite <- nth_default_eq. reflexivity.
 
@@ -1062,7 +1051,7 @@ Proof.
            eapply erases_deps_mkApps_inv in Hty_vc' as (? & ?).
            now eapply nth_error_forall in H1; eauto.
     + exists EAst.tBox. split. econstructor.
-      eapply Is_type_eval. 4: eassumption. all:eauto. constructor. econstructor. eauto.
+      eapply Is_type_eval. 3: eassumption. all:eauto. constructor. econstructor. eauto.
 
   - assert (Hty' := Hty).
     assert (Hunf := H).
@@ -1080,7 +1069,7 @@ Proof.
 
     + exists EAst.tBox. split; [|now constructor; constructor].
       econstructor.
-      eapply Is_type_eval. 4:eapply X. eauto. eauto.
+      eapply Is_type_eval. 3:eapply X. eauto.
       eapply eval_fix; eauto.
       rewrite /cunfold_fix e0 //. congruence.
     + depelim Hed.
@@ -1151,10 +1140,11 @@ Proof.
              assert(Σ ;;; [] |- mkApps (tFix mfix idx) (argsv ++ [av]) : PCUICLiftSubst.subst [av] 0 x1).
              { rewrite -mkApps_nested. eapply PCUICValidity.type_App'; eauto.
                eapply subject_reduction_eval; eauto. }
-             epose proof (fix_app_is_constructor Σ (args:=argsv ++ [av]) axfree X).
+             epose proof (fix_app_is_constructor Σ (args:=argsv ++ [av]) X).
              rewrite /unfold_fix e0 in X0.
              specialize (X0 eq_refl). simpl in X0.
              rewrite nth_error_snoc in X0. auto. apply X0.
+             eapply value_axiom_free, eval_to_value; eauto.
              eapply value_whnf; eauto.
              eapply eval_closed; eauto. now eapply PCUICClosed.subject_closed in t0.
              eapply eval_to_value; eauto. }
@@ -1214,7 +1204,7 @@ Proof.
         -- exists EAst.tBox.
            split.
            ++ econstructor.
-              eapply Is_type_eval. 4:eauto. all:eauto.
+              eapply Is_type_eval. 3:eauto. all:eauto.
               rewrite -mkApps_nested.
               eapply eval_fix; eauto. 
               1-2:eapply value_final, eval_to_value; eauto.
@@ -1232,7 +1222,7 @@ Proof.
     destruct Hty' as (? & ? & ? & ? & ? & ?).
 
     eapply subject_reduction in t as typ_stuck_fix; [|eauto|]; first last.
-    { eapply wcbeval_red. 4:eauto. all:eauto. }
+    { eapply wcbeval_red. 3:eauto. all:eauto. }
 
     eapply erases_App in He as He'; [|eauto].
     destruct He' as [(-> & [])|(? & ? & -> & ? & ?)].
@@ -1242,12 +1232,12 @@ Proof.
       eapply Is_type_red.
       * eauto.
       * eapply PCUICReduction.red_app.
-        -- eapply wcbeval_red; [eauto|eauto| |eauto]. eauto.
-        -- eapply wcbeval_red; [eauto|eauto| |eauto]. eauto.
+        -- eapply wcbeval_red; [eauto| |eauto]. eauto.
+        -- eapply wcbeval_red; [eauto| |eauto]. eauto.
       * eauto.
     + depelim Hed.
       eapply subject_reduction in t0 as typ_arg; [|eauto|]; first last.
-      { eapply wcbeval_red; [eauto|eauto| |eauto]. eauto. }
+      { eapply wcbeval_red; [eauto| |eauto]. eauto. }
 
       eapply IHeval1 in H1 as (? & ? & [?]); [|now eauto|now eauto].
       eapply IHeval2 in H2 as (? & ? & [?]); [|now eauto|now eauto].

erasure/theories/ErasureFunction.v

@@ -1187,18 +1187,16 @@ Proof.
 Qed.
 
 Lemma erase_correct (wfl := Ee.default_wcbv_flags) (Σ : global_env_ext) (wfΣ : wf_ext Σ) t v Σ' t' deps :
-  axiom_free Σ.1 ->
   forall wt : welltyped Σ [] t,
   erase Σ (sq wfΣ) [] t wt = t' ->
   KernameSet.subset (term_global_deps t') deps ->
   erase_global deps Σ (sq (wfΣ.1)) = Σ' ->
   Σ |-p t ▷ v ->
   exists v', Σ;;; [] |- v ⇝ℇ v' /\ ∥ Σ' ⊢ t' ▷ v' ∥.
 Proof.
-  intros axiomfree wt.
+  intros wt.
   generalize (sq wfΣ.1) as swfΣ.
   intros swfΣ HΣ' Hsub Ht' ev.
-  assert (extraction_pre Σ) by now constructor.
   pose proof (erases_erase (wfΣ := sq wfΣ) wt); eauto.
   rewrite HΣ' in H.
   destruct wt as [T wt].

erasure/theories/Prelim.v

@@ -16,8 +16,6 @@ Module P := PCUICWcbvEval.
 
 Ltac inv H := inversion H; subst; clear H.
 
-Existing Class axiom_free.
-
 Lemma nth_error_app_inv X (x : X) n l1 l2 :
   nth_error (l1 ++ l2) n = Some x -> (n < #|l1| /\ nth_error l1 n = Some x) \/ (n >= #|l1| /\ nth_error l2 (n - List.length l1) = Some x).
 Proof.
@@ -121,7 +119,7 @@ Proof.
   now exists A.
 Qed.
 
-Theorem subject_reduction_eval {Σ :global_env_ext} {t u T} {wfΣ : wf Σ} {axfree : axiom_free Σ} :
+Theorem subject_reduction_eval {Σ :global_env_ext} {t u T} {wfΣ : wf Σ} :
   Σ ;;; [] |- t : T -> PCUICWcbvEval.eval Σ t u -> Σ ;;; [] |- u : T.
 Proof.
   intros Hty Hred.
@@ -133,7 +131,7 @@ Lemma typing_spine_eval:
   (X : All2 (PCUICWcbvEval.eval Σ) args args') (bla : wf Σ)
     (T x x0 : PCUICAst.term) (t0 : typing_spine Σ [] x args x0) 
     (c : Σ;;; [] |- x0 <= T) (x1 : PCUICAst.term)
-    (c0 : Σ;;; [] |- x1 <= x), axiom_free Σ -> isType Σ [] T -> typing_spine Σ [] x1 args' T.
+    (c0 : Σ;;; [] |- x1 <= x), isType Σ [] T -> typing_spine Σ [] x1 args' T.
 Proof.
   intros. eapply typing_spine_red; eauto.
   eapply typing_spine_wt in t0; auto.