From f0f58ccabdf52ed665c73217ebe862e6b38bd78e Mon Sep 17 00:00:00 2001 From: Jakob Botsch Nielsen Date: Thu, 17 Dec 2020 11:48:14 +0100 Subject: [PATCH 1/2] 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. --- erasure/theories/EArities.v | 4 +- erasure/theories/EOptimizePropDiscr.v | 14 +-- erasure/theories/ErasureCorrectness.v | 38 +++--- erasure/theories/ErasureFunction.v | 4 +- erasure/theories/Prelim.v | 6 +- pcuic/theories/PCUICCanonicity.v | 165 +++++++++++++++++--------- pcuic/theories/PCUICWcbvEval.v | 65 +--------- template-coq/theories/WcbvEval.v | 62 +--------- 8 files changed, 141 insertions(+), 217 deletions(-) diff --git a/erasure/theories/EArities.v b/erasure/theories/EArities.v index 9637f483f..7918dda63 100644 --- 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 index d995ae094..0307689b9 100644 --- a/erasure/theories/EOptimizePropDiscr.v +++ b/erasure/theories/EOptimizePropDiscr.v @@ -232,17 +232,15 @@ 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 -> @@ -250,9 +248,9 @@ Lemma erase_eval_to_box (wfl := Ee.default_wcbv_flags) {Σ : global_env_ext} {w 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,7 +455,6 @@ 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) = Σ' -> @@ -465,10 +462,9 @@ Lemma erase_opt_correct (wfl := Ee.default_wcbv_flags) (Σ : global_env_ext) (wf ∃ 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. \ No newline at end of file diff --git a/erasure/theories/ErasureCorrectness.v b/erasure/theories/ErasureCorrectness.v index ab746583e..2112a51a2 100644 --- 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 index 31429f511..247fd006d 100644 --- a/erasure/theories/ErasureFunction.v +++ b/erasure/theories/ErasureFunction.v @@ -1187,7 +1187,6 @@ 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 -> @@ -1195,10 +1194,9 @@ Lemma erase_correct (wfl := Ee.default_wcbv_flags) (Σ : global_env_ext) (wfΣ : Σ |-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 index 3746e7034..042748fdb 100644 --- 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. diff --git a/pcuic/theories/PCUICCanonicity.v b/pcuic/theories/PCUICCanonicity.v index abc7b956d..52f3d911d 100644 --- a/pcuic/theories/PCUICCanonicity.v +++ b/pcuic/theories/PCUICCanonicity.v @@ -802,7 +802,7 @@ Section WeakNormalization. Transparent construct_cofix_discr. - Lemma value_whnf t : closed t -> value Σ t -> wh_normal Σ [] t. + Lemma value_whnf t : closed t -> value t -> wh_normal Σ [] t. Proof. intros cl ev. induction ev in cl |- * using value_values_ind. @@ -814,10 +814,6 @@ Section WeakNormalization. now rewrite nth_error_nil. - eapply (whnf_cofixapp _ _ [] _ _ []). - unfold value_head in H. destruct t => //. - constructor; eapply whne_mkApps. - cbn in H; destruct lookup_env eqn:eq => //. - destruct g => //. destruct c => //. destruct cst_body => //. - eapply whne_const; eauto. - destruct f => //. cbn in H. destruct cunfold_fix as [[rarg body]|] eqn:unf => //. pose proof cl as cl'. @@ -1014,41 +1010,92 @@ Section WeakNormalization. eapply PCUICConfluence.red_mkApps_tInd in r as [? [eq _]]; auto. solve_discr. Qed. - - Lemma wh_neutral_empty_gen t Γ : axiom_free Σ -> wh_neutral Σ Γ t -> forall ty, Σ ;;; Γ |- t : ty -> Γ = [] -> False - with wh_normal_empty_gen t Γ i u args : axiom_free Σ -> wh_normal Σ Γ t -> Σ ;;; Γ |- t : mkApps (tInd i u) args -> - Γ = [] -> construct_cofix_discr (head t). + + Fixpoint axiom_free_value Σ args t := + match t with + | tApp hd arg => axiom_free_value Σ (axiom_free_value Σ [] arg :: args) hd + | tConst kn _ => match lookup_env Σ kn with + | Some (ConstantDecl {| cst_body := Some _ |}) => true + | _ => false + end + | tCase _ _ discr _ => axiom_free_value Σ [] discr + | tProj _ t => axiom_free_value Σ [] t + | tFix defs i => + match nth_error defs i with + | Some def => nth (rarg def) args true + | None => true + end + | _ => true + end. + + Lemma axiom_free_value_mkApps Σ' args hd args' : + axiom_free_value Σ' args (mkApps hd args') = + axiom_free_value Σ' (map (axiom_free_value Σ' []) args' ++ args) hd. Proof. - intros axfree ne ty typed. - 2:intros axfree ne typed. - all:pose proof (subject_closed wfΣ typed) as cl; - destruct ne; intros eqΓ; simpl in *; try discriminate. - - rewrite eqΓ in cl => //. + revert hd args. + induction args' using MCList.rev_ind; intros hd args; cbn; auto. + rewrite -mkApps_nested /=. + rewrite IHargs'. + now rewrite map_app /= -app_assoc. + Qed. + + Lemma wh_neutral_empty_gen Γ free t ty : + axiom_free_value Σ free t -> + wh_neutral Σ [] t -> + Σ ;;; Γ |- t : ty -> + Γ = [] -> + False. + Proof. + intros axfree ne typed. + induction ne in free, t, ty, axfree, ne, typed |- *; intros ->; simpl in *; try discriminate. + - apply inversion_Rel in typed as (?&?&?&?); auto. + rewrite nth_error_nil in e0; discriminate. - now eapply typing_var in typed. - now eapply typing_evar in typed. - - clear wh_neutral_empty_gen wh_normal_empty_gen. subst. - apply inversion_Const in typed as [decl' [wfd [declc [cu cum]]]]; eauto. - specialize (axfree _ _ declc). - red in declc. rewrite declc in e. noconf e. congruence. - - simpl in cl; move/andP: cl => [clf cla]. - eapply inversion_App in typed as [na [A [B [Hf _]]]]; eauto. - - specialize (wh_neutral_empty_gen _ _ axfree ne). subst. - simpl in cl. - eapply inversion_mkApps in typed as (? & ? & ?); eauto. + - apply inversion_Const in typed as [decl' [wfd [declc [cu cum]]]]; eauto. + red in declc. + rewrite declc in e, axfree. + noconf e. + destruct decl; cbn in *. + rewrite e0 in axfree; congruence. + - eapply inversion_App in typed as [na [A [B [Hf _]]]]; eauto. + - eapply inversion_mkApps in typed as (? & ? & ?); eauto. eapply inversion_Fix in t as (? & ? & ? & ? & ? & ? & ?); auto. eapply typing_spine_strengthen in t0; eauto. eapply nth_error_all in a; eauto. simpl in a. rewrite /unfold_fix in e. rewrite e1 in e. noconf e. eapply (wf_fixpoint_spine wfΣ) in t0; eauto. rewrite e0 in t0. destruct t0 as [ind [u [indargs [tyarg ckind]]]]. - clear wh_normal_empty_gen. - now specialize (wh_neutral_empty_gen _ tyarg eq_refl). - - move/andP: cl => [/andP[_ clc] _]. - eapply inversion_Case in typed as (? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ?); auto. - eapply wh_neutral_empty_gen; eauto. - - eapply inversion_Proj in typed as (? & ? & ? & ? & ? & ? & ? & ? & ?); auto. - eapply wh_neutral_empty_gen; eauto. - - eapply wh_neutral_empty_gen in w; eauto. + rewrite axiom_free_value_mkApps in axfree. + cbn in axfree. + rewrite e1 nth_nth_error nth_error_app1 in axfree. + 1: { rewrite map_length. + apply nth_error_Some_length in e0; auto. } + rewrite nth_error_map e0 in axfree. + cbn in axfree. + eauto. + - eapply inversion_Case in typed as + (? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ? & ?); eauto. + - eapply inversion_Proj in typed as (? & ? & ? & ? & ? & ? & ? & ? & ?); eauto. + Qed. + + Lemma wh_neutral_empty t ty : + axiom_free_value Σ [] t -> + wh_neutral Σ [] t -> + Σ ;;; [] |- t : ty -> + False. + Proof. eauto using wh_neutral_empty_gen. Qed. + + Lemma wh_normal_ind_discr t i u args : + axiom_free_value Σ [] t -> + wh_normal Σ [] t -> + Σ ;;; [] |- t : mkApps (tInd i u) args -> + construct_cofix_discr (head t). + Proof. + intros axfree ne typed. + pose proof (subject_closed wfΣ typed) as cl. + depelim ne; simpl in *. + - eauto using wh_neutral_empty. - eapply inversion_Sort in typed as (? & ? & ?); auto. eapply invert_cumul_sort_l in c as (? & ? & ?); auto. eapply red_mkApps_tInd in r as (? & eq & ?); eauto; eauto. @@ -1068,20 +1115,8 @@ Section WeakNormalization. - now eapply inversion_Prim in typed. Qed. - Lemma wh_neutral_empty t ty : axiom_free Σ -> - Σ ;;; [] |- t : ty -> - wh_neutral Σ [] t -> - False. - Proof. intros; eapply wh_neutral_empty_gen; eauto. Qed. - - Lemma wh_normal_ind_discr t i u args : axiom_free Σ -> - Σ ;;; [] |- t : mkApps (tInd i u) args -> - wh_normal Σ [] t -> - construct_cofix_discr (head t). - Proof. intros. eapply wh_normal_empty_gen; eauto. Qed. - Lemma whnf_ind_finite t ind u indargs : - axiom_free Σ -> + axiom_free_value Σ [] t -> Σ ;;; [] |- t : mkApps (tInd ind u) indargs -> wh_normal Σ [] t -> check_recursivity_kind Σ (inductive_mind ind) Finite -> @@ -1099,15 +1134,14 @@ Section WeakNormalization. Qed. Lemma fix_app_is_constructor {mfix idx args ty narg fn} : - axiom_free Σ -> Σ;;; [] |- mkApps (tFix mfix idx) args : ty -> unfold_fix mfix idx = Some (narg, fn) -> match nth_error args narg return Type with - | Some a => wh_normal Σ [] a -> isConstruct_app a + | Some a => axiom_free_value Σ [] a -> wh_normal Σ [] a -> isConstruct_app a | None => ∑ na dom codom, Σ ;;; [] |- tProd na dom codom <= ty end. Proof. - intros axfree typed unf. + intros typed unf. eapply inversion_mkApps in typed as (? & ? & ?); eauto. eapply inversion_Fix in t as (? & ? & ? & ? & ? & ? & ?); auto. eapply typing_spine_strengthen in t0; eauto. @@ -1117,10 +1151,32 @@ Section WeakNormalization. eapply (wf_fixpoint_spine wfΣ) in t0; eauto. rewrite /is_constructor. destruct (nth_error args (rarg x0)) eqn:hnth. destruct_sigma t0. destruct t0. - intros norm. + intros axfree norm. eapply whnf_ind_finite in t0; eauto. assumption. Qed. + + Lemma value_axiom_free Σ' t : + value t -> + axiom_free_value Σ' [] t. + Proof. + intros val. + induction val using value_values_ind. + - destruct t; try discriminate; auto. + cbn. + destruct ?; auto. + destruct ?; auto. + - rewrite axiom_free_value_mkApps. + destruct t; auto. + - rewrite axiom_free_value_mkApps. + destruct f; try discriminate. + cbn. + unfold isStuckFix, cunfold_fix in H. + destruct nth_error; auto. + rewrite nth_overflow; auto. + rewrite app_nil_r map_length; auto. + toProp; auto. + Qed. (** Evaluation on well-typed terms corresponds to reduction. It differs in two ways from standard reduction: @@ -1129,11 +1185,10 @@ Section WeakNormalization. have a constructor at their recursive argument as it is ensured by typing. *) Lemma wcbeval_red t ty u : - axiom_free Σ -> Σ ;;; [] |- t : ty -> eval Σ t u -> red Σ [] t u. Proof. - intros axfree Hc He. + intros Hc He. revert ty Hc. induction He; simpl; move=> ty Ht; try solve[econstructor; eauto]. @@ -1220,7 +1275,7 @@ Section WeakNormalization. eapply red_fix; eauto. assert (Σ ;;; [] |- mkApps (tFix mfix idx) (argsv ++ [av]) : B {0 := av}). { rewrite -mkApps_nested /=. eapply type_App'; eauto. } - epose proof (fix_app_is_constructor axfree X0 e); eauto. + epose proof (fix_app_is_constructor X0 e); eauto. rewrite /is_constructor. destruct nth_error eqn:hnth => //. assert (All (closedn 0) (argsv ++ [av])). @@ -1228,7 +1283,7 @@ Section WeakNormalization. rewrite closedn_mkApps in X0. move/andP: X0 => [clfix clargs]. now eapply forallb_All in clargs. } - assert (All (value Σ) (argsv ++ [av])). + assert (All value (argsv ++ [av])). { eapply All_app_inv; [|constructor; [|constructor]]. eapply eval_to_value in He1. eapply value_mkApps_inv in He1 as [[[-> Hat]|[vh vargs]]|[hstuck vargs]] => //. @@ -1236,6 +1291,7 @@ Section WeakNormalization. solve_all. eapply nth_error_all in X3; eauto. simpl in X3. destruct X3 as [cl val]. eapply X1, value_whnf; auto. + eapply value_axiom_free; auto. eapply nth_error_None in hnth; len in hnth; simpl in *. lia. } redt _; eauto. @@ -1273,14 +1329,15 @@ Section WeakNormalization. Qed. Lemma eval_ind_canonical t i u args : - axiom_free Σ -> Σ ;;; [] |- t : mkApps (tInd i u) args -> forall t', eval Σ t t' -> construct_cofix_discr (head t'). Proof. - intros axfree Ht t' eval. + intros Ht t' eval. pose proof (subject_closed wfΣ Ht). eapply subject_reduction in Ht. 3:eapply wcbeval_red; eauto. 2:auto. + eapply eval_to_value in eval as axfree. + eapply value_axiom_free in axfree. eapply eval_whne in eval; auto. eapply wh_normal_ind_discr; eauto. Qed. diff --git a/pcuic/theories/PCUICWcbvEval.v b/pcuic/theories/PCUICWcbvEval.v index d5b17f105..772cbd61a 100644 --- a/pcuic/theories/PCUICWcbvEval.v +++ b/pcuic/theories/PCUICWcbvEval.v @@ -93,26 +93,6 @@ Definition isConstruct t := | _ => false end. -Definition isAssRel Γ x := - match x with - | tRel i => - match option_map decl_body (nth_error Γ i) with - | Some None => true - | _ => false - end - | _ => false - end. - -Definition isAxiom Σ x := - match x with - | tConst c u => - match lookup_env Σ c with - | Some (ConstantDecl {| cst_body := None |}) => true - | _ => false - end - | _ => false - end. - Definition substl defs body : term := fold_left (fun bod term => csubst term 0 bod) defs body. @@ -165,29 +145,12 @@ Section Wcbv. eval (csubst b0' 0 b1) res -> eval (tLetIn na b0 t b1) res - (** - (** Local variables: defined or undefined *) - | eval_rel_def i body res : - option_map decl_body (nth_error Γ i) = Some (Some body) -> - eval (lift0 (S i) body) res -> - eval (tRel i) res - - | eval_rel_undef i : - option_map decl_body (nth_error Γ i) = Some None -> - eval (tRel i) (tRel i) - *) - (** Constant unfolding *) | eval_delta c decl body (isdecl : declared_constant Σ c decl) u res : decl.(cst_body) = Some body -> eval (subst_instance_constr u body) res -> eval (tConst c u) res - (** Axiom *) - | eval_axiom c decl (isdecl : declared_constant Σ c decl) u : - decl.(cst_body) = None -> - eval (tConst c u) (tConst c u) - (** Case *) | eval_iota ind pars discr c u args p brs res : eval discr (mkApps (tConstruct ind c u) args) -> @@ -257,14 +220,13 @@ Section Wcbv. *) Definition value_head x := - isInd x || isConstruct x || isCoFix x || isAxiom Σ x. + isInd x || isConstruct x || isCoFix x. (* Lemma value_head_atom x : value_head x -> atom x. *) (* Proof. destruct x; auto. Qed. *) Inductive value : term -> Type := | value_atom t : atom t -> value t - (* | value_evar n l l' : Forall value l -> Forall value l' -> value (mkApps (tEvar n l) l') *) | value_app t l : value_head t -> All value l -> value (mkApps t l) | value_stuck_fix f args : All value args -> @@ -274,8 +236,6 @@ Section Wcbv. Lemma value_values_ind : forall P : term -> Type, (forall t, atom t -> P t) -> - (* (forall n l l', Forall value l -> Forall P l -> Forall value l' -> Forall P l' -> *) - (* P (mkApps (tEvar n l) l')) -> *) (forall t l, value_head t -> All value l -> All P l -> P (mkApps t l)) -> (forall f args, All value args -> @@ -335,11 +295,6 @@ Section Wcbv. Lemma eval_to_value e e' : eval e e' -> value e'. Proof. induction 1; simpl; auto using value. - - eapply (value_app (tConst c u) []). - red in isdecl. - rewrite /value_head /= isdecl. - destruct decl as [? [b|] ?]; try discriminate. - constructor. constructor. - change (tApp ?h ?a) with (mkApps h [a]). rewrite mkApps_nested. apply value_mkApps_inv in IHX1; [|easy]. @@ -443,15 +398,6 @@ Section Wcbv. move/(_ H) => Ht. induction l using rev_ind. simpl. destruct t; try discriminate. - (* * constructor. - unfold value_head in H. simpl in H. destruct option_map as [[o|]|] => //. *) - * unfold value_head in H. simpl in H. - destruct lookup_env eqn:Heq => //. - destruct g eqn:Heq' => //. - destruct c as [? [b|] ?] eqn:Heq'' => //. subst. - eapply eval_axiom. red. - rewrite Heq. reflexivity. - easy. * now eapply eval_atom. * now eapply eval_atom. * now eapply eval_atom. @@ -723,10 +669,6 @@ Section Wcbv. assert (e0 = e) as -> by now apply uip. assert (isdecl0 = isdecl) as -> by now apply uip. now specialize (IHev _ ev'); noconf IHev. - - depelim ev'; try go. - pose proof (PCUICWeakeningEnv.declared_constant_inj _ _ isdecl isdecl0) as <-. - assert (isdecl0 = isdecl) as -> by now apply uip. - now assert (e0 = e) as -> by now apply uip. - depelim ev'; try go. + specialize (IHev1 _ ev'1); noconf IHev1. apply (f_equal pr1) in IHev1 as apps_eq; cbn in *. @@ -861,13 +803,10 @@ Section Wcbv. ∑ decl, declared_constant Σ c decl * match cst_body decl with | Some body => eval (subst_instance_constr u body) v - | None => v = tConst c u + | None => False end. Proof. intros H; depelim H. - - exists decl. - split; [easy|]. - now rewrite e. - exists decl. split; [easy|]. now rewrite e. diff --git a/template-coq/theories/WcbvEval.v b/template-coq/theories/WcbvEval.v index 6aa05b0b9..ad96f1edf 100644 --- a/template-coq/theories/WcbvEval.v +++ b/template-coq/theories/WcbvEval.v @@ -71,26 +71,6 @@ Definition isConstruct t := | _ => false end. -Definition isAssRel Γ x := - match x with - | tRel i => - match option_map decl_body (nth_error Γ i) with - | Some None => true - | _ => false - end - | _ => false - end. - -Definition isAxiom Σ x := - match x with - | tConst c u => - match lookup_env Σ c with - | Some (ConstantDecl {| cst_body := None |}) => true - | _ => false - end - | _ => false - end. - Definition isStuckFix t args := match t with | tFix mfix idx => @@ -128,27 +108,18 @@ Section Wcbv. eval (subst10 b0' b1) res -> eval (tLetIn na b0 t b1) res - (** Local variables: defined or undefined *) + (** Local variable with bodies *) | eval_rel_def i body res : option_map decl_body (nth_error Γ i) = Some (Some body) -> eval (lift0 (S i) body) res -> eval (tRel i) res - | eval_rel_undef i : - option_map decl_body (nth_error Γ i) = Some None -> - eval (tRel i) (tRel i) - (** Constant unfolding *) | eval_delta c decl body (isdecl : declared_constant Σ c decl) u res : decl.(cst_body) = Some body -> eval (subst_instance_constr u body) res -> eval (tConst c u) res - (** Axiom *) - | eval_axiom c decl (isdecl : declared_constant Σ c decl) u : - decl.(cst_body) = None -> - eval (tConst c u) (tConst c u) - (** Case *) | eval_iota ind pars r discr c u args p brs res : eval discr (mkApps (tConstruct ind c u) args) -> @@ -223,14 +194,11 @@ Section Wcbv. (forall (i : nat) (body res : term), option_map decl_body (nth_error Γ i) = Some (Some body) -> eval ((lift0 (S i)) body) res -> P ((lift0 (S i)) body) res -> P (tRel i) res) -> - (forall i : nat, option_map decl_body (nth_error Γ i) = Some None -> P (tRel i) (tRel i)) -> (forall c (decl : constant_body) (body : term), declared_constant Σ c decl -> forall (u : Instance.t) (res : term), cst_body decl = Some body -> eval (subst_instance_constr u body) res -> P (subst_instance_constr u body) res -> P (tConst c u) res) -> - (forall c (decl : constant_body), - declared_constant Σ c decl -> forall u : Instance.t, cst_body decl = None -> P (tConst c u) (tConst c u)) -> (forall (ind : inductive) (pars : nat) r (discr : term) (c : nat) (u : Instance.t) (args : list term) (p : term) (brs : list (nat × term)) (res : term), eval discr (mkApps (tConstruct ind c u) args) -> @@ -277,15 +245,13 @@ Section Wcbv. All2 eval a a' -> All2 P a a' -> P (tApp f a) (mkApps f' a')) -> (forall t : term, atom t -> P t t) -> forall t t0 : term, eval t t0 -> P t t0. Proof. - intros P Hbeta Hlet Hreldef Hrelvar Hcst Hax Hcase Hproj Hfix Hstuckfix Hcofixcase Hcofixproj Happcong Hatom. + intros P Hbeta Hlet Hreldef Hcst Hcase Hproj Hfix Hstuckfix Hcofixcase Hcofixproj Happcong Hatom. fix eval_evals_ind 3. destruct 1; try solve [match goal with [ H : _ |- _ ] => match type of H with forall t t0, eval t t0 -> _ => fail 1 | _ => eapply H end end; eauto]. - - eapply Hrelvar, e. - - eapply Hax; [eapply isdecl|eapply e]. - eapply Hfix; eauto. clear -a eval_evals_ind. revert args argsv a. @@ -308,7 +274,7 @@ Section Wcbv. *) Definition value_head x := - isConstruct x || isCoFix x || isAssRel Γ x || isAxiom Σ x. + isConstruct x || isCoFix x. (* Lemma value_head_atom x : value_head x -> atom x. *) (* Proof. destruct x; auto. Qed. *) @@ -390,12 +356,6 @@ Section Wcbv. Proof. intros eve. induction eve using eval_evals_ind; simpl; intros; auto using value. - - eapply (value_app (tRel i) []). now rewrite /value_head /= H. constructor. - - eapply (value_app (tConst c u) []). - red in H. - rewrite /value_head /= H. - destruct decl as [? [b|] ?]; try discriminate. - constructor. constructor. - eapply value_stuck_fix. + apply All_app_inv. * now eapply value_mkApps_values. @@ -433,17 +393,8 @@ Section Wcbv. eval t t. Proof. destruct t; intros vt nt; try discriminate. - * constructor. - unfold value_head in vt. simpl in vt. destruct option_map as [[o|]|] => //. - * unfold value_head in vt. simpl in vt. - destruct lookup_env eqn:Heq => //. - destruct g eqn:Heq' => //. - destruct c0 as [? [b|] ?] eqn:Heq'' => //. subst. - intros. eapply eval_axiom. red. - now rewrite Heq. - easy. - * now eapply eval_atom. - * now eapply eval_atom. + - now eapply eval_atom. + - now eapply eval_atom. Qed. Lemma value_final e : value e -> eval e e. @@ -584,12 +535,11 @@ Section Wcbv. ∑ decl, declared_constant Σ c decl * match cst_body decl with | Some body => eval (subst_instance_constr u body) v - | None => v = tConst c u + | None => False end. Proof. intros H; depind H; try solve_discr'; try now easy. - exists decl. intuition auto. now rewrite e. - - exists decl. intuition auto. now rewrite e. - symmetry in H1. eapply mkApps_nisApp in H1 => //; intuition subst; auto. depelim a. eapply eval_to_stuck_fix_inv in H; [|easy]. From f1655e7d22e4d385bec489754167b9943fbe0877 Mon Sep 17 00:00:00 2001 From: Jakob Botsch Nielsen Date: Thu, 17 Dec 2020 12:56:30 +0100 Subject: [PATCH 2/2] Add a proof of consistency using safe reduction and canonicity --- pcuic/theories/PCUICCanonicity.v | 253 +----------------------- safechecker/_CoqProject.in | 1 + safechecker/theories/PCUICConsistency.v | 220 +++++++++++++++++++++ 3 files changed, 229 insertions(+), 245 deletions(-) create mode 100644 safechecker/theories/PCUICConsistency.v diff --git a/pcuic/theories/PCUICCanonicity.v b/pcuic/theories/PCUICCanonicity.v index 52f3d911d..86594c38b 100644 --- a/pcuic/theories/PCUICCanonicity.v +++ b/pcuic/theories/PCUICCanonicity.v @@ -606,188 +606,6 @@ Section Spines. End Spines. -(* -Section Normalization. - Context {cf:checker_flags} (Σ : global_env_ext). - Context {wfΣ : wf Σ}. - - Section reducible. - Lemma reducible Γ t : sum (∑ t', red1 Σ Γ t t') (forall t', red1 Σ Γ t t' -> False). - Proof. - Local Ltac lefte := left; eexists; econstructor; eauto. - Local Ltac leftes := left; eexists; econstructor; solve [eauto]. - Local Ltac righte := right; intros t' red; depelim red; solve_discr; eauto 2. - induction t in Γ |- * using term_forall_list_ind. - (*all:try solve [righte]. - - destruct (nth_error Γ n) eqn:hnth. - destruct c as [na [b|] ty]; [lefte|righte]. - * rewrite hnth; reflexivity. - * rewrite hnth /= // in e. - * righte. rewrite hnth /= // in e. - - admit. - - destruct (IHt1 Γ) as [[? ?]|]; [lefte|]. - destruct (IHt2 (Γ ,, vass n t1)) as [[? ?]|]; [|righte]. - leftes. - - destruct (IHt1 Γ) as [[? ?]|]; [lefte|]. - destruct (IHt2 (Γ ,, vass n t1)) as [[? ?]|]; [|righte]. - leftes. - - destruct (IHt1 Γ) as [[? ?]|]; [lefte|]. - destruct (IHt2 Γ) as [[? ?]|]; [lefte|]. - destruct (IHt3 (Γ ,, vdef n t1 t2)) as [[? ?]|]; [|]. - leftes. lefte. - - destruct (IHt1 Γ) as [[? ?]|]; [lefte|]. - destruct (IHt2 Γ) as [[? ?]|]; [leftes|]. - destruct (PCUICParallelReductionConfluence.view_lambda_fix_app t1 t2). - * rewrite [tApp _ _](mkApps_nested _ _ [a]). - destruct (unfold_fix mfix i) as [[rarg body]|] eqn:unf. - destruct (is_constructor rarg (l ++ [a])) eqn:isc; [leftes|]; eauto. - right => t' red; depelim red; solve_discr; eauto. - rewrite -mkApps_nested in H. noconf H. eauto. - rewrite -mkApps_nested in H. noconf H. eauto. - eapply (f_equal (@length _)) in H1. rewrite /= app_length /= // in H1; lia. - eapply (f_equal (@length _)) in H1. rewrite /= app_length /= // in H1; lia. - righte; try (rewrite -mkApps_nested in H; noconf H); eauto. - eapply (f_equal (@length _)) in H1. rewrite /= app_length /= // in H1; lia. - eapply (f_equal (@length _)) in H1. rewrite /= app_length /= // in H1; lia. - * admit. - * righte. destruct args using rev_case; solve_discr; noconf H. - rewrite H in i. eapply negb_False; eauto. - rewrite -mkApps_nested; eapply isFixLambda_app_mkApps' => //. - - admit. - - admit. - - admit. - - admit. - - admit.*) - - Admitted. - End reducible. - - Lemma reducible' Γ t : sum (∑ t', red1 Σ Γ t t') (normal Σ Γ t). - Proof. - Ltac lefte := left; eexists; econstructor; eauto. - Ltac leftes := left; eexists; econstructor; solve [eauto]. - Ltac righte := right; (solve [repeat (constructor; eauto)])||(repeat constructor). - induction t in Γ |- * using term_forall_list_ind. - all:try solve [righte]. - - destruct (nth_error Γ n) eqn:hnth. - destruct c as [na [b|] ty]; [lefte|]. - * rewrite hnth; reflexivity. - * right. do 2 constructor; rewrite hnth /= //. - * righte. rewrite hnth /= //. - - admit. - - destruct (IHt1 Γ) as [[? ?]|]; [lefte|]. - destruct (IHt2 (Γ ,, vass n t1)) as [[? ?]|]; [|]. - leftes. right; solve[constructor; eauto]. - - destruct (IHt1 Γ) as [[? ?]|]; [lefte|]. - destruct (IHt2 (Γ ,, vass n t1)) as [[? ?]|]; [leftes|leftes]. - - destruct (IHt1 Γ) as [[? ?]|]; [lefte|]. - destruct (IHt2 Γ) as [[? ?]|]; [leftes|]. - destruct (PCUICParallelReductionConfluence.view_lambda_fix_app t1 t2). - * rewrite [tApp _ _](mkApps_nested _ _ [a]). - destruct (unfold_fix mfix i) as [[rarg body]|] eqn:unf. - destruct (is_constructor rarg (l ++ [a])) eqn:isc; [leftes|]; eauto. - right; constructor. rewrite -mkApps_nested. constructor. admit. admit. admit. - * admit. - * admit. - - admit. - - admit. - - admit. - - admit. - - admit. - Admitted. - - Lemma normalizer {Γ t ty} : - Σ ;;; Γ |- t : ty -> - ∑ nf, (red Σ.1 Γ t nf) * normal Σ Γ nf. - Proof. - intros Hty. - unshelve epose proof (PCUICSN.normalisation Σ Γ t (iswelltyped _ _ _ ty Hty)). - clear ty Hty. - move: t H. eapply Fix_F. - intros x IH. - destruct (reducible' Γ x) as [[t' red]|nred]. - specialize (IH t'). forward IH by (constructor; auto). - destruct IH as [nf [rednf norm]]. - exists nf; split; auto. now transitivity t'. - exists x. split; [constructor|assumption]. - Qed. - - Derive Signature for neutral normal. - - Lemma typing_var {Γ n ty} : Σ ;;; Γ |- (tVar n) : ty -> False. - Proof. intros Hty; depind Hty; eauto. Qed. - - Lemma typing_evar {Γ n l ty} : Σ ;;; Γ |- (tEvar n l) : ty -> False. - Proof. intros Hty; depind Hty; eauto. Qed. - - Definition axiom_free Σ := - forall c decl, declared_constant Σ c decl -> cst_body decl <> None. - - Lemma neutral_empty t ty : axiom_free Σ -> Σ ;;; [] |- t : ty -> neutral Σ [] t -> False. - Proof. - intros axfree typed ne. - pose proof (PCUICClosed.subject_closed wfΣ typed) as cl. - depind ne. - - now simpl in cl. - - now eapply typing_var in typed. - - now eapply typing_evar in typed. - - eapply inversion_Const in typed as [decl [wfd [declc [cu cum]]]]; eauto. - specialize (axfree _ _ declc). specialize (H decl). - destruct (cst_body decl); try congruence. - now specialize (H t declc eq_refl). - - simpl in cl; move/andP: cl => [clf cla]. - eapply inversion_App in typed as [na [A [B [Hf _]]]]; eauto. - - simpl in cl; move/andP: cl => [/andP[_ clc] _]. - eapply inversion_Case in typed; pcuicfo eauto. - - eapply inversion_Proj in typed; pcuicfo auto. - Qed. - - Lemma ind_normal_constructor t i u args : - axiom_free Σ -> - Σ ;;; [] |- t : mkApps (tInd i u) args -> normal Σ [] t -> construct_cofix_discr (head t). - Proof. - intros axfree Ht capp. destruct capp. - - eapply neutral_empty in H; eauto. - - eapply inversion_Sort in Ht as (? & ? & ? & ? & ?); auto. - eapply invert_cumul_sort_l in c as (? & ? & ?). - eapply red_mkApps_tInd in r as (? & eq & ?); eauto; eauto. - solve_discr. - - eapply inversion_Prod in Ht as (? & ? & ? & ? & ?); auto. - eapply invert_cumul_sort_l in c as (? & ? & ?). - eapply red_mkApps_tInd in r as (? & eq & ?); eauto; eauto. - solve_discr. - - eapply inversion_Lambda in Ht as (? & ? & ? & ? & ?); auto. - eapply invert_cumul_prod_l in c as (? & ? & ? & (? & ?) & ?); auto. - eapply red_mkApps_tInd in r as (? & eq & ?); eauto; eauto. - solve_discr. - - now rewrite head_mkApps /= /head /=. - - eapply PCUICValidity.inversion_mkApps in Ht as (? & ? & ?); auto. - eapply inversion_Ind in t as (? & ? & ? & decli & ? & ?); auto. - eapply PCUICSpine.typing_spine_strengthen in t0; eauto. - pose proof (on_declared_inductive wfΣ decli) as [onind oib]. - rewrite oib.(ind_arity_eq) in t0. - rewrite !subst_instance_constr_it_mkProd_or_LetIn in t0. - eapply typing_spine_arity_mkApps_Ind in t0; eauto. - eexists; split; [sq|]; eauto. - now do 2 eapply isArity_it_mkProd_or_LetIn. - - admit. (* wf of fixpoints *) - - now rewrite /head /=. - Admitted. - - Lemma red_normal_constructor t i u args : - axiom_free Σ -> - Σ ;;; [] |- t : mkApps (tInd i u) args -> - ∑ hnf, (red Σ.1 [] t hnf) * construct_cofix_discr (head hnf). - Proof. - intros axfree Ht. destruct (normalizer Ht) as [nf [rednf capp]]. - exists nf; split; auto. - eapply subject_reduction in Ht; eauto. - now eapply ind_normal_constructor. - Qed. - -End Normalization. -*) - (** Evaluation is a subrelation of reduction: *) Tactic Notation "redt" uconstr(y) := eapply (CRelationClasses.transitivity (R:=red _ _) (y:=y)). @@ -833,69 +651,12 @@ Section WeakNormalization. now eapply value_whnf. Qed. - (* - Lemma reducible Γ t : sum (∑ t', red1 Σ Γ t t') (wh_normal Σ Γ t). - Proof. - Ltac lefte := left; eexists; econstructor; eauto. - Ltac leftes := left; eexists; econstructor; solve [eauto]. - Ltac righte := right; (solve [repeat (constructor; eauto)])||(repeat constructor). - induction t in Γ |- * using term_forall_list_ind. - all:try solve [righte]. - - destruct (nth_error Γ n) eqn:hnth. - destruct c as [na [b|] ty]; [lefte|]. - * rewrite hnth; reflexivity. - * right. do 2 constructor; rewrite hnth /= //. - * righte. rewrite hnth /= //. admit. - - destruct (IHt1 Γ) as [[? ?]|]; [lefte|]. - destruct (IHt2 Γ) as [[? ?]|]; [leftes|]. - destruct (IHt2 (Γ ,, vass n t1)) as [[? ?]|]; [|]. - leftes. leftes. - - destruct (IHt1 Γ) as [[? ?]|]; [lefte|]. - destruct (IHt2 Γ) as [[? ?]|]; [leftes|]. - destruct (PCUICParallelReductionConfluence.view_lambda_fix_app t1 t2). - * rewrite [tApp _ _](mkApps_nested _ _ [a]). - destruct (unfold_fix mfix i) as [[rarg body]|] eqn:unf. - + destruct (is_constructor rarg (l ++ [a])) eqn:isc; [leftes|]; eauto. - right. rewrite /is_constructor in isc. - destruct nth_error eqn:eq. - ++ constructor; eapply whne_fixapp; eauto. admit. - ++ eapply whnf_fixapp. rewrite unf //. - + right. eapply whnf_fixapp. rewrite unf //. - * left. induction l; simpl. eexists. constructor. - eexists. eapply app_red_l. eapply red1_mkApps_l. constructor. - * admit. - - admit. - - admit. - - admit. - - admit. - - admit. - Admitted. - - Lemma normalizer {Γ t ty} : - Σ ;;; Γ |- t : ty -> - ∑ nf, (red Σ.1 Γ t nf) * wh_normal Σ Γ nf. - Proof. - intros Hty. - unshelve epose proof (PCUICSN.normalisation Σ Γ t (iswelltyped _ _ _ ty Hty)). - clear ty Hty. - move: t H. eapply Fix_F. - intros x IH. - destruct (reducible Γ x) as [[t' red]|nred]. - specialize (IH t'). forward IH by (constructor; auto). - destruct IH as [nf [rednf norm]]. - exists nf; split; auto. now transitivity t'. - exists x. split; [constructor|assumption]. - Qed. *) - Lemma typing_var {Γ n ty} : Σ ;;; Γ |- (tVar n) : ty -> False. Proof. intros Hty; depind Hty; eauto. Qed. Lemma typing_evar {Γ n l ty} : Σ ;;; Γ |- (tEvar n l) : ty -> False. Proof. intros Hty; depind Hty; eauto. Qed. - Definition axiom_free Σ := - forall c decl, declared_constant Σ c decl -> cst_body decl <> None. - Lemma invert_cumul_prod_ind {Γ na dom codom ind u args} : Σ ;;; Γ |- tProd na dom codom <= mkApps (tInd ind u) args -> False. Proof. @@ -1015,8 +776,8 @@ Section WeakNormalization. match t with | tApp hd arg => axiom_free_value Σ (axiom_free_value Σ [] arg :: args) hd | tConst kn _ => match lookup_env Σ kn with - | Some (ConstantDecl {| cst_body := Some _ |}) => true - | _ => false + | Some (ConstantDecl {| cst_body := None |}) => false + | _ => true end | tCase _ _ discr _ => axiom_free_value Σ [] discr | tProj _ t => axiom_free_value Σ [] t @@ -1119,7 +880,7 @@ Section WeakNormalization. axiom_free_value Σ [] t -> Σ ;;; [] |- t : mkApps (tInd ind u) indargs -> wh_normal Σ [] t -> - check_recursivity_kind Σ (inductive_mind ind) Finite -> + ~check_recursivity_kind Σ (inductive_mind ind) CoFinite -> isConstruct_app t. Proof. intros axfree typed whnf ck. @@ -1130,7 +891,7 @@ Section WeakNormalization. destruct hd eqn:eqh => //. subst hd. eapply decompose_app_inv in da. subst. eapply typing_cofix_coind in typed. - now move: (check_recursivity_kind_inj typed ck). + auto. Qed. Lemma fix_app_is_constructor {mfix idx args ty narg fn} : @@ -1149,11 +910,13 @@ Section WeakNormalization. rewrite /unfold_fix in unf. rewrite e in unf. noconf unf. eapply (wf_fixpoint_spine wfΣ) in t0; eauto. - rewrite /is_constructor. destruct (nth_error args (rarg x0)) eqn:hnth. + rewrite /is_constructor. destruct (nth_error args (rarg x0)) eqn:hnth; [|assumption]. destruct_sigma t0. destruct t0. intros axfree norm. eapply whnf_ind_finite in t0; eauto. - assumption. + intros chk. + pose proof (check_recursivity_kind_inj chk i1). + discriminate. Qed. Lemma value_axiom_free Σ' t : diff --git a/safechecker/_CoqProject.in b/safechecker/_CoqProject.in index 29115f2f4..1b751f2da 100644 --- a/safechecker/_CoqProject.in +++ b/safechecker/_CoqProject.in @@ -10,5 +10,6 @@ theories/PCUICTypeChecker.v theories/PCUICSafeChecker.v theories/SafeTemplateChecker.v theories/PCUICSafeRetyping.v +theories/PCUICConsistency.v theories/Extraction.v diff --git a/safechecker/theories/PCUICConsistency.v b/safechecker/theories/PCUICConsistency.v new file mode 100644 index 000000000..297ca7f33 --- /dev/null +++ b/safechecker/theories/PCUICConsistency.v @@ -0,0 +1,220 @@ +(* The safe checker gives us a sound and complete wh-normalizer for + PCUIC, assuming strong normalization. Combined with canonicity, + this allows us to prove that PCUIC is consistent, i.e. there + is no axiom-free proof of [forall (P : Prop), P] in the empty + context. To do so we use weakening to add an empty inductive, the + provided term to build an inhabitant and then canonicity to show + that this is a contradiction. *) + +From Coq Require Import Ascii String. +From Equations Require Import Equations. +From MetaCoq.PCUIC Require Import PCUICAst. +From MetaCoq.PCUIC Require Import PCUICAstUtils. +From MetaCoq.PCUIC Require Import PCUICCanonicity. +From MetaCoq.PCUIC Require Import PCUICInductiveInversion. +From MetaCoq.PCUIC Require Import PCUICInversion. +From MetaCoq.PCUIC Require Import PCUICLiftSubst. +From MetaCoq.PCUIC Require Import PCUICSR. +From MetaCoq.PCUIC Require Import PCUICSafeLemmata. +From MetaCoq.PCUIC Require Import PCUICTyping. +From MetaCoq.PCUIC Require Import PCUICUnivSubst. +From MetaCoq.PCUIC Require Import PCUICValidity. +From MetaCoq.PCUIC Require Import PCUICWeakeningEnv. +From MetaCoq.Template Require Import config utils. +From MetaCoq.SafeChecker Require Import PCUICSafeReduce. + +Local Opaque hnf. + +Fixpoint string_repeat c (n : nat) : string := + match n with + | 0 => "" + | S n => String c (string_repeat c n) + end. + +Lemma string_repeat_length c n : + String.length (string_repeat c n) = n. +Proof. + induction n; cbn; auto. +Qed. + +Definition max_name_length (Σ : global_env) : nat := + fold_right max 0 (map (fun '(kn, _) => String.length (string_of_kername kn)) Σ). + +Lemma max_name_length_ge Σ : + Forall (fun '(kn, _) => String.length (string_of_kername kn) <= max_name_length Σ) Σ. +Proof. + induction Σ as [|(kn&decl) Σ IH]; cbn; constructor. + - lia. + - eapply Forall_impl; eauto. + intros (?&?); cbn; intros. + fold (max_name_length Σ). + lia. +Qed. + +Definition make_fresh_name (Σ : global_env) : kername := + (MPfile [], string_repeat "a"%char (S (max_name_length Σ))). + +Lemma make_fresh_name_fresh Σ : + fresh_global (make_fresh_name Σ) Σ. +Proof. + pose proof (max_name_length_ge Σ) as all. + eapply Forall_impl; eauto. + cbn. + intros (kn&decl) le. + cbn. + intros ->. + unfold make_fresh_name in le. + cbn in le. + rewrite string_repeat_length in le. + lia. +Qed. + +Definition Prop_univ := Universe.of_levels (inl PropLevel.lProp). + +Definition False_oib : one_inductive_body := + {| ind_name := ""; + ind_type := tSort Prop_univ; + ind_kelim := IntoAny; + ind_ctors := []; + ind_projs := []; + ind_relevance := Relevant |}. + +Definition False_mib : mutual_inductive_body := + {| ind_finite := BiFinite; + ind_npars := 0; + ind_params := []; + ind_bodies := [False_oib]; + ind_universes := Monomorphic_ctx ContextSet.empty; + ind_variance := None |}. + +Definition axiom_free Σ := + forall c decl, declared_constant Σ c decl -> cst_body decl <> None. + +Lemma axiom_free_axiom_free_value Σ t : + axiom_free Σ -> + axiom_free_value Σ [] t. +Proof. + intros axfree. + cut (Forall is_true []); [|constructor]. + generalize ([] : list bool). + induction t; intros axfree_args all_true; cbn; auto. + - destruct lookup_env eqn:find; auto. + destruct g; auto. + destruct c; auto. + apply axfree in find; cbn in *. + now destruct cst_body. + - destruct nth_error; auto. + rewrite nth_nth_error. + destruct nth_error eqn:nth; auto. + eapply nth_error_forall in nth; eauto. +Qed. + +Definition binder := {| binder_name := nNamed "P"; binder_relevance := Relevant |}. + +Theorem pcuic_consistent {cf:checker_flags} Σ t : + wf_ext Σ -> + axiom_free Σ -> + (* t : forall (P : Prop), P *) + Σ ;;; [] |- t : tProd binder (tSort Prop_univ) (tRel 0) -> + False. +Proof. + intros wfΣ axfree cons. + set (Σext := ((make_fresh_name Σ, InductiveDecl False_mib) :: Σ.1, Σ.2)). + assert (wf': wf_ext Σext). + { constructor; [constructor|]. + - destruct wfΣ; auto. + - apply make_fresh_name_fresh. + - red. + cbn. + split. + { now intros ? ?%LevelSet.empty_spec. } + split. + { now intros ? ?%ConstraintSet.empty_spec. } + split; auto. + destruct wfΣ as (?&(?&?&?&[val sat])). + exists val. + intros l isin. + apply sat; auto. + apply ConstraintSet.union_spec. + apply ConstraintSet.union_spec in isin as [?%ConstraintSet.empty_spec|]; auto. + - hnf. + constructor. + + constructor. + * econstructor; cbn. + -- instantiate (2 := []); reflexivity. + -- exists (Universe.super Prop_univ). + constructor; auto. + constructor. + -- instantiate (1 := []). + constructor. + -- intros. + congruence. + -- constructor. + -- intros ? [=]. + * constructor. + + constructor. + + reflexivity. + + reflexivity. + - destruct wfΣ; auto. } + eapply (env_prop_typing _ _ PCUICWeakeningEnv.weakening_env) in cons; auto. + 3: exists [(make_fresh_name Σ, InductiveDecl False_mib)]; reflexivity. + 2: now destruct wf'. + + set (Σ' := _ ++ _) in cons. + set (False_ty := tInd (mkInd (make_fresh_name Σ) 0) []). + assert (typ_false: (Σ', Σ.2);;; [] |- tApp t False_ty : False_ty). + { apply validity_term in cons as typ_prod; auto. + destruct typ_prod. + eapply type_App with (B := tRel 0) (u := False_ty); eauto. + eapply type_Ind with (u := []) (mdecl := False_mib) (idecl := False_oib); eauto. + - hnf. + cbn. + unfold declared_minductive. + cbn. + rewrite eq_kername_refl. + auto. + - cbn. + auto. } + assert (sqwf: ∥ wf (Σ', Σ.2).1 ∥) by now destruct wf'. + pose proof (iswelltyped _ _ _ _ typ_false) as wt. + pose proof (@hnf_sound _ _ sqwf _ _ wt) as [r]. + pose proof (@hnf_complete _ _ sqwf _ _ wt) as [w]. + eapply subject_reduction in typ_false; eauto. + eapply whnf_ind_finite with (indargs := []) in typ_false as ctor; auto. + - unfold isConstruct_app in ctor. + destruct decompose_app eqn:decomp. + apply decompose_app_inv in decomp. + rewrite decomp in typ_false. + destruct t0; try discriminate ctor. + apply inversion_mkApps in typ_false as H; auto. + destruct H as (?&typ_ctor&_). + apply inversion_Construct in typ_ctor as (?&?&?&?&?&?&?); auto. + unshelve eapply Construct_Ind_ind_eq with (args' := []) in typ_false. + 5: eassumption. + 1: eauto. + destruct on_declared_constructor. + destruct p. + destruct s. + destruct p. + destruct typ_false as ((((->&_)&_)&_)&_). + clear -d. + destruct d as ((?&?)&?). + cbn in *. + red in H. + cbn in *. + rewrite eq_kername_refl in H. + noconf H. + noconf H0. + cbn in H1. + rewrite nth_error_nil in H1. + discriminate. + - eapply axiom_free_axiom_free_value. + intros kn decl isdecl. + hnf in isdecl. + cbn in isdecl. + destruct eq_kername; [noconf isdecl|]. + eapply axfree; eauto. + - unfold check_recursivity_kind. + cbn. + rewrite eq_kername_refl; auto. +Qed.