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..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)). @@ -802,7 +620,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 +632,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'. @@ -837,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. @@ -1014,41 +771,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 := None |}) => false + | _ => true + 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,23 +876,11 @@ 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 -> + ~check_recursivity_kind Σ (inductive_mind ind) CoFinite -> isConstruct_app t. Proof. intros axfree typed whnf ck. @@ -1095,19 +891,18 @@ 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} : - 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. @@ -1115,11 +910,35 @@ 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 norm. + 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 : + 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. @@ -1129,11 +948,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 +1038,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 +1046,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 +1054,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 +1092,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/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. 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].