Merge pull request #538 from jakobbotsch/eval-no-axioms

Remove evaluation of axioms from wcbv and add proof of consistency using safe reduction + canonicity
MetaCoq · Jan 4, 2021 · 8d576c7 · 8d576c7
2 parents 18d18e0 + f1655e7
commit 8d576c7
Show file tree

Hide file tree

Showing 10 changed files with 368 additions and 460 deletions.
diff --git a/erasure/theories/EArities.v b/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]]].

diff --git a/erasure/theories/EOptimizePropDiscr.v b/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.
diff --git a/erasure/theories/ErasureCorrectness.v b/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].

diff --git a/erasure/theories/ErasureFunction.v b/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].

diff --git a/erasure/theories/Prelim.v b/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.