From a8e1a97542f717055a377c584d6706a52dcd4def Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 17 Nov 2023 17:49:00 +0100 Subject: [PATCH] Done with template <-> PCUIC. Working on safe checker --- .vscode/metacoq.code-workspace | 71 ++++++++++++++----- pcuic/theories/Syntax/PCUICPosition.v | 57 ++++++++++++++- pcuic/theories/Syntax/PCUICReflect.v | 2 +- pcuic/theories/utils/PCUICPrimitive.v | 22 +++--- safechecker/theories/PCUICEqualityDec.v | 41 ++++++++++- safechecker/theories/PCUICErrors.v | 53 ++++++++++++++ safechecker/theories/PCUICSafeConversion.v | 27 +++++++ safechecker/theories/PCUICSafeReduce.v | 12 ++-- safechecker/theories/PCUICSafeRetyping.v | 2 +- template-coq/theories/TermEquality.v | 7 +- template-coq/theories/Typing.v | 31 +++++++- template-coq/theories/TypingWf.v | 3 +- template-coq/theories/WcbvEval.v | 1 + template-pcuic/theories/PCUICToTemplate.v | 5 +- .../theories/PCUICToTemplateCorrectness.v | 29 +++++--- .../theories/TemplateMonadToPCUIC.v | 7 +- template-pcuic/theories/TemplateToPCUIC.v | 5 ++ .../theories/TemplateToPCUICCorrectness.v | 44 +++++++++++- .../theories/TemplateToPCUICExpanded.v | 3 + .../theories/TemplateToPCUICWcbvEval.v | 1 + 20 files changed, 359 insertions(+), 64 deletions(-) diff --git a/.vscode/metacoq.code-workspace b/.vscode/metacoq.code-workspace index 6a0a8cce3..d6ac88a4c 100644 --- a/.vscode/metacoq.code-workspace +++ b/.vscode/metacoq.code-workspace @@ -11,31 +11,64 @@ - "-R", "safechecker-plugin/theories", "MetaCoq.SafeCheckerPlugin", + "-R", "safechecker-plugin/theories,MetaCoq.SafeCheckerPlugin", - "-R", "utils/theories", "MetaCoq.Utils", - "-R", "common/theories", "MetaCoq.Common", - "-R", "template-pcuic/theories", "MetaCoq.TemplatePCUIC", + "-R", "utils/theories,MetaCoq.Utils", + "-R", "common/theories,MetaCoq.Common", + "-R", "template-pcuic/theories,MetaCoq.TemplatePCUIC", - "-I", "template-coq", + "-I template-coq", // "-bt", get backtraces from Coq on errors - "-I", "template-coq/build", - "-R", "template-coq/theories", "MetaCoq.Template", - "-R", "examples", "MetaCoq.Examples", - "-R", "checker/theories", "MetaCoq.Checker", - "-R", "pcuic/theories", "MetaCoq.PCUIC", - "-I", "safechecker/src", - "-R", "safechecker/theories", "MetaCoq.SafeChecker", - "-I", "erasure/src", - "-R", "erasure/theories", "MetaCoq.Erasure", - "-R", "erasure-plugin/theories", "MetaCoq.ErasurePlugin", - "-R", "translations", "MetaCoq.Translations", - "-R", "test-suite/plugin-demo/theories", "MetaCoq.ExtractedPluginDemo", - "-R", "test-suite", "MetaCoq.TestSuite" + "-I template-coq/build", + "-R", "template-coq/theories,MetaCoq.Template", + "-R", "examples,MetaCoq.Examples", + "-R", "checker/theories,MetaCoq.Checker", + "-R", "pcuic/theories,MetaCoq.PCUIC", + "-I safechecker/src", + "-R", "safechecker/theories,MetaCoq.SafeChecker", + "-I erasure/src", + "-R", "erasure/theories,MetaCoq.Erasure", + "-R", "erasure-plugin/theories,MetaCoq.ErasurePlugin", + "-R", "translations,MetaCoq.Translations", + "-R", "test-suite/plugin-demo/theories,MetaCoq.ExtractedPluginDemo", + "-R", "test-suite,MetaCoq.TestSuite" ], // When enabled, will trim trailing whitespace when saving a file. "files.trimTrailingWhitespace": true, - "coqtop.binPath": "_opam/bin" + "coqtop.binPath": "_opam/bin", + "files.exclude": { + "**/*.vo": true, + "**/*.vok": true, + "**/*.vos": true, + "**/*.aux": true, + "**/*.glob": true, + "**/.git": true, + "**/.svn": true, + "**/.hg": true, + "**/CVS": true, + "**/.DS_Store": true, + "**/Thumbs.db": true + }, + "coq-lsp.args": [ + "-R", "safechecker-plugin/theories,MetaCoq.SafeCheckerPlugin", + "-R", "utils/theories,MetaCoq.Utils", + "-R", "common/theories,MetaCoq.Common", + "-R", "template-pcuic/theories,MetaCoq.TemplatePCUIC", + + "-I", "template-coq", + //"-bt", // get backtraces from Coq on errors + //"-Itemplate-coq/build", + "-R", "template-coq/theories,MetaCoq.Template", + "-R", "examples,MetaCoq.Examples", + "-R", "pcuic/theories,MetaCoq.PCUIC", + "-R", "safechecker/theories,MetaCoq.SafeChecker", + "-R", "erasure/theories,MetaCoq.Erasure", + "-R", "erasure-plugin/theories,MetaCoq.ErasurePlugin", + "-R", "translations,MetaCoq.Translations", + "-R", "test-suite/plugin-demo/theories,MetaCoq.ExtractedPluginDemo", + "-R", "test-suite,MetaCoq.TestSuite" + ], + "coq-lsp.path": "_opam/bin/coq-lsp" } } diff --git a/pcuic/theories/Syntax/PCUICPosition.v b/pcuic/theories/Syntax/PCUICPosition.v index 18ee68f23..439689ef7 100644 --- a/pcuic/theories/Syntax/PCUICPosition.v +++ b/pcuic/theories/Syntax/PCUICPosition.v @@ -47,7 +47,10 @@ Inductive choice := | prod_r | let_bd | let_ty -| let_in. +| let_in +| array_def +| array_ty +| array_val (n : nat). Derive NoConfusion NoConfusionHom EqDec for choice. @@ -115,6 +118,13 @@ Fixpoint validpos t (p : position) {struct p} := | let_bd, tLetIn na b B t => validpos b p | let_ty, tLetIn na b B t => validpos B p | let_in, tLetIn na b B t => validpos t p + | array_def, tPrim (primArray; primArrayModel a) => validpos (array_default a) p + | array_ty, tPrim (primArray; primArrayModel a) => validpos (array_type a) p + | array_val n, tPrim (primArray; primArrayModel a) => + match nth_error (array_value a) n with + | Some d => validpos d p + | None => false + end | _, _ => false end end. @@ -253,6 +263,11 @@ Proof. * simpl in *. apply some_inj in e. subst. destruct y as [na' ty' bo' ra']. simpl in *. intuition eauto. * simpl in *. eapply IHa. all: eauto. + + depelim e. depelim o; eauto. + + depelim e; depelim o; eauto. + + depelim e. depelim o; eauto. + cbn in vp. destruct (nth_error (array_value a) n) eqn:e'; try discriminate. + cbn. eapply All2_nth_error_Some in a0 as [t' [-> ?]]; tea. eapply ih; tea. Qed. Lemma eq_term_valid_pos : @@ -690,6 +705,34 @@ Proof. unshelve eapply Acc_cofix_mfix_bd with (1 := e1) (p := exist q _). -- simpl. rewrite e1 in e. assumption. -- eapply ihm. + - destruct q as [q e]. destruct q as [| c q]. + + constructor. intros [p' e'] h. + unfold posR in h. cbn in h. + dependent destruction h. + destruct p as [? []]; + destruct c. all: noconf e'. + * simpl in e'. + case_eq (nth_error m n0). + 2:{ intro h. pose proof e' as hh. rewrite h in hh. discriminate. } + intros [na ty bo ra] e1. + eapply All_nth_error in X as ihm. 2: exact e1. + simpl in ihm. + unshelve eapply Acc_cofix_mfix_ty with (1 := e1) (p := exist p _). + -- simpl. rewrite e1 in e'. assumption. + -- eapply ihm. + * simpl in e'. + case_eq (nth_error m n0). + 2:{ intro h. pose proof e' as hh. rewrite h in hh. discriminate. } + intros [na ty bo ra] e1. + eapply All_nth_error in X as ihm. 2: exact e1. + simpl in ihm. + unshelve eapply Acc_cofix_mfix_bd with (1 := e1) (p := exist p _). + -- simpl. rewrite e1 in e'. assumption. + -- eapply ihm. + + + destruct p as [? []]; cbn in X, e; intuition eauto; cbn in e. + + destruct x eqn:hp; try discriminate; cbn in e. constructor. Qed. Fixpoint atpos t (p : position) {struct p} : term := @@ -933,7 +976,11 @@ Variant stack_entry : Type := | Lambda_bd (na : aname) (A : term) | LetIn_bd (na : aname) (B t : term) | LetIn_ty (na : aname) (b t : term) -| LetIn_in (na : aname) (b B : term). +| LetIn_in (na : aname) (b B : term) +| PrimArray_ty (l : Level.t) (l : list term) (def : term) +| PrimArray_def (l : Level.t) (l : list term) (ty : term) +(* Hole in one of the values *) +| PrimArray_val (l : Level.t) (bef : list term) (after : list term) (def : term) (ty : term). Definition stack := list stack_entry. @@ -1029,6 +1076,9 @@ Definition fill_hole (t : term) (se : stack_entry) : term := | LetIn_bd na B u => tLetIn na t B u | LetIn_ty na b u => tLetIn na b t u | LetIn_in na b B => tLetIn na b B t + | PrimArray_def l v ty => tPrim (primArray; primArrayModel {| array_level := l; array_value := v; array_default := t; array_type := ty |}) + | PrimArray_ty l v def => tPrim (primArray; primArrayModel {| array_level := l; array_value := v; array_default := def; array_type := t |}) + | PrimArray_val l bef after def ty => tPrim (primArray; primArrayModel {| array_level := l; array_value := bef ++ (t :: after); array_default := def; array_type := ty |}) end. (* Not using fold_left here to get the right unfolding behavior *) @@ -1307,6 +1357,9 @@ Definition closedn_stack_entry k se := | LetIn_bd na B u => closedn k B && closedn (S k) u | LetIn_ty na b u => closedn k b && closedn (S k) u | LetIn_in na b B => closedn k b && closedn k B + | PrimArray_def l v ty => forallb (closedn k) v && closedn k ty + | PrimArray_ty l v def => forallb (closedn k) v && closedn k def + | PrimArray_val l bef after def ty => forallb (closedn k) bef && forallb (closedn k) after && closedn k def && closedn k ty end. Fixpoint closedn_stack k π := diff --git a/pcuic/theories/Syntax/PCUICReflect.v b/pcuic/theories/Syntax/PCUICReflect.v index 92ae085e0..47fafc878 100644 --- a/pcuic/theories/Syntax/PCUICReflect.v +++ b/pcuic/theories/Syntax/PCUICReflect.v @@ -115,7 +115,7 @@ Fixpoint eqb_term (u v : term) : bool := eqb x.(rarg) y.(rarg) && eqb x.(dname) y.(dname)) mfix mfix' - | tPrim p, tPrim p' => @eqb_prim_val _ eqb_term p p' + | tPrim p, tPrim p' => @eqb_prim_val _ eqb eqb_term p p' | _, _ => false end. diff --git a/pcuic/theories/utils/PCUICPrimitive.v b/pcuic/theories/utils/PCUICPrimitive.v index 04b856b97..ac205a86e 100644 --- a/pcuic/theories/utils/PCUICPrimitive.v +++ b/pcuic/theories/utils/PCUICPrimitive.v @@ -78,15 +78,15 @@ Instance reflect_eq_spec_float : ReflectEq SpecFloat.spec_float := EqDec_Reflect Import ReflectEq. -Definition eqb_array {term} {eqt : term -> term -> bool} (x y : array_model term) : bool := - eqb x.(array_level) y.(array_level) && +Definition eqb_array {term} {equ : Level.t -> Level.t -> bool} {eqt : term -> term -> bool} (x y : array_model term) : bool := + equ x.(array_level) y.(array_level) && forallb2 eqt x.(array_value) y.(array_value) && eqt x.(array_default) y.(array_default) && eqt x.(array_type) y.(array_type). #[program,global] Instance reflect_eq_array {term} {req : ReflectEq term}: ReflectEq (array_model term) := - { eqb := eqb_array (eqt := eqb) }. + { eqb := eqb_array (equ := eqb) (eqt := eqb) }. Next Obligation. intros term req [] []; cbn. unfold eqb_array. cbn. change (forallb2 eqb) with (eqb (A := list term)). @@ -97,14 +97,14 @@ Next Obligation. all:constructor; congruence. Qed. -Equations eqb_prim_model {term} {req : term -> term -> bool} {t : prim_tag} (x y : prim_model term t) : bool := +Equations eqb_prim_model {term} {equ : Level.t -> Level.t -> bool} {req : term -> term -> bool} {t : prim_tag} (x y : prim_model term t) : bool := | primIntModel x, primIntModel y := ReflectEq.eqb x y | primFloatModel x, primFloatModel y := ReflectEq.eqb x y - | primArrayModel x, primArrayModel y := eqb_array (eqt:=req) x y. + | primArrayModel x, primArrayModel y := eqb_array (equ := equ) (eqt:=req) x y. #[global, program] Instance prim_model_reflecteq {term} {req : ReflectEq term} {p : prim_tag} : ReflectEq (prim_model term p) := - {| ReflectEq.eqb := eqb_prim_model (req := eqb) |}. + {| ReflectEq.eqb := eqb_prim_model (equ := eqb) (req := eqb) |}. Next Obligation. intros. depelim x; depelim y; simp eqb_prim_model. case: ReflectEq.eqb_spec; constructor; subst; auto. congruence. @@ -116,15 +116,15 @@ Qed. #[global] Instance prim_model_eqdec {term} {req : ReflectEq term} : forall p : prim_tag, EqDec (prim_model term p) := _. -Equations eqb_prim_val {term} {req : term -> term -> bool} (x y : prim_val term) : bool := - | (primInt; i), (primInt; i') := eqb_prim_model (req := req) i i' - | (primFloat; f), (primFloat; f') := eqb_prim_model (req := req) f f' - | (primArray; a), (primArray; a') := eqb_prim_model (req := req) a a' +Equations eqb_prim_val {term} {equ : Level.t -> Level.t -> bool} {req : term -> term -> bool} (x y : prim_val term) : bool := + | (primInt; i), (primInt; i') := eqb_prim_model (equ := equ) (req := req) i i' + | (primFloat; f), (primFloat; f') := eqb_prim_model (equ := equ) (req := req) f f' + | (primArray; a), (primArray; a') := eqb_prim_model (equ := equ) (req := req) a a' | x, y := false. #[global, program] Instance prim_val_reflect_eq {term} {req : ReflectEq term} : ReflectEq (prim_val term) := - {| ReflectEq.eqb := eqb_prim_val (req := eqb) |}. + {| ReflectEq.eqb := eqb_prim_val (equ := eqb) (req := eqb) |}. Next Obligation. intros. funelim (eqb_prim_val x y); simp eqb_prim_val. change (eqb_prim_model i i') with (eqb i i'). diff --git a/safechecker/theories/PCUICEqualityDec.v b/safechecker/theories/PCUICEqualityDec.v index b79ef3c25..1d6c7ccc6 100644 --- a/safechecker/theories/PCUICEqualityDec.v +++ b/safechecker/theories/PCUICEqualityDec.v @@ -2,7 +2,7 @@ From Coq Require Import ProofIrrelevance ssreflect ssrbool. From MetaCoq.Utils Require Import utils. From MetaCoq.Common Require Import config uGraph. -From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICTactics +From MetaCoq.PCUIC Require Import PCUICAst PCUICAstUtils PCUICPrimitive PCUICTactics PCUICReflect PCUICLiftSubst PCUICUnivSubst PCUICTyping PCUICGlobalEnv PCUICCumulativity PCUICEquality PCUICWfUniverses PCUICInduction. @@ -158,7 +158,8 @@ Fixpoint eqb_term_upto_univ_napp eqb_binder_annot x.(dname) y.(dname) ) mfix mfix' - | tPrim p, tPrim p' => eqb p p' + | tPrim p, tPrim p' => eqb_prim_val (equ := fun l l' => equ (Universe.make l) (Universe.make l')) + (req := eqb_term_upto_univ_napp equ equ gen_compare_global_instance 0) p p' | _, _ => false end. @@ -396,6 +397,8 @@ Proof. eapply All_impl ; tea. move => ? [? ?]. now apply /andP. + - destruct p as [? []]; cbn in *; rtoProp; intuition eauto. + solve_all. Qed. Definition reflect_eq_predicate {Σ equ lequ} @@ -530,6 +533,8 @@ Proof. destruct gr; auto; now repeat rewrite hlookup. Qed. +Transparent eqb_prim_val eqb_prim_model. + Lemma reflect_eq_term_upto_univ Σ equ lequ (p : Universe.t -> bool) (q : nat -> term -> bool) (Re Rle : Universe.t -> Universe.t -> Prop) @@ -754,7 +759,34 @@ Proof. constructor. constructor. constructor ; try easy. now inversion e3. - - cbn - [eqb]. eqspecs. do 2 constructor. + - destruct p0 as [? []], prim as [? []]; + cbn in X, ht, ht'; + rewrite /eqb_prim_val /eqb_prim_model; cbn -[eqb]; try eqspecs; + try repeat constructor. + 1-8:intros e; depelim e; try depelim o; intuition eauto. + unfold eqb_array. eqspecs; rewrite ?andb_true_r ?andb_false_r. + rtoProp; intuition auto. specialize (a1 equ Re 0 he _ H4 H0). + specialize (a2 equ Re 0 he _ H5 H1). + case: a1; rewrite ?andb_true_r ?andb_false_r; [intros eq|constructor; intros e; depelim e; depelim o]; eauto. + case: a2; rewrite ?andb_true_r ?andb_false_r; [intros eq'|constructor; intros e; depelim e; depelim o]; eauto. + equspec equ he; eauto; cbn. + 2:constructor; intros e; depelim e; depelim o; eauto. + repeat toAll. + revert b0 H2. + destruct a as [l d ty v], a0 as [l' d' ty' v']; cbn in *. + intros a. + induction a in v' |- *; intros. + * depelim H2; cbn; constructor; eauto; try repeat constructor; cbn; eauto. + intros heq; depelim heq; cbn in *; depelim o; eauto. depelim a0. + * intuition auto. depelim H2; cbn; try constructor; eauto. + ++ intros heq; depelim heq; depelim o; eauto. depelim a2. + ++ specialize (IHa _ H2). case: IHa; intros htl. + +++ rewrite andb_true_r. specialize (b equ Re 0 he _ a0 i). + case: b; repeat constructor; eauto; depelim htl; depelim o; eauto. + intros heq; depelim heq; depelim o; cbn in *; eauto. eapply f. now depelim a3. + +++ rewrite andb_false_r; constructor. + intros heq; depelim heq; depelim o; cbn in *; eauto. eapply htl. + repeat constructor; eauto. cbn. now depelim a2. Qed. Lemma eqb_term_upto_univ_impl (equ lequ : _ -> _ -> bool) @@ -944,6 +976,9 @@ Proof. - eapply forallb_All in wt; eapply All_mix in X; try apply wt; clear wt. eapply All_All2; eauto; simpl; intuition eauto; apply andb_and in a as [? ?]; eauto. + - destruct p as [? []]; cbn -[Universe.make] in X, wt; rtoProp; intuition eauto; constructor; eauto. + + eapply hRe. now move/wf_universe_reflect: H. + + solve_all. eapply All_All2; eauto; simpl; intuition eauto. Defined. Lemma eqb_term_upto_univ_refl Σ (eqb leqb : Universe.t -> Universe.t -> bool) (Re : Universe.t -> Universe.t -> Prop) diff --git a/safechecker/theories/PCUICErrors.v b/safechecker/theories/PCUICErrors.v index aefec8e10..361b6688a 100644 --- a/safechecker/theories/PCUICErrors.v +++ b/safechecker/theories/PCUICErrors.v @@ -89,6 +89,26 @@ Inductive ConversionError := (Γ : context) (mfix : mfixpoint term) (Γ' : context) (mfix' : mfixpoint term) +| DistinctPrimTags + (Γ : context) (p : prim_val) + (Γ' : context) (p' : prim_val) + +| DistinctPrimValues + (Γ : context) (p : prim_val) + (Γ' : context) (p' : prim_val) + +| ArrayNotConvertibleValues + (Γ : context) (a : array_model term) (Γ' : context) (a' : array_model term) + (e : ConversionError) + +| ArrayNotConvertibleDefault + (Γ : context) (a : array_model term) (Γ' : context) (a' : array_model term) + (e : ConversionError) + +| ArrayNotConvertibleTypes + (Γ : context) (a : array_model term) (Γ' : context) (a' : array_model term) + (e : ConversionError) + | StackHeadError (leq : conv_pb) (Γ1 : context) @@ -271,6 +291,39 @@ Fixpoint string_of_conv_error Σ (e : ConversionError) : string := nl ^ "and" ^ nl ^ print_term Σ Γ' (tCoFix mfix' idx) ^ nl ^ "have a different number of mutually defined functions." + | ArrayNotConvertibleValues Γ a Γ' a' e => + "The two arrays " ^ nl ^ + print_term Σ Γ (tPrim (primArray; primArrayModel a)) ^ + nl ^ "and" ^ nl ^ + print_term Σ Γ (tPrim (primArray; primArrayModel a')) ^ + nl ^ " have non-convertible values: " ^ + nl ^ string_of_conv_error Σ e + | ArrayNotConvertibleTypes Γ a Γ' a' e => + "The two arrays " ^ nl ^ + print_term Σ Γ (tPrim (primArray; primArrayModel a)) ^ + nl ^ "and" ^ nl ^ + print_term Σ Γ (tPrim (primArray; primArrayModel a')) ^ + nl ^ " have non-convertible types: " ^ + nl ^ string_of_conv_error Σ e + | ArrayNotConvertibleDefault Γ a Γ' a' e => + "The two arrays " ^ nl ^ + print_term Σ Γ (tPrim (primArray; primArrayModel a)) ^ + nl ^ "and" ^ nl ^ + print_term Σ Γ (tPrim (primArray; primArrayModel a')) ^ + nl ^ " have non-convertible default values: " ^ + nl ^ string_of_conv_error Σ e + | DistinctPrimTags Γ p Γ' p' => + "The two primitive values " ^ nl ^ + print_term Σ Γ (tPrim p) ^ + nl ^ "and" ^ nl ^ + print_term Σ Γ (tPrim p') ^ + nl ^ " have distinct tags" + | DistinctPrimValues Γ p Γ' p' => + "The two primitive values " ^ nl ^ + print_term Σ Γ (tPrim p) ^ + nl ^ "and" ^ nl ^ + print_term Σ Γ (tPrim p') ^ + nl ^ " have distinct values" | StackHeadError leq Γ1 t1 args1 u1 l1 Γ2 t2 u2 l2 e => "TODO stackheaderror" ^ nl ^ string_of_conv_error Σ e diff --git a/safechecker/theories/PCUICSafeConversion.v b/safechecker/theories/PCUICSafeConversion.v index 57544eeac..c49846fcd 100644 --- a/safechecker/theories/PCUICSafeConversion.v +++ b/safechecker/theories/PCUICSafeConversion.v @@ -732,6 +732,7 @@ Section Conversion. prog_discr (tProj _ _) (tProj _ _) := False ; prog_discr (tFix _ _) (tFix _ _) := False ; prog_discr (tCoFix _ _) (tCoFix _ _) := False ; + prog_discr (tPrim _) (tPrim _) := False ; prog_discr _ _ := True. (* Note that the arity of this should be the same for all s as otherwise @@ -1298,6 +1299,9 @@ Section Conversion. | prog_view_CoFix mfix idx mfix' idx' : prog_view (tCoFix mfix idx) (tCoFix mfix' idx') + | prog_view_Prim p p' : + prog_view (tPrim p) (tPrim p') + | prog_view_other : forall u v, prog_discr u v -> prog_view u v. @@ -1326,6 +1330,9 @@ Section Conversion. prog_viewc (tCoFix mfix idx) (tCoFix mfix' idx') := prog_view_CoFix mfix idx mfix' idx' ; + prog_viewc (tPrim p) (tPrim p') := + prog_view_Prim p p' ; + prog_viewc u v := prog_view_other u v I. Lemma welltyped_wf_local Σ Γ t : @@ -3476,6 +3483,26 @@ Qed. ) } ; + | prog_view_Prim p p' with inspect (eqb (prim_val_tag p) (prim_val_tag p')) := { + | @exist false tag_uneq := + no (DistinctPrimTag (Γ ,,, stack_context π1) p (Γ ,,, stack_context π2) p') + | @exist true eqtag with p, p' := { + | (primInt; primIntModel i) | (primInt, primIntModel i') with inspect (eqb i i') := + { | @exist true eqi := yes + | @exist false neqi := no (DistingPrimValues (Γ ,,, stack_context π1) p (Γ ,,, stack_context π2) p') } + | (primFloat; primFloatModel f) | (primFloat; primFloatModel f') with inspect (eqb f f') := + { | @exist true eqf := yes + | @exist false neqf := no (DistingPrimValues (Γ ,,, stack_context π1) p (Γ ,,, stack_context π2) p') } + | (primArray; primArrayModel a) | (primArray; primArrayModel a') with + with isconv_red_raw Conv (array_type a) (Prod_l na B1 :: π1) (array_type a') (Prod_l na' B2 :: π2) aux : + inspect (eqb f f') := + { | @exist true eqf := yes + | @exist false neqf := no (DistingPrimValues (Γ ,,, stack_context π1) p (Γ ,,, stack_context π2) p') } + + + } + } ; + | prog_view_other t1 t2 h := isconv_fallback leq t1 π1 t2 π2 aux }. diff --git a/safechecker/theories/PCUICSafeReduce.v b/safechecker/theories/PCUICSafeReduce.v index 65f8c71b2..a61cabcc5 100644 --- a/safechecker/theories/PCUICSafeReduce.v +++ b/safechecker/theories/PCUICSafeReduce.v @@ -1319,8 +1319,8 @@ Corollary R_Acc_aux : unfold is_true in typ. unfold PCUICAst.PCUICEnvironment.fst_ctx in *. congruence. - - eapply inversion_Prim in typ as (prim_ty & cdecl & [? ? ? [? []]]); tea. - now eapply invert_cumul_axiom_ind in w; tea. + - eapply inversion_Prim in typ as (prim_ty & cdecl & [? ? ? ?]); tea. + now eapply (invert_cumul_prim_type_ind) in w; tea. Qed. Definition isCoFix_app t := @@ -1353,8 +1353,8 @@ Corollary R_Acc_aux : unfold unfold_fix. destruct o as [[? [-> ?]] | ->]; eauto. - unfold isCoFix_app in cof. now rewrite decompose_app_mkApps in cof. - - eapply inversion_Prim in typ as [prim_ty [cdecl [? ? ? [? []]]]]; tea. - now eapply invert_cumul_axiom_ind in w; tea. + - eapply inversion_Prim in typ as [prim_ty [cdecl [? ? ? ?]]]; tea. + now eapply invert_cumul_prim_type_ind in w; tea. Qed. Lemma whnf_fix_arg_whne mfix idx body Σ Γ t before args aftr ty : @@ -1532,8 +1532,8 @@ Corollary R_Acc_aux : simpl in h. rewrite stack_context_appstack in h. destruct h as [T h]. apply inversion_App in h as (?&?&?&?&?); auto. - apply inversion_Prim in t0 as (prim_ty & cdecl & [? ? ? [s []]]); auto. - eapply PCUICClassification.invert_cumul_axiom_prod; eauto. + apply inversion_Prim in t0 as (prim_ty & cdecl & [? ? ? ?]); auto. + eapply PCUICClassification.invert_cumul_prim_type_prod; eauto. - unfold zipp. case_eq (decompose_stack π). intros l ρ e. constructor. constructor. eapply whne_mkApps. eapply whne_rel_nozeta. assumption. diff --git a/safechecker/theories/PCUICSafeRetyping.v b/safechecker/theories/PCUICSafeRetyping.v index eb31d9b85..385dabc26 100644 --- a/safechecker/theories/PCUICSafeRetyping.v +++ b/safechecker/theories/PCUICSafeRetyping.v @@ -366,7 +366,7 @@ Qed. | exist None _ => ! }; infer Γ wfΓ (tPrim p) wt with inspect (abstract_primitive_constant X p.π1) := - { | exist (Some prim_ty) eqp => ret (tConst prim_ty []) + { | exist (Some prim_ty) eqp => ret (prim_type p prim_ty) | exist None _ => ! }. Next Obligation. diff --git a/template-coq/theories/TermEquality.v b/template-coq/theories/TermEquality.v index a11f62bb4..653533f9a 100644 --- a/template-coq/theories/TermEquality.v +++ b/template-coq/theories/TermEquality.v @@ -241,9 +241,10 @@ Inductive eq_term_upto_univ_napp Σ (Re Rle : Universe.t -> Universe.t -> Prop) | eq_Int i : eq_term_upto_univ_napp Σ Re Rle napp (tInt i) (tInt i) | eq_Float f : eq_term_upto_univ_napp Σ Re Rle napp (tFloat f) (tFloat f) | eq_Array u u' arr arr' def def' ty ty' : - All2 (eq_term_upto_univ_napp Σ Re Rle 0) arr arr' -> - eq_term_upto_univ_napp Σ Re Rle 0 def def' -> - eq_term_upto_univ_napp Σ Re Rle 0 ty ty' -> + Re (Universe.make u) (Universe.make u') -> + All2 (eq_term_upto_univ_napp Σ Re Re 0) arr arr' -> + eq_term_upto_univ_napp Σ Re Re 0 def def' -> + eq_term_upto_univ_napp Σ Re Re 0 ty ty' -> eq_term_upto_univ_napp Σ Re Rle napp (tArray u arr def ty) (tArray u' arr' def' ty'). Notation eq_term_upto_univ Σ Re Rle := (eq_term_upto_univ_napp Σ Re Rle 0). diff --git a/template-coq/theories/Typing.v b/template-coq/theories/Typing.v index cc451c39b..7fa6c4555 100644 --- a/template-coq/theories/Typing.v +++ b/template-coq/theories/Typing.v @@ -276,7 +276,19 @@ Inductive red1 (Σ : global_env) (Γ : context) : term -> term -> Type := | cofix_red_body mfix0 mfix1 idx : OnOne2 (on_Trel_eq (red1 Σ (Γ ,,, fix_context mfix0)) dbody (fun x => (dname x, dtype x, rarg x))) mfix0 mfix1 -> - red1 Σ Γ (tCoFix mfix0 idx) (tCoFix mfix1 idx). + red1 Σ Γ (tCoFix mfix0 idx) (tCoFix mfix1 idx) + +| array_red_val l v v' d ty : + OnOne2 (fun t u => red1 Σ Γ t u) v v' -> + red1 Σ Γ (tArray l v d ty) (tArray l v' d ty) + +| array_red_def l v d d' ty : + red1 Σ Γ d d' -> + red1 Σ Γ (tArray l v d ty) (tArray l v d' ty) + +| array_red_type l v d ty ty' : + red1 Σ Γ ty ty' -> + red1 Σ Γ (tArray l v d ty) (tArray l v d ty'). Lemma red1_ind_all : forall (Σ : global_env) (P : context -> term -> term -> Type), @@ -398,9 +410,19 @@ Lemma red1_ind_all : (fun x => (dname x, dtype x, rarg x))) mfix0 mfix1 -> P Γ (tCoFix mfix0 idx) (tCoFix mfix1 idx)) -> + (forall Γ l v v' d ty, + OnOne2 (fun t u => Trel_conj (red1 Σ Γ) (P Γ) t u) v v' -> + P Γ (tArray l v d ty) (tArray l v' d ty)) -> + + (forall Γ l v d d' ty, + red1 Σ Γ d d' -> P Γ d d' -> P Γ (tArray l v d ty) (tArray l v d' ty)) -> + + (forall Γ l v d ty ty', + red1 Σ Γ ty ty' -> P Γ ty ty' -> P Γ (tArray l v d ty) (tArray l v d ty')) -> + forall (Γ : context) (t t0 : term), red1 Σ Γ t t0 -> P Γ t t0. Proof. - intros. rename X30 into Xlast. revert Γ t t0 Xlast. + intros. rename X33 into Xlast. revert Γ t t0 Xlast. fix aux 4. intros Γ t T. move aux at top. destruct 1; @@ -458,8 +480,11 @@ Proof. revert o. generalize (fix_context mfix0). intros c H28. revert mfix0 mfix1 H28; fix auxl 3; intros l l' Hl; destruct Hl; constructor; try split; auto; intuition. -Defined. + - eapply X30. + revert v v' o. fix auxl 3; intros ? ? Hl; destruct Hl; + constructor; try split; auto; intuition. +Defined. (** *** Reduction diff --git a/template-coq/theories/TypingWf.v b/template-coq/theories/TypingWf.v index a4f97e740..affb93cc9 100644 --- a/template-coq/theories/TypingWf.v +++ b/template-coq/theories/TypingWf.v @@ -847,6 +847,7 @@ Section WfRed. cbn. unfold wf_decl. simpl. intros ? [? ? ? ?] ?. simpl in *. intuition eauto with wf. + - constructor; eauto. eapply (OnOne2_All_All X); tea; intuition eauto. Qed. @@ -1143,7 +1144,7 @@ Section TypingWf. Proof using Type. intros wfx; revert y. induction wfx using term_wf_forall_list_ind; intros [] wfy; - eapply wf_inv in wfy; simpl in wfy; simpl; + eapply wf_inv in wfy; simpl in wfy; simpl; try intros [= ?]; try intuition congruence. Qed. diff --git a/template-coq/theories/WcbvEval.v b/template-coq/theories/WcbvEval.v index a41410626..72be49adb 100644 --- a/template-coq/theories/WcbvEval.v +++ b/template-coq/theories/WcbvEval.v @@ -55,6 +55,7 @@ Fixpoint csubst t k u := let mfix' := List.map (map_def (csubst t k) (csubst t k')) mfix in tCoFix mfix' idx | tCast c kd c' => tCast (csubst t k c) kd (csubst t k c') + | tArray l v d ty => tArray l (List.map (csubst t k) v) (csubst t k d) (csubst t k ty) | x => x end. diff --git a/template-pcuic/theories/PCUICToTemplate.v b/template-pcuic/theories/PCUICToTemplate.v index 4656b28d5..a1f4d1933 100644 --- a/template-pcuic/theories/PCUICToTemplate.v +++ b/template-pcuic/theories/PCUICToTemplate.v @@ -13,10 +13,11 @@ Definition uint63_from_model (i : uint63_model) : Uint63.int := Definition float64_from_model (f : float64_model) : PrimFloat.float := FloatOps.SF2Prim (proj1_sig f). -Definition trans_prim (t : prim_val) : Ast.term := +Definition trans_prim (trans : PCUICAst.term -> Ast.term) (t : prim_val) : Ast.term := match t.π2 with | primIntModel i => Ast.tInt i | primFloatModel f => Ast.tFloat f + | primArrayModel a => Ast.tArray (array_level a) (map trans (array_value a)) (trans (array_default a)) (trans (array_type a)) end. Definition trans_predicate (t : PCUICAst.predicate Ast.term) : predicate Ast.term := @@ -53,7 +54,7 @@ Fixpoint trans (t : PCUICAst.term) : Ast.term := | PCUICAst.tCoFix mfix idx => let mfix' := List.map (map_def trans trans) mfix in tCoFix mfix' idx - | PCUICAst.tPrim i => trans_prim i + | PCUICAst.tPrim i => trans_prim trans i end. Notation trans_decl := (map_decl trans). diff --git a/template-pcuic/theories/PCUICToTemplateCorrectness.v b/template-pcuic/theories/PCUICToTemplateCorrectness.v index 03a23608f..0f80efe77 100644 --- a/template-pcuic/theories/PCUICToTemplateCorrectness.v +++ b/template-pcuic/theories/PCUICToTemplateCorrectness.v @@ -106,7 +106,7 @@ Proof. rewrite b. now rewrite forget_types_length map_context_length. - f_equal; auto; red in X; solve_list. - f_equal; auto; red in X; solve_list. - - destruct p as [? []]; eauto. + - destruct p as [? []]; cbn in X; cbn; f_equal; intuition eauto; solve_all. Qed. Definition on_fst {A B C} (f:A->C) (p:A×B) := (f p.1, p.2). @@ -284,7 +284,7 @@ Proof. cbn in *. now rewrite e e0. + apply IHX. - - destruct p as [? []]; eauto. + - destruct p as [? []]; cbn in X |- *; f_equal; intuition eauto; solve_all. Qed. Lemma trans_subst10 u B: @@ -334,7 +334,7 @@ Proof. destruct p. now rewrite e e0. + apply IHX. - - destruct p as [? []]; eauto. + - destruct p as [? []]; cbn in X |- *; f_equal; intuition eauto; solve_all. Qed. Lemma trans_subst_instance_ctx Γ u : @@ -683,6 +683,7 @@ Section wtsub. | tFix mfix idx | tCoFix mfix idx => All (fun d => wt Γ d.(dtype) × wt (Γ ,,, fix_context mfix) d.(dbody)) mfix | tEvar _ l => False + | tPrim p => tPrimProp (wt Γ) p | _ => unit end. Import PCUICGeneration PCUICInversion. @@ -749,6 +750,9 @@ Section wtsub. eapply All_prod. eapply (All_impl a). intros ? h; exact h. eapply (All_impl a0). intros ? h; eexists; tea. + - eapply inversion_Prim in h as (?&?&[]); eauto. + destruct prim as [? []]; cbn in *; eauto; try exact tt. + depelim p0. repeat split. now eexists. now eexists. solve_all. now eexists. Qed. End wtsub. @@ -1028,7 +1032,7 @@ Proof. cbn; eauto. cbn in p0. destruct p0. eauto. - cbn. red in X. solve_all. - cbn. red in X. solve_all. - - destruct p as [? []]; constructor. + - destruct p as [? []]; cbn in X, H |- *; constructor; solve_all; eauto. Qed. #[global] Hint Resolve trans_wf : wf. @@ -1058,6 +1062,7 @@ Proof. - constructor; solve_all. - eapply Typing.cofix_red_body; solve_all. eapply b0, All2_app => //. reflexivity. + - eapply Typing.array_red_val. solve_all. Qed. Lemma map_map2 {A B C D} (f : A -> B) (g : C -> D -> A) l l' : @@ -1381,6 +1386,9 @@ Proof. intuition auto. rewrite /trans_local map_app in X. now rewrite -trans_fix_context. + - cbn. apply TT.array_red_val. + eapply OnOne2_All_mix_left in X; tea. + eapply OnOne2_map. solve_all. Qed. Lemma trans_R_global_instance Σ Re Rle gref napp u u' : @@ -1449,7 +1457,7 @@ Proof. red in X0. solve_all_one. eapply trans_eq_context_gen_eq_binder_annot in a. now rewrite !map_context_trans. - - destruct p as [? []]; constructor. + - depelim X0; cbn in X |- *; try econstructor; intuition eauto; solve_all. Qed. Lemma trans_leq_term {cf} Σ ϕ T U : @@ -2363,11 +2371,14 @@ Proof. + fold trans;subst types. now apply trans_mfix_All2. + now rewrite trans_wf_cofixpoint. - - cbn. destruct p as [? []]; cbn; econstructor; eauto. - 1,3: eapply trans_declared_constant; tea. - all:move: X0; rewrite /Ast.Env.primitive_invariants /primitive_invariants; - intros [s []]; exists s; split => //; + - cbn. destruct p as [? []]; simp prim_type; cbn; econstructor; eauto. + 1,3,5: eapply trans_declared_constant; tea. + all:cbn in *. + all:move: X0; rewrite /Ast.Env.primitive_invariants /primitive_invariants. + 1-2:intros [s []]; exists s; split => //; destruct cdecl as [ty [?|] ?]; cbn in *; subst; auto => //. + intros []; split => //. rewrite H1 //. rewrite H2 //. + all:depelim X2; eauto. intros _. solve_all. - eapply TT.type_Conv. + eassumption. + eassumption. diff --git a/template-pcuic/theories/TemplateMonadToPCUIC.v b/template-pcuic/theories/TemplateMonadToPCUIC.v index 48726cffd..06477c287 100644 --- a/template-pcuic/theories/TemplateMonadToPCUIC.v +++ b/template-pcuic/theories/TemplateMonadToPCUIC.v @@ -163,7 +163,12 @@ Section with_tc. ret (tCoFix mfix' idx) | Ast.tInt n => ret (tPrim (primInt; primIntModel n)) | Ast.tFloat n => ret (tPrim (primFloat; primFloatModel n)) - end. + | Ast.tArray l v d ty => + v' <- monad_map@{t u t t} monad_trans' v ;; + d' <- monad_trans' d ;; + ty' <- monad_trans' ty ;; + ret (tPrim ((primArray; primArrayModel {| array_level := l; array_value := v'; array_default := d'; array_type := ty' |}))) + end. End with_helper. End with_tc. diff --git a/template-pcuic/theories/TemplateToPCUIC.v b/template-pcuic/theories/TemplateToPCUIC.v index 7568a7985..595df18f5 100644 --- a/template-pcuic/theories/TemplateToPCUIC.v +++ b/template-pcuic/theories/TemplateToPCUIC.v @@ -103,6 +103,11 @@ Section Trans. tCoFix mfix' idx | Ast.tInt n => tPrim (primInt; primIntModel n) | Ast.tFloat n => tPrim (primFloat; primFloatModel n) + | Ast.tArray l v d ty => tPrim (primArray; primArrayModel + {| array_level := l; + array_value := List.map trans v; + array_default := trans d; + array_type := trans ty |}) end. Definition trans_decl (d : Ast.Env.context_decl) := diff --git a/template-pcuic/theories/TemplateToPCUICCorrectness.v b/template-pcuic/theories/TemplateToPCUICCorrectness.v index 3eae7d881..76845a68a 100644 --- a/template-pcuic/theories/TemplateToPCUICCorrectness.v +++ b/template-pcuic/theories/TemplateToPCUICCorrectness.v @@ -239,6 +239,7 @@ Proof. red in X0. f_equal => //. rewrite /id. unfold trans_predicate. f_equal; solve_all. f_equal. solve_all. + do 4 f_equal; solve_all. Qed. Lemma trans_decl_weakening {cf} Σ {Σ' : global_env_map} t : @@ -379,6 +380,10 @@ Proof. rewrite e. now rewrite map_length. - f_equal; auto. maps. solve_all. - f_equal; auto; solve_all. + - f_equal; auto. + - f_equal; auto. + - cbn; do 4 f_equal; auto. + rewrite /map_array_model. f_equal; eauto. cbn. solve_all. Qed. Lemma trans_mkApp u a : trans (Template.Ast.mkApp u a) = tApp (trans u) (trans a). @@ -435,6 +440,10 @@ Proof. f_equal; auto; solve_all. - f_equal; auto; solve_list. - f_equal; auto; solve_list. + - f_equal; auto. + - f_equal; auto. + - cbn; f_equal; auto. rewrite /map_array_model; cbn; do 3 f_equal; eauto. + solve_all. Qed. Notation Tterm :=Template.Ast.term. @@ -470,6 +479,9 @@ Proof. rewrite /map_branch /trans_branch /= /id. now intros; f_equal. - rewrite /id /map_predicate /=. f_equal; solve_all. + - f_equal; auto. + - f_equal; auto. + - cbn. rewrite /mapu_array_model; cbn; do 4 f_equal; auto; solve_all. Qed. @@ -958,6 +970,10 @@ Section Trans_Global. intros [? ? ? ?] [? ? ? ?] [[[? ?] [[ih1 ih2] [? ?]]] [? ?]]. simpl in *. intuition eauto. now eapply ih1. now eapply ih2. + - constructor; eauto. intuition auto; constructor; cbn; eauto. + eapply (IHt1 Re); eauto. reflexivity. + eapply (IHt2 Re); eauto. reflexivity. + solve_all. eapply a; eauto. reflexivity. Qed. Lemma trans_leq_term ϕ T U : @@ -1698,6 +1714,8 @@ Section Trans_Global. cbn. rewrite /trans_decl /vass /=. now rewrite trans_lift. + simpl; congruence. + - simpl. eapply array_red_val. eapply (OnOne2_All_mix_left a) in X. + apply OnOne2_map; solve_all. Qed. End Trans_Global. @@ -2451,18 +2469,39 @@ Proof. now eapply TypingWf.typing_wf in Hs'. -- destruct decl; reflexivity. - - cbn. econstructor; cbn; eauto. + - cbn. replace (tConst prim_ty []) with (prim_type (primInt; primIntModel p) prim_ty) by now simp prim_type. + econstructor; cbn; eauto. + rewrite trans_env_retroknowledge //. + now apply forall_decls_declared_constant. + move: X0; rewrite /Ast.Env.primitive_invariants /primitive_invariants. intros [s []]; exists s; split => //; destruct cdecl as [ty [?|] ?]; cbn in *; subst; auto => //. - - cbn. econstructor; cbn; eauto. + + constructor. + - cbn. replace (tConst prim_ty []) with (prim_type (primFloat; primFloatModel p) prim_ty) by now simp prim_type. + econstructor; cbn; eauto. + rewrite trans_env_retroknowledge //. + now apply forall_decls_declared_constant. + move: X0; rewrite /Ast.Env.primitive_invariants /primitive_invariants. intros [s []]; exists s; split => //; destruct cdecl as [ty [?|] ?]; cbn in *; subst; auto => //. + + constructor. + - cbn. set (a := {| array_level := _ |}). + replace (tApp (tConst prim_ty [u]) (trans (trans_global_env Σ.1) ty)) with (prim_type (primArray; primArrayModel a) prim_ty) by now simp prim_type. + econstructor; cbn; eauto. + + rewrite trans_env_retroknowledge //. + + now apply forall_decls_declared_constant. + + move: X0; rewrite /Ast.Env.primitive_invariants /primitive_invariants. + intros []; split => //; eauto. + * apply forall_decls_declared_constant in H0; eauto. + rewrite /trans_constant_body in H0 |- *. + now rewrite H1 H2 H3 /= in H0 |- *. + * rewrite /trans_constant_body in H0 |- *. + now rewrite H1 H2 H3 /= in H0 |- *. + + constructor; eauto. cbn [array_level a]. eapply validity in X2; eauto. + eapply PCUICWfUniverses.isType_wf_universes in X2. cbn [trans PCUICWfUniverses.wf_universes] in X2. + unfold PCUICWfUniverses.wf_universes in X2. cbn [PCUICWfUniverses.on_universes] in X2. + move: X2. case: PCUICWfUniverses.wf_universe_reflect => //; eauto. eauto. + cbn [a array_value]. solve_all. - assert (WfAst.wf Σ B). { now apply typing_wf in X2. } eapply type_Cumul; eauto. @@ -2594,6 +2633,7 @@ Proof. rewrite map2_length; len. eauto. - unfold test_def; red in X. solve_all. - unfold test_def; solve_all. + - solve_all. Qed. From MetaCoq.PCUIC Require Import PCUICOnFreeVars. diff --git a/template-pcuic/theories/TemplateToPCUICExpanded.v b/template-pcuic/theories/TemplateToPCUICExpanded.v index bd4dfd7e8..cf6f8e115 100644 --- a/template-pcuic/theories/TemplateToPCUICExpanded.v +++ b/template-pcuic/theories/TemplateToPCUICExpanded.v @@ -235,6 +235,9 @@ Proof with eauto using expanded. - wf_inv wf ?. econstructor. solve_all. - wf_inv wf [[[]]]. eapply forall_decls_declared_constructor in H; eauto. 2: now eapply template_to_pcuic_env. eapply expanded_tConstruct_app. eauto. cbn. unfold trans_local. now rewrite map_length context_assumptions_map. solve_all. + - repeat constructor. + - repeat constructor. + - wf_inv wf [[] ?]. repeat cbn; constructor. constructor; cbn; eauto. solve_all. Qed. diff --git a/template-pcuic/theories/TemplateToPCUICWcbvEval.v b/template-pcuic/theories/TemplateToPCUICWcbvEval.v index a3a1b7b07..2e95e9d3d 100644 --- a/template-pcuic/theories/TemplateToPCUICWcbvEval.v +++ b/template-pcuic/theories/TemplateToPCUICWcbvEval.v @@ -158,6 +158,7 @@ Proof. f_equal; auto; solve_all. - f_equal; auto; solve_list. - f_equal; auto; solve_list. + - cbn; f_equal; auto. do 3 f_equal. rewrite /map_array_model /=; f_equal; eauto; solve_all. Qed. Lemma trans_substl {cf} Σ a b :