From f1655e7d22e4d385bec489754167b9943fbe0877 Mon Sep 17 00:00:00 2001 From: Jakob Botsch Nielsen Date: Thu, 17 Dec 2020 12:56:30 +0100 Subject: [PATCH] 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.