diff --git a/.github/workflows/nix-action-default-macos.yml b/.github/workflows/nix-action-default-macos.yml new file mode 100644 index 000000000..f598ff280 --- /dev/null +++ b/.github/workflows/nix-action-default-macos.yml @@ -0,0 +1,127 @@ +jobs: + coq: + needs: [] + runs-on: macos-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup metacoq + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"default\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "coq" + equations: + needs: [] + runs-on: macos-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup metacoq + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target equations + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"default\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "equations" + metacoq: + needs: + - equations + runs-on: macos-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup metacoq + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"default\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "metacoq" +name: Nix CI for bundle default +'on': + pull_request: + paths: + - .github/workflows/** + pull_request_target: + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/.github/workflows/nix-action-default-ubuntu.yml b/.github/workflows/nix-action-default-ubuntu.yml new file mode 100644 index 000000000..f7ab44e8f --- /dev/null +++ b/.github/workflows/nix-action-default-ubuntu.yml @@ -0,0 +1,127 @@ +jobs: + coq: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup metacoq + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target coq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"default\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "coq" + equations: + needs: [] + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup metacoq + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target equations + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"default\" --argstr job \"equations\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "equations" + metacoq: + needs: + - equations + runs-on: ubuntu-latest + steps: + - name: Determine which commit to test + run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\ + \ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\ + \ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\ + \ | cut -f1)\n if [ -z \"$merge_commit\" ]; then\n echo \"tested_commit=${{\ + \ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n else\n echo\ + \ \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n" + - name: Git checkout + uses: actions/checkout@v2 + with: + fetch-depth: 0 + ref: ${{ env.tested_commit }} + - name: Cachix install + uses: cachix/install-nix-action@v16 + with: + nix_path: nixpkgs=channel:nixpkgs-unstable + - name: Cachix setup metacoq + uses: cachix/cachix-action@v10 + with: + authToken: ${{ secrets.CACHIX_AUTH_TOKEN }} + extraPullNames: coq, coq-community + name: metacoq + - id: stepCheck + name: Checking presence of CI target metacoq + run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\ + \ bundle \"default\" --argstr job \"metacoq\" \\\n --dry-run 2>&1 > /dev/null)\n\ + echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\ + \ \"built:\" | sed \"s/.*/built/\")\n" + - if: steps.stepCheck.outputs.status == 'built' + name: 'Building/fetching previous CI target: equations' + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "equations" + - if: steps.stepCheck.outputs.status == 'built' + name: Building/fetching current CI target + run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "default" + --argstr job "metacoq" +name: Nix CI for bundle default +'on': + pull_request: + paths: + - .github/workflows/** + pull_request_target: + types: + - opened + - synchronize + - reopened + push: + branches: + - master diff --git a/erasure/theories/EConstructorsAsBlocks.v b/erasure/theories/EConstructorsAsBlocks.v index 167a4ae2a..a13882d9f 100644 --- a/erasure/theories/EConstructorsAsBlocks.v +++ b/erasure/theories/EConstructorsAsBlocks.v @@ -88,7 +88,6 @@ Section transform_blocks. Hint Rewrite @map_InP_spec : transform_blocks. Arguments eqb : simpl never. - Opaque transform_blocks_unfold_clause_1. Opaque transform_blocks. Opaque isEtaExp. @@ -276,7 +275,6 @@ Section transform_blocks. rewrite -> ?map_map_compose, ?compose_on_snd, ?compose_map_def, ?map_length; unfold test_def in *; simpl closed in *; try solve [simpl subst; simpl closed; f_equal; auto; rtoProp; solve_all]; try easy. - - destruct Nat.compare => //. - f_equal. solve_all. move/andP: b => [] _ he. solve_all. - rewrite csubst_mkApps. @@ -357,7 +355,6 @@ Section transform_blocks. rewrite forallb_rev forallb_skipn //. now rewrite map_rev map_skipn. Qed. - Lemma transform_blocks_fix_subst mfix : EGlobalEnv.fix_subst (map (map_def transform_blocks) mfix) = map transform_blocks (EGlobalEnv.fix_subst mfix). Proof using Type. unfold EGlobalEnv.fix_subst. diff --git a/erasure/theories/EGenericMapEnv.v b/erasure/theories/EGenericMapEnv.v index a664c58d8..e6aa927d3 100644 --- a/erasure/theories/EGenericMapEnv.v +++ b/erasure/theories/EGenericMapEnv.v @@ -120,7 +120,6 @@ destruct (lookup_env Σ kn) eqn:hl. - eapply lookup_env_gen_transform_env_Some in hl as [Σ' [ext wf' hl']] => /=. rewrite hl'. f_equal. eapply wellformed_gen_transform_decl_extends; eauto. auto. - - cbn. now eapply lookup_env_gen_transform_env_None in hl. Qed. diff --git a/erasure/theories/EInlineProjections.v b/erasure/theories/EInlineProjections.v index 02a6f07be..f042c6d82 100644 --- a/erasure/theories/EInlineProjections.v +++ b/erasure/theories/EInlineProjections.v @@ -378,7 +378,6 @@ Proof. - eapply lookup_env_optimize_env_Some in hl as [Σ' [ext wf' hl']] => /=. rewrite hl'. f_equal. eapply wellformed_optimize_decl_extends; eauto. auto. - - cbn. now eapply lookup_env_optimize_env_None in hl. Qed. @@ -502,7 +501,7 @@ Proof. eapply eval_wellformed in ev2; tea => //. eapply eval_wellformed in ev1; tea => //. econstructor; eauto. - rewrite -(optimize_csubst _ 1) //. + rewrite -(optimize_csubst _ 1) //. apply IHev3. eapply wellformed_csubst => //. - move/andP => [] clb0 clb1. diff --git a/erasure/theories/ELiftSubst.v b/erasure/theories/ELiftSubst.v index fae9cb614..390a08218 100644 --- a/erasure/theories/ELiftSubst.v +++ b/erasure/theories/ELiftSubst.v @@ -108,7 +108,7 @@ Require Import PeanoNat. Import Nat. Lemma lift_rel_ge : - forall k n p, p <= n -> lift k p (tRel n) = tRel (k + n). + forall k n p, p <= n -> lift k p (tRel n) = tRel (k + n). Proof. intros; simpl in |- *. now elim (leb_spec p n). diff --git a/erasure/theories/EWcbvEval.v b/erasure/theories/EWcbvEval.v index 6f5589724..f1a67cf83 100644 --- a/erasure/theories/EWcbvEval.v +++ b/erasure/theories/EWcbvEval.v @@ -107,6 +107,8 @@ Section Wcbv. Context {wfl : WcbvFlags}. Context (Σ : global_declarations). (* The local context is fixed: we are only doing weak reductions *) + + Local Unset Elimination Schemes. Local Unset Elimination Schemes. @@ -217,7 +219,6 @@ Section Wcbv. nth_error args (p.(proj_npars) + p.(proj_arg)) = Some a -> eval a res -> eval (tProj p discr) res - (** Proj *) | eval_proj_block p cdecl discr args a res : with_constructor_as_block = true -> @@ -327,7 +328,6 @@ Defined. Set Equations Transparent. Section eval_rect. - Variables (wfl : WcbvFlags) (Σ : global_declarations) (P : forall x y, eval Σ x y → Type). Equations All2_over {A B : Set} {P : A → B → Set} {l : list A} {l' : list B} : @@ -697,6 +697,15 @@ Section Wcbv. - repeat eexists; eauto. - invs i. destruct args; invs H0. exists []. repeat econstructor. Qed. + + Lemma eval_Construct_inv ind c args e : + eval (tConstruct ind c args) e -> + ∑ args', e = tConstruct ind c args' × All2 eval args args'. + Proof. + intros H. depind H. + - repeat eexists; eauto. + - invs i. destruct args; invs H0. exists []. repeat econstructor. + Qed. Lemma eval_to_value e e' : eval e e' -> value e'. Proof. @@ -724,12 +733,10 @@ Section Wcbv. + rewrite -[tApp _ _](mkApps_app _ _ [a']). eapply value_app. cbn; auto. econstructor; tea. cbn; len. eapply All_app_inv; auto. - - econstructor 2; tea. now rewrite -(All2_length a). clear -a iha. induction a. constructor. destruct iha as [va' ih]. constructor. exact va'. now apply IHa. - - destruct (mkApps_elim f' [a']). eapply value_mkApps_inv in IHev1 => //. destruct IHev1 as [?|[]]; intuition subst. @@ -1608,7 +1615,6 @@ Definition mk_env_flags has_ax has_pars tfl has_blocks := has_cstr_params := has_pars; term_switches := tfl ; cstr_as_blocks := has_blocks |}. - Global Hint Rewrite andb_true_r andb_false_r : simplifications. Global Hint Rewrite orb_false_r orb_true_r : simplifications. @@ -2017,7 +2023,7 @@ Proof. eapply (eval_mkApps_Construct_inv _ _ _ [] _ hblock) in x as [? []]; auto. subst f''. depelim a1. f_equal. eapply eval_deterministic_all; tea. - eapply All2_impl; tea; cbn; eauto. now intros x y []. + eapply All2_impl; tea; cbn; eauto. now intros x y []. Qed. Lemma eval_construct_size {fl : WcbvFlags} [Σ kn c args e] : diff --git a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v index 75b312bed..504c71c74 100644 --- a/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v +++ b/erasure/theories/EWcbvEvalCstrsAsBlocksInd.v @@ -112,7 +112,6 @@ Proof. eapply qpres in hfix. depelim hfix. depelim i0. eapply nth_error_all in a; tea. now rewrite Nat.add_0_r in a. assumption. Qed. - #[export] Instance Qsubst_Qcofixs {etfl : ETermFlags} Q : Qpres Q -> Qcofix Q -> Qsubst Q -> Qcofixs Q. Proof. move=> qpres qfix; rewrite /Qsubst /Qfixs. diff --git a/erasure/theories/EWcbvEvalEtaInd.v b/erasure/theories/EWcbvEvalEtaInd.v index 7af660c4b..6601402a3 100644 --- a/erasure/theories/EWcbvEvalEtaInd.v +++ b/erasure/theories/EWcbvEvalEtaInd.v @@ -72,7 +72,6 @@ Class Qcofixs (Q : nat -> term -> Type) := qcofixs : forall mfix idx, Q 0 (tCoFi forall args fn, cunfold_cofix mfix idx = Some (args, fn) -> Q 0 fn. #[export] Hint Mode Qcofixs ! : typeclass_instances. - Lemma Qfix_subst {etfl : ETermFlags} mfix Q : has_tFix -> Qfix Q -> Qpres Q -> forall idx, idx < #|mfix| -> Q 0 (tFix mfix idx) -> All (Q 0) (fix_subst mfix). Proof. intros hasfix qfix qpre; unfold fix_subst. @@ -704,7 +703,6 @@ Definition env_flags := term_switches := term_flags ; cstr_as_blocks := false |}. - From MetaCoq.Erasure Require Import ELiftSubst. Lemma Qpreserves_wellformed (efl : EEnvFlags) Σ : cstr_as_blocks = false -> diff --git a/erasure/theories/EWellformed.v b/erasure/theories/EWellformed.v index 3fccd987a..65783fe45 100644 --- a/erasure/theories/EWellformed.v +++ b/erasure/theories/EWellformed.v @@ -73,7 +73,6 @@ Definition all_env_flags_blocks := term_switches := all_term_flags; has_cstr_params := true ; cstr_as_blocks := true |}. - Section wf. Context {efl : EEnvFlags}. @@ -91,7 +90,6 @@ Section wf. (idx true | _ => false end. - Fixpoint wellformed k (t : term) : bool := match t with | tRel i => has_tRel && Nat.ltb i k diff --git a/examples/modules.v b/examples/modules.v new file mode 100644 index 000000000..7b4aa0761 --- /dev/null +++ b/examples/modules.v @@ -0,0 +1,90 @@ +From MetaCoq.Template Require Import All. +Import MCMonadNotation. + + Inductive roseTree := + | node (xs : list roseTree). + (* | node_nil + | node_cons (r: roseTree) (xs: roseTree). *) + +Inductive All {A} (P : A -> Prop) : list A -> Prop := + | All_nil : All P nil + | All_cons : forall (x : A) (l : list A), + P x -> All P l -> All P (cons x l). + + (* Check roseTree_ind. + Theorem roseTree_ind' : forall P : roseTree -> Prop, + (forall (xs : list roseTree) (allxs : All P xs), P (node xs)) -> forall r : roseTree, P r. + Proof. + intros P IH r. destruct r. induction xs; apply IH. + - apply All_nil. + - specialize (IH (cons r xs)). + + *) + +Module M. + MetaCoq Quote Recursively Definition a := 0. + Print a. + Module N. + MetaCoq Quote Recursively Definition b := 0. + Print b. (* should see a, b in env *) + Check a. + Module N1. + MetaCoq Quote Recursively Definition b := 0. + Print b. (* should see a, b in env *) + Check a. + End N1. + End N. + MetaCoq Quote Recursively Definition c := 0. + Print c. (* should see a in env *) +End M. + +Module N := M. + + +MetaCoq Run (tmQuoteModule "M"%bs >>= tmPrint). +MetaCoq Run (tmQuoteModule "N"%bs >>= tmPrint). + +MetaCoq Quote Recursively Definition a := 0. + +Module MM := M. +MetaCoq Run (tmQuoteModule "MM"%bs >>= tmPrint). + +Print a. + +Module M1. + Definition b1 := 0. + + MetaCoq Quote Recursively Definition a := 0. + Print a. + Module N1. + End N1. + MetaCoq Test Quote "N1"%bs. + Module M := N1. + MetaCoq Test Quote "M"%bs. + + + Definition div (n m: nat) := exists d: nat, d * n = m. + Definition div_strict (a b: nat) := (div a b) /\ (a <> b). (* Strict partial order *) + Theorem one_div_everything (n: nat): div 1 n. + Proof. + induction n. now exists 0. + now exists (S n). + Qed. + + Definition b2 := true. + + Module N2. + MetaCoq Quote Recursively Definition c := 100. + Print c. + End N2. + + Definition b3 := "b3". +End M1. + +Definition a1 := "a1". + +Module M2. + Definition b4 := "b4". +End M2. + +Definition a2 := "a2". diff --git a/pcuic/_CoqProject.in b/pcuic/_CoqProject.in index ad625dff4..b8e037a7e 100644 --- a/pcuic/_CoqProject.in +++ b/pcuic/_CoqProject.in @@ -1,5 +1,7 @@ -R theories MetaCoq.PCUIC +theories/Environment.v +theories/EnvironmentTyping.v theories/PCUICAst.v theories/utils/PCUICOnOne.v diff --git a/pcuic/theories/Environment.v b/pcuic/theories/Environment.v new file mode 100644 index 000000000..05809e31f --- /dev/null +++ b/pcuic/theories/Environment.v @@ -0,0 +1,779 @@ +(* Distributed under the terms of the MIT license. *) +From Coq Require Import ssreflect ssrbool ssrfun Morphisms Setoid. +From MetaCoq.Template Require Import utils BasicAst Primitive. +From MetaCoq.Template Require Import Universes. +From MetaCoq.Template Require Environment. + +Module Type Term := Environment.Term. + +Module Retroknowledge := Environment.Retroknowledge. + +Module Environment (T : Term). + + Import T. + #[global] Existing Instance subst_instance_constr. + + Definition typ_or_sort := typ_or_sort_ term. + + (** ** Declarations *) + Notation context_decl := (context_decl term). + + (** Local (de Bruijn) variable binding *) + + Definition vass x A : context_decl := + {| decl_name := x ; decl_body := None ; decl_type := A |}. + + (** Local (de Bruijn) let-binding *) + + Definition vdef x t A : context_decl := + {| decl_name := x ; decl_body := Some t ; decl_type := A |}. + + (** Local (de Bruijn) context *) + + Definition context := list context_decl. + + (** Last declaration first *) + + Definition lift_decl n k d := (map_decl (lift n k) d). + + Definition lift_context n k (Γ : context) : context := + fold_context_k (fun k' => lift n (k' + k)) Γ. + + Lemma lift_context_alt n k Γ : + lift_context n k Γ = + mapi (fun k' d => lift_decl n (Nat.pred #|Γ| - k' + k) d) Γ. + Proof. + unfold lift_context. apply: fold_context_k_alt. + Qed. + + Lemma lift_context_length n k Γ : #|lift_context n k Γ| = #|Γ|. + Proof. now rewrite /lift_context; len. Qed. + #[global] Hint Rewrite lift_context_length : len. + + Definition subst_context s k (Γ : context) : context := + fold_context_k (fun k' => subst s (k' + k)) Γ. + + Definition subst_decl s k (d : context_decl) := map_decl (subst s k) d. + + Lemma subst_context_length s n Γ : #|subst_context s n Γ| = #|Γ|. + Proof. now rewrite /subst_context; len. Qed. + #[global] Hint Rewrite subst_context_length : len. + + Lemma subst_context_nil s n : subst_context s n [] = []. + Proof. reflexivity. Qed. + + Lemma subst_context_alt s k Γ : + subst_context s k Γ = + mapi (fun k' d => subst_decl s (Nat.pred #|Γ| - k' + k) d) Γ. + Proof. + unfold subst_context, fold_context_k. rewrite rev_mapi. rewrite List.rev_involutive. + apply mapi_ext. intros. f_equal. now rewrite List.rev_length. + Qed. + + Lemma subst_context_snoc s k Γ d : subst_context s k (d :: Γ) = subst_context s k Γ ,, subst_decl s (#|Γ| + k) d. + Proof. + now rewrite /subst_context fold_context_k_snoc0. + Qed. + + Definition subst_telescope s k (Γ : context) : context := + mapi (fun k' decl => map_decl (subst s (k' + k)) decl) Γ. + + Global Instance subst_instance_decl : UnivSubst context_decl + := map_decl ∘ subst_instance. + + Global Instance subst_instance_context : UnivSubst context + := map_context ∘ subst_instance. + + Lemma subst_instance_length u (ctx : context) + : #|subst_instance u ctx| = #|ctx|. + Proof. unfold subst_instance, subst_instance_context, map_context. now rewrite map_length. Qed. + #[global] Hint Rewrite subst_instance_length : len. + + Definition set_binder_name (na : aname) (x : context_decl) : context_decl := + {| decl_name := na; + decl_body := decl_body x; + decl_type := decl_type x |}. + + Fixpoint context_assumptions (Γ : context) := + match Γ with + | [] => 0 + | d :: Γ => + match d.(decl_body) with + | Some _ => context_assumptions Γ + | None => S (context_assumptions Γ) + end + end. + + Fixpoint is_assumption_context (Γ : context) := + match Γ with + | [] => true + | d :: Γ => + match d.(decl_body) with + | Some _ => false + | None => is_assumption_context Γ + end + end. + + (** Smashing a context produces an assumption context. *) + + Fixpoint smash_context (Γ Γ' : context) : context := + match Γ' with + | {| decl_body := Some b |} :: Γ' => smash_context (subst_context [b] 0 Γ) Γ' + | {| decl_body := None |} as d :: Γ' => smash_context (Γ ++ [d]) Γ' + | [] => Γ + end. + + Lemma smash_context_length Γ Γ' : #|smash_context Γ Γ'| = #|Γ| + context_assumptions Γ'. + Proof. + induction Γ' as [|[na [body|] ty] tl] in Γ |- *; cbn; eauto. + - now rewrite IHtl subst_context_length. + - rewrite IHtl app_length. simpl. lia. + Qed. + #[global] Hint Rewrite smash_context_length : len. + + (* Smashing a context Γ with Δ depending on it is the same as smashing Γ + and substituting all references to Γ in Δ by the expansions of let bindings. *) + + Lemma smash_context_app Δ Γ Γ' : + smash_context Δ (Γ ++ Γ') = smash_context (smash_context Δ Γ) Γ'. + Proof. + revert Δ; induction Γ as [|[na [b|] ty]]; intros Δ; simpl; auto. + Qed. + + Fixpoint extended_subst (Γ : context) (n : nat) + (* Δ, smash_context Γ, n |- extended_subst Γ n : Γ *) := + match Γ with + | nil => nil + | cons d vs => + match decl_body d with + | Some b => + (* Δ , vs |- b *) + let s := extended_subst vs n in + (* Δ , smash_context vs , n |- s : vs *) + let b' := lift (context_assumptions vs + n) #|s| b in + (* Δ, smash_context vs, n , vs |- b' *) + let b' := subst s 0 b' in + (* Δ, smash_context vs , n |- b' *) + b' :: s + | None => tRel n :: extended_subst vs (S n) + end + end. + + Lemma extended_subst_length Γ n : #|extended_subst Γ n| = #|Γ|. + Proof. + induction Γ in n |- *; simpl; auto. + now destruct a as [? [?|] ?] => /=; simpl; rewrite IHΓ. + Qed. + #[global] Hint Rewrite extended_subst_length : len. + + Definition expand_lets_k Γ k t := + (subst (extended_subst Γ 0) k (lift (context_assumptions Γ) (k + #|Γ|) t)). + + Definition expand_lets Γ t := expand_lets_k Γ 0 t. + + Definition expand_lets_k_ctx Γ k Δ := + (subst_context (extended_subst Γ 0) k (lift_context (context_assumptions Γ) (k + #|Γ|) Δ)). + + Definition expand_lets_ctx Γ Δ := expand_lets_k_ctx Γ 0 Δ. + + Lemma expand_lets_k_ctx_length Γ k Δ : #|expand_lets_k_ctx Γ k Δ| = #|Δ|. + Proof. now rewrite /expand_lets_k_ctx; len. Qed. + #[global] Hint Rewrite expand_lets_k_ctx_length : len. + + Lemma expand_lets_ctx_length Γ Δ : #|expand_lets_ctx Γ Δ| = #|Δ|. + Proof. now rewrite /expand_lets_ctx; len. Qed. + #[global] Hint Rewrite expand_lets_ctx_length : len. + + Definition fix_context (m : mfixpoint term) : context := + List.rev (mapi (fun i d => vass d.(dname) (lift i 0 d.(dtype))) m). + + (** *** Environments *) + + Record constructor_body := { + cstr_name : ident; + (* The arguments and indices are typeable under the context of + arities of the mutual inductive + parameters *) + cstr_args : context; + cstr_indices : list term; + cstr_type : term; + (* Closed type: on well-formed constructors: forall params, cstr_args, I params cstr_indices *) + cstr_arity : nat; (* arity, w/o lets, w/o parameters *) + }. + + Record projection_body := { + proj_name : ident; + (* The arguments and indices are typeable under the context of + arities of the mutual inductive + parameters *) + proj_relevance : relevance; + proj_type : term; (* Type under context of params and inductive object *) + }. + + Definition map_constructor_body npars arities f c := + {| cstr_name := c.(cstr_name); + cstr_args := fold_context_k (fun x => f (x + npars + arities)) c.(cstr_args); + cstr_indices := map (f (npars + arities + #|c.(cstr_args)|)) c.(cstr_indices); + (* Note only after positivity checking we can ensure that the indices do not mention the + inductive type.. beware of lets! *) + cstr_type := f arities c.(cstr_type); + cstr_arity := c.(cstr_arity) |}. + + (* Here npars should be the [context_assumptions] of the parameters context. *) + Definition map_projection_body npars f c := + {| proj_name := c.(proj_name); + proj_relevance := c.(proj_relevance); + proj_type := f (S npars) c.(proj_type) + |}. + + (** See [one_inductive_body] from [declarations.ml]. *) + Record one_inductive_body := { + ind_name : ident; + ind_indices : context; (* Indices of the inductive types, under params *) + ind_sort : Universe.t; (* Sort of the inductive. *) + ind_type : term; (* Closed arity = forall mind_params, ind_indices, tSort ind_sort *) + ind_kelim : allowed_eliminations; (* Allowed eliminations *) + ind_ctors : list constructor_body; + ind_projs : list projection_body; (* names and types of projections, if any. *) + ind_relevance : relevance (* relevance of the inductive definition *) }. + + Definition map_one_inductive_body npars arities f m := + match m with + | Build_one_inductive_body ind_name ind_indices ind_sort + ind_type ind_kelim ind_ctors ind_projs ind_relevance => + Build_one_inductive_body + ind_name (fold_context_k (fun x => f (npars + x)) ind_indices) ind_sort + (f 0 ind_type) ind_kelim (map (map_constructor_body npars arities f) ind_ctors) + (map (map_projection_body npars f) ind_projs) ind_relevance + end. + + (** See [mutual_inductive_body] from [declarations.ml]. *) + Record mutual_inductive_body := { + ind_finite : recursivity_kind; + ind_npars : nat; + ind_params : context; + ind_bodies : list one_inductive_body ; + ind_universes : universes_decl; + ind_variance : option (list Universes.Variance.t) }. + + (** See [constant_body] from [declarations.ml] *) + Record constant_body := { + cst_type : term; + cst_body : option term; + cst_universes : universes_decl; + cst_relevance : relevance }. + + Definition map_constant_body f decl := + {| cst_type := f decl.(cst_type); + cst_body := option_map f decl.(cst_body); + cst_universes := decl.(cst_universes); + cst_relevance := decl.(cst_relevance) |}. + + Lemma map_cst_type f decl : + f (cst_type decl) = cst_type (map_constant_body f decl). + Proof. destruct decl; reflexivity. Qed. + + Lemma map_cst_body f decl : + option_map f (cst_body decl) = cst_body (map_constant_body f decl). + Proof. destruct decl; reflexivity. Qed. + + Inductive global_decl := + | ConstantDecl : constant_body -> global_decl + | InductiveDecl : mutual_inductive_body -> global_decl. + Derive NoConfusion for global_decl. + + Definition global_declarations := list (kername * global_decl). + + Record global_env := mk_global_env + { universes : ContextSet.t; + declarations : global_declarations; + retroknowledge : Retroknowledge.t }. + + Coercion universes : global_env >-> ContextSet.t. + + Definition empty_global_env := + {| universes := ContextSet.empty; + declarations := []; + retroknowledge := Retroknowledge.empty |}. + + Definition add_global_decl decl Σ := + {| universes := Σ.(universes); + declarations := decl :: Σ.(declarations); + retroknowledge := Σ.(retroknowledge) |}. + + Lemma eta_global_env Σ : Σ = {| universes := Σ.(universes); declarations := Σ.(declarations); + retroknowledge := Σ.(retroknowledge) |}. + Proof. now destruct Σ. Qed. + + Definition set_declarations Σ decls := + {| universes := Σ.(universes); + declarations := decls; + retroknowledge := Σ.(retroknowledge) |}. + + Fixpoint lookup_global (Σ : global_declarations) (kn : kername) : option global_decl := + match Σ with + | nil => None + | d :: tl => + if kn == d.1 then Some d.2 + else lookup_global tl kn + end. + + Definition lookup_env (Σ : global_env) (kn : kername) := lookup_global Σ.(declarations) kn. + + Definition extends (Σ Σ' : global_env) := + [× Σ.(universes) ⊂_cs Σ'.(universes), + ∑ Σ'', Σ'.(declarations) = Σ'' ++ Σ.(declarations) & + Retroknowledge.extends Σ.(retroknowledge) Σ'.(retroknowledge)]. + + Definition extends_decls (Σ Σ' : global_env) := + [× Σ.(universes) = Σ'.(universes), + ∑ Σ'', Σ'.(declarations) = Σ'' ++ Σ.(declarations) & + Σ.(retroknowledge) = Σ'.(retroknowledge)]. + + Existing Class extends. + Existing Class extends_decls. + + Lemma lookup_global_None Σ kn : ~In kn (List.map fst Σ) <-> lookup_global Σ kn = None. + Proof. + move: Σ; elim => //=; try tauto. + move => ??; case: eqb_spec; intuition congruence. + Qed. + + Lemma lookup_global_Some_iff_In_NoDup Σ kn decl (H : NoDup (List.map fst Σ)) + : In (kn, decl) Σ <-> lookup_global Σ kn = Some decl. + Proof. + move: Σ H; elim => //=; try tauto. + move => [??]?; case: eqb_spec => ? IH; inversion 1; subst; try rewrite <- IH by assumption. + all: intuition try congruence; subst. + all: cbn in *. + all: repeat match goal with H : (_, _) = (_, _) |- _ => inversion H; clear H end. + all: repeat match goal with H : Some _ = Some _ |- _ => inversion H; clear H end. + all: subst => //=; auto. + all: try now epose proof (@in_map _ _ fst _ (_, _)); cbn in *; exfalso; eauto. + Qed. + + #[global] Instance extends_decls_extends Σ Σ' : extends_decls Σ Σ' -> extends Σ Σ'. + Proof. + destruct Σ, Σ'; intros []. cbn in *; subst. split => //=. + split; [lsets|csets]. apply Retroknowledge.extends_refl. + Qed. + + #[global] Instance extends_decls_refl : CRelationClasses.Reflexive extends_decls. + Proof. red. intros x. split => //; try exists [] => //. Qed. + + Lemma extends_refl : CRelationClasses.Reflexive extends. + Proof. red. intros x. split; [apply incl_cs_refl | now exists [] | apply Retroknowledge.extends_refl]. Qed. + + (* easy prefers this to the local hypotheses, which is annoying + #[global] Instance extends_refl : CRelationClasses.Reflexive extends. + Proof. apply extends_refl. Qed. + *) + + Local Ltac extends_trans_t := + intros [?] [?] [?] [?] [?]; red; cbn in *; split; + try solve [ etransitivity; eassumption | eapply incl_cs_trans; eassumption ]; + repeat first [ progress subst + | match goal with + | [ H : ∑ x : _, _ |- _ ] => destruct H + | [ H : forall c : kername, _, kn : kername |- _ ] => specialize (H kn) + | [ H : ?x = _ |- context[?x] ] => rewrite H + end + | split + | intro + | now eexists; rewrite app_assoc ]. + #[global] Instance extends_decls_trans : CRelationClasses.Transitive extends_decls. + Proof. extends_trans_t. Qed. + #[global] Instance extends_trans : CRelationClasses.Transitive extends. + Proof. extends_trans_t. Qed. + + Definition primitive_constant (Σ : global_env) (p : prim_tag) : option kername := + match p with + | primInt => Σ.(retroknowledge).(Retroknowledge.retro_int63) + | primFloat => Σ.(retroknowledge).(Retroknowledge.retro_float64) + end. + + Definition primitive_invariants (cdecl : constant_body) := + ∑ s, [/\ cdecl.(cst_type) = tSort s, cdecl.(cst_body) = None & + cdecl.(cst_universes) = Monomorphic_ctx]. + + + (** A context of global declarations + global universe constraints, + i.e. a global environment *) + + Definition global_env_ext : Type := global_env * universes_decl. + + (** Use a coercion for this common projection of the global context. *) + Definition fst_ctx : global_env_ext -> global_env := fst. + Coercion fst_ctx : global_env_ext >-> global_env. + + Definition empty_ext (Σ : global_env) : global_env_ext + := (Σ, Monomorphic_ctx). + + (** *** Programs + + A set of declarations and a term, as produced by [MetaCoq Quote Recursively]. *) + + Definition program : Type := global_env * term. + + (* TODO MOVE AstUtils factorisation *) + + Definition app_context (Γ Γ' : context) : context := Γ' ++ Γ. + Notation "Γ ,,, Γ'" := + (app_context Γ Γ') (at level 25, Γ' at next level, left associativity). + + (** Make a lambda/let-in string of abstractions from a context [Γ], ending with term [t]. *) + + Definition mkLambda_or_LetIn d t := + match d.(decl_body) with + | None => tLambda d.(decl_name) d.(decl_type) t + | Some b => tLetIn d.(decl_name) b d.(decl_type) t + end. + + Definition it_mkLambda_or_LetIn (l : context) (t : term) := + List.fold_left (fun acc d => mkLambda_or_LetIn d acc) l t. + + (** Make a prod/let-in string of abstractions from a context [Γ], ending with term [t]. *) + + Definition mkProd_or_LetIn d t := + match d.(decl_body) with + | None => tProd d.(decl_name) d.(decl_type) t + | Some b => tLetIn d.(decl_name) b d.(decl_type) t + end. + + Definition it_mkProd_or_LetIn (l : context) (t : term) := + List.fold_left (fun acc d => mkProd_or_LetIn d acc) l t. + + Lemma it_mkProd_or_LetIn_app l l' t : + it_mkProd_or_LetIn (l ++ l') t = it_mkProd_or_LetIn l' (it_mkProd_or_LetIn l t). + Proof. induction l in l', t |- *; simpl; auto. Qed. + + Fixpoint reln (l : list term) (p : nat) (Γ0 : list context_decl) {struct Γ0} : list term := + match Γ0 with + | [] => l + | {| decl_body := Some _ |} :: hyps => reln l (p + 1) hyps + | {| decl_body := None |} :: hyps => reln (tRel p :: l) (p + 1) hyps + end. + + Definition to_extended_list_k Γ k := reln [] k Γ. + Definition to_extended_list Γ := to_extended_list_k Γ 0. + + Lemma reln_fold f ctx n acc : + reln acc n (fold_context_k f ctx) = + reln acc n ctx. + Proof. + induction ctx as [|[na [b|] ty] ctx] in n, acc |- *; simpl; auto; + rewrite fold_context_k_snoc0 /=; apply IHctx. + Qed. + + Lemma reln_list_lift_above l p Γ : + Forall (fun x => exists n, x = tRel n /\ p <= n /\ n < p + length Γ) l -> + Forall (fun x => exists n, x = tRel n /\ p <= n /\ n < p + length Γ) (reln l p Γ). + Proof. + generalize (Nat.le_refl p). + generalize p at 1 3 5. + induction Γ in p, l |- *. simpl. auto. + intros. destruct a. destruct decl_body. simpl. + assert(p0 <= S p) by lia. + specialize (IHΓ l (S p) p0 H1). rewrite <- Nat.add_succ_comm, Nat.add_1_r. + simpl in *. rewrite <- Nat.add_succ_comm in H0. eauto. + simpl in *. + specialize (IHΓ (tRel p :: l) (S p) p0 ltac:(lia)). + rewrite <- Nat.add_succ_comm, Nat.add_1_r. + eapply IHΓ. simpl in *. rewrite <- Nat.add_succ_comm in H0. auto. + simpl in *. + constructor. exists p. intuition lia. auto. + Qed. + + Lemma to_extended_list_k_spec Γ k : + Forall (fun x => exists n, x = tRel n /\ k <= n /\ n < k + length Γ) + (to_extended_list_k Γ k). + Proof. + pose (reln_list_lift_above [] k Γ). + unfold to_extended_list_k. + forward f. constructor. apply f. + Qed. + + Lemma to_extended_list_lift_above Γ : + Forall (fun x => exists n, x = tRel n /\ n < length Γ) (to_extended_list Γ). + Proof. + pose (reln_list_lift_above [] 0 Γ). + unfold to_extended_list. + forward f. constructor. eapply Forall_impl; eauto. intros. + destruct H; eexists; intuition eauto. + Qed. + + Fixpoint reln_alt p (Γ : context) := + match Γ with + | [] => [] + | {| decl_body := Some _ |} :: Γ => reln_alt (p + 1) Γ + | {| decl_body := None |} :: Γ => tRel p :: reln_alt (p + 1) Γ + end. + + Lemma reln_alt_eq l Γ k : reln l k Γ = List.rev (reln_alt k Γ) ++ l. + Proof. + induction Γ in l, k |- *; simpl; auto. + destruct a as [na [body|] ty]; simpl. + now rewrite IHΓ. + now rewrite IHΓ -app_assoc. + Qed. + + Lemma to_extended_list_k_cons d Γ k : + to_extended_list_k (d :: Γ) k = + match d.(decl_body) with + | None => to_extended_list_k Γ (S k) ++ [tRel k] + | Some b => to_extended_list_k Γ (S k) + end. + Proof. + unfold to_extended_list_k. + rewrite reln_alt_eq. simpl. + destruct d as [na [body|] ty]. simpl. + now rewrite reln_alt_eq Nat.add_1_r. + simpl. rewrite reln_alt_eq. + now rewrite <- app_assoc, !app_nil_r, Nat.add_1_r. + Qed. + + + Definition arities_context (l : list one_inductive_body) := + rev_map (fun ind => vass (mkBindAnn (nNamed ind.(ind_name)) + (ind.(ind_relevance))) ind.(ind_type)) l. + + Lemma arities_context_length l : #|arities_context l| = #|l|. + Proof. unfold arities_context. now rewrite rev_map_length. Qed. + #[global] Hint Rewrite arities_context_length : len. + + Lemma app_context_nil_l Γ : [] ,,, Γ = Γ. + Proof. + unfold app_context. rewrite app_nil_r. reflexivity. + Qed. + + Lemma app_context_assoc Γ Γ' Γ'' : Γ ,,, (Γ' ,,, Γ'') = Γ ,,, Γ' ,,, Γ''. + Proof. unfold app_context; now rewrite app_assoc. Qed. + + Lemma app_context_cons Γ Γ' A : Γ ,,, (Γ' ,, A) = (Γ ,,, Γ') ,, A. + Proof. exact (app_context_assoc _ _ [A]). Qed. + + Lemma app_context_length Γ Γ' : #|Γ ,,, Γ'| = #|Γ'| + #|Γ|. + Proof. unfold app_context. now rewrite app_length. Qed. + #[global] Hint Rewrite app_context_length : len. + + Lemma nth_error_app_context_ge v Γ Γ' : + #|Γ'| <= v -> nth_error (Γ ,,, Γ') v = nth_error Γ (v - #|Γ'|). + Proof. apply nth_error_app_ge. Qed. + + Lemma nth_error_app_context_lt v Γ Γ' : + v < #|Γ'| -> nth_error (Γ ,,, Γ') v = nth_error Γ' v. + Proof. apply nth_error_app_lt. Qed. + + + Definition map_mutual_inductive_body f m := + match m with + | Build_mutual_inductive_body finite ind_npars ind_pars ind_bodies ind_universes ind_variance => + let arities := arities_context ind_bodies in + let pars := fold_context_k f ind_pars in + Build_mutual_inductive_body finite ind_npars pars + (map (map_one_inductive_body (context_assumptions pars) (length arities) f) ind_bodies) + ind_universes ind_variance + end. + + Lemma ind_type_map f npars_ass arities oib : + ind_type (map_one_inductive_body npars_ass arities f oib) = f 0 (ind_type oib). + Proof. destruct oib. reflexivity. Qed. + + Lemma ind_ctors_map f npars_ass arities oib : + ind_ctors (map_one_inductive_body npars_ass arities f oib) = + map (map_constructor_body npars_ass arities f) (ind_ctors oib). + Proof. destruct oib; simpl; reflexivity. Qed. + + Lemma ind_pars_map f m : + ind_params (map_mutual_inductive_body f m) = + fold_context_k f (ind_params m). + Proof. destruct m; simpl; reflexivity. Qed. + + Lemma ind_projs_map f npars_ass arities oib : + ind_projs (map_one_inductive_body npars_ass arities f oib) = + map (map_projection_body npars_ass f) (ind_projs oib). + Proof. destruct oib; simpl. reflexivity. Qed. + + Fixpoint projs ind npars k := + match k with + | 0 => [] + | S k' => (tProj (mkProjection ind npars k') (tRel 0)) :: projs ind npars k' + end. + + Lemma projs_length ind npars k : #|projs ind npars k| = k. + Proof. induction k; simpl; auto. Qed. + + Lemma context_assumptions_fold Γ f : context_assumptions (fold_context_k f Γ) = context_assumptions Γ. + Proof. + rewrite fold_context_k_alt. + unfold mapi. generalize 0 (Nat.pred #|Γ|). + induction Γ as [|[na [body|] ty] tl]; cbn; intros; eauto. + Qed. + #[global] Hint Rewrite context_assumptions_fold : len. + + Lemma nth_error_fold_context_k (f : nat -> term -> term): + forall (Γ' Γ'' : context) (v : nat), + v < length Γ' -> forall nth, + nth_error Γ' v = Some nth -> + nth_error (fold_context_k f Γ') v = Some (map_decl (f (length Γ' - S v)) nth). + Proof. + induction Γ'; intros. + - easy. + - simpl. destruct v; rewrite fold_context_k_snoc0. + + simpl. repeat f_equal; try lia. simpl in *. congruence. + + simpl. apply IHΓ'; simpl in *; (lia || congruence). + Qed. + + Lemma nth_error_fold_context_k_eq: + forall (Γ' : context) (v : nat) (f : nat -> term -> term), + nth_error (fold_context_k f Γ') v = + option_map (map_decl (f (length Γ' - S v))) (nth_error Γ' v). + Proof. + induction Γ'; intros. + - simpl. unfold fold_context_k; simpl. now rewrite nth_error_nil. + - simpl. destruct v; rewrite fold_context_k_snoc0. + + simpl. repeat f_equal; try lia. + + simpl. apply IHΓ'; simpl in *; (lia || congruence). + Qed. + + Lemma nth_error_ge {Γ Γ' v Γ''} (f : nat -> term -> term) : + length Γ' <= v -> + nth_error (Γ' ++ Γ) v = + nth_error (fold_context_k f Γ' ++ Γ'' ++ Γ) (length Γ'' + v). + Proof. + intros Hv. + rewrite -> !nth_error_app_ge, ?fold_context_k_length. f_equal. lia. + rewrite fold_context_k_length. lia. + rewrite fold_context_k_length. lia. auto. + Qed. + + Lemma nth_error_lt {Γ Γ' Γ'' v} (f : nat -> term -> term) : + v < length Γ' -> + nth_error (fold_context_k f Γ' ++ Γ'' ++ Γ) v = + option_map (map_decl (f (length Γ' - S v))) (nth_error (Γ' ++ Γ) v). + Proof. + simpl. intros Hv. + rewrite -> !nth_error_app_lt. + rewrite nth_error_fold_context_k_eq. + do 2 f_equal. lia. now rewrite fold_context_k_length. + Qed. + + Lemma context_assumptions_length_bound Γ : context_assumptions Γ <= #|Γ|. + Proof. + induction Γ; simpl; auto. destruct a as [? [?|] ?]; simpl; auto. + lia. + Qed. + + Lemma context_assumptions_map f Γ : context_assumptions (map_context f Γ) = context_assumptions Γ. + Proof. + induction Γ as [|[? [?|] ?] ?]; simpl; auto. + Qed. + + Lemma context_assumptions_app Γ Δ : context_assumptions (Γ ++ Δ) = + context_assumptions Γ + context_assumptions Δ. + Proof. + induction Γ as [|[? [] ?] ?]; simpl; auto. + Qed. + + Lemma context_assumptions_rev Γ : context_assumptions (List.rev Γ) = context_assumptions Γ. + Proof using Type. + induction Γ; simpl; auto. rewrite context_assumptions_app IHΓ /=. + destruct (decl_body a); simpl; lia. + Qed. + + + Lemma context_assumptions_mapi f Γ : context_assumptions (mapi (fun i => map_decl (f i)) Γ) = + context_assumptions Γ. + Proof. + rewrite /mapi; generalize 0. + induction Γ; simpl; intros; eauto. + destruct a as [? [b|] ?]; simpl; auto. + Qed. + + #[global] Hint Rewrite context_assumptions_map context_assumptions_mapi context_assumptions_app : len. + + Lemma context_assumptions_subst_instance u Γ : + context_assumptions (subst_instance u Γ) = + context_assumptions Γ. + Proof. apply context_assumptions_map. Qed. + + Lemma context_assumptions_subst_context s k Γ : + context_assumptions (subst_context s k Γ) = + context_assumptions Γ. + Proof. apply context_assumptions_fold. Qed. + + Lemma context_assumptions_lift_context n k Γ : + context_assumptions (lift_context n k Γ) = + context_assumptions Γ. + Proof. apply context_assumptions_fold. Qed. + + #[global] Hint Rewrite context_assumptions_subst_instance + context_assumptions_subst_context context_assumptions_lift_context : len. + + (** Lifting a relation to declarations, without alpha renaming. *) + Inductive All_decls (P : term -> term -> Type) : context_decl -> context_decl -> Type := + | on_vass na t t' : + P t t' -> + All_decls P (vass na t) (vass na t') + + | on_vdef na b t b' t' : + P b b' -> + P t t' -> + All_decls P (vdef na b t) (vdef na b' t'). + Derive Signature NoConfusion for All_decls. + + (** Allow alpha-renaming of binders *) + Inductive All_decls_alpha (P : term -> term -> Type) : context_decl -> context_decl -> Type := + | on_vass_alpha na na' t t' : + eq_binder_annot na na' -> + P t t' -> + All_decls_alpha P (vass na t) (vass na' t') + + | on_vdef_alpha na na' b t b' t' : + eq_binder_annot na na' -> + P b b' -> + P t t' -> + All_decls_alpha P (vdef na b t) (vdef na' b' t'). + Derive Signature NoConfusion for All_decls_alpha. + + Lemma All_decls_impl (P Q : term -> term -> Type) d d' : + All_decls P d d' -> + (forall t t', P t t' -> Q t t') -> + All_decls Q d d'. + Proof. + intros ond H; destruct ond; constructor; auto. + Qed. + + Lemma All_decls_alpha_impl (P Q : term -> term -> Type) d d' : + All_decls_alpha P d d' -> + (forall t t', P t t' -> Q t t') -> + All_decls_alpha Q d d'. + Proof. + intros ond H; destruct ond; constructor; auto. + Qed. + + Lemma All_decls_to_alpha (P : term -> term -> Type) d d' : + All_decls P d d' -> + All_decls_alpha P d d'. + Proof. + intros []; constructor; auto; reflexivity. + Qed. + + Definition All2_fold_over (P : context -> context -> context_decl -> context_decl -> Type) Γ Γ' := + All2_fold (All_over P Γ Γ'). + + Notation on_decls P := (fun Γ Γ' => All_decls (P Γ Γ')). + Notation on_contexts P := (All2_fold (on_decls P)). + Notation on_contexts_over P Γ Γ' := (All2_fold (All_over (on_decls P) Γ Γ')). + +End Environment. + +Module Type EnvironmentSig (T : Term). + Include Environment T. +End EnvironmentSig. + +Module Type TermUtils (T: Term) (E: EnvironmentSig T). + Import T E. + + Parameter Inline destArity : context -> term -> option (context × Universe.t). + Parameter Inline inds : kername -> Instance.t -> list one_inductive_body -> list term. + +End TermUtils. diff --git a/pcuic/theories/EnvironmentTyping.v b/pcuic/theories/EnvironmentTyping.v new file mode 100644 index 000000000..d5020a507 --- /dev/null +++ b/pcuic/theories/EnvironmentTyping.v @@ -0,0 +1,1457 @@ +(* Distributed under the terms of the MIT license. *) +From Coq Require Import ssreflect ssrbool. +From MetaCoq.Template Require Import config utils BasicAst Universes Primitive. +From MetaCoq.PCUIC Require Import Environment. +From Equations Require Import Equations. + +Module Lookup (T : Term) (E : EnvironmentSig T). + + Import T E. + + (** ** Environment lookup *) + + Definition declared_constant_gen (lookup : kername -> option global_decl) (id : kername) decl : Prop := + lookup id = Some (ConstantDecl decl). + + Definition declared_constant (Σ : global_env) := declared_constant_gen (lookup_env Σ). + + Definition declared_minductive_gen (lookup : kername -> option global_decl) mind decl := + lookup mind = Some (InductiveDecl decl). + + Definition declared_minductive Σ := declared_minductive_gen (lookup_env Σ). + + Definition declared_inductive_gen lookup ind mdecl decl := + declared_minductive_gen lookup (inductive_mind ind) mdecl /\ + List.nth_error mdecl.(ind_bodies) (inductive_ind ind) = Some decl. + + Definition declared_inductive Σ := declared_inductive_gen (lookup_env Σ). + + Definition declared_constructor_gen lookup cstr mdecl idecl cdecl : Prop := + declared_inductive_gen lookup (fst cstr) mdecl idecl /\ + List.nth_error idecl.(ind_ctors) (snd cstr) = Some cdecl. + + Definition declared_constructor Σ := declared_constructor_gen (lookup_env Σ). + + Definition declared_projection_gen lookup (proj : projection) mdecl idecl cdecl pdecl + : Prop := + declared_constructor_gen lookup (proj.(proj_ind), 0) mdecl idecl cdecl /\ + List.nth_error idecl.(ind_projs) proj.(proj_arg) = Some pdecl /\ + mdecl.(ind_npars) = proj.(proj_npars). + + Definition declared_projection Σ := declared_projection_gen (lookup_env Σ). + + Definition lookup_constant_gen (lookup : kername -> option global_decl) kn := + match lookup kn with + | Some (ConstantDecl d) => Some d + | _ => None + end. + + Definition lookup_constant Σ := lookup_constant_gen (lookup_env Σ). + + Definition lookup_minductive_gen (lookup : kername -> option global_decl) mind := + match lookup mind with + | Some (InductiveDecl decl) => Some decl + | _ => None + end. + + Definition lookup_minductive Σ := lookup_minductive_gen (lookup_env Σ). + + Definition lookup_inductive_gen lookup ind := + match lookup_minductive_gen lookup (inductive_mind ind) with + | Some mdecl => + match nth_error mdecl.(ind_bodies) (inductive_ind ind) with + | Some idecl => Some (mdecl, idecl) + | None => None + end + | None => None + end. + + Definition lookup_inductive Σ := lookup_inductive_gen (lookup_env Σ). + + Definition lookup_constructor_gen lookup ind k := + match lookup_inductive_gen lookup ind with + | Some (mdecl, idecl) => + match nth_error idecl.(ind_ctors) k with + | Some cdecl => Some (mdecl, idecl, cdecl) + | None => None + end + | _ => None + end. + + Definition lookup_constructor Σ := lookup_constructor_gen (lookup_env Σ). + + Definition lookup_projection_gen lookup p := + match lookup_constructor_gen lookup p.(proj_ind) 0 with + | Some (mdecl, idecl, cdecl) => + match nth_error idecl.(ind_projs) p.(proj_arg) with + | Some pdecl => Some (mdecl, idecl, cdecl, pdecl) + | None => None + end + | _ => None + end. + + Definition lookup_projection Σ := lookup_projection_gen (lookup_env Σ). + + Lemma declared_constant_lookup {lookup kn cdecl} : + declared_constant_gen lookup kn cdecl -> + lookup_constant_gen lookup kn = Some cdecl. + Proof. + unfold declared_constant_gen, lookup_constant_gen. + now intros ->. + Qed. + + Lemma lookup_constant_declared {lookup kn cdecl} : + lookup_constant_gen lookup kn = Some cdecl -> + declared_constant_gen lookup kn cdecl. + Proof. + unfold declared_constant_gen, lookup_constant_gen. + destruct lookup as [[]|] => //. congruence. + Qed. + + Lemma declared_minductive_lookup {lookup ind mdecl} : + declared_minductive_gen lookup ind mdecl -> + lookup_minductive_gen lookup ind = Some mdecl. + Proof. + rewrite /declared_minductive_gen /lookup_minductive_gen. + now intros ->. + Qed. + + Lemma lookup_minductive_declared {lookup ind mdecl} : + lookup_minductive_gen lookup ind = Some mdecl -> + declared_minductive_gen lookup ind mdecl. + Proof. + rewrite /declared_minductive_gen /lookup_minductive_gen. + destruct lookup as [[]|] => //. congruence. + Qed. + + Lemma declared_inductive_lookup {lookup ind mdecl idecl} : + declared_inductive_gen lookup ind mdecl idecl -> + lookup_inductive_gen lookup ind = Some (mdecl, idecl). + Proof. + rewrite /declared_inductive_gen /lookup_inductive_gen. + intros []. now rewrite (declared_minductive_lookup H) H0. + Qed. + + Lemma lookup_inductive_declared {lookup ind mdecl idecl} : + lookup_inductive_gen lookup ind = Some (mdecl, idecl) -> + declared_inductive_gen lookup ind mdecl idecl. + Proof. + rewrite /declared_inductive_gen /lookup_inductive_gen. + destruct lookup_minductive_gen as [[]|] eqn:hl => //=. + destruct nth_error eqn:hnth => //. intros [= <- <-]. + split => //. + apply (lookup_minductive_declared hl). + Qed. + + Lemma declared_constructor_lookup {lookup id mdecl idecl cdecl} : + declared_constructor_gen lookup id mdecl idecl cdecl -> + lookup_constructor_gen lookup id.1 id.2 = Some (mdecl, idecl, cdecl). + Proof. + intros []. unfold lookup_constructor_gen. + rewrite (declared_inductive_lookup (lookup := lookup) H) /= H0 //. + Qed. + + Lemma lookup_constructor_declared {lookup id mdecl idecl cdecl} : + lookup_constructor_gen lookup id.1 id.2 = Some (mdecl, idecl, cdecl) -> + declared_constructor_gen lookup id mdecl idecl cdecl. + Proof. + unfold lookup_constructor_gen. + destruct lookup_inductive_gen as [[]|] eqn:hl => //=. + destruct nth_error eqn:hnth => //. intros [= <- <-]. + split => //. + apply (lookup_inductive_declared hl). congruence. + Qed. + + Lemma declared_projection_lookup {lookup p mdecl idecl cdecl pdecl} : + declared_projection_gen lookup p mdecl idecl cdecl pdecl -> + lookup_projection_gen lookup p = Some (mdecl, idecl, cdecl, pdecl). + Proof. + intros [? []]. unfold lookup_projection_gen. + rewrite (declared_constructor_lookup (lookup := lookup) H) /= H0 //. + Qed. + + Lemma lookup_projection_declared {lookup p mdecl idecl cdecl pdecl} : + ind_npars mdecl = p.(proj_npars) -> + lookup_projection_gen lookup p = Some (mdecl, idecl, cdecl, pdecl) -> + declared_projection_gen lookup p mdecl idecl cdecl pdecl. + Proof. + intros hp. unfold lookup_projection_gen. + destruct lookup_constructor_gen as [[[] ?]|] eqn:hl => //=. + destruct nth_error eqn:hnth => //. intros [= <- <-]. subst c p0. + split => //. + apply (lookup_constructor_declared (id:=(proj_ind p, 0)) hl). + Qed. + + Definition on_udecl_decl {A} (F : universes_decl -> A) d : A := + match d with + | ConstantDecl cb => F cb.(cst_universes) + | InductiveDecl mb => F mb.(ind_universes) + end. + + Definition universes_decl_of_decl := on_udecl_decl (fun x => x). + + (* Definition LevelSet_add_list l := LevelSet.union (LevelSetProp.of_list l). *) + + Definition global_levels (univs : ContextSet.t) : LevelSet.t := + LevelSet.union (ContextSet.levels univs) (LevelSet.singleton (Level.lzero)). + + Lemma global_levels_InSet Σ : + LevelSet.In Level.lzero (global_levels Σ). + Proof. + apply LevelSet.union_spec; right. + now apply LevelSet.singleton_spec. + Qed. + + Lemma global_levels_memSet univs : + LevelSet.mem Level.lzero (global_levels univs) = true. + Proof. + apply LevelSet.mem_spec, global_levels_InSet. + Qed. + + (** One can compute the constraints associated to a global environment or its + extension by folding over its constituent definitions. + + We make *only* the second of these computations an implicit coercion + for more readability. Note that [fst_ctx] is also a coercion which goes + from a [global_env_ext] to a [global_env]: coercion coherence would *not* + be ensured if we added [global_constraints] as well as a coercion, as it + would forget the extension's constraints. *) + + Definition global_constraints (Σ : global_env) : ConstraintSet.t := + snd Σ.(universes). + + Definition global_uctx (Σ : global_env) : ContextSet.t := + (global_levels Σ.(universes), global_constraints Σ). + + Definition global_ext_levels (Σ : global_env_ext) : LevelSet.t := + LevelSet.union (levels_of_udecl (snd Σ)) (global_levels Σ.1.(universes)). + + Definition global_ext_constraints (Σ : global_env_ext) : ConstraintSet.t := + ConstraintSet.union + (constraints_of_udecl (snd Σ)) + (global_constraints Σ.1). + + Coercion global_ext_constraints : global_env_ext >-> ConstraintSet.t. + + Definition global_ext_uctx (Σ : global_env_ext) : ContextSet.t := + (global_ext_levels Σ, global_ext_constraints Σ). + + + Lemma global_ext_levels_InSet Σ : + LevelSet.In Level.lzero (global_ext_levels Σ). + Proof. + apply LevelSet.union_spec; right. + now apply global_levels_InSet. + Qed. + + (** Check that [uctx] instantiated at [u] is consistent with + the current universe graph. *) + + Definition consistent_instance `{checker_flags} (lvs : LevelSet.t) (φ : ConstraintSet.t) uctx (u : Instance.t) := + match uctx with + | Monomorphic_ctx => List.length u = 0 + | Polymorphic_ctx c => + (* levels of the instance already declared *) + forallb (fun l => LevelSet.mem l lvs) u /\ + List.length u = List.length c.1 /\ + valid_constraints φ (subst_instance_cstrs u c.2) + end. + + Definition consistent_instance_ext `{checker_flags} Σ := + consistent_instance (global_ext_levels Σ) (global_ext_constraints Σ). + + Lemma consistent_instance_length {cf : checker_flags} {Σ : global_env_ext} {univs u} : + consistent_instance_ext Σ univs u -> + #|u| = #|abstract_instance univs|. + Proof. + unfold consistent_instance_ext, consistent_instance. + destruct univs; simpl; auto. + intros [_ [H _]]. + destruct cst; simpl in *. + now rewrite H; cbn; autorewrite with len. + Qed. + + Definition wf_universe Σ s : Prop := + Universe.on_sort + (fun u => forall l, LevelExprSet.In l u -> LevelSet.In (LevelExpr.get_level l) (global_ext_levels Σ)) + True s. + + Lemma declared_ind_declared_constructors `{cf : checker_flags} {Σ ind mib oib} : + declared_inductive Σ ind mib oib -> + Alli (fun i => declared_constructor Σ (ind, i) mib oib) 0 (ind_ctors oib). + Proof using. + move=> inddecl. + apply: forall_nth_error_Alli=> /= i x eq. + apply: lookup_constructor_declared=> /=. + rewrite /lookup_constructor_gen (declared_inductive_lookup inddecl) eq //. + Qed. + +End Lookup. + +Module Type LookupSig (T : Term) (E : EnvironmentSig T). + Include Lookup T E. +End LookupSig. + +Module EnvTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E). + + Import T E TU. + + Section TypeLocal. + Context (typing : forall (Γ : context), term -> typ_or_sort -> Type). + + Inductive All_local_env : context -> Type := + | localenv_nil : + All_local_env [] + + | localenv_cons_abs Γ na t : + All_local_env Γ -> + typing Γ t Sort -> + All_local_env (Γ ,, vass na t) + + | localenv_cons_def Γ na b t : + All_local_env Γ -> + typing Γ t Sort -> + typing Γ b (Typ t) -> + All_local_env (Γ ,, vdef na b t). + Derive Signature NoConfusion for All_local_env. + End TypeLocal. + + Arguments localenv_nil {_}. + Arguments localenv_cons_def {_ _ _ _ _} _ _. + Arguments localenv_cons_abs {_ _ _ _} _ _. + + Lemma All_local_env_fold P f Γ : + All_local_env (fun Γ t T => P (fold_context_k f Γ) (f #|Γ| t) (typ_or_sort_map (f #|Γ|) T)) Γ <~> + All_local_env P (fold_context_k f Γ). + Proof. + split. + - induction 1; simpl; try unfold snoc; rewrite ?fold_context_k_snoc0; try constructor; auto. + - induction Γ; simpl; try unfold snoc; rewrite ?fold_context_k_snoc0; intros H. + * constructor. + * destruct a as [na [b|] ty]; depelim H; specialize (IHΓ H); constructor; simpl; auto. + Qed. + + Lemma All_local_env_impl (P Q : context -> term -> typ_or_sort -> Type) l : + All_local_env P l -> + (forall Γ t T, P Γ t T -> Q Γ t T) -> + All_local_env Q l. + Proof. + induction 1; intros; simpl; econstructor; eauto. + Qed. + + Lemma All_local_env_impl_ind {P Q : context -> term -> typ_or_sort -> Type} {l} : + All_local_env P l -> + (forall Γ t T, All_local_env Q Γ -> P Γ t T -> Q Γ t T) -> + All_local_env Q l. + Proof. + induction 1; intros; simpl; econstructor; eauto. + Qed. + + Lemma All_local_env_skipn P Γ : All_local_env P Γ -> forall n, All_local_env P (skipn n Γ). + Proof. + induction 1; simpl; intros; destruct n; simpl; try econstructor; eauto. + Qed. + #[global] + Hint Resolve All_local_env_skipn : wf. + + Section All_local_env_rel. + + Definition All_local_rel P Γ Γ' + := (All_local_env (fun Γ0 t T => P (Γ ,,, Γ0) t T) Γ'). + + Definition All_local_rel_nil {P Γ} : All_local_rel P Γ [] + := localenv_nil. + + Definition All_local_rel_abs {P Γ Γ' A na} : + All_local_rel P Γ Γ' -> P (Γ ,,, Γ') A Sort + -> All_local_rel P Γ (Γ',, vass na A) + := localenv_cons_abs. + + Definition All_local_rel_def {P Γ Γ' t A na} : + All_local_rel P Γ Γ' -> + P (Γ ,,, Γ') A Sort -> + P (Γ ,,, Γ') t (Typ A) -> + All_local_rel P Γ (Γ',, vdef na t A) + := localenv_cons_def. + + Lemma All_local_rel_local : + forall P Γ, + All_local_env P Γ -> + All_local_rel P [] Γ. + Proof. + intros P Γ h. eapply All_local_env_impl. + - exact h. + - intros Δ t [] h'. + all: cbn. + + rewrite app_context_nil_l. assumption. + + rewrite app_context_nil_l. assumption. + Defined. + + Lemma All_local_local_rel P Γ : + All_local_rel P [] Γ -> All_local_env P Γ. + Proof. + intro X. eapply All_local_env_impl. exact X. + intros Γ0 t [] XX; cbn in XX; rewrite app_context_nil_l in XX; assumption. + Defined. + + Lemma All_local_app_rel {P Γ Γ'} : + All_local_env P (Γ ,,, Γ') -> All_local_env P Γ × All_local_rel P Γ Γ'. + Proof. + induction Γ'. + - intros hΓ. + split. + 1: exact hΓ. + constructor. + - inversion 1 ; subst. + all: edestruct IHΓ' ; auto. + all: split ; auto. + all: constructor ; auto. + Defined. + + Lemma All_local_rel_app {P Γ Γ'} : + All_local_env P Γ -> All_local_rel P Γ Γ' -> All_local_env P (Γ ,,, Γ'). + Proof. + intros ? hΓ'. + induction hΓ'. + - assumption. + - cbn. + constructor ; auto. + - cbn. + constructor ; auto. + Defined. + + End All_local_env_rel. + + (** Well-formedness of local environments embeds a sorting for each variable *) + + Definition on_local_decl (P : context -> term -> typ_or_sort -> Type) Γ d := + match d.(decl_body) with + | Some b => P Γ b (Typ d.(decl_type)) + | None => P Γ d.(decl_type) Sort + end. + + Definition on_def_type (P : context -> term -> typ_or_sort -> Type) Γ d := + P Γ d.(dtype) Sort. + + Definition on_def_body (P : context -> term -> typ_or_sort -> Type) types Γ d := + P (Γ ,,, types) d.(dbody) (Typ (lift0 #|types| d.(dtype))). + + Definition lift_judgment + (check : global_env_ext -> context -> term -> term -> Type) + (infer_sort : global_env_ext -> context -> term -> Type) : + (global_env_ext -> context -> term -> typ_or_sort -> Type) := + fun Σ Γ t T => + match T with + | Typ T => check Σ Γ t T + | Sort => infer_sort Σ Γ t + end. + + Lemma lift_judgment_impl {P Ps Q Qs Σ Σ' Γ Γ' t t' T} : + lift_judgment P Ps Σ Γ t T -> + (forall T, P Σ Γ t T -> Q Σ' Γ' t' T) -> + (Ps Σ Γ t -> Qs Σ' Γ' t') -> + lift_judgment Q Qs Σ' Γ' t' T. + Proof. + intros HT HPQ HPsQs. + destruct T; simpl. + * apply HPQ, HT. + * apply HPsQs, HT. + Qed. + + (* Common uses *) + + Definition lift_wf_term wf_term := (lift_judgment (fun Σ Γ t T => wf_term Σ Γ t × wf_term Σ Γ T) wf_term). + + Definition infer_sort (sorting : global_env_ext -> context -> term -> Universe.t -> Type) := (fun Σ Γ T => { s : Universe.t & sorting Σ Γ T s }). + Notation typing_sort typing := (fun Σ Γ T s => typing Σ Γ T (tSort s)). + + Definition lift_typing typing := lift_judgment typing (infer_sort (typing_sort typing)). + Definition lift_sorting checking sorting := lift_judgment checking (infer_sort sorting). + + Notation Prop_conj P Q := (fun Σ Γ t T => P Σ Γ t T × Q Σ Γ t T). + + Definition lift_typing2 P Q := lift_typing (Prop_conj P Q). + + Lemma infer_sort_impl {P Q} {Σ Σ' : global_env_ext} {Γ Γ' : context} {t t' : term} : + forall f, forall tu: infer_sort P Σ Γ t, + let s := tu.π1 in + (P Σ Γ t s -> Q Σ' Γ' t' (f s)) -> + infer_sort Q Σ' Γ' t'. + Proof. + intros ? (? & Hs) s HPQ. eexists. now apply HPQ. + Qed. + + Lemma infer_typing_sort_impl {P Q} {Σ Σ' : global_env_ext} {Γ Γ' : context} {t t' : term} : + forall f, forall tu: infer_sort (typing_sort P) Σ Γ t, + let s := tu.π1 in + (P Σ Γ t (tSort s) -> Q Σ' Γ' t' (tSort (f s))) -> + infer_sort (typing_sort Q) Σ' Γ' t'. + Proof. + apply (infer_sort_impl (P := typing_sort P) (Q := typing_sort Q)). + Qed. + + Lemma lift_typing_impl {P Q Σ Σ' Γ Γ' t t' T} : + lift_typing P Σ Γ t T -> + (forall T, P Σ Γ t T -> Q Σ' Γ' t' T) -> + lift_typing Q Σ' Γ' t' T. + Proof. + intros HT HPQ. + apply lift_judgment_impl with (1 := HT); tas. + intro Hs; apply infer_typing_sort_impl with id Hs; apply HPQ. + Qed. + + Section TypeLocalOver. + Context (checking : global_env_ext -> context -> term -> term -> Type). + Context (sorting : global_env_ext -> context -> term -> Type). + Context (cproperty : forall (Σ : global_env_ext) (Γ : context), + All_local_env (lift_judgment checking sorting Σ) Γ -> + forall (t T : term), checking Σ Γ t T -> Type). + Context (sproperty : forall (Σ : global_env_ext) (Γ : context), + All_local_env (lift_judgment checking sorting Σ) Γ -> + forall (t : term), sorting Σ Γ t -> Type). + + Inductive All_local_env_over_gen (Σ : global_env_ext) : + forall (Γ : context), All_local_env (lift_judgment checking sorting Σ) Γ -> Type := + | localenv_over_nil : + All_local_env_over_gen Σ [] localenv_nil + + | localenv_over_cons_abs Γ na t + (all : All_local_env (lift_judgment checking sorting Σ) Γ) : + All_local_env_over_gen Σ Γ all -> + forall (tu : lift_judgment checking sorting Σ Γ t Sort) + (Hs: sproperty Σ Γ all _ tu), + All_local_env_over_gen Σ (Γ ,, vass na t) + (localenv_cons_abs all tu) + + | localenv_over_cons_def Γ na b t + (all : All_local_env (lift_judgment checking sorting Σ) Γ) (tb : checking Σ Γ b t) : + All_local_env_over_gen Σ Γ all -> + forall (Hc: cproperty Σ Γ all _ _ tb), + forall (tu : lift_judgment checking sorting Σ Γ t Sort) + (Hs: sproperty Σ Γ all _ tu), + All_local_env_over_gen Σ (Γ ,, vdef na b t) + (localenv_cons_def all tu tb). + + End TypeLocalOver. + Derive Signature for All_local_env_over_gen. + + Definition All_local_env_over typing property := + (All_local_env_over_gen typing (infer_sort (typing_sort typing)) property (fun Σ Γ H t tu => property _ _ H _ _ tu.π2)). + + Definition All_local_env_over_sorting checking sorting cproperty (sproperty : forall Σ Γ _ t s, sorting Σ Γ t s -> Type) := + (All_local_env_over_gen checking (infer_sort sorting) cproperty (fun Σ Γ H t tu => sproperty Σ Γ H t tu.π1 tu.π2)). + + Section TypeCtxInst. + Context (typing : forall (Σ : global_env_ext) (Γ : context), term -> term -> Type). + + (* Γ |- s : Δ, where Δ is a telescope (reverse context) *) + Inductive ctx_inst Σ (Γ : context) : list term -> context -> Type := + | ctx_inst_nil : ctx_inst Σ Γ [] [] + | ctx_inst_ass na t i inst Δ : + typing Σ Γ i t -> + ctx_inst Σ Γ inst (subst_telescope [i] 0 Δ) -> + ctx_inst Σ Γ (i :: inst) (vass na t :: Δ) + | ctx_inst_def na b t inst Δ : + ctx_inst Σ Γ inst (subst_telescope [b] 0 Δ) -> + ctx_inst Σ Γ inst (vdef na b t :: Δ). + Derive Signature NoConfusion for ctx_inst. + End TypeCtxInst. + + Lemma ctx_inst_impl P Q Σ Γ inst Δ : + ctx_inst P Σ Γ inst Δ -> + (forall t T, P Σ Γ t T -> Q Σ Γ t T) -> + ctx_inst Q Σ Γ inst Δ. + Proof. + intros H HPQ. induction H; econstructor; auto. + Qed. + + Section All_local_env_size. + Context {P : forall (Σ : global_env_ext) (Γ : context), term -> typ_or_sort -> Type}. + Context (Psize : forall (Σ : global_env_ext) Γ t T, P Σ Γ t T -> size). + + Fixpoint All_local_env_size_gen base Σ Γ (w : All_local_env (P Σ) Γ) : size := + match w with + | localenv_nil => base + | localenv_cons_abs Γ' na t w' p => Psize _ _ _ _ p + All_local_env_size_gen base _ _ w' + | localenv_cons_def Γ' na b t w' pt pb => Psize _ _ _ _ pt + Psize _ _ _ _ pb + All_local_env_size_gen base _ _ w' + end. + + Lemma All_local_env_size_pos base Σ Γ w : base <= All_local_env_size_gen base Σ Γ w. + Proof using Type. + induction w. + all: simpl ; lia. + Qed. + End All_local_env_size. + + Notation All_local_rel_size_gen Psize base := (fun Σ Γ Δ (w : All_local_rel _ Γ Δ) => + All_local_env_size_gen (fun Σ Δ => Psize Σ (Γ ,,, Δ)) base Σ Δ w). + + Lemma All_local_env_size_app P Psize base Σ Γ Γ' (wfΓ : All_local_env (P Σ) Γ) (wfΓ' : All_local_rel (P Σ) Γ Γ') : + All_local_env_size_gen Psize base _ _ (All_local_rel_app wfΓ wfΓ') + base = All_local_env_size_gen Psize base _ _ wfΓ + All_local_rel_size_gen Psize base _ _ _ wfΓ'. + Proof. + induction Γ'. + - dependent inversion wfΓ'. + reflexivity. + - revert IHΓ'. + dependent inversion wfΓ' ; subst ; intros. + + cbn. + etransitivity. + 2: rewrite Nat.add_comm -Nat.add_assoc [X in _ + X]Nat.add_comm -IHΓ' Nat.add_assoc ; reflexivity. + reflexivity. + + cbn. + etransitivity. + 2: rewrite Nat.add_comm -Nat.add_assoc [X in _ + X]Nat.add_comm -IHΓ' Nat.add_assoc ; reflexivity. + reflexivity. + Qed. + + Section lift_judgment_size. + Context {checking : global_env_ext -> context -> term -> term -> Type}. + Context {sorting : global_env_ext -> context -> term -> Type}. + Context (csize : forall (Σ : global_env_ext) (Γ : context) (t T : term), checking Σ Γ t T -> size). + Context (ssize : forall (Σ : global_env_ext) (Γ : context) (t : term), sorting Σ Γ t -> size). + + Definition lift_judgment_size Σ Γ t T (w : lift_judgment checking sorting Σ Γ t T) : size := + match T return lift_judgment checking sorting Σ Γ t T -> size with + | Typ T => csize _ _ _ _ + | Sort => ssize _ _ _ + end w. + End lift_judgment_size. + + Implicit Types (Σ : global_env_ext) (Γ : context) (t : term). + + Notation infer_sort_size typing_size := (fun Σ Γ t (tu: infer_sort _ Σ Γ t) => let 'existT s d := tu in typing_size Σ Γ t s d). + Notation typing_sort_size typing_size := (fun Σ Γ t s (tu: typing_sort _ Σ Γ t s) => typing_size Σ Γ t (tSort s) tu). + + Section Regular. + Context {typing : global_env_ext -> context -> term -> term -> Type}. + Context (typing_size : forall Σ Γ t T, typing Σ Γ t T -> size). + + Definition lift_typing_size := lift_judgment_size typing_size (infer_sort_size (typing_sort_size typing_size)). + Definition All_local_env_size := All_local_env_size_gen lift_typing_size 0. + Definition All_local_rel_size := All_local_rel_size_gen lift_typing_size 0. + End Regular. + + Section Bidirectional. + Context {checking : global_env_ext -> context -> term -> term -> Type} {sorting : global_env_ext -> context -> term -> Universe.t -> Type}. + Context (checking_size : forall Σ Γ t T, checking Σ Γ t T -> size). + Context (sorting_size : forall Σ Γ t s, sorting Σ Γ t s -> size). + + Definition lift_sorting_size := lift_judgment_size checking_size (infer_sort_size sorting_size). + Definition All_local_env_sorting_size := All_local_env_size_gen lift_sorting_size 1. + Definition All_local_rel_sorting_size := All_local_rel_size_gen lift_sorting_size 1. + End Bidirectional. + +End EnvTyping. + +Module Type EnvTypingSig (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E). + Include EnvTyping T E TU. +End EnvTypingSig. + +Module Conversion (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E) (ET : EnvTypingSig T E TU). + Import T E TU ET. + + Section Conversion. + Context (cumul_gen : global_env_ext -> context -> conv_pb -> term -> term -> Type). + + Inductive All_decls_alpha_pb {pb} {P : conv_pb -> term -> term -> Type} : + context_decl -> context_decl -> Type := + | all_decls_alpha_vass {na na' : binder_annot name} {t t' : term} + (eqna : eq_binder_annot na na') + (eqt : P pb t t') : + All_decls_alpha_pb (vass na t) (vass na' t') + + | all_decls_alpha_vdef {na na' : binder_annot name} {b t b' t' : term} + (eqna : eq_binder_annot na na') + (eqb : P Conv b b') (* Note that definitions must be convertible, otherwise this notion + of cumulativity is useless *) + (eqt : P pb t t') : + All_decls_alpha_pb (vdef na b t) (vdef na' b' t'). + + Derive Signature NoConfusion for All_decls_alpha_pb. + + Arguments All_decls_alpha_pb pb P : clear implicits. + + Definition cumul_pb_decls pb (Σ : global_env_ext) (Γ Γ' : context) : forall (x y : context_decl), Type := + All_decls_alpha_pb pb (cumul_gen Σ Γ). + + Definition cumul_pb_context pb (Σ : global_env_ext) := + All2_fold (cumul_pb_decls pb Σ). + + Definition cumul_ctx_rel Σ Γ Δ Δ' := + All2_fold (fun Δ Δ' => cumul_pb_decls Cumul Σ (Γ ,,, Δ) (Γ ,,, Δ')) Δ Δ'. + End Conversion. + + Arguments All_decls_alpha_pb pb P : clear implicits. + Notation conv cumul_gen Σ Γ := (cumul_gen Σ Γ Conv). + Notation cumul cumul_gen Σ Γ := (cumul_gen Σ Γ Cumul). + + Notation conv_decls cumul_gen := (cumul_pb_decls cumul_gen Conv). + Notation cumul_decls cumul_gen := (cumul_pb_decls cumul_gen Cumul). + Notation conv_context cumul_gen Σ := (cumul_pb_context cumul_gen Conv Σ). + Notation cumul_context cumul_gen Σ := (cumul_pb_context cumul_gen Cumul Σ). + +End Conversion. + +Module Type ConversionSig (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E) (ET : EnvTypingSig T E TU). + Include Conversion T E TU ET. +End ConversionSig. + + +Module GlobalMaps (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvTypingSig T E TU) (C: ConversionSig T E TU ET) (L: LookupSig T E). + (** *** Typing of inductive declarations *) + Import T E TU ET C L. + + Section GlobalMaps. + + Context {cf: checker_flags}. + Context (Pcmp: global_env_ext -> context -> conv_pb -> term -> term -> Type). + Context (P : global_env_ext -> context -> term -> typ_or_sort -> Type). + Definition on_context Σ ctx := + All_local_env (P Σ) ctx. + + (** For well-formedness of inductive declarations we need a way to check that a assumptions + of a given context is typable in a sort [u]. We also force well-typing of the let-ins + in any universe to imply wf_local. *) + Fixpoint type_local_ctx Σ (Γ Δ : context) (u : Universe.t) : Type := + match Δ with + | [] => wf_universe Σ u + | {| decl_body := None; decl_type := t |} :: Δ => type_local_ctx Σ Γ Δ u × P Σ (Γ ,,, Δ) t (Typ (tSort u)) + | {| decl_body := Some b; decl_type := t |} :: Δ => type_local_ctx Σ Γ Δ u × P Σ (Γ ,,, Δ) t Sort × P Σ (Γ ,,, Δ) b (Typ t) + end. + + Fixpoint sorts_local_ctx Σ (Γ Δ : context) (us : list Universe.t) : Type := + match Δ, us with + | [], [] => unit + | {| decl_body := None; decl_type := t |} :: Δ, u :: us => + sorts_local_ctx Σ Γ Δ us × P Σ (Γ ,,, Δ) t (Typ (tSort u)) + | {| decl_body := Some b; decl_type := t |} :: Δ, us => + sorts_local_ctx Σ Γ Δ us × P Σ (Γ ,,, Δ) t Sort × P Σ (Γ ,,, Δ) b (Typ t) + | _, _ => False + end. + + Implicit Types (mdecl : mutual_inductive_body) (idecl : one_inductive_body) (cdecl : constructor_body). + + Definition on_type Σ Γ T := P Σ Γ T Sort. + + Open Scope type_scope. + + Definition univs_ext_constraints univs φ := + ConstraintSet.union (constraints_of_udecl φ) univs. + + Definition satisfiable_udecl (univs : ContextSet.t) φ + := consistent (univs_ext_constraints (ContextSet.constraints univs) φ). + + (* Constraints from udecl between *global* universes + are implied by the constraints in univs *) + Definition valid_on_mono_udecl (univs : ContextSet.t) ϕ := + consistent_extension_on univs (constraints_of_udecl ϕ). + + (* Check that: *) + (* - declared levels are fresh *) + (* - all levels used in constraints are declared *) + Definition on_udecl (univs : ContextSet.t) (udecl : universes_decl) + := let levels := levels_of_udecl udecl in + let global_levels := global_levels univs in + let all_levels := LevelSet.union levels global_levels in + LevelSet.For_all (fun l => ~ LevelSet.In l global_levels) levels + /\ ConstraintSet.For_all (declared_cstr_levels all_levels) (constraints_of_udecl udecl) + /\ satisfiable_udecl univs udecl + /\ valid_on_mono_udecl univs udecl. + + (** Positivity checking of the inductive, ensuring that the inductive itself + can only appear at the right of an arrow in each argument's types. *) + (* + Definition positive_cstr_arg ninds npars narg (arg : term) : bool := + (* We decompose the constructor's arguments' type and verify the inductive references + only appear in the conclusion, if any. *) + let (ctx, concl) := decompose_prod_assum [] arg in + (* Again, we smash the context, as Coq does *) + let ctx := smash_context [] ctx in + alli (fun i d => noccur_between (npars + narg + i) ninds d.(decl_type)) 0 (List.rev ctx) && + let (hd, args) := decompose_app concl in + match hd with + | tRel i => + if noccur_between (npars + narg + #|ctx|) ninds (tRel i) then + (* Call to an unrelated variable *) + true + else (* Recursive call to the inductive *) + (* Coq disallows the inductive to be applied to another inductive in the block *) + forallb (noccur_between (npars + narg + #|ctx|) ninds) args + | tInd ind u => + if forallb (noccur_between (npars + narg + #|ctx|) ninds) args then + (* Unrelated inductive *) + true + else (* Nested inductive *) + true + end. + + Definition positive_cstr_args ninds npars (args : context) : bool := + alli (fun i decl => positive_cstr_arg nind npars i decl.(decl_type)) + (* We smash the context, just as Coq's kernel computes positivity on + weak-head normalized types *) + (List.rev (smash_context [] args)) + *) + + (** A constructor argument type [t] is positive w.r.t. an inductive block [mdecl] + when it's zeta-normal form is of the shape Π Δ. concl and: + - [t] does not refer to any inductive in the block. + In that case [t] must be a closed type under the context of parameters and + previous arguments. + - None of the variable assumptions in Δ refer to any inductive in the block, + but the conclusion [concl] is of the form [mkApps (tRel k) args] for k + refering to an inductive in the block, and none of the arguments [args] + refer to the inductive. #|args| must be the length of the full inductive application. + + Let-in assumptions in Δ are systematically unfolded, i.e. we really consider: + the zeta-reduction of [t]. *) + + Definition ind_realargs (o : one_inductive_body) := + match destArity [] o.(ind_type) with + | Some (ctx, _) => #|smash_context [] ctx| + | _ => 0 + end. + + Inductive positive_cstr_arg mdecl ctx : term -> Type := + | positive_cstr_arg_closed t : + closedn #|ctx| t -> + positive_cstr_arg mdecl ctx t + + | positive_cstr_arg_concl l k i : + (** Mutual inductive references in the conclusion are ok *) + #|ctx| <= k -> k < #|ctx| + #|mdecl.(ind_bodies)| -> + All (closedn #|ctx|) l -> + nth_error (List.rev mdecl.(ind_bodies)) (k - #|ctx|) = Some i -> + #|l| = ind_realargs i -> + positive_cstr_arg mdecl ctx (mkApps (tRel k) l) + + | positive_cstr_arg_let na b ty t : + positive_cstr_arg mdecl ctx (subst [b] 0 t) -> + positive_cstr_arg mdecl ctx (tLetIn na b ty t) + + | positive_cstr_arg_ass na ty t : + closedn #|ctx| ty -> + positive_cstr_arg mdecl (vass na ty :: ctx) t -> + positive_cstr_arg mdecl ctx (tProd na ty t). + + (** A constructor type [t] is positive w.r.t. an inductive block [mdecl] + and inductive [i] when it's zeta normal-form is of the shape Π Δ. concl and: + - All of the arguments in Δ are positive. + - The conclusion is of the shape [mkApps (tRel k) indices] + where [k] refers to the current inductive [i] and [indices] does not mention + any of the inductive types in the block. I.e. [indices] are closed terms + in [params ,,, args]. *) + + Inductive positive_cstr mdecl i (ctx : context) : term -> Type := + | positive_cstr_concl indices : + let headrel : nat := + (#|mdecl.(ind_bodies)| - S i + #|ctx|)%nat in + All (closedn #|ctx|) indices -> + positive_cstr mdecl i ctx (mkApps (tRel headrel) indices) + + | positive_cstr_let na b ty t : + positive_cstr mdecl i ctx (subst [b] 0 t) -> + positive_cstr mdecl i ctx (tLetIn na b ty t) + + | positive_cstr_ass na ty t : + positive_cstr_arg mdecl ctx ty -> + positive_cstr mdecl i (vass na ty :: ctx) t -> + positive_cstr mdecl i ctx (tProd na ty t). + + Definition lift_level n l := + match l with + | Level.lzero | Level.Level _ => l + | Level.Var k => Level.Var (n + k) + end. + + Definition lift_instance n l := + map (lift_level n) l. + + Definition lift_constraint n (c : Level.t * ConstraintType.t * Level.t) := + let '((l, r), l') := c in + ((lift_level n l, r), lift_level n l'). + + Definition lift_constraints n cstrs := + ConstraintSet.fold (fun elt acc => ConstraintSet.add (lift_constraint n elt) acc) + cstrs ConstraintSet.empty. + + Definition level_var_instance n (inst : list name) := + mapi_rec (fun i _ => Level.Var i) inst n. + + Fixpoint variance_cstrs (v : list Variance.t) (u u' : Instance.t) := + match v, u, u' with + | _, [], [] => ConstraintSet.empty + | v :: vs, u :: us, u' :: us' => + match v with + | Variance.Irrelevant => variance_cstrs vs us us' + | Variance.Covariant => ConstraintSet.add (u, ConstraintType.Le 0, u') (variance_cstrs vs us us') + | Variance.Invariant => ConstraintSet.add (u, ConstraintType.Eq, u') (variance_cstrs vs us us') + end + | _, _, _ => (* Impossible due to on_variance invariant *) ConstraintSet.empty + end. + + (** This constructs a duplication of the polymorphic universe context of the inductive, + where the two instances are additionally related according to the variance information. + *) + + Definition variance_universes univs v := + match univs with + | Monomorphic_ctx => None + | Polymorphic_ctx auctx => + let (inst, cstrs) := auctx in + let u' := level_var_instance 0 inst in + let u := lift_instance #|inst| u' in + let cstrs := ConstraintSet.union cstrs (lift_constraints #|inst| cstrs) in + let cstrv := variance_cstrs v u u' in + let auctx' := (inst ++ inst, ConstraintSet.union cstrs cstrv) in + Some (Polymorphic_ctx auctx', u, u') + end. + + (** A constructor type respects the given variance [v] if each constructor + argument respects it and each index (in the conclusion) does as well. + We formalize this by asking for a cumulativity relation between the contexts + of arguments and conversion of the lists of indices instanciated with [u] and + [u'] where [u `v` u']. *) + + Definition ind_arities mdecl := arities_context (ind_bodies mdecl). + + Definition ind_respects_variance Σ mdecl v indices := + let univs := ind_universes mdecl in + match variance_universes univs v with + | Some (univs, u, u') => + cumul_ctx_rel Pcmp (Σ, univs) (smash_context [] (ind_params mdecl))@[u] + (expand_lets_ctx (ind_params mdecl) (smash_context [] indices))@[u] + (expand_lets_ctx (ind_params mdecl) (smash_context [] indices))@[u'] + | None => False + end. + + Definition cstr_respects_variance Σ mdecl v cs := + let univs := ind_universes mdecl in + match variance_universes univs v with + | Some (univs, u, u') => + cumul_ctx_rel Pcmp (Σ, univs) (ind_arities mdecl ,,, smash_context [] (ind_params mdecl))@[u] + (expand_lets_ctx (ind_params mdecl) (smash_context [] (cstr_args cs)))@[u] + (expand_lets_ctx (ind_params mdecl) (smash_context [] (cstr_args cs)))@[u'] * + All2 + (Pcmp (Σ, univs) (ind_arities mdecl ,,, smash_context [] (ind_params mdecl ,,, cstr_args cs))@[u] Conv) + (map (subst_instance u ∘ expand_lets (ind_params mdecl ,,, cstr_args cs)) (cstr_indices cs)) + (map (subst_instance u' ∘ expand_lets (ind_params mdecl ,,, cstr_args cs)) (cstr_indices cs)) + | None => False (* Monomorphic inductives have no variance attached *) + end. + + (* Conclusion head: reference to the current inductive in the block *) + Definition cstr_concl_head mdecl i cdecl := + tRel (#|mdecl.(ind_bodies)| - S i + #|mdecl.(ind_params)| + #|cstr_args cdecl|). + + (* Constructor conclusion shape: the inductives type applied to variables for + the (non-let) parameters + followed by the indices *) + Definition cstr_concl mdecl i cdecl := + (mkApps (cstr_concl_head mdecl i cdecl) + (to_extended_list_k mdecl.(ind_params) #|cstr_args cdecl| + ++ cstr_indices cdecl)). + + Record on_constructor Σ mdecl i idecl ind_indices cdecl cunivs := { + (* cdecl.1 fresh ?? *) + cstr_args_length : context_assumptions (cstr_args cdecl) = cstr_arity cdecl; + + cstr_eq : cstr_type cdecl = + it_mkProd_or_LetIn mdecl.(ind_params) + (it_mkProd_or_LetIn (cstr_args cdecl) + (cstr_concl mdecl i cdecl)); + (* The type of the constructor canonically has this shape: parameters, real + arguments ending with a reference to the inductive applied to the + (non-lets) parameters and arguments *) + + on_ctype : on_type Σ (arities_context mdecl.(ind_bodies)) (cstr_type cdecl); + on_cargs : + sorts_local_ctx Σ (arities_context mdecl.(ind_bodies) ,,, mdecl.(ind_params)) + cdecl.(cstr_args) cunivs; + on_cindices : + ctx_inst (fun Σ Γ t T => P Σ Γ t (Typ T)) Σ (arities_context mdecl.(ind_bodies) ,,, mdecl.(ind_params) ,,, cdecl.(cstr_args)) + cdecl.(cstr_indices) + (List.rev (lift_context #|cdecl.(cstr_args)| 0 ind_indices)); + + on_ctype_positive : (* The constructor type is positive *) + positive_cstr mdecl i [] (cstr_type cdecl); + + on_ctype_variance : (* The constructor type respect the variance annotation + on polymorphic universes, if any. *) + forall v, ind_variance mdecl = Some v -> + cstr_respects_variance Σ mdecl v cdecl; + + on_lets_in_type : if lets_in_constructor_types + then True else is_true (is_assumption_context (cstr_args cdecl)) + }. + + Arguments on_ctype {Σ mdecl i idecl ind_indices cdecl cunivs}. + Arguments on_cargs {Σ mdecl i idecl ind_indices cdecl cunivs}. + Arguments on_cindices {Σ mdecl i idecl ind_indices cdecl cunivs}. + Arguments cstr_args_length {Σ mdecl i idecl ind_indices cdecl cunivs}. + Arguments cstr_eq {Σ mdecl i idecl ind_indices cdecl cunivs}. + + Definition on_constructors Σ mdecl i idecl ind_indices := + All2 (on_constructor Σ mdecl i idecl ind_indices). + + (** Each projection type corresponds to a non-let argument of the + corresponding constructor. It is parameterized over the + parameters of the inductive type and all the preceding arguments + of the constructor. When computing the type of a projection for argument + [n] at a given instance of the parameters and a given term [t] in the inductive + type, we instantiate the argument context by corresponsping projections + [t.π1 ... t.πn-1]. This is essential for subject reduction to hold: each + projections type can only refer to the record object through projections. + + Projection types have their parameter and argument contexts smashed to avoid + costly computations during type-checking and reduction: we can just substitute + the instances of parameters and the inductive value without considering the + presence of let bindings. *) + + Record on_proj mdecl mind i k (p : projection_body) decl := + { on_proj_name : (* All projections are be named after a constructor argument. *) + binder_name (decl_name decl) = nNamed p.(proj_name); + on_proj_type : + (** The stored projection type already has the references to the inductive + type substituted along with the previous arguments replaced by projections. *) + let u := abstract_instance mdecl.(ind_universes) in + let ind := {| inductive_mind := mind; inductive_ind := i |} in + p.(proj_type) = subst (inds mind u mdecl.(ind_bodies)) (S (ind_npars mdecl)) + (subst (projs ind mdecl.(ind_npars) k) 0 + (lift 1 k (decl_type decl))); + on_proj_relevance : p.(proj_relevance) = decl.(decl_name).(binder_relevance) }. + + Definition on_projection mdecl mind i cdecl (k : nat) (p : projection_body) := + let Γ := smash_context [] (cdecl.(cstr_args) ++ mdecl.(ind_params)) in + match nth_error Γ (context_assumptions cdecl.(cstr_args) - S k) with + | None => False + | Some decl => on_proj mdecl mind i k p decl + end. + + Record on_projections mdecl mind i idecl (ind_indices : context) cdecl := + { on_projs_record : #|idecl.(ind_ctors)| = 1; + (** The inductive must be a record *) + + on_projs_noidx : #|ind_indices| = 0; + (** The inductive cannot have indices *) + + on_projs_elim : idecl.(ind_kelim) = IntoAny; + (** This ensures that all projections are definable *) + + on_projs_all : #|idecl.(ind_projs)| = context_assumptions (cstr_args cdecl); + (** There are as many projections as (non-let) constructor arguments *) + + on_projs : Alli (on_projection mdecl mind i cdecl) 0 idecl.(ind_projs) }. + + Definition check_constructors_smaller φ cunivss ind_sort := + Forall (fun cunivs => + Forall (fun argsort => leq_universe φ argsort ind_sort) cunivs) cunivss. + + (** This ensures that all sorts in kelim are lower + or equal to the top elimination sort, if set. + For inductives in Type we do not check [kelim] currently. *) + + Definition constructor_univs := list Universe.t. + (* The sorts of the arguments context (without lets) *) + + Definition elim_sort_prop_ind (ind_ctors_sort : list constructor_univs) := + match ind_ctors_sort with + | [] => (* Empty inductive proposition: *) IntoAny + | [ s ] => + if forallb Universes.is_propositional s then + IntoAny (* Singleton elimination *) + else + IntoPropSProp (* Squashed: some arguments are higher than Prop, restrict to Prop *) + | _ => (* Squashed: at least 2 constructors *) IntoPropSProp + end. + + Definition elim_sort_sprop_ind (ind_ctors_sort : list constructor_univs) := + match ind_ctors_sort with + | [] => (* Empty inductive strict proposition: *) IntoAny + | _ => (* All other inductives in SProp are squashed *) IntoSProp + end. + + Definition check_ind_sorts (Σ : global_env_ext) + params kelim ind_indices cdecls ind_sort : Type := + if Universe.is_prop ind_sort then + (** The inductive is declared in the impredicative sort Prop *) + (** No universe-checking to do: any size of constructor argument is allowed, + however elimination restrictions apply. *) + (allowed_eliminations_subset kelim (elim_sort_prop_ind cdecls) : Type) + else if Universe.is_sprop ind_sort then + (** The inductive is declared in the impredicative sort SProp *) + (** No universe-checking to do: any size of constructor argument is allowed, + however elimination restrictions apply. *) + (allowed_eliminations_subset kelim (elim_sort_sprop_ind cdecls) : Type) + else + (** The inductive is predicative: check that all constructors arguments are + smaller than the declared universe. *) + check_constructors_smaller Σ cdecls ind_sort + × if indices_matter then + type_local_ctx Σ params ind_indices ind_sort + else True. + + Record on_ind_body Σ mind mdecl i idecl := + { (** The type of the inductive must be an arity, sharing the same params + as the rest of the block, and maybe having a context of indices. *) + ind_arity_eq : idecl.(ind_type) + = it_mkProd_or_LetIn mdecl.(ind_params) + (it_mkProd_or_LetIn idecl.(ind_indices) (tSort idecl.(ind_sort))); + + (** It must be well-typed in the empty context. *) + onArity : on_type Σ [] idecl.(ind_type); + + (** The sorts of the arguments contexts of each constructor *) + ind_cunivs : list constructor_univs; + + (** Constructors are well-typed *) + onConstructors : + on_constructors Σ mdecl i idecl idecl.(ind_indices) idecl.(ind_ctors) ind_cunivs; + + (** Projections, if any, are well-typed *) + onProjections : + match idecl.(ind_projs), idecl.(ind_ctors) return Type with + | [], _ => True + | _, [ o ] => + on_projections mdecl mind i idecl idecl.(ind_indices) o + | _, _ => False + end; + + (** The universes and elimination sorts must be correct w.r.t. + the universe of the inductive and the universes in its constructors, which + are declared in [on_constructors]. *) + ind_sorts : + check_ind_sorts Σ mdecl.(ind_params) idecl.(ind_kelim) + idecl.(ind_indices) ind_cunivs idecl.(ind_sort); + + onIndices : + (* The inductive type respect the variance annotation on polymorphic universes, if any. *) + match ind_variance mdecl with + | Some v => ind_respects_variance Σ mdecl v idecl.(ind_indices) + | None => True + end + }. + + Definition on_variance Σ univs (variances : option (list Variance.t)) := + match univs return Type with + | Monomorphic_ctx => variances = None + | Polymorphic_ctx auctx => + match variances with + | None => unit + | Some v => + ∑ univs' i i', + [× (variance_universes univs v = Some (univs', i, i')), + consistent_instance_ext (Σ, univs') univs i, + consistent_instance_ext (Σ, univs') univs i' & + List.length v = #|UContext.instance (AUContext.repr auctx)|] + end + end. + + (** We allow empty blocks for simplicity + (no well-typed reference to them can be made). *) + + Record on_inductive Σ mind mdecl := + { onInductives : Alli (on_ind_body Σ mind mdecl) 0 mdecl.(ind_bodies); + (** We check that the context of parameters is well-formed and that + the size annotation counts assumptions only (no let-ins). *) + onParams : on_context Σ mdecl.(ind_params); + onNpars : context_assumptions mdecl.(ind_params) = mdecl.(ind_npars); + (** We check that the variance annotations are well-formed: i.e. they + form a valid universe context. *) + onVariance : on_variance Σ mdecl.(ind_universes) mdecl.(ind_variance); + }. + + (** *** Typing of constant declarations *) + + Definition on_constant_decl Σ d := + match d.(cst_body) with + | Some trm => P Σ [] trm (Typ d.(cst_type)) + | None => on_type Σ [] d.(cst_type) + end. + + Definition on_global_decl Σ kn decl := + match decl with + | ConstantDecl d => on_constant_decl Σ d + | InductiveDecl inds => on_inductive Σ kn inds + end. + + (** *** Typing of global environment + + All declarations should be typeable and the global + set of universe constraints should be consistent. *) + + (** Well-formed global environments have no name clash. *) + + Definition fresh_global (s : kername) (g : global_declarations) : Prop := + Forall (fun g => g.1 <> s) g. + + Record on_global_decls_data (univs : ContextSet.t) retro (Σ : global_declarations) (kn : kername) (d : global_decl) := + { + kn_fresh : fresh_global kn Σ ; + udecl := universes_decl_of_decl d ; + on_udecl_udecl : on_udecl univs udecl ; + on_global_decl_d : on_global_decl (mk_global_env univs Σ retro, udecl) kn d + }. + + Inductive on_global_decls (univs : ContextSet.t) (retro : Retroknowledge.t): global_declarations -> Type := + | globenv_nil : on_global_decls univs retro [] + | globenv_decl Σ kn d : + on_global_decls univs retro Σ -> + on_global_decls_data univs retro Σ kn d -> + on_global_decls univs retro (Σ ,, (kn, d)). + + Derive Signature for on_global_decls. + + Lemma fresh_global_iff_not_In kn Σ + : fresh_global kn Σ <-> ~ In kn (map fst Σ). + Proof using Type. + rewrite /fresh_global; split; [ induction 1 | induction Σ; constructor ]; cbn in *. + all: tauto. + Qed. + + Lemma fresh_global_iff_lookup_global_None kn Σ + : fresh_global kn Σ <-> lookup_global Σ kn = None. + Proof using Type. rewrite fresh_global_iff_not_In lookup_global_None //. Qed. + + Lemma NoDup_on_global_decls univs retro decls + : on_global_decls univs retro decls -> NoDup (List.map fst decls). + Proof using Type. + induction 1; cbn in *; constructor => //. + let H := match goal with H : on_global_decls_data _ _ _ _ _ |- _ => H end in + move: H. + case. + rewrite fresh_global_iff_not_In; auto. + Qed. + + Definition on_global_univs (c : ContextSet.t) := + let levels := global_levels c in + let cstrs := ContextSet.constraints c in + ConstraintSet.For_all (declared_cstr_levels levels) cstrs /\ + LS.For_all (negb ∘ Level.is_var) levels /\ + consistent cstrs. + + Definition on_global_env (g : global_env) : Type := + on_global_univs g.(universes) × on_global_decls g.(universes) g.(retroknowledge) g.(declarations). + + Definition on_global_env_ext (Σ : global_env_ext) := + on_global_env Σ.1 × on_udecl Σ.(universes) Σ.2. + + End GlobalMaps. + + Arguments cstr_args_length {_ Pcmp P Σ mdecl i idecl ind_indices cdecl cunivs}. + Arguments cstr_eq {_ Pcmp P Σ mdecl i idecl ind_indices cdecl cunivs}. + Arguments on_ctype {_ Pcmp P Σ mdecl i idecl ind_indices cdecl cunivs}. + Arguments on_cargs {_ Pcmp P Σ mdecl i idecl ind_indices cdecl cunivs}. + Arguments on_cindices {_ Pcmp P Σ mdecl i idecl ind_indices cdecl cunivs}. + Arguments on_ctype_positive {_ Pcmp P Σ mdecl i idecl ind_indices cdecl cunivs}. + Arguments on_ctype_variance {_ Pcmp P Σ mdecl i idecl ind_indices cdecl cunivs}. + + Arguments ind_arity_eq {_ Pcmp P Σ mind mdecl i idecl}. + Arguments ind_cunivs {_ Pcmp P Σ mind mdecl i idecl}. + Arguments onArity {_ Pcmp P Σ mind mdecl i idecl}. + Arguments onConstructors {_ Pcmp P Σ mind mdecl i idecl}. + Arguments onProjections {_ Pcmp P Σ mind mdecl i idecl}. + Arguments ind_sorts {_ Pcmp P Σ mind mdecl i idecl}. + Arguments onIndices {_ Pcmp P Σ mind mdecl i idecl}. + + Arguments onInductives {_ Pcmp P Σ mind mdecl}. + Arguments onParams {_ Pcmp P Σ mind mdecl}. + Arguments onNpars {_ Pcmp P Σ mind mdecl}. + Arguments onVariance {_ Pcmp P Σ mind mdecl}. + + + Lemma type_local_ctx_impl (P Q : global_env_ext -> context -> term -> typ_or_sort -> Type) Σ Γ Δ u : + type_local_ctx P Σ Γ Δ u -> + (forall Γ t T, P Σ Γ t T -> Q Σ Γ t T) -> + type_local_ctx Q Σ Γ Δ u. + Proof. + intros HP HPQ. revert HP; induction Δ in Γ, HPQ |- *; simpl; auto. + destruct a as [na [b|] ty]; simpl; auto. + intros. intuition auto. intuition auto. + Qed. + + Lemma sorts_local_ctx_impl (P Q : global_env_ext -> context -> term -> typ_or_sort -> Type) Σ Γ Δ u : + sorts_local_ctx P Σ Γ Δ u -> + (forall Γ t T, P Σ Γ t T -> Q Σ Γ t T) -> + sorts_local_ctx Q Σ Γ Δ u. + Proof. + intros HP HPQ. revert HP; induction Δ in Γ, HPQ, u |- *; simpl; auto. + destruct a as [na [b|] ty]; simpl; auto. + intros. intuition auto. intuition auto. + destruct u; auto. intuition eauto. + Qed. + + Lemma on_global_env_impl {cf : checker_flags} Pcmp P Q : + (forall Σ Γ t T, + on_global_env Pcmp P Σ.1 -> + on_global_env Pcmp Q Σ.1 -> + P Σ Γ t T -> Q Σ Γ t T) -> + forall Σ, on_global_env Pcmp P Σ -> on_global_env Pcmp Q Σ. + Proof. + intros X Σ [cu IH]. split; auto. + revert cu IH; generalize (universes Σ) as univs, (retroknowledge Σ) as retro, (declarations Σ). clear Σ. + induction g; intros; auto. constructor; auto. + depelim IH. specialize (IHg cu IH). constructor; auto. + pose proof (globenv_decl _ _ _ _ _ _ _ IH o). + destruct o. constructor; auto. + assert (X' := fun Γ t T => X ({| universes := univs; declarations := _ |}, udecl0) Γ t T + (cu, IH) (cu, IHg)); clear X. + rename X' into X. + clear IH IHg. destruct d; simpl. + - destruct c; simpl. destruct cst_body0; cbn in *; now eapply X. + - destruct on_global_decl_d0 as [onI onP onNP]. + constructor; auto. + -- eapply Alli_impl; tea. intros. + refine {| ind_arity_eq := X1.(ind_arity_eq); + ind_cunivs := X1.(ind_cunivs) |}. + --- apply onArity in X1. unfold on_type in *; simpl in *. + now eapply X. + --- pose proof X1.(onConstructors) as X11. red in X11. + eapply All2_impl; eauto. + simpl. intros. destruct X2 as [? ? ? ?]; unshelve econstructor; eauto. + * apply X; eauto. + * clear -X0 X on_cargs0. revert on_cargs0. + generalize (cstr_args x0). + induction c in y |- *; destruct y; simpl; auto; + destruct a as [na [b|] ty]; simpl in *; auto; + split; intuition eauto. + * clear -X0 X on_cindices0. + revert on_cindices0. + generalize (List.rev (lift_context #|cstr_args x0| 0 (ind_indices x))). + generalize (cstr_indices x0). + induction 1; simpl; constructor; auto. + --- simpl; intros. pose (onProjections X1) as X2. simpl in *; auto. + --- destruct X1. simpl. unfold check_ind_sorts in *. + destruct Universe.is_prop; auto. + destruct Universe.is_sprop; auto. + split. + * apply ind_sorts0. + * destruct indices_matter; auto. + eapply type_local_ctx_impl; eauto. + eapply ind_sorts0. + --- eapply X1.(onIndices). + -- red in onP. red. + eapply All_local_env_impl; tea. + Qed. + +End GlobalMaps. + +Module Type GlobalMapsSig (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvTypingSig T E TU) (C: ConversionSig T E TU ET) (L: LookupSig T E). + Include GlobalMaps T E TU ET C L. +End GlobalMapsSig. + +Module Type ConversionParSig (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E) (ET : EnvTypingSig T E TU). + + Import T E TU ET. + + Parameter Inline cumul_gen : forall {cf : checker_flags}, global_env_ext -> context -> conv_pb -> term -> term -> Type. + +End ConversionParSig. + +Module Type Typing (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E) (ET : EnvTypingSig T E TU) + (CT : ConversionSig T E TU ET) (CS : ConversionParSig T E TU ET). + + Import T E TU ET CT CS. + + Parameter Inline typing : forall `{checker_flags}, global_env_ext -> context -> term -> term -> Type. + + Notation " Σ ;;; Γ |- t : T " := + (typing Σ Γ t T) (at level 50, Γ, t, T at next level) : type_scope. + + Notation wf_local Σ Γ := (All_local_env (lift_typing Σ) Γ). + +End Typing. + +Module DeclarationTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E) + (ET : EnvTypingSig T E TU) (CT : ConversionSig T E TU ET) + (CS : ConversionParSig T E TU ET) (Ty : Typing T E TU ET CT CS) + (L : LookupSig T E) (GM : GlobalMapsSig T E TU ET CT L). + + Import T E L TU ET CT GM CS Ty. + + Definition isType `{checker_flags} (Σ : global_env_ext) (Γ : context) (t : term) := + infer_sort (typing_sort typing) Σ Γ t. + + (** This predicate enforces that there exists typing derivations for every typable term in env. *) + + Definition Forall_decls_typing `{checker_flags} + (P : global_env_ext -> context -> term -> term -> Type) + := on_global_env cumul_gen (lift_typing P). + + (** *** Typing of local environments *) + + Definition type_local_decl `{checker_flags} Σ Γ d := + match d.(decl_body) with + | None => isType Σ Γ d.(decl_type) + | Some body => Σ ;;; Γ |- body : d.(decl_type) + end. + + (** ** Induction principle for typing up-to a global environment *) + + Lemma refine_type `{checker_flags} Σ Γ t T U : Σ ;;; Γ |- t : T -> T = U -> Σ ;;; Γ |- t : U. + Proof. now intros Ht ->. Qed. + + Definition wf_local_rel `{checker_flags} Σ := All_local_rel (lift_typing typing Σ). + + (** Functoriality of global environment typing derivations + folding of the well-formed + environment assumption. *) + Lemma on_wf_global_env_impl `{checker_flags} {Σ : global_env} {wfΣ : on_global_env cumul_gen (lift_typing typing) Σ} P Q : + (forall Σ Γ t T, on_global_env cumul_gen (lift_typing typing) Σ.1 -> + on_global_env cumul_gen P Σ.1 -> + on_global_env cumul_gen Q Σ.1 -> + P Σ Γ t T -> Q Σ Γ t T) -> + on_global_env cumul_gen P Σ -> on_global_env cumul_gen Q Σ. + Proof. + unfold on_global_env in *. + intros X [hu X0]. split; auto. + simpl in *. destruct wfΣ as [cu wfΣ]. revert cu wfΣ. + revert X0. generalize (universes Σ) as univs, (retroknowledge Σ) as retro, (declarations Σ). clear hu Σ. + induction 1; constructor; try destruct o; try constructor; auto. + { depelim wfΣ. eauto. } + depelim wfΣ. specialize (IHX0 cu wfΣ). destruct o. + assert (X' := fun Γ t T => X ({| universes := univs; declarations := Σ |}, udecl0) Γ t T + (cu, wfΣ) (cu, X0) (cu, IHX0)); clear X. + rename X' into X. + clear IHX0. destruct d; simpl. + - destruct c; simpl. destruct cst_body0; simpl in *; now eapply X. + - simpl in *. destruct on_global_decl_d0 as [onI onP onNP]. + constructor; auto. + -- eapply Alli_impl; tea. intros. + refine {| ind_arity_eq := X1.(ind_arity_eq); + ind_cunivs := X1.(ind_cunivs) |}. + --- apply onArity in X1. unfold on_type in *; simpl in *. + now eapply X. + --- pose proof X1.(onConstructors) as X11. red in X11. + eapply All2_impl; eauto. + simpl. intros. destruct X2 as [? ? ? ?]; unshelve econstructor; eauto. + * apply X; eauto. + * clear -X0 X on_cargs0. revert on_cargs0. + generalize (cstr_args x0). + induction c in y |- *; destruct y; simpl; auto; + destruct a as [na [b|] ty]; simpl in *; auto; + split; intuition eauto. + * clear -X0 X on_cindices0. + revert on_cindices0. + generalize (List.rev (lift_context #|cstr_args x0| 0 (ind_indices x))). + generalize (cstr_indices x0). + induction 1; simpl; constructor; auto. + --- simpl; intros. pose (onProjections X1). simpl in *; auto. + --- destruct X1. simpl. unfold check_ind_sorts in *. + destruct Universe.is_prop; auto. + destruct Universe.is_sprop; auto. + split. + * apply ind_sorts0. + * destruct indices_matter; auto. + eapply type_local_ctx_impl; eauto. + eapply ind_sorts0. + --- eapply X1.(onIndices). + -- red in onP. red. + eapply All_local_env_impl; tea. + Qed. + +End DeclarationTyping. + +Module Type DeclarationTypingSig (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E) + (ET : EnvTypingSig T E TU) (CT : ConversionSig T E TU ET) + (CS : ConversionParSig T E TU ET) (Ty : Typing T E TU ET CT CS) + (L : LookupSig T E) (GM : GlobalMapsSig T E TU ET CT L). + Include DeclarationTyping T E TU ET CT CS Ty L GM. +End DeclarationTypingSig. diff --git a/pcuic/theories/PCUICAst.v b/pcuic/theories/PCUICAst.v index f2e4f3c72..ab60e9124 100644 --- a/pcuic/theories/PCUICAst.v +++ b/pcuic/theories/PCUICAst.v @@ -1,8 +1,8 @@ (* Distributed under the terms of the MIT license. *) From Coq Require Import ssreflect Morphisms. -From MetaCoq.Template Require Export utils Universes BasicAst Environment Reflect. -From MetaCoq.Template Require EnvironmentTyping. +From MetaCoq.Template Require Export utils Universes BasicAst Reflect. From MetaCoq.PCUIC Require Export PCUICPrimitive. +From MetaCoq.PCUIC Require Environment EnvironmentTyping. From Equations Require Import Equations. (** * AST of the Polymorphic Cumulative Calculus of Inductive Constructions @@ -443,7 +443,7 @@ Fixpoint closedu (k : nat) (t : term) : bool := | _ => true end. -Module PCUICTerm <: Term. +Module PCUICTerm <: Environment.Term. Definition term := term. @@ -465,7 +465,7 @@ End PCUICTerm. (* These functors derive the notion of local context and lift substitution, term lifting, the closed predicate to them. *) -Module PCUICEnvironment := Environment PCUICTerm. +Module PCUICEnvironment := Environment.Environment PCUICTerm. Export PCUICEnvironment. (* Do NOT `Include` this module, as this would sadly duplicate the rewrite database... *) @@ -489,7 +489,7 @@ Definition inds ind u (l : list one_inductive_body) := end in aux (List.length l). -Module PCUICTermUtils <: TermUtils PCUICTerm PCUICEnvironment. +Module PCUICTermUtils <: Environment.TermUtils PCUICTerm PCUICEnvironment. Definition destArity := destArity. Definition inds := inds. diff --git a/pcuic/theories/PCUICTypedAst.v b/pcuic/theories/PCUICTypedAst.v index 6f8460909..85b9fd159 100644 --- a/pcuic/theories/PCUICTypedAst.v +++ b/pcuic/theories/PCUICTypedAst.v @@ -1,7 +1,7 @@ (* Distributed under the terms of the MIT license. *) From Coq Require Import Morphisms. From MetaCoq.Template Require Export utils Universes BasicAst Environment Reflect. -From MetaCoq.Template Require EnvironmentTyping. +From MetaCoq.PCUIC Require EnvironmentTyping. From MetaCoq.PCUIC Require Export PCUICPrimitive. From Equations Require Import Equations. Require Vector Fin. diff --git a/pcuic/theories/PCUICTyping.v b/pcuic/theories/PCUICTyping.v index 95bd4e3a9..1d5bc53e6 100644 --- a/pcuic/theories/PCUICTyping.v +++ b/pcuic/theories/PCUICTyping.v @@ -1252,7 +1252,7 @@ Section All_local_env. split. * red; cbn. split; [split;[lsets|csets]| |]. exists [(kn, decl)] => //. - apply Retroknowledge.extends_refl. + apply Environment.Retroknowledge.extends_refl. * split => //. * destruct o; assumption. - intros hl. destruct (IHΣp hl) as [Σ' []]. diff --git a/pcuic/theories/TemplateToPCUIC.v b/pcuic/theories/TemplateToPCUIC.v index 03b590283..806ba9334 100644 --- a/pcuic/theories/TemplateToPCUIC.v +++ b/pcuic/theories/TemplateToPCUIC.v @@ -1,5 +1,5 @@ (* Distributed under the terms of the MIT license. *) -From Coq Require Import Uint63 FloatOps FloatAxioms. +From Coq Require Import Uint63 FloatOps FloatAxioms Logic.Decidable. From MetaCoq.Template Require Import config utils AstUtils Primitive EnvMap. From MetaCoq.Template Require TemplateProgram. From MetaCoq.PCUIC Require Import PCUICAst PCUICPrimitive PCUICCases PCUICProgram. @@ -146,15 +146,376 @@ Section Trans. ind_universes := md.(Ast.Env.ind_universes); ind_variance := md.(Ast.Env.ind_variance) |}. - Definition trans_global_decl (d : Ast.Env.global_decl) := - match d with - | Ast.Env.ConstantDecl bd => ConstantDecl (trans_constant_body bd) - | Ast.Env.InductiveDecl bd => InductiveDecl (trans_minductive_body bd) + (* kn := Coq.Init.M := (Coq.Init, M) *) + Definition kn_append (kn: kername) (id: ident) : kername := ((MPdot kn.1 kn.2), id). + + Inductive kn_extends : kername -> kername -> Prop := + | kn_extends_one kn id : kn_extends kn (kn_append kn id) + | kn_extends_step id kn kn' (H: kn_extends kn kn') : kn_extends kn (kn_append kn' id). + + Lemma kn_extends_exists : forall kn kn', kn_extends kn kn' -> exists l: list ident, + l <> [] /\ fold_right (fun id kn => kn_append kn id) kn l = kn'. + Proof. + intros kn kn' Hext. + induction Hext. + - exists [id]. split; auto. discriminate. + - destruct IHHext as [l [Hne H]]. + exists (id::l). + split. simpl. discriminate. + simpl. now rewrite <- H. + Qed. + + Lemma kn_append_neq : forall kn id, kn_append kn id <> kn. + Proof. + intros [mp i]. revert i. + induction mp; try discriminate. + intros i' id'. + unfold kn_append in *; simpl in *. + intros contra. inversion contra; subst. + assert ((MPdot mp id, id) = (mp, id)) by now rewrite H0. + apply IHmp in H. apply H. + Qed. + + Lemma kn_extends' : forall id kn kn', + kn_extends (kn_append kn id) kn' -> kn_extends kn kn'. + Proof. + intros id kn kn' H. + remember (kn_append kn id) as knid. + induction H; subst. + - apply kn_extends_step. apply kn_extends_one. + - assert (kn_extends kn kn') by now apply IHkn_extends. + now apply kn_extends_step. + Qed. + + Lemma kn_extends_trans : forall kn kn' kn'', + kn_extends kn kn' -> kn_extends kn' kn'' -> kn_extends kn kn''. + Proof. + intros kn kn' kn'' H1 H2. + generalize dependent kn''. + induction H1. + - remember (kn_append kn id) as knid. + intros kn'' H2. induction H2; subst. + -- apply kn_extends_step. apply kn_extends_one. + -- assert (kn_extends kn kn') by now apply IHkn_extends. + now apply kn_extends_step. + - intros kn'' H2. apply IHkn_extends. + remember (kn_append kn' id) as kn'id. + induction H2; subst. + -- apply kn_extends_step. apply kn_extends_one. + -- apply kn_extends_step. + assert (kn_extends kn (kn_append kn'0 id0)). { + apply IHkn_extends. apply kn_extends_step. + now apply kn_extends' with (id := id). + } + now apply IHkn_extends0. + Qed. + + Lemma kn_extends_inversion_true : forall mp mp' i i' id id', + kn_extends (MPdot mp i, id) (MPdot mp' i', id') -> kn_extends (mp, i) (mp', i'). + Proof. + intros. inversion H; subst. + - apply kn_extends_one. + - destruct kn' as [mp' i']; cbn in *. + apply (kn_extends' id). + apply H2. + Qed. + + Lemma kn_appended_is_mpdot : forall kn id, + exists mp i, (kn_append kn id) = (MPdot mp i, id). + Proof. + intros. unfold kn_append. now exists kn.1, kn.2. + Qed. + + Lemma kn_extends_is_mpdot : forall kn kn', kn_extends kn kn' -> exists mp i, kn'.1 = (MPdot mp i). + Proof. + intros. apply kn_extends_exists in H as [l [Hne H]]. + destruct l. contradiction. + simpl in H. remember (fold_right (fun (id : ident) (kn : kername) => kn_append kn id) kn l) as kn''. + pose proof (kn_appended_is_mpdot kn'' i) as [mp [id Hdot]]. + exists mp, id. + subst kn'. rewrite Hdot. reflexivity. + Qed. + + Lemma kn_extends_irrefl : forall kn, ~(kn_extends kn kn). + Proof. + intros [mp id]. + revert id. + induction mp. + - intros id contra. apply kn_extends_is_mpdot in contra as [? [? ?]]. + discriminate. + - intros id' contra. apply kn_extends_is_mpdot in contra as [? [? ?]]. + discriminate. + - intros id' H. inversion H; subst. + -- rewrite H2 in H. now apply IHmp in H. + -- destruct kn' as [mp i]; cbn in *. + apply kn_extends_inversion_true in H. + now apply IHmp in H. + Qed. + + Lemma kn_extends_neq : forall kn kn', kn_extends kn kn' -> kn <> kn'. + Proof. + intros kn kn' H contra. + rewrite contra in H. + now apply kn_extends_irrefl in H. + Qed. + + (** + Claim: The aliasing is a tree. + Reason: + 1. One can only alias backwards to a already defined module. + 2. As a naive implementation, aliasing is (deep) copying. + + We can than verify the claim inductively: an actual module is a + single-node tree. For the inductive step, suppose we already have a tree + of aliases. Then a new alias can only refer to a node on the tree, forming + a tree. + + For the case of aliasing of submodules such as: + Module M. + Module A. + Module B: End B. + End A. + Module C: End C. + End M. + + M + / \ + A,L C + \ + B + + The "submodule" relation can also be considered as a different directed + edge on the tree, and will not affect the tree structure (because cannot + have self-reference). Once one proves the submodule relationship forms a + tree (identical to above), one can prove "aliasing with submodules" form + a tree too, inductively: + + Base case: A module is a tree. + Inductive case: Suppose an alias refers to a certain (sub)module (aliased or not) + on the existing tree, which refers to a whole subtree identifiable by a node + (technically: kername). Call the node K and its parent K'. The aliasing is + equivalent to copying K to a sibling L under K', where L is the new aliased + module. This is still a tree. Qed. + *) + + (** + Therefore, strategy: + Build and store such a tree. + In technical terms, all of these are [structure_body]s. + We can use sfmod with fullstruct. + Finding the correct branch is tree-traversal given a path (kername). + However, every time a subtree is aliased, we add the aliased name to the + list of labels for that root node. + + [([idents...], tree), ([idents...], tree), ... ] + + *) + + Fixpoint trans_structure_field kn id (sf : Ast.Env.structure_field) := + let kn' := kn_append kn id in + match sf with + | Ast.Env.sfconst c => [(kn', ConstantDecl (trans_constant_body c))] + | Ast.Env.sfmind m => [(kn', InductiveDecl (trans_minductive_body m))] + | Ast.Env.sfmod mi sb => match mi with + | Ast.Env.mi_fullstruct => trans_structure_body kn' sb + | Ast.Env.mi_struct s => trans_structure_body kn' s + | _ => trans_module_impl kn' mi + end + | Ast.Env.sfmodtype _ => [] + end + with trans_module_impl kn (mi: Ast.Env.module_implementation) := + match mi with + | Ast.Env.mi_abstract => [] + | Ast.Env.mi_algebraic kn' => [] + (* let target := find_target_structure_body kn' in trans_structure_body kn' target *) + | Ast.Env.mi_struct sb => trans_structure_body kn sb + | Ast.Env.mi_fullstruct => [] + end + with trans_structure_body kn (sb: Ast.Env.structure_body) := + match sb with + | Ast.Env.sb_nil => [] + | Ast.Env.sb_cons id sf tl => + trans_structure_field kn id sf ++ trans_structure_body kn tl + end. + + Definition trans_modtype_decl := trans_structure_body. + + Definition trans_module_decl kn (m: Ast.Env.module_decl) : list(kername × global_decl) := + match m with + | (Ast.Env.mi_fullstruct, mt) => trans_modtype_decl kn mt + | (mi, _) => trans_module_impl kn mi + end. + + + Lemma translated_structure_field_all_kn_extends: + forall sf kn id, Forall (fun '(kn', _) => kn_extends kn kn') (trans_structure_field kn id sf). + Proof. + set (P := fun sf => forall kn id, Forall (fun '(kn', _) => kn_extends kn kn') (trans_structure_field kn id sf)). + set (P0 := fun mi => forall kn, Forall (fun '(kn', _) => kn_extends kn kn') (trans_module_impl kn mi)). + set (P1 := fun sb => forall kn, Forall (fun '(kn', _) => kn_extends kn kn') (trans_structure_body kn sb)). + apply (Ast.Env.sf_mi_sb_mutind P P0 P1); subst P P0 P1; cbn; try auto. + - intros c kn id. rewrite Forall_forall. + intros [kn' d] []. + inversion H. + constructor. + inversion H. + - intros m kn id. rewrite Forall_forall. + intros [kn' d] []. + inversion H. + constructor. + inversion H. + - intros mi Hmi sb Hsb kn id. + rewrite Forall_forall. intros [kn' d]. + destruct mi; cbn; try auto. + -- intros Hin. specialize (Hmi (kn_append kn id)). + rewrite Forall_forall in Hmi. + specialize (Hmi (kn', d)). + simpl in Hmi. specialize (Hmi Hin). + apply kn_extends_trans with (kn' := (kn_append kn id)); auto. + constructor. + -- intros Hin. specialize (Hsb (kn_append kn id)). + rewrite Forall_forall in Hsb. + specialize (Hsb (kn', d)). + simpl in Hsb. specialize (Hsb Hin). + apply kn_extends_trans with (kn' := (kn_append kn id)); auto. + constructor. + - intros i sf Hsf sb Hsb kn. + apply Forall_forall. + intros [kn' d] Hin. + apply in_app_or in Hin. destruct Hin. + -- specialize (Hsf kn i). + rewrite Forall_forall in Hsf. + specialize (Hsf (kn', d)). + simpl in Hsf. apply (Hsf H). + -- specialize (Hsb kn). + rewrite Forall_forall in Hsb. + specialize (Hsb (kn', d)). + simpl in Hsb. apply (Hsb H). + Qed. + + Lemma translated_module_impl_all_kn_extends: + forall mi kn, Forall (fun '(kn', _) => kn_extends kn kn') (trans_module_impl kn mi). + Proof. + set (P := fun sf => forall kn id, Forall (fun '(kn', _) => kn_extends kn kn') (trans_structure_field kn id sf)). + set (P0 := fun mi => forall kn, Forall (fun '(kn', _) => kn_extends kn kn') (trans_module_impl kn mi)). + set (P1 := fun sb => forall kn, Forall (fun '(kn', _) => kn_extends kn kn') (trans_structure_body kn sb)). + apply (Ast.Env.sf_mi_sb_mutind P P0 P1); subst P P0 P1; cbn; try auto. + - intros c kn id. rewrite Forall_forall. + intros [kn' d] []. + inversion H. + constructor. + inversion H. + - intros m kn id. rewrite Forall_forall. + intros [kn' d] []. + inversion H. + constructor. + inversion H. + - intros mi Hmi sb Hsb kn id. + rewrite Forall_forall. intros [kn' d]. + destruct mi; cbn; try auto. + -- intros Hin. specialize (Hmi (kn_append kn id)). + rewrite Forall_forall in Hmi. + specialize (Hmi (kn', d)). + simpl in Hmi. specialize (Hmi Hin). + apply kn_extends_trans with (kn' := (kn_append kn id)); auto. + constructor. + -- intros Hin. specialize (Hsb (kn_append kn id)). + rewrite Forall_forall in Hsb. + specialize (Hsb (kn', d)). + simpl in Hsb. specialize (Hsb Hin). + apply kn_extends_trans with (kn' := (kn_append kn id)); auto. + constructor. + - intros i sf Hsf sb Hsb kn. + apply Forall_forall. + intros [kn' d] Hin. + apply in_app_or in Hin. destruct Hin. + -- specialize (Hsf kn i). + rewrite Forall_forall in Hsf. + specialize (Hsf (kn', d)). + simpl in Hsf. apply (Hsf H). + -- specialize (Hsb kn). + rewrite Forall_forall in Hsb. + specialize (Hsb (kn', d)). + simpl in Hsb. apply (Hsb H). + Qed. + + Lemma translated_structure_body_all_kn_extends: + forall sb kn, Forall (fun '(kn', _) => kn_extends kn kn') (trans_structure_body kn sb). + Proof. + set (P := fun sf => forall kn id, Forall (fun '(kn', _) => kn_extends kn kn') (trans_structure_field kn id sf)). + set (P0 := fun mi => forall kn, Forall (fun '(kn', _) => kn_extends kn kn') (trans_module_impl kn mi)). + set (P1 := fun sb => forall kn, Forall (fun '(kn', _) => kn_extends kn kn') (trans_structure_body kn sb)). + apply (Ast.Env.sf_mi_sb_mutind P P0 P1); subst P P0 P1; cbn; try auto. + - intros c kn id. rewrite Forall_forall. + intros [kn' d] []. + inversion H. + constructor. + inversion H. + - intros m kn id. rewrite Forall_forall. + intros [kn' d] []. + inversion H. + constructor. + inversion H. + - intros mi Hmi sb Hsb kn id. + rewrite Forall_forall. intros [kn' d]. + destruct mi; cbn; try auto. + -- intros Hin. specialize (Hmi (kn_append kn id)). + rewrite Forall_forall in Hmi. + specialize (Hmi (kn', d)). + simpl in Hmi. specialize (Hmi Hin). + apply kn_extends_trans with (kn' := (kn_append kn id)); auto. + constructor. + -- intros Hin. specialize (Hsb (kn_append kn id)). + rewrite Forall_forall in Hsb. + specialize (Hsb (kn', d)). + simpl in Hsb. specialize (Hsb Hin). + apply kn_extends_trans with (kn' := (kn_append kn id)); auto. + constructor. + - intros i sf Hsf sb Hsb kn. + apply Forall_forall. + intros [kn' d] Hin. + apply in_app_or in Hin. destruct Hin. + -- specialize (Hsf kn i). + rewrite Forall_forall in Hsf. + specialize (Hsf (kn', d)). + simpl in Hsf. apply (Hsf H). + -- specialize (Hsb kn). + rewrite Forall_forall in Hsb. + specialize (Hsb (kn', d)). + simpl in Hsb. apply (Hsb H). + Qed. + + Lemma translated_module_decl_all_kn_extends: + forall m kn, Forall (fun '(kn', _) => kn_extends kn kn') (trans_module_decl kn m). + Proof. + destruct m as [[] mt]; cbn; auto; apply translated_structure_body_all_kn_extends. + Qed. + + Lemma translated_modtype_decl_all_kn_neq: + forall mt kn, Forall (fun '(kn', _) => kn <> kn') (trans_modtype_decl kn mt). + Proof. + intros mt kn; apply (Forall_impl (P := (fun '(kn', _) => kn_extends kn kn'))). + apply translated_structure_body_all_kn_extends. + intros [kn' _]; apply kn_extends_neq. + Qed. + + Lemma translated_module_decl_all_kn_neq: + forall m kn, Forall (fun '(kn', _) => kn <> kn') (trans_module_decl kn m). + Proof. + destruct m as [[] mt]; cbn; auto; apply translated_modtype_decl_all_kn_neq. + Qed. + + Definition trans_global_decl (d : kername × Ast.Env.global_decl) := + let (kn, decl) := d in match decl with + | Ast.Env.ConstantDecl bd => [(kn, ConstantDecl (trans_constant_body bd))] + | Ast.Env.InductiveDecl bd => [(kn, InductiveDecl (trans_minductive_body bd))] + | Ast.Env.ModuleDecl bd => trans_module_decl kn bd + | Ast.Env.ModuleTypeDecl _ => [] end. End Trans. -Program Definition add_global_decl (env : global_env_map) (d : kername × global_decl) := - {| trans_env_env := add_global_decl env.(trans_env_env) d; +Program Definition add_global_decl (d : kername × global_decl) (env : global_env_map) := + {| trans_env_env := add_global_decl d env.(trans_env_env); trans_env_map := EnvMap.add d.1 d.2 env.(trans_env_map) |}. Next Obligation. pose proof env.(trans_env_repr). @@ -163,8 +524,8 @@ Qed. Definition trans_global_decls env (d : Ast.Env.global_declarations) : global_env_map := fold_right (fun decl Σ' => - let decl' := on_snd (trans_global_decl Σ') decl in - add_global_decl Σ' decl') env d. + let decls := (trans_global_decl Σ' decl) in + fold_right add_global_decl Σ' decls) env d. Definition empty_trans_env univs retro := let init_global_env := {| universes := univs; declarations := []; retroknowledge := retro |} in diff --git a/pcuic/theories/TemplateToPCUICCorrectness.v b/pcuic/theories/TemplateToPCUICCorrectness.v index 288187407..f01ba3b61 100644 --- a/pcuic/theories/TemplateToPCUICCorrectness.v +++ b/pcuic/theories/TemplateToPCUICCorrectness.v @@ -81,8 +81,8 @@ Proof. destruct o; auto. Qed. -Lemma of_global_env_cons {cf:checker_flags} d g : EnvMap.fresh_globals (add_global_decl g d).(declarations) -> - EnvMap.of_global_env (add_global_decl g d).(declarations) = EnvMap.add d.1 d.2 (EnvMap.of_global_env g.(declarations)). +Lemma of_global_env_cons {cf:checker_flags} d g : EnvMap.fresh_globals (add_global_decl d g).(declarations) -> + EnvMap.of_global_env (add_global_decl d g).(declarations) = EnvMap.add d.1 d.2 (EnvMap.of_global_env g.(declarations)). Proof. unfold EnvMap.of_global_env. simpl. unfold KernameMapFact.uncurry. reflexivity. @@ -105,6 +105,48 @@ Proof. rewrite trans_lookup_minductive //. Qed. +Lemma lookup_env_add_global_decl : forall univs decls retro kn d, + lookup_env (add_global_decl (kn, d) + (build_global_env_map({| universes := univs; declarations := decls; retroknowledge := retro |}))) = + lookup_env ({| universes := univs; declarations := (kn, d)::decls; retroknowledge := retro |}). +Proof. + simpl. unfold PCUICEnvironment.add_global_decl; simpl. + reflexivity. +Qed. + +(* Lemma lookup_env_trans_global_decl_app : forall univs decls retro kn d, +let Σmap := (build_global_env_map {| universes := univs; declarations := decls; retroknowledge := retro |}) in +trans_global_decls Σmap [(kn,d)] = +(build_global_env_map {| + universes := univs; + declarations := (trans_global_decl Σmap (kn, d)) ++ decls; + retroknowledge := retro |}). +Proof. + intros univs decls retro kn d Σmap. + destruct d; cbn; auto. + - unfold add_global_decl; cbn. + unfold build_global_env_map; cbn. + unfold PCUICEnvironment.add_global_decl; cbn. + unfold PCUICProgram.build_global_env_map_obligation_1; cbn. + unfold TemplateToPCUIC.add_global_decl_obligation_1. *) + + +Lemma trans_lookup_module {cf} {Σ : Ast.Env.global_env} cst m : + Ast.Env.lookup_env Σ cst = Some (Ast.Env.ModuleDecl m) -> + lookup_env (trans_global_env Σ) cst = None. +Proof. + destruct Σ as [univs decls retro]. + intros H. + cbn -[fold_right]. + induction decls as [|[kn g] tl IHtl]; cbn -[fold_right]; auto. + cbn in H. + (** immediately to inductive case: a::Σ *) + destruct eq_kername eqn: E. + - apply eqb_eq in E. subst kn. + unfold trans_global_env in *; simpl in *. + (* remember (fun (decl : kername × Ast.Env.global_decl) (Σ' : global_env_map) => fold_right add_global_decl Σ' (trans_global_decl Σ' decl)) as f. *) + + Lemma mkApps_morphism (f : term -> term) u v : (forall x y, f (tApp x y) = tApp (f x) (f y)) -> f (mkApps u v) = mkApps (f u) (List.map f v). @@ -148,16 +190,27 @@ Proof. split; [lsets|csets]. Qed. +Lemma invariant_fold {A B: Type} (f: B -> A -> A) (P: A -> Prop): + (forall a b, (P a -> P (f b a))) -> (forall a l, P a -> P (fold_right f a l)). +Proof. + intros H a l. + induction l; try now cbn. +Qed. + Lemma extends_trans_global_decls_acc (Σ' : global_env_map) (Σ : Ast.Env.global_declarations) : extends_decls Σ' (trans_global_decls Σ' Σ). Proof. induction Σ. * split; cbn; now try exists []. - * rewrite /=. - destruct IHΣ as [univs [Σ'' eq]]. cbn in *. - split; cbn; auto. - eexists (_ :: Σ''). - rewrite -app_comm_cons. now f_equal. + * destruct IHΣ as [univs [Σ'' eq]]. + split. + - simpl. now apply invariant_fold. + - simpl. + exists ((trans_global_decl (trans_global_decls Σ' Σ) a) ++ Σ''). + induction (trans_global_decl (trans_global_decls Σ' Σ) a); cbn in *. + -- exact eq. + -- f_equal. exact IHl. + - simpl; now apply invariant_fold. Qed. Definition wf_global_decl {cf} (Σ : Ast.Env.global_env_ext) kn decl := @@ -169,13 +222,18 @@ Definition wf_global_decl {cf} (Σ : Ast.Env.global_env_ext) kn decl := Lemma trans_lookup_env {cf} {Σ : Ast.Env.global_env} cst {wfΣ : Typing.wf Σ} : match Ast.Env.lookup_env Σ cst with | None => lookup_env (trans_global_env Σ) cst = None - | Some d => - ∑ Σ' : Ast.Env.global_env, - [× Ast.Env.extends_decls Σ' Σ, - Typing.wf Σ', - wf_global_decl (Σ', Ast.universes_decl_of_decl d) cst d, - extends_decls (trans_global_env Σ') (trans_global_env Σ) & - lookup_env (trans_global_env Σ) cst = Some (trans_global_decl (trans_global_env Σ') d)] + | Some d => match d with + | Ast.Env.ConstantDecl _ | Ast.Env.InductiveDecl _ => + ∑ (Σ' : Ast.Env.global_env) (d': global_decl), + [× Ast.Env.extends_decls Σ' Σ, + Typing.wf Σ', + wf_global_decl (Σ', Ast.universes_decl_of_decl d) cst d, + extends_decls (trans_global_env Σ') (trans_global_env Σ), + trans_global_decl (trans_global_env Σ') (cst, d) = (cst, d')::[] & + lookup_env (trans_global_env Σ) cst = Some d'] + (** Modules are elaborated away. *) + | Ast.Env.ModuleDecl _ | Ast.Env.ModuleTypeDecl _ => lookup_env (trans_global_env Σ) cst = None + end end. Proof. destruct Σ as [univs Σ retro]. @@ -183,24 +241,198 @@ Proof. - cbn; auto. - unfold Ast.Env.lookup_env. cbn -[trans_global_env]. destruct eq_kername eqn:eqk. - change (eq_kername cst a.1) with (eqb cst a.1) in eqk. + (* change (eq_kername cst a.1) with (eqb cst a.1) in eqk. *) apply eqb_eq in eqk; subst. - eexists {| S.Env.universes := univs; S.Env.declarations := Σ; S.Env.retroknowledge := retro |}. - split. - * split => //. now exists [a]. - * destruct wfΣ as [onu ond]. depelim ond. - split => //. - * eapply TypingWf.typing_wf_sigma in wfΣ. - destruct wfΣ as [onu ond]. depelim ond. now destruct o. - * split => //. - now exists [(a.1, trans_global_decl (trans_global_env {| S.Env.universes := univs; S.Env.declarations := Σ; - S.Env.retroknowledge := retro |}) a.2)]. - * cbn. now rewrite eq_kername_refl. - * destruct wfΣ as [onu ond]. depelim ond. + set {| S.Env.universes := univs; S.Env.declarations := Σ; S.Env.retroknowledge := retro |} as Σmap. + set {| S.Env.universes := univs; S.Env.declarations := a::Σ; S.Env.retroknowledge := retro |} as Σmap'. + + -- (** Case 1: looking up [cst] in [a::Σ], and a.1 == cst. + Strategy: if a.2 is constant or inductive, then we should be able to + find its obvious translation. If a.2 is a module or inductive, cst + should not exist in the translated environment. *) + destruct a.2 eqn:E => //= . + + --- (** a.2 is a Constant decl *) + exists Σmap. + exists (ConstantDecl (trans_constant_body (trans_global_env Σmap) c)). + split => //=. + * split => //. now exists [a]. + * destruct wfΣ as [onu ond]. depelim ond. + split => //. + * eapply TypingWf.typing_wf_sigma in wfΣ. + destruct wfΣ as [onu ond]. depelim ond. + simpl in E. rewrite E in o; now destruct o. + * subst Σmap Σmap'. unfold trans_global_env. + split => /=; try now apply invariant_fold. + induction (trans_global_decl (trans_global_decls (empty_trans_env univs retro) Σ) a). + ** now exists []. + ** simpl. destruct IHl as [Σ'' IHl]. + exists (a0 :: Σ''). now rewrite IHl. + * destruct wfΣ as [onu ond]. depelim ond. + specialize (IHΣ (onu, ond)). + unfold Ast.Env.lookup_env in IHΣ. cbn [Ast.Env.declarations] in IHΣ. + destruct (Ast.Env.lookup_global Σ (kn, d).1) eqn:h. + ** simpl in *. subst. + destruct o. apply ST.fresh_global_iff_lookup_global_None in kn_fresh. + rewrite kn_fresh in h. exfalso. inversion h. + ** simpl in *. subst. + cbn. now rewrite eqb_refl. + + --- (** a.2 is an Inductive decl *) + exists Σmap. exists (InductiveDecl (trans_minductive_body (trans_global_env Σmap) m)). + split => //=. + * split => //. now exists [a]. + * destruct wfΣ as [onu ond]. depelim ond. + split => //. + * eapply TypingWf.typing_wf_sigma in wfΣ. + destruct wfΣ as [onu ond]. depelim ond. + simpl in E. rewrite E in o; now destruct o. + * subst Σmap Σmap'. unfold trans_global_env. + split => /=; try now apply invariant_fold. + induction (trans_global_decl (trans_global_decls (empty_trans_env univs retro) Σ) a). + ** now exists []. + ** simpl. destruct IHl as [Σ'' IHl]. + exists (a0 :: Σ''). now rewrite IHl. + * destruct wfΣ as [onu ond]. depelim ond. + specialize (IHΣ (onu, ond)). + unfold Ast.Env.lookup_env in IHΣ. cbn [Ast.Env.declarations] in IHΣ. + destruct (Ast.Env.lookup_global Σ (kn, d).1) eqn:h. + ** simpl in *. subst. + destruct o. apply ST.fresh_global_iff_lookup_global_None in kn_fresh. + rewrite kn_fresh in h. inversion h. + ** simpl in *. subst. + cbn. now rewrite eqb_refl. + + (** Module. *) + --- (** a.2 is a *) + unfold trans_global_env. subst Σmap'; simpl. + destruct a as [kn d]; simpl in *. + rewrite E. + remember (trans_global_decls (empty_trans_env univs retro) Σ) as Σtrans. + set (P := fun sf => forall id, lookup_env (fold_right add_global_decl Σtrans (trans_structure_field Σtrans kn id sf)) kn = None). + set (P0 := fun mi => lookup_env (fold_right add_global_decl Σtrans (trans_module_impl Σtrans kn mi)) kn = None). + set (P1 := fun mt => lookup_env (fold_right add_global_decl Σtrans (trans_structure_body Σtrans kn mt)) kn = None). + assert ((forall s : Ast.Env.structure_field, P s) × (forall m : Ast.Env.module_implementation, P0 m) × (forall s : Ast.Env.structure_body, P1 s)). + (** proving assertion by mutual induction *) + * subst P P0 P1. apply Ast.Env.sf_mi_sb_mutind => //=. + ** cbn. intros c id. + pose proof (kn_appended_not_eq kn id). + destruct eq_kername eqn: K. + apply eqb_eq in K; contradiction. + destruct wfΣ as [onu ond]. depelim ond. + specialize (IHΣ (onu, ond)). + unfold Ast.Env.lookup_env in IHΣ. cbn [Ast.Env.declarations] in IHΣ. + destruct (Ast.Env.lookup_global Σ kn) eqn:h. + *** simpl in *. subst. + destruct o. apply ST.fresh_global_iff_lookup_global_None in kn_fresh. + rewrite kn_fresh in h. inversion h. + *** subst. apply IHΣ. + ** cbn. intros i id. + pose proof (kn_appended_not_eq kn id). + destruct eq_kername eqn: K. + apply eqb_eq in K; contradiction. + destruct wfΣ as [onu ond]. depelim ond. + specialize (IHΣ (onu, ond)). + unfold Ast.Env.lookup_env in IHΣ. cbn [Ast.Env.declarations] in IHΣ. + destruct (Ast.Env.lookup_global Σ kn) eqn:h. + *** simpl in *. subst. + destruct o. apply ST.fresh_global_iff_lookup_global_None in kn_fresh. + rewrite kn_fresh in h. inversion h. + *** subst. apply IHΣ. + ** intros [] Hmi sb Hsb id; cbn; auto. + *** admit. + *** + + + + * destruct m as [[] mt] => /=. + ** + generalize (trans_global_decls (empty_trans_env univs retro) Σ). + generalize m. + * + + + (** Module Type. *) + --- admit. + + + -- (** Case where a.1 != cst. *) + destruct wfΣ as [onu ond]. depelim ond. specialize (IHΣ (onu, ond)). unfold Ast.Env.lookup_env in IHΣ. cbn [Ast.Env.declarations] in IHΣ. destruct (Ast.Env.lookup_global Σ cst) eqn:h. - destruct IHΣ as [Σ' [ext wf ext' hl]]. + destruct g => //=. + + --- destruct IHΣ as [Σ' [d' [ext wf ext' sth hl]]]. + exists Σ', d'. split => //. + * split => //=. + ** apply ext. + ** destruct ext as [_ [Σ'' HΣ''] _]. + exists ((kn,d)::Σ''). simpl in HΣ''. + now rewrite HΣ''. + ** apply ext. + * destruct sth as [Hunivs [Σ'' HΣ] Hretro]. split => //=. + ** cbn. now apply invariant_fold. + ** exists ((trans_global_decl (trans_global_decls (empty_trans_env univs retro) Σ) (kn, d)) ++ Σ''). + destruct d => /=; try now rewrite HΣ. + unfold trans_global_env; simpl. + induction (trans_module_decl (trans_global_decls (empty_trans_env univs retro) Σ) + kn m); try now cbn. + ** cbn. now apply invariant_fold. + * unfold lookup_env. + unfold lookup_global; simpl. + destruct d => /=; try now rewrite eqk. + (** prove that kn of module cannot be found in the translated env. + most probably need to do an induction. *) + ** unfold trans_global_env; simpl. + destruct m as [mi mt]. + admit. + ** unfold trans_global_env; simpl. apply e. + + --- destruct IHΣ as [Σ' [d' [ext wf ext' sth hl]]]. + exists Σ', d'. split => //. + * split => //=. + ** apply ext. + ** destruct ext as [_ [Σ'' HΣ''] _]. + exists ((kn,d)::Σ''). simpl in HΣ''. + now rewrite HΣ''. + ** apply ext. + * destruct sth as [Hunivs [Σ'' HΣ] Hretro]. split => //=. + ** cbn. now apply invariant_fold. + ** exists ((trans_global_decl (trans_global_decls (empty_trans_env univs retro) Σ) (kn, d)) ++ Σ''). + destruct d => /=; try now rewrite HΣ. + unfold trans_global_env; simpl. + induction (trans_module_decl (trans_global_decls (empty_trans_env univs retro) Σ) + kn m0); try now cbn. + ** cbn. now apply invariant_fold. + * unfold lookup_env. + unfold lookup_global; simpl. + destruct d => /=; try now rewrite eqk. + (** A repeat of the above (possibly) induction. *) + ** unfold trans_global_env; simpl. + destruct m as [mi mt]. + admit. + ** apply e. + + --- unfold lookup_env. + unfold lookup_global; simpl. + destruct d => /=; try now rewrite eqk. + (** another repeat *) + admit. apply IHΣ. + + --- unfold lookup_env. + unfold lookup_global; simpl. + destruct d => /=; try now rewrite eqk. + (** another repeat *) + admit. apply IHΣ. + + --- unfold lookup_env. + unfold lookup_global; simpl. + destruct d => /=; try now rewrite eqk. + (** another repeat *) + admit. apply IHΣ. +Admitted. + (* destruct IHΣ as [Σ' [ext wf ext' hl]]. exists Σ'. split => //. destruct ext as [equ [? eq]]. split => //. exists ((kn, d) :: x). cbn. @@ -212,7 +444,7 @@ Proof. cbn. rewrite -eq'. reflexivity. cbn. rewrite eqk /=. apply e. cbn. now rewrite eqk. -Qed. +Qed. *) Lemma trans_weakening {cf} Σ {Σ' : global_env_map} t : Typing.wf Σ -> extends_decls (trans_global_env Σ) Σ' -> wf Σ' -> @@ -237,7 +469,7 @@ Proof. red in X0. f_equal => //. rewrite /id. unfold trans_predicate. f_equal; solve_all. f_equal. solve_all. -Qed. +Admitted. Lemma trans_decl_weakening {cf} Σ {Σ' : global_env_map} t : Typing.wf Σ -> extends_decls (trans_global_env Σ) Σ' -> wf Σ' -> @@ -288,7 +520,7 @@ Qed. Lemma trans_global_decl_weaken {cf} (Σ : Ast.Env.global_env_ext) {Σ' : global_env_map} kn d : Typing.wf Σ -> extends_decls (trans_global_env Σ) Σ' -> wf Σ' -> wf_global_decl Σ kn d -> - trans_global_decl (trans_global_env Σ) d = trans_global_decl Σ' d. + trans_global_decl (trans_global_env Σ) (kn,d) = trans_global_decl Σ' (kn,d). Proof. intros. destruct d; cbn; f_equal. @@ -305,7 +537,7 @@ Proof. eapply TypingWf.on_global_inductive_wf_params in X2. solve_all. * eapply TypingWf.on_global_inductive_wf_bodies in X2. solve_all. rewrite trans_ind_body_weakening //. -Qed. +Admitted. Import TypingWf. @@ -318,7 +550,8 @@ Proof. destruct T; intuition eauto using wf_extends. Qed. -Lemma trans_lookup {cf} Σ cst : +(** FIXME: only true if cst refers to constant or mutind *) +(* Lemma trans_lookup {cf} Σ cst : Typing.wf Σ -> wf (trans_global_env Σ) -> lookup_env (trans_global_env Σ) cst = @@ -330,7 +563,7 @@ Proof. intros [Σ' [ext wfΣ' wfdecl ext' hl]]. rewrite hl. cbn. f_equal. eapply (trans_global_decl_weaken (Σ', Ast.universes_decl_of_decl g)); tea. -Qed. +Qed. *) Section Translation. Context (Σ : Ast.Env.global_env). @@ -669,7 +902,7 @@ Section Trans_Global. Ast.declared_constant Σ cst decl -> declared_constant Σ' cst (trans_constant_body Σ' decl). Proof. - unfold declared_constant, Ast.declared_constant, + unfold declared_constant, Ast.declared_constant, declared_constant_gen, Ast.declared_constant_gen. now rewrite trans_lookup => -> /=. Qed. @@ -743,7 +976,7 @@ Lemma declared_inductive_inj {Σ mdecl mdecl' ind idecl idecl'} : mdecl = mdecl' /\ idecl = idecl'. Proof. intros [] []. unfold Ast.declared_minductive in *. - unfold Ast.declared_minductive_gen in H1. + unfold Ast.declared_minductive_gen in H1. rewrite H in H1. inversion H1. subst. rewrite H2 in H0. inversion H0. eauto. Qed. @@ -752,10 +985,10 @@ Lemma lookup_inductive_None Σ ind : lookup_inductive Σ ind = None -> Proof. intros hl [mdecl [idecl [decli hnth]]]. unfold declared_inductive, declared_minductive in decli. - unfold lookup_inductive, lookup_inductive_gen, + unfold lookup_inductive, lookup_inductive_gen, lookup_minductive, lookup_minductive_gen in hl. - unfold declared_minductive_gen in decli. - destruct lookup_env eqn:heq. + unfold declared_minductive_gen in decli. + destruct lookup_env eqn:heq. noconf decli. cbn in hl. destruct nth_error; congruence. congruence. Qed. @@ -774,7 +1007,7 @@ Section Trans_Global. unfold SEq.R_global_instance, SEq.global_variance. destruct gref; simpl; auto. - unfold R_global_instance_gen, R_opt_variance; cbn. - unfold Ast.lookup_inductive_gen, lookup_inductive_gen, + unfold Ast.lookup_inductive_gen, lookup_inductive_gen, Ast.lookup_minductive_gen, lookup_minductive_gen. rewrite trans_lookup. destruct Ast.Env.lookup_env eqn:look => //; simpl. destruct g => /= //. @@ -1287,7 +1520,7 @@ Section Trans_Global. lookup_inductive Σ' ind = Some (mdecl, idecl). Proof. intros []. unfold lookup_inductive, lookup_minductive. - unfold lookup_inductive_gen, lookup_minductive_gen. + unfold lookup_inductive_gen, lookup_minductive_gen. now rewrite H H0. Qed. @@ -1989,17 +2222,20 @@ Proof. destruct l; auto. now rewrite -trans_check_rec_kind. Qed. -Lemma trans_global_decl_universes Σ d : - Ast.universes_decl_of_decl d = - universes_decl_of_decl (trans_global_decl Σ d). +Lemma trans_global_decl_universes Σ kn d : + Forall (fun '(_, d') => Ast.universes_decl_of_decl d = universes_decl_of_decl d') + (trans_global_decl Σ (kn,d)). Proof. - destruct d; reflexivity. -Qed. + destruct d; try now cbn. + apply Forall_forall. + (** possibly induction again. *) +Admitted. -Lemma trans_consistent_instance_ext {cf:checker_flags} Σ d u : +Lemma trans_consistent_instance_ext {cf:checker_flags} Σ kn d u : let Σ' := trans_global Σ in Ast.consistent_instance_ext Σ (Ast.universes_decl_of_decl d) u -> - consistent_instance_ext Σ' (universes_decl_of_decl (trans_global_decl Σ' d)) u. + Forall (fun '(_, d') => consistent_instance_ext Σ' (universes_decl_of_decl d') u) + (trans_global_decl Σ' (kn, d)). Proof. intros Σ'. unfold Ast.consistent_instance_ext, consistent_instance_ext. diff --git a/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v b/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v index a7f6b32c2..e0ae7cf61 100644 --- a/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v +++ b/pcuic/theories/Typing/PCUICWeakeningEnvTyp.v @@ -336,7 +336,7 @@ Proof. split => //. - split; [lsets|csets]. - exists []; simpl; destruct Σ; eauto. - - apply Retroknowledge.extends_refl. + - apply Environment.Retroknowledge.extends_refl. Qed. Lemma weaken_decls_lookup_on_global_env `{checker_flags} P Σ c decl : diff --git a/pcuic/theories/utils/PCUICPrimitive.v b/pcuic/theories/utils/PCUICPrimitive.v index 9d7cb25ca..5f47ca192 100644 --- a/pcuic/theories/utils/PCUICPrimitive.v +++ b/pcuic/theories/utils/PCUICPrimitive.v @@ -1,6 +1,6 @@ (* Distributed under the terms of the MIT license. *) -From MetaCoq.Template Require Import utils Universes BasicAst Primitive Reflect - Environment EnvironmentTyping. +From MetaCoq.Template Require Import utils Universes BasicAst Primitive Reflect. +From MetaCoq.PCUIC Require Import Environment EnvironmentTyping. From Equations Require Import Equations. From Coq Require Import ssreflect. From Coq Require Import Uint63 SpecFloat. diff --git a/safechecker/theories/PCUICSafeConversion.v b/safechecker/theories/PCUICSafeConversion.v index 6dd6d3e67..58b2fe9c2 100644 --- a/safechecker/theories/PCUICSafeConversion.v +++ b/safechecker/theories/PCUICSafeConversion.v @@ -215,7 +215,6 @@ Section Conversion. Defined. Derive Signature for Subterm.lexprod. - Lemma R_aux_Acc : forall Γ t p w q s, (forall Σ, abstract_env_ext_rel X Σ -> welltyped Σ Γ t) -> diff --git a/template-coq/src/plugin_core.ml b/template-coq/src/plugin_core.ml index 79ffcb202..06346e874 100644 --- a/template-coq/src/plugin_core.ml +++ b/template-coq/src/plugin_core.ml @@ -169,7 +169,7 @@ let tmQuoteUniverses : UGraph.t tm = let quote_module (qualid : qualid) : global_reference list = let mp = Nametab.locate_module qualid in let mb = Global.lookup_module mp in - let rec aux mb = + let rec aux mp mb = let open Declarations in let me = mb.mod_expr in let get_refs s = @@ -179,7 +179,7 @@ let quote_module (qualid : qualid) : global_reference list = match field with | SFBconst _ -> [GlobRef.ConstRef (Constant.make2 mp label)] | SFBmind _ -> [GlobRef.IndRef (MutInd.make2 mp label, 0)] - | SFBmodule mb -> aux mb + | SFBmodule mb -> aux (MPdot (mp,label)) mb | SFBmodtype mtb -> [] in CList.map_append get_ref body @@ -189,7 +189,7 @@ let quote_module (qualid : qualid) : global_reference list = | Algebraic _ -> [] | Struct s -> get_refs s | FullStruct -> get_refs mb.Declarations.mod_type - in aux mb + in aux mp mb let tmQuoteModule (qualid : qualid) : global_reference list tm = fun ~st env evd success _fail -> diff --git a/template-coq/theories/Checker.v b/template-coq/theories/Checker.v index f84cd6e4e..584081919 100644 --- a/template-coq/theories/Checker.v +++ b/template-coq/theories/Checker.v @@ -5,7 +5,7 @@ Import MCMonadNotation. (** * Coq type-checker for kernel terms - Implemets [typecheck_program] which returns an error and + Implements [typecheck_program] which returns an error and on success should guarantee that the term has the given type. Currently uses fuel to implement reduction and is unverified. @@ -864,19 +864,50 @@ Section Checker. Definition infer_term Σ G t := wrap_error "" (infer Σ G [] t). - Definition check_wf_decl Σ G kn (g : global_decl) : EnvCheck () := - match g with - | ConstantDecl cst => - match cst.(cst_body) with - | Some term => check_wf_judgement (string_of_kername kn) Σ G term cst.(cst_type) - | None => check_wf_type (string_of_kername kn) Σ G cst.(cst_type) - end - | InductiveDecl inds => + Definition check_wf_const_body Σ G kn cst: EnvCheck ():= + match cst.(cst_body) with + | Some term => check_wf_judgement (string_of_kername kn) Σ G term cst.(cst_type) + | None => check_wf_type (string_of_kername kn) Σ G cst.(cst_type) + end. + + Definition check_wf_ind_body Σ G inds: EnvCheck () := List.fold_left (fun acc body => acc ;; check_wf_type body.(ind_name) Σ G body.(ind_type)) - inds.(ind_bodies) (ret ()) + inds.(ind_bodies) (ret ()). + + (* FIXME: modify this to follow closely https://coq.inria.fr/refman/language/core/modules.html#typing-modules *) + Fixpoint check_wf_mod_impl Σ G kn impl: EnvCheck () := + match impl with + | mi_abstract | mi_fullstruct | mi_algebraic _ => CorrectDecl () + | mi_struct sb => check_wf_structure_body Σ G kn sb + end + with check_wf_structure_field Σ G kn sf: EnvCheck () := + match sf with + | sfconst cst => check_wf_const_body Σ G kn cst + | sfmind inds => check_wf_ind_body Σ G inds + | sfmod impl modtype => check_wf_mod_impl Σ G kn impl ;; check_wf_structure_body Σ G kn modtype + | sfmodtype mt => check_wf_structure_body Σ G kn mt + end + with check_wf_structure_body Σ G kn sb : EnvCheck() := + match sb with + | sb_nil => CorrectDecl () + | sb_cons id sf sb' => + check_wf_structure_field Σ G ((MPdot kn.1 kn.2), id) sf ;; check_wf_structure_body Σ G kn sb' end. + Definition check_wf_modtype_decl := check_wf_structure_body. + + Definition check_wf_mod_decl Σ G kn m := + check_wf_mod_impl Σ G kn m.1 ;; check_wf_modtype_decl Σ G kn m.2. + + Definition check_wf_decl Σ G kn (g : global_decl) : EnvCheck () := + match g with + | ConstantDecl cst => check_wf_const_body Σ G kn cst + | InductiveDecl inds => check_wf_ind_body Σ G inds + | ModuleDecl m => check_wf_mod_decl Σ G kn m + | ModuleTypeDecl mt => check_wf_modtype_decl Σ G kn mt + end. + Fixpoint check_fresh id (env : global_declarations) : EnvCheck () := match env with | [] => ret () diff --git a/template-coq/theories/Environment.v b/template-coq/theories/Environment.v index 6ba5c0d31..bed7fffa7 100644 --- a/template-coq/theories/Environment.v +++ b/template-coq/theories/Environment.v @@ -2,6 +2,7 @@ From Coq Require Import ssreflect ssrbool ssrfun Morphisms Setoid. From MetaCoq.Template Require Import utils BasicAst Primitive. From MetaCoq.Template Require Import Universes. +From Equations Require Import Equations. Module Type Term. @@ -318,63 +319,248 @@ Module Environment (T : Term). option_map f (cst_body decl) = cst_body (map_constant_body f decl). Proof. destruct decl; reflexivity. Qed. - Inductive global_decl := - | ConstantDecl : constant_body -> global_decl - | InductiveDecl : mutual_inductive_body -> global_decl. - Derive NoConfusion for global_decl. + (** See [generic_module_body] from [declarations.ml]. We do not include the modpath + in the body since it is already included in [global_declarations]. *) + (** implementation -> module type -> algebraic (colon-annotated) module type (TODO) *) + Inductive structure_field := + | ConstantDecl : constant_body -> structure_field + | InductiveDecl : mutual_inductive_body -> structure_field + | ModuleDecl : module_implementation -> list (ident × structure_field) -> structure_field + | ModuleTypeDecl : list (ident × structure_field) -> structure_field + with module_implementation := + | mi_abstract : module_implementation (** Declare Module M: T. *) + | mi_algebraic : kername -> module_implementation (** Module M [:T] := N. *) + | mi_struct : list (ident × structure_field) -> module_implementation (** Module M:T. ... End M.*) + | mi_fullstruct : module_implementation (** Module M. ... End M.*). + + Notation structure_body := (list (ident × structure_field))%type. + + Section Induction. + Variable (P : structure_field -> Type) (P0 : module_implementation -> Type). + Definition P1 : structure_body -> Type := All (fun x => P (snd x)). + + Variable (f : forall c : constant_body, P (ConstantDecl c)) + (f0 : forall m : mutual_inductive_body, P (InductiveDecl m)) + (f1 : forall m : module_implementation, + P0 m -> forall s : structure_body, P1 s -> P (ModuleDecl m s)) + (f2 : forall s : structure_body, P1 s -> P (ModuleTypeDecl s)) + (f3 : P0 mi_abstract) (f4 : forall k : kername, P0 (mi_algebraic k)) + (f5 : forall s : structure_body, P1 s -> P0 (mi_struct s)) + (f6 : P0 mi_fullstruct). + + Definition f7 : P1 nil := All_nil. + Definition f8 : forall (i : ident) (s : structure_field), + P s -> forall s0 : structure_body, P1 s0 -> P1 (cons (i,s) s0). + Proof. intros i sf Psf sb Psb. apply All_cons => //. Defined. + + Section Nested. + Variable F : forall (s: structure_field), P s. + Fixpoint F1 (s : structure_body) : P1 s := + match s as s0 return (P1 s0) with + | nil => f7 + | cons (i,s0) s1 => f8 i s0 (F s0) s1 (F1 s1) + end. + End Nested. + + Fixpoint F (s : structure_field) : P s := + match s as s0 return (P s0) with + | ConstantDecl c => f c + | InductiveDecl m => f0 m + | ModuleDecl m s0 => f1 m (F0 m) s0 (F1 F s0) + | ModuleTypeDecl s0 => f2 s0 (F1 F s0) + end + with F0 (m : module_implementation) : P0 m := + match m as m0 return (P0 m0) with + | mi_abstract => f3 + | mi_algebraic k => f4 k + | mi_struct s => f5 s (F1 F s) + | mi_fullstruct => f6 + end. - Definition global_declarations := list (kername * global_decl). + Definition structureField_rect := F. + Definition moduleImpl_rect := F0. + Definition structureBody_rect := F1 F. + End Induction. + + Definition sf_mi_sb_mutrect + (P : structure_field -> Type) (P0 : module_implementation -> Type) + (P1 : structure_body -> Type := All (fun x => P (snd x))) + (f : forall c : constant_body, P (ConstantDecl c)) + (f0 : forall m : mutual_inductive_body, P (InductiveDecl m)) + (f1 : forall m : module_implementation, + P0 m -> forall s : structure_body, P1 s -> P (ModuleDecl m s)) + (f2 : forall s : structure_body, P1 s -> P (ModuleTypeDecl s)) + (f3 : P0 mi_abstract) (f4 : forall k : kername, P0 (mi_algebraic k)) + (f5 : forall s : structure_body, P1 s -> P0 (mi_struct s)) + (f6 : P0 mi_fullstruct) : + (forall s: structure_field, P s) * (forall m: module_implementation, P0 m) + * (forall s: structure_body, P1 s). + Proof. + repeat split. + eapply structureField_rect; eauto. + eapply moduleImpl_rect; eauto. + eapply structureBody_rect; eauto. + Defined. + + Definition module_type_decl := structure_body. + Definition module_decl := module_implementation × module_type_decl. + Notation global_decl := structure_field. + Notation global_declarations := structure_body. + + Section WellFounded. + Equations alt_size_sf (sf: structure_field) : nat := + | ConstantDecl _ := 1; + | InductiveDecl _ := 1; + | ModuleDecl mi mt := 1 + (max (alt_size_mi mi) (alt_size_sb mt)); + | ModuleTypeDecl mt := 1 + (alt_size_sb mt); + where alt_size_sb (sb: structure_body) : nat := + | nil := 0; + | (hd::tl) := alt_size_sf hd.2 + alt_size_sb tl; + where alt_size_mi (mi: module_implementation) : nat := + | mi_struct s := alt_size_sb s; + | _ := 0. + + Lemma alt_size_sf_ge_one: (forall sf: structure_field, 0 < alt_size_sf sf). + Proof. + destruct sf; simp alt_size_sf; lia. + Qed. + + Equations paths_of_structure_field (sf: structure_field) (prefix: list ident) + : list (list ident) by wf (alt_size_sf sf) lt := + | ConstantDecl _, p := [p]; + | InductiveDecl _, p := [p]; + | ModuleDecl (mi_struct nil) _, p := []; + | ModuleDecl (mi_struct (hd::tl)) _, p := + (paths_of_structure_field hd.2 (p++[hd.1])) ++ + (paths_of_structure_field (ModuleTypeDecl tl) p) + | ModuleDecl (mi_fullstruct) nil, p := []; + | ModuleDecl (mi_fullstruct) (hd::tl), p := + (paths_of_structure_field hd.2 (p++[hd.1])) ++ + (paths_of_structure_field (ModuleTypeDecl tl) p) + | ModuleDecl _ mt, p := []; + | ModuleTypeDecl nil, p := []; + | ModuleTypeDecl (hd::tl), p := + (paths_of_structure_field hd.2 (p++[hd.1])) ++ + (paths_of_structure_field (ModuleTypeDecl tl) p). + Next Obligation. + simp alt_size_sf. + simpl; rewrite Nat.succ_max_distr. lia. + Defined. Next Obligation. + pose proof (alt_size_sf_ge_one s). + simp alt_size_sf. + simpl; rewrite Nat.succ_max_distr. lia. + Defined. Next Obligation. + pose proof (alt_size_sf_ge_one s). + simp alt_size_sf. + simpl. lia. + Defined. Next Obligation. + pose proof (alt_size_sf_ge_one s). + simp alt_size_sf. simpl. lia. + Defined. Next Obligation. + pose proof (alt_size_sf_ge_one s). + simp alt_size_sf. simpl. lia. + Defined. Next Obligation. + pose proof (alt_size_sf_ge_one s). + simp alt_size_sf. simpl. lia. + Defined. + + Definition paths_of_structure_body (sb: structure_body) (prefix: list ident) + : list (list ident) + := fold_left + (fun acc '(i, sf) => acc ++ (paths_of_structure_field sf (prefix ++ [i]))) + sb []. + End WellFounded. Record global_env := mk_global_env { universes : ContextSet.t; - declarations : global_declarations; - retroknowledge : Retroknowledge.t }. + declarations : structure_body; + retroknowledge : Retroknowledge.t; + path : dirpath }. Coercion universes : global_env >-> ContextSet.t. Definition empty_global_env := {| universes := ContextSet.empty; declarations := []; - retroknowledge := Retroknowledge.empty |}. + retroknowledge := Retroknowledge.empty; + path := []; |}. Definition add_global_decl Σ decl := {| universes := Σ.(universes); declarations := decl :: Σ.(declarations); - retroknowledge := Σ.(retroknowledge) |}. + retroknowledge := Σ.(retroknowledge); + path := Σ.(path) |}. - Lemma eta_global_env Σ : Σ = {| universes := Σ.(universes); declarations := Σ.(declarations); - retroknowledge := Σ.(retroknowledge) |}. + Lemma eta_global_env Σ : + Σ = {| universes := Σ.(universes); declarations := Σ.(declarations); + retroknowledge := Σ.(retroknowledge); path := Σ.(path) |}. Proof. now destruct Σ. Qed. Definition set_declarations Σ decls := {| universes := Σ.(universes); declarations := decls; - retroknowledge := Σ.(retroknowledge) |}. - - Fixpoint lookup_global (Σ : global_declarations) (kn : kername) : option global_decl := - match Σ with + retroknowledge := Σ.(retroknowledge); + path := Σ.(path) |}. + + (* MetaCoq.TemplateCoq.Environment.Environment.destruct_kername => + (MetaCoq.TemplateCoq.Environment, [Environment; destruct_kername]) + for easy lookup. *) + Definition destruct_kername kn : dirpath × list ident := + let destruct_modpath := fix aux mp := + match mp with + | MPfile dp => (dp, []) + | MPbound dp id n => (dp, [id]) + | MPdot mp id => let (dp, l) := aux mp in (dp, l++[id]) + end in + let (dp, l) := destruct_modpath kn.1 in (dp, l++[kn.2]). + + Fixpoint lookup_ident_structure_body (sb: structure_body) i : option structure_field := + match sb with | nil => None - | d :: tl => - if kn == d.1 then Some d.2 - else lookup_global tl kn + | (id, sf) :: tl => if id == i then Some sf else lookup_ident_structure_body tl i end. - Definition lookup_env (Σ : global_env) (kn : kername) := lookup_global Σ.(declarations) kn. + Fixpoint lookup_idents_structure_body (sb: structure_body) (ids: list ident) + : option structure_field := + match ids with + | nil => None + | hd :: nil => lookup_ident_structure_body sb hd + | hd :: tl => match lookup_ident_structure_body sb hd with + | Some (ModuleDecl mi mt) => match mi with + | mi_struct bd => lookup_idents_structure_body bd tl + | mi_fullstruct => lookup_idents_structure_body mt tl + | _ => None + end + | Some (ModuleTypeDecl mt) => lookup_idents_structure_body mt tl + | _ => None + end + end. + + Definition lookup_global (s : global_declarations) (dp: dirpath) (kn : kername) + : option structure_field := + let (kn_dp, kn_l) := destruct_kername kn in + if (dp == kn_dp) then lookup_idents_structure_body s kn_l + else None. + + Definition lookup_env (Σ : global_env) (kn : kername) : option structure_field := + lookup_global Σ.(declarations) Σ.(path) kn. Definition extends (Σ Σ' : global_env) := [× Σ.(universes) ⊂_cs Σ'.(universes), - ∑ Σ'', Σ'.(declarations) = Σ'' ++ Σ.(declarations) & - Retroknowledge.extends Σ.(retroknowledge) Σ'.(retroknowledge)]. + ∑ Σ'', Σ'.(declarations) = Σ'' ++ Σ.(declarations), + Retroknowledge.extends Σ.(retroknowledge) Σ'.(retroknowledge) & + Σ.(path) = Σ'.(path)]. Definition extends_decls (Σ Σ' : global_env) := [× Σ.(universes) = Σ'.(universes), - ∑ Σ'', Σ'.(declarations) = Σ'' ++ Σ.(declarations) & - Σ.(retroknowledge) = Σ'.(retroknowledge)]. + ∑ Σ'', Σ'.(declarations) = Σ'' ++ Σ.(declarations), + Σ.(retroknowledge) = Σ'.(retroknowledge) & + Σ.(path) = Σ'.(path)]. Existing Class extends. Existing Class extends_decls. - Lemma lookup_global_None Σ kn : ~In kn (List.map fst Σ) <-> lookup_global Σ kn = None. + (* Lemma lookup_global_None Σ kn : ~In kn (List.map fst Σ) <-> lookup_global Σ kn = None. Proof. move: Σ; elim => //=; try tauto. move => ??; case: eqb_spec; intuition congruence. @@ -391,7 +577,7 @@ Module Environment (T : Term). all: repeat match goal with H : Some _ = Some _ |- _ => inversion H; clear H end. all: subst => //=; auto. all: try now epose proof (@in_map _ _ fst _ (_, _)); cbn in *; exfalso; eauto. - Qed. + Qed. *) #[global] Instance extends_decls_extends Σ Σ' : extends_decls Σ Σ' -> extends Σ Σ'. Proof. @@ -403,7 +589,8 @@ Module Environment (T : Term). Proof. red. intros x. split => //; try exists [] => //. Qed. Lemma extends_refl : CRelationClasses.Reflexive extends. - Proof. red. intros x. split; [apply incl_cs_refl | now exists [] | apply Retroknowledge.extends_refl]. Qed. + Proof. red. intros x. unfold extends. + split; [apply incl_cs_refl | now exists [] | apply Retroknowledge.extends_refl | reflexivity]. Qed. (* easy prefers this to the local hypotheses, which is annoying #[global] Instance extends_refl : CRelationClasses.Reflexive extends. diff --git a/template-coq/theories/EnvironmentTyping.v b/template-coq/theories/EnvironmentTyping.v index 44d366b7f..b2e12f110 100644 --- a/template-coq/theories/EnvironmentTyping.v +++ b/template-coq/theories/EnvironmentTyping.v @@ -37,6 +37,12 @@ Module Lookup (T : Term) (E : EnvironmentSig T). List.nth_error idecl.(ind_projs) proj.(proj_arg) = Some pdecl /\ mdecl.(ind_npars) = proj.(proj_npars). + Definition declared_module Σ kn moddecl := + lookup_env Σ kn = Some (ModuleDecl moddecl). + + Definition declared_modtype Σ kn mtdecl := + lookup_env Σ kn = Some (ModuleTypeDecl mtdecl). + Definition declared_projection Σ := declared_projection_gen (lookup_env Σ). Definition lookup_constant_gen (lookup : kername -> option global_decl) kn := @@ -89,13 +95,25 @@ Module Lookup (T : Term) (E : EnvironmentSig T). | _ => None end. + Definition lookup_module Σ kn: option module_decl := + match lookup_env Σ kn with + | Some (ModuleDecl d) => Some d + | _ => None + end. + + Definition lookup_modtype Σ kn := + match lookup_env Σ kn with + | Some (ModuleTypeDecl d) => Some d + | _ => None + end. + Definition lookup_projection Σ := lookup_projection_gen (lookup_env Σ). - + Lemma declared_constant_lookup {lookup kn cdecl} : declared_constant_gen lookup kn cdecl -> lookup_constant_gen lookup kn = Some cdecl. Proof. - unfold declared_constant_gen, lookup_constant_gen. + unfold declared_constant_gen, lookup_constant_gen. now intros ->. Qed. @@ -103,7 +121,7 @@ Module Lookup (T : Term) (E : EnvironmentSig T). lookup_constant_gen lookup kn = Some cdecl -> declared_constant_gen lookup kn cdecl. Proof. - unfold declared_constant_gen, lookup_constant_gen. + unfold declared_constant_gen, lookup_constant_gen. destruct lookup as [[]|] => //. congruence. Qed. @@ -181,10 +199,43 @@ Module Lookup (T : Term) (E : EnvironmentSig T). apply (lookup_constructor_declared (id:=(proj_ind p, 0)) hl). Qed. + Lemma declared_module_lookup {Σ mp mdecl} : + declared_module Σ mp mdecl -> + lookup_module Σ mp = Some mdecl. + Proof. + unfold declared_module, lookup_module. now intros ->. + Qed. + + Lemma lookup_module_declared {Σ kn mdecl} : + lookup_module Σ kn = Some mdecl -> + declared_module Σ kn mdecl. + Proof. + unfold declared_module, lookup_module. + destruct lookup_env as [[]|] => //. congruence. + Qed. + + Lemma declared_modtype_lookup {Σ mp mtdecl} : + declared_modtype Σ mp mtdecl -> + lookup_modtype Σ mp = Some mtdecl. + Proof. + unfold declared_modtype, lookup_modtype. now intros ->. + Qed. + + Lemma lookup_modtype_declared {Σ kn mtdecl} : + lookup_modtype Σ kn = Some mtdecl -> + declared_modtype Σ kn mtdecl. + Proof. + unfold declared_modtype, lookup_modtype. + destruct lookup_env as [[]|] => //. congruence. + Qed. + Definition on_udecl_decl {A} (F : universes_decl -> A) d : A := match d with | ConstantDecl cb => F cb.(cst_universes) | InductiveDecl mb => F mb.(ind_universes) + (** FIXME: Recursively check the universes of fields? *) + | ModuleDecl _ => F Monomorphic_ctx + | ModuleTypeDecl _ => F Monomorphic_ctx end. Definition universes_decl_of_decl := on_udecl_decl (fun x => x). @@ -1166,10 +1217,47 @@ Module GlobalMaps (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvT | None => on_type Σ [] d.(cst_type) end. + (** Interactive definitions are stored in modtype if not type-annotated. + Otherwise, the interactive definition is in impl, type annotation in modtype. *) + Inductive on_structure_field Σ : structure_field -> Type := + | on_sfconst c : on_constant_decl Σ c -> on_structure_field Σ (sfconst c) + | on_sfmind kn inds : on_inductive Σ kn inds -> on_structure_field Σ (sfmind inds) + | on_sfmod mi sb : on_module_impl Σ mi -> on_structure_body Σ sb -> on_structure_field Σ (sfmod mi sb) + | on_sfmodtype mtd : on_structure_body Σ mtd -> on_structure_field Σ (sfmodtype mtd) + + with on_structure_body Σ : structure_body -> Type := + | on_sb_nil : on_structure_body Σ sb_nil + | on_sb_cons kn sf sb : on_structure_field Σ sf + -> on_structure_body Σ sb + -> on_structure_body Σ (sb_cons kn sf sb) + with on_module_impl Σ : module_implementation -> Type := + | on_mi_abstract : on_module_impl Σ mi_abstract + | on_mi_algebraic kn : on_module_impl Σ (mi_algebraic kn) + | on_mi_struct sb : on_structure_body Σ sb -> on_module_impl Σ (mi_struct sb) + | on_mi_fullstruct : on_module_impl Σ mi_fullstruct. + (* with on_module_decl Σ : (module_implementation × module_type_decl) -> Type := + | on_mi_abstract_decl mt : on_structure_body Σ mt -> on_module_decl Σ (mi_abstract, mt) + | on_mi_algebraic_decl kn mt: on_structure_body Σ mt -> on_module_decl Σ ((mi_algebraic kn), mt) + | on_mi_struct_decl sb mt: on_structure_body Σ mt -> on_structure_body Σ sb -> on_module_decl Σ ((mi_struct sb), mt) + | on_mi_fullstruct_decl mt: on_structure_body Σ mt -> on_module_decl Σ (mi_fullstruct, mt). *) + + Definition on_module_type_decl := on_structure_body. + Definition on_module_decl Σ m := on_module_impl Σ m.1 × on_module_type_decl Σ m.2. + + Scheme onStructField_rect := Induction for on_structure_field Sort Type + with onModuleImpl_rect := Induction for on_module_impl Sort Type + with onStructBody_rect := Induction for on_structure_body Sort Type. + + (** Generate mutual induction principle for module declarations. *) + Combined Scheme on_mi_sf_sb_mutrect from + onModuleImpl_rect,onStructField_rect,onStructBody_rect. + Definition on_global_decl Σ kn decl := match decl with | ConstantDecl d => on_constant_decl Σ d | InductiveDecl inds => on_inductive Σ kn inds + | ModuleDecl mb => on_module_decl Σ mb + | ModuleTypeDecl mtd => on_structure_body Σ mtd end. (** *** Typing of global environment @@ -1278,25 +1366,25 @@ Module GlobalMaps (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvT destruct u; auto. intuition eauto. Qed. - Lemma on_global_env_impl {cf : checker_flags} Pcmp P Q : - (forall Σ Γ t T, - on_global_env Pcmp P Σ.1 -> - on_global_env Pcmp Q Σ.1 -> - P Σ Γ t T -> Q Σ Γ t T) -> - forall Σ, on_global_env Pcmp P Σ -> on_global_env Pcmp Q Σ. + Lemma on_constant_decl_impl {cf : checker_flags} Pcmp P Q Σ d : + (forall Γ t T, + on_global_env Pcmp P Σ.1 -> + P Σ Γ t T -> Q Σ Γ t T) -> + on_global_env Pcmp P Σ.1 -> + on_constant_decl P Σ d -> on_constant_decl Q Σ d. Proof. - intros X Σ [cu IH]. split; auto. - revert cu IH; generalize (universes Σ) as univs, (retroknowledge Σ) as retro, (declarations Σ). clear Σ. - induction g; intros; auto. constructor; auto. - depelim IH. specialize (IHg cu IH). constructor; auto. - pose proof (globenv_decl _ _ _ _ _ _ _ IH o). - destruct o. constructor; auto. - assert (X' := fun Γ t T => X ({| universes := univs; declarations := _ |}, udecl0) Γ t T - (cu, IH) (cu, IHg)); clear X. - rename X' into X. - clear IH IHg. destruct d; simpl. - - destruct c; simpl. destruct cst_body0; cbn in *; now eapply X. - - destruct on_global_decl_d0 as [onI onP onNP]. + intros X X0 X1. destruct d; destruct cst_body0; unfold on_constant_decl in *; unfold on_type; now simpl. + Qed. + + Lemma on_inductive_decl_impl {cf : checker_flags} Pcmp P Q Σ kn mdecl : + (forall Γ t T, + on_global_env Pcmp P Σ.1 -> + P Σ Γ t T -> Q Σ Γ t T) -> + on_global_env Pcmp P Σ.1 -> + on_inductive Pcmp P Σ kn mdecl -> on_inductive Pcmp Q Σ kn mdecl. + Proof. + intros X X0. + - intros [onI onP onNP]. constructor; auto. -- eapply Alli_impl; tea. intros. refine {| ind_arity_eq := X1.(ind_arity_eq); @@ -1324,13 +1412,55 @@ Module GlobalMaps (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvT split. * apply ind_sorts0. * destruct indices_matter; auto. - eapply type_local_ctx_impl; eauto. - eapply ind_sorts0. - --- eapply X1.(onIndices). + eapply type_local_ctx_impl. eapply ind_sorts0. eauto. + --- apply X1.(onIndices). -- red in onP. red. - eapply All_local_env_impl; tea. + eapply All_local_env_impl; eauto. Qed. + Lemma on_global_decl_impl {cf : checker_flags} Pcmp P Q Σ kn d : + (forall Γ t T, + on_global_env Pcmp P Σ.1 -> + P Σ Γ t T -> Q Σ Γ t T) -> + on_global_env Pcmp P Σ.1 -> + on_global_decl Pcmp P Σ kn d -> on_global_decl Pcmp Q Σ kn d. + Proof. + intros H HP. + cut ((forall (m : module_implementation), on_module_impl Pcmp P Σ m -> on_module_impl Pcmp Q Σ m) + × (forall (p : structure_field), on_structure_field Pcmp P Σ p -> on_structure_field Pcmp Q Σ p) + × (forall (s : structure_body), on_structure_body Pcmp P Σ s -> on_structure_body Pcmp Q Σ s)). + intro md_sf_sb. + destruct d; simpl. + - now eapply on_constant_decl_impl. + - now eapply on_inductive_decl_impl. + - unfold on_module_decl. destruct m as [mi mt]; simpl. + intros [onmip onmtp]. split; now apply md_sf_sb. + - apply md_sf_sb. + - apply (on_mi_sf_sb_mutrect); try now constructor. + -- intros c oncp. constructor. now apply on_constant_decl_impl with (Pcmp := Pcmp) (P := P). + -- intros kn' mind onip. apply on_sfmind with (kn := kn'). now apply on_inductive_decl_impl with (Pcmp := Pcmp) (P := P). + Qed. + + Lemma on_global_env_impl {cf : checker_flags} Pcmp P Q : + (forall Σ Γ t T, + on_global_env Pcmp P Σ.1 -> + on_global_env Pcmp Q Σ.1 -> + P Σ Γ t T -> Q Σ Γ t T) -> + forall Σ, on_global_env Pcmp P Σ -> on_global_env Pcmp Q Σ. + Proof. + intros X Σ [cu IH]. split; auto. + revert cu IH; generalize (universes Σ) as univs, (retroknowledge Σ) as retro, (declarations Σ). clear Σ. + induction g; intros; auto. constructor; auto. + depelim IH. specialize (IHg cu IH). constructor; auto. + pose proof (globenv_decl _ _ _ _ _ _ _ IH o). + destruct o. constructor; auto. + assert (X' := fun Γ t T => X ({| universes := univs; declarations := _ |}, udecl0) Γ t T + (cu, IH) (cu, IHg)); clear X. + rename X' into X. + eapply on_global_decl_impl; tea. + - intros; apply X => //. + - split => //. + Qed. End GlobalMaps. Module Type GlobalMapsSig (T: Term) (E: EnvironmentSig T) (TU : TermUtils T E) (ET: EnvTypingSig T E TU) (C: ConversionSig T E TU ET) (L: LookupSig T E). @@ -1409,41 +1539,35 @@ Module DeclarationTyping (T : Term) (E : EnvironmentSig T) (TU : TermUtils T E) assert (X' := fun Γ t T => X ({| universes := univs; declarations := Σ |}, udecl0) Γ t T (cu, wfΣ) (cu, X0) (cu, IHX0)); clear X. rename X' into X. - clear IHX0. destruct d; simpl. + clear IHX0. + destruct d; simpl. + - destruct c; simpl. destruct cst_body0; simpl in *; now eapply X. - - simpl in *. destruct on_global_decl_d0 as [onI onP onNP]. - constructor; auto. - -- eapply Alli_impl; tea. intros. - refine {| ind_arity_eq := X1.(ind_arity_eq); - ind_cunivs := X1.(ind_cunivs) |}. - --- apply onArity in X1. unfold on_type in *; simpl in *. - now eapply X. - --- pose proof X1.(onConstructors) as X11. red in X11. - eapply All2_impl; eauto. - simpl. intros. destruct X2 as [? ? ? ?]; unshelve econstructor; eauto. - * apply X; eauto. - * clear -X0 X on_cargs0. revert on_cargs0. - generalize (cstr_args x0). - induction c in y |- *; destruct y; simpl; auto; - destruct a as [na [b|] ty]; simpl in *; auto; - split; intuition eauto. - * clear -X0 X on_cindices0. - revert on_cindices0. - generalize (List.rev (lift_context #|cstr_args x0| 0 (ind_indices x))). - generalize (cstr_indices x0). - induction 1; simpl; constructor; auto. - --- simpl; intros. pose (onProjections X1). simpl in *; auto. - --- destruct X1. simpl. unfold check_ind_sorts in *. - destruct Universe.is_prop; auto. - destruct Universe.is_sprop; auto. - split. - * apply ind_sorts0. - * destruct indices_matter; auto. - eapply type_local_ctx_impl; eauto. - eapply ind_sorts0. - --- eapply X1.(onIndices). - -- red in onP. red. - eapply All_local_env_impl; tea. + + - simpl in *. apply on_inductive_decl_impl with (P := P); auto. + unfold on_global_env; auto. + + - set (gex := ({| universes := univs; declarations := Σ; retroknowledge := retro |}, Monomorphic_ctx)). + cut ((forall (m : module_implementation), on_module_impl cumul_gen P gex m -> on_module_impl cumul_gen Q gex m) + × (forall (p: structure_field), on_structure_field cumul_gen P gex p -> on_structure_field cumul_gen Q gex p) + × (forall (s : structure_body), on_structure_body cumul_gen P gex s -> on_structure_body cumul_gen Q gex s)). + intros [Hmi [Hsf Hsb]]. + -- constructor; destruct on_global_decl_d0 as [omip omtp]. + + now apply Hmi. + + now apply Hsb. + -- apply on_mi_sf_sb_mutrect; try now constructor. + + constructor. destruct c; simpl. destruct cst_body0; simpl in *; now eapply X. + + intros kn0 inds0 oi. apply on_sfmind with (kn := kn0). apply on_inductive_decl_impl with (P := P); unfold on_global_env; auto. + + - set (gex := ({| universes := univs; declarations := Σ; retroknowledge := retro |}, Monomorphic_ctx)). + cut ((forall (m : module_implementation), on_module_impl cumul_gen P gex m -> on_module_impl cumul_gen Q gex m) + × (forall (p: structure_field), on_structure_field cumul_gen P gex p -> on_structure_field cumul_gen Q gex p) + × (forall (s : structure_body), on_structure_body cumul_gen P gex s -> on_structure_body cumul_gen Q gex s)). + intros [Hmi [Hsf Hsb]]. + -- destruct on_global_decl_d0; now constructor. + -- apply on_mi_sf_sb_mutrect; try now constructor. + + constructor. destruct c; simpl. destruct cst_body0; simpl in *; now eapply X. + + intros kn0 inds0 oi. apply on_sfmind with (kn := kn0). apply on_inductive_decl_impl with (P := P); unfold on_global_env; auto. Qed. End DeclarationTyping. diff --git a/template-coq/theories/EtaExpand.v b/template-coq/theories/EtaExpand.v index 0af3bac89..8f02c3992 100644 --- a/template-coq/theories/EtaExpand.v +++ b/template-coq/theories/EtaExpand.v @@ -204,10 +204,35 @@ Definition eta_minductive_decl Σ mdecl := ind_universes := mdecl.(ind_universes); ind_variance := mdecl.(ind_variance); |}. +Fixpoint eta_structure_field Σ sf := + match sf with + | sfconst c => sfconst (eta_global_decl Σ c) + | sfmind m => sfmind (eta_minductive_decl Σ m) + | sfmod impl modtype => sfmod (eta_module_impl Σ impl) (eta_structure_body Σ modtype) + | sfmodtype modtype => sfmodtype (eta_structure_body Σ modtype) + end +with eta_module_impl Σ mi := + match mi with + | mi_struct sb => mi_struct (eta_structure_body Σ sb) + | _ => mi + end +with eta_structure_body Σ mt := + match mt with + | sb_nil => sb_nil + | sb_cons kn sf sb => sb_cons kn (eta_structure_field Σ sf) (eta_structure_body Σ sb) +end. + +Definition eta_module_type_decl := eta_structure_body. + +Definition eta_module_decl Σ m := + (eta_module_impl Σ m.1, eta_module_type_decl Σ m.2). + Definition eta_global_declaration (Σ : GlobalEnvMap.t) decl : global_decl := match decl with | ConstantDecl cb => ConstantDecl (eta_global_decl Σ cb) | InductiveDecl idecl => InductiveDecl (eta_minductive_decl Σ idecl) + | ModuleDecl mdecl => ModuleDecl (eta_module_decl Σ mdecl) + | ModuleTypeDecl modtype => ModuleTypeDecl (eta_module_type_decl Σ modtype) end. Definition eta_global_declarations (Σ : GlobalEnvMap.t) (decls : global_declarations) := @@ -405,10 +430,44 @@ Record expanded_minductive_decl Σ mdecl := { expanded_params : expanded_context Σ [] mdecl.(ind_params); expanded_ind_bodies : Forall (expanded_inductive_decl Σ mdecl) mdecl.(ind_bodies) }. +Inductive expanded_structure_field Σ: structure_field -> Prop := + | expanded_sfconst c : expanded_constant_decl Σ c -> expanded_structure_field Σ (sfconst c) + | expanded_sfmind inds : expanded_minductive_decl Σ inds -> expanded_structure_field Σ (sfmind inds) + | expanded_sfmod mi mt: + expanded_module_impl Σ mi -> + expanded_structure_body Σ mt -> + expanded_structure_field Σ (sfmod mi mt) + | expanded_sfmodtype mtd : expanded_structure_body Σ mtd -> expanded_structure_field Σ (sfmodtype mtd) + +with expanded_structure_body Σ : structure_body -> Prop := + | expanded_sb_nil : expanded_structure_body Σ sb_nil + | expanded_sb_cons kn sf tl : + expanded_structure_field Σ sf -> + expanded_structure_body Σ tl -> + expanded_structure_body Σ (sb_cons kn sf tl) + +with expanded_module_impl Σ : module_implementation -> Prop := + | expanded_mi_abstract : expanded_module_impl Σ mi_abstract + | expanded_mi_algebraic kn : expanded_module_impl Σ (mi_algebraic kn) + | expanded_mi_struct sb : expanded_structure_body Σ sb -> expanded_module_impl Σ (mi_struct sb) + | expanded_mi_fullstruct : expanded_module_impl Σ mi_fullstruct. + +Definition expanded_modtype_decl := expanded_structure_body. +Definition expanded_module_decl Σ m := + expanded_module_impl Σ m.1 × expanded_modtype_decl Σ m.2. + +Scheme expanded_sf_ind := Induction for expanded_structure_field Sort Prop +with expanded_sb_ind := Induction for expanded_structure_body Sort Prop +with expanded_mi_ind := Induction for expanded_module_impl Sort Prop. + +Combined Scheme expanded_md_sf_sb_mutind from expanded_mi_ind, expanded_sf_ind, expanded_sb_ind. + Definition expanded_decl Σ d := match d with | Ast.Env.ConstantDecl cb => expanded_constant_decl Σ cb | Ast.Env.InductiveDecl idecl => expanded_minductive_decl Σ idecl + | Ast.Env.ModuleDecl m => expanded_module_decl Σ m + | Ast.Env.ModuleTypeDecl mt => expanded_structure_body Σ mt end. Inductive expanded_global_declarations (univs : ContextSet.t) (retro : Environment.Retroknowledge.t) : forall (Σ : Ast.Env.global_declarations), Prop := @@ -932,7 +991,7 @@ Lemma repr_lookup_constructor {Σg Σ} : forall ind idx r, lookup_constructor Σ ind idx = Some r -> GlobalEnvMap.lookup_constructor Σg ind idx = Some r. Proof. intros hrepr ind idx r. - rewrite /lookup_constructor /lookup_constructor_gen /lookup_inductive /lookup_inductive_gen + rewrite /lookup_constructor /lookup_constructor_gen /lookup_inductive /lookup_inductive_gen /lookup_minductive /lookup_minductive_gen /lookup_env. destruct lookup_global eqn:hl => //. apply hrepr in hl. @@ -1268,6 +1327,11 @@ Proof. move: hl. induction (declarations Σ); cbn => //. destruct a as [kn' []] => /=. + (** TODO: refactor repeated code *) + case: eqb_spec. intros ->. intros [= <- <-] => //. + intros neq. auto. + case: eqb_spec. intros ->. intros [= <- <-] => //. + intros neq. auto. case: eqb_spec. intros ->. intros [= <- <-] => //. intros neq. auto. case: eqb_spec. intros ->. intros [= <- <-] => //. @@ -1297,13 +1361,13 @@ Lemma eta_declared_constructor {Σ : GlobalEnvMap.t} {ind mdecl idecl cdecl} : Proof. rewrite /declared_constructor. intros [[] ?]. - move: H. - rewrite /declared_inductive /declared_inductive_gen /declared_minductive /declared_minductive_gen + move: H. + rewrite /declared_inductive /declared_inductive_gen /declared_minductive /declared_minductive_gen /lookup_env /=. destruct (lookup_global Σ.(declarations) _) eqn:heq => //. move: (eta_lookup_global (inductive_mind ind.1) g heq) => hl. - intros [= ->]. - unfold declared_constructor_gen, declared_inductive_gen, declared_minductive_gen. + intros [= ->]. + unfold declared_constructor_gen, declared_inductive_gen, declared_minductive_gen. rewrite hl; split => //. split => //. rewrite nth_error_map H0 //. rewrite nth_error_map H1 //. @@ -1353,17 +1417,30 @@ Lemma expanded_decl_env_irrel (Σ Σ' : global_env) t : Proof. intros hrepr. unfold expanded_decl. - destruct t => //. - intros []. constructor. - destruct (cst_body c) => //. cbn in *. - now eapply expanded_env_irrel. - intros []. split. - eapply expanded_context_env_irrel; tea. - solve_all. - destruct H. constructor. - solve_all. destruct H; split. - eapply expanded_context_env_irrel; tea. - eapply expanded_env_irrel; tea. + cut ((forall (m : module_implementation), expanded_module_impl Σ m -> expanded_module_impl Σ' m) /\ + (forall (p : structure_field), expanded_structure_field Σ p -> expanded_structure_field Σ' p) /\ + (forall (s : structure_body), expanded_structure_body Σ s -> expanded_structure_body Σ' s)). + intros [Hmd [Hsf Hsb]]. + destruct t => //; auto. + - intros []. constructor. + destruct (cst_body c) => //. cbn in *. + now eapply expanded_env_irrel. + - intros []. split. + eapply expanded_context_env_irrel; tea. + solve_all. + destruct H. constructor. + solve_all. destruct H; split. + eapply expanded_context_env_irrel; tea. + eapply expanded_env_irrel; tea. + - constructor; destruct H; auto. now apply Hsb. + - apply expanded_md_sf_sb_mutind; try now constructor. + -- repeat constructor. destruct e. destruct (cst_body c) => //. cbn in *. now eapply expanded_env_irrel. + -- constructor. split; destruct e; solve_all. + + eapply expanded_context_env_irrel; tea. + + destruct H. constructor. + solve_all. destruct H; split. + eapply expanded_context_env_irrel; tea. + eapply expanded_env_irrel; tea. Qed. Coercion wf_ext_wf : wf_ext >-> wf. @@ -1451,6 +1528,66 @@ Lemma eta_context_length g n ctx : #|eta_context g n ctx| = #|ctx|. Proof. now rewrite /eta_context; len. Qed. #[export] Hint Rewrite @eta_context_length : len. +Lemma eta_expand_constant_decl_expanded {cf : checker_flags} (Σ : global_env_ext) (Σg : global_env_ext_map) c : + repr_decls Σg Σ -> + Typing.wf_ext Σ -> + on_constant_decl (lift_typing typing) Σ c -> + expanded_constant_decl Σ (eta_global_decl Σg c). +Proof. + intros hrepr wf ond. + destruct c as [na body ty rel]; cbn in *. + destruct body. constructor => //; cbn. + apply (eta_expand_expanded (Σ := Σ) [] [] t0 na wf ond). constructor. + apply hrepr. + destruct ond as [s Hs]. constructor => //. +Qed. + +Lemma eta_expand_inductive_expanded {cf : checker_flags} (Σ : global_env_ext) (Σg : global_env_ext_map) kn m : + repr_decls Σg Σ -> + Typing.wf_ext Σ -> + on_inductive cumul_gen (lift_typing typing) Σ kn m -> + expanded_minductive_decl Σ (eta_minductive_decl Σg m). +Proof. + intros hrepr wf ond. + destruct ond as [onI onP onN onV]. + constructor. cbn. + eapply eta_expand_context => //. + solve_all. cbn. eapply All_map, Alli_All; tea => n idecl oni. + constructor. + cbn. solve_all. + pose proof oni.(onConstructors). + red in X. + eapply All2_All_left; tea; cbn => cdecl cunivs onc. + constructor. cbn. len. + pose proof onc.(on_cargs). + eapply eta_expand_context_sorts in X0. now len in X0. exact hrepr. + len. len. + pose proof onc.(on_ctype). destruct X0. + epose proof (eta_expand_expanded (Σ := Σ) _ (repeat None #|ind_bodies m|) _ _ wf t0). + forward H. rewrite -arities_context_length. + clear. induction (arities_context _); constructor; auto. + specialize (H _ hrepr). + now rewrite map_repeat in H. +Qed. + +Lemma eta_expand_modtype_decl_expanded {cf : checker_flags} (Σ : global_env_ext) (Σg : global_env_ext_map) mt : + repr_decls Σg Σ -> + Typing.wf_ext Σ -> + on_structure_body cumul_gen (lift_typing typing) Σ mt -> + expanded_modtype_decl Σ (eta_module_type_decl Σg mt). +Proof. + intros hrepr wf onm. + assert (H_md_sf_sd: (forall (m : module_implementation) (e : on_module_impl cumul_gen (lift_typing typing) Σ m), expanded_module_impl Σ (eta_module_impl Σg m)) × + (forall (p : structure_field) (e : on_structure_field cumul_gen (lift_typing typing) Σ p), expanded_structure_field Σ (eta_structure_field Σg p)) × + (forall (s : structure_body) (e : on_structure_body cumul_gen (lift_typing typing) Σ s), expanded_structure_body Σ (eta_structure_body Σg s))). + { + apply on_mi_sf_sb_mutrect; try now constructor; simpl. + - intros c onc. constructor. now apply eta_expand_constant_decl_expanded. + - intros kn i oni. constructor. now apply eta_expand_inductive_expanded with (kn := kn). + } + destruct onm; now repeat constructor. +Qed. + Lemma eta_expand_global_decl_expanded {cf : checker_flags} (Σ : global_env_ext) (Σg : global_env_ext_map) kn d : repr_decls Σg Σ -> Typing.wf_ext Σ -> @@ -1458,32 +1595,19 @@ Lemma eta_expand_global_decl_expanded {cf : checker_flags} (Σ : global_env_ext) expanded_decl Σ (eta_global_declaration Σg d). Proof. intros hrepr wf ond. + assert (H_md_sf_sd: (forall (m : module_implementation) (e : on_module_impl cumul_gen (lift_typing typing) Σ m), expanded_module_impl Σ (eta_module_impl Σg m)) × + (forall (p : structure_field) (e : on_structure_field cumul_gen (lift_typing typing) Σ p), expanded_structure_field Σ (eta_structure_field Σg p)) × + (forall (s : structure_body) (e : on_structure_body cumul_gen (lift_typing typing) Σ s), expanded_structure_body Σ (eta_structure_body Σg s))). + { + unshelve eapply (on_mi_sf_sb_mutrect cumul_gen (lift_typing typing) Σ); try now constructor; simpl. + - intros. constructor. now apply eta_expand_constant_decl_expanded. + - intros. constructor. now eapply eta_expand_inductive_expanded. + } destruct d; cbn in *. - - unfold on_constant_decl in ond. - destruct c as [na body ty rel]; cbn in *. - destruct body. constructor => //; cbn. - apply (eta_expand_expanded (Σ := Σ) [] [] t0 na wf ond). constructor. - apply hrepr. - destruct ond as [s Hs]. constructor => //. - - destruct ond as [onI onP onN onV]. - constructor. cbn. - eapply eta_expand_context => //. - solve_all. cbn. eapply All_map, Alli_All; tea => n idecl oni. - constructor. - cbn. solve_all. - pose proof oni.(onConstructors). - red in X. - eapply All2_All_left; tea; cbn => cdecl cunivs onc. - constructor. cbn. len. - pose proof onc.(on_cargs). - eapply eta_expand_context_sorts in X0. now len in X0. exact hrepr. - len. len. - pose proof onc.(on_ctype). destruct X0. - epose proof (eta_expand_expanded (Σ := Σ) _ (repeat None #|ind_bodies m|) _ _ wf t0). - forward H. rewrite -arities_context_length. - clear. induction (arities_context _); constructor; auto. - specialize (H _ hrepr). - now rewrite map_repeat in H. + - now apply eta_expand_constant_decl_expanded. + - now apply eta_expand_inductive_expanded with (kn := kn). + - destruct ond. constructor; now apply H_md_sf_sd. + - now apply H_md_sf_sd. Qed. Lemma eta_context_assumptions Σ n Γ : context_assumptions Γ = context_assumptions (eta_context Σ n Γ). @@ -1501,7 +1625,7 @@ Proof. induction Σ; intros ind idx mdecl idecl cdecl. - unfold declared_constructor, declared_inductive, declared_minductive. cbn => [[[]]] //. - - unfold declared_constructor, declared_constructor_gen, declared_inductive, declared_inductive_gen, + - unfold declared_constructor, declared_constructor_gen, declared_inductive, declared_inductive_gen, declared_minductive, declared_minductive_gen. cbn. destruct a as [kn decl]; cbn. case: eqb_spec. diff --git a/template-coq/theories/Pretty.v b/template-coq/theories/Pretty.v index c40e3604a..df4fbda28 100644 --- a/template-coq/theories/Pretty.v +++ b/template-coq/theories/Pretty.v @@ -326,6 +326,47 @@ Module PrintTermTree. (print_recursivity_kind mie.(mind_entry_finite) ^ " " ^ print_list (print_one_ind_entry Σ' with_universes short names mie) (nl ^ "with ") mie.(mind_entry_inds) ^ "." ^ nl). + Definition print_const_decl kn cb with_universes (short: bool) Σ' := + (match cb.(cst_body) with | Some _ => "Definition " | None => "Axiom " end) ^ + string_of_kername kn ^ " : " ^ print_term Σ' with_universes nil true cb.(cst_type) ^ + match cb.(cst_body) with + | Some b => if short then ("..." ^ nl) else (" := " ^ nl ^ print_term Σ' with_universes nil true b ^ "." ^ nl) + | None => "." + end. + + Definition print_assoc_list {A B: Type} (f: A -> B -> t) (sep: t) (l : list (prod A B)) : t := + let fix aux l := match l return t with + | nil => "" + | cons (kn, a) nil => f kn a + | cons (kn, a) l => (f kn a) ^ sep ^ aux l + end in aux l. + + Definition kername_append (kn: kername) (id: ident) := ((MPdot kn.1 kn.2), id). + + Definition print_structure_body (f: kername -> structure_field -> t) sep kn sb := + let fix aux s := match s return t with + | sb_nil => "" + | sb_cons id sf sb_nil => f (kername_append kn id) sf + | sb_cons id sf sb' => f (kername_append kn id) sf ^ sep ^ aux sb' + end in aux sb. + + Fixpoint print_module_decl kn impl modtype_str with_universes (short: bool) (Σ: global_env) {struct impl}:= + let kn_string := string_of_kername kn in match impl with + | mi_abstract => "Module " ^ kn_string ^ "." + | mi_algebraic kn' => "Module " ^ kn_string ^ " := " ^ (string_of_kername kn') ^ "." + | mi_struct sb => + let sb_str := if short then string "..." else print_structure_body (print_structure_field with_universes short Σ) nl kn sb in + "Module " ^ kn_string ^ ". " ^ sb_str ^ " End " ^ kn_string ^ "." + | mi_fullstruct => "Module " ^ kn_string ^ ". " ^ modtype_str ^ " End " ^ kn_string ^ "." + end ^ if short then string "" else "Module Type: " ^ nl ^ modtype_str + with print_structure_field with_universes (short: bool) (Σ: global_env) kn sf {struct sf}: t := + match sf with + | sfconst cb => let Σ' := (Σ, cb.(cst_universes)) in print_const_decl kn cb with_universes short Σ' + | sfmind mib => print_mib Σ with_universes short mib + | sfmod impl modtype => print_module_decl kn impl (print_structure_body (print_structure_field with_universes short Σ) nl kn modtype) with_universes short Σ + | sfmodtype mt => print_structure_body (print_structure_field with_universes short Σ) nl kn mt + end. + Fixpoint print_env_aux with_universes (short : bool) (prefix : nat) (Σ : global_env) (acc : t) : t := match prefix with | 0 => match Σ.(declarations) with [] => acc | _ => ("..." ^ nl ^ acc) end @@ -350,6 +391,13 @@ Module PrintTermTree. else (" := " ^ nl ^ print_term Σ' with_universes nil true b ^ "." ^ nl) | None => "." end ^ acc) + | (kn, ModuleDecl (impl, modtype)) :: Σ => + let Σ := {| Env.universes := univs; declarations := Σ; retroknowledge := retro |} in + let modtype_str := print_structure_body (print_structure_field with_universes short Σ) nl kn modtype in + print_env_aux with_universes short n Σ (print_module_decl kn impl modtype_str with_universes short Σ ^ acc) + | (kn, ModuleTypeDecl mt) :: Σ => + let Σ := {| Env.universes := univs; declarations := Σ; retroknowledge := retro |} in + print_structure_body (print_structure_field with_universes short Σ) nl kn mt end end. diff --git a/template-coq/theories/ReflectAst.v b/template-coq/theories/ReflectAst.v index 01cb872e8..b27cbcd1e 100644 --- a/template-coq/theories/ReflectAst.v +++ b/template-coq/theories/ReflectAst.v @@ -230,10 +230,79 @@ Proof. unfold eqb_mutual_inductive_body; finish_reflect. Defined. +Fixpoint eqb_structure_field (sf sf': structure_field) {struct sf}:= + match sf, sf' with + | sfconst c, sfconst c' => c ==? c' + | sfmind m, sfmind m' => m ==? m' + | sfmod mi mt, sfmod mi' mt' => eqb_module_impl mi mi' && eqb_module_type_decl mt mt' + | sfmodtype mt, sfmodtype mt' => eqb_module_type_decl mt mt' + | _, _ => false + end +with eqb_module_impl (mi mi': module_implementation) {struct mi}:= + match mi, mi' with + | mi_abstract, mi_abstract | mi_fullstruct, mi_fullstruct => true + | mi_algebraic kn, mi_algebraic kn' => kn ==? kn' + | mi_struct mt, mi_struct mt' => eqb_module_type_decl mt mt' + | _, _ => false + end +with eqb_module_type_decl (mt mt': module_type_decl) {struct mt} := + match mt, mt' with + | sb_nil, sb_nil => true + | sb_cons k sf sb, sb_cons k' sf' sb' => + k ==? k' && eqb_structure_field sf sf' && eqb_module_type_decl sb sb' + | _, _ => false + end. + +Lemma reflect_sf_mi_sb: +(forall f f': structure_field, reflectProp (f = f') (eqb_structure_field f f')) × +(forall m m': module_implementation, reflectProp (m = m') (eqb_module_impl m m')) × +(forall s s': structure_body, reflectProp (s = s') (eqb_module_type_decl s s')). +Proof. + apply sf_mi_sb_mutind; intros. + - destruct f'; simpl; try now constructor. destruct (eqb_spec c c0); now constructor. + - destruct f'; simpl; try now constructor. destruct (eqb_spec m m0); now constructor. + - destruct f'; simpl; try now constructor. + destruct (H m0), (H0 s0); simpl; now constructor. + - destruct f'; simpl; try now constructor. + destruct (H s0); simpl; now constructor. + - destruct m'; simpl; now constructor. + - destruct m'; simpl; try now constructor. + destruct (eqb_spec k k0); now constructor. + - destruct m'; simpl; try now constructor. + destruct (H s0); simpl; now constructor. + - destruct m'; simpl; now constructor. + - destruct s'; simpl; now constructor. + - destruct s'; simpl; try now constructor. + destruct (eqb_spec i i0), (H s1), (H0 s'); simpl; now constructor. +Qed. + +#[global] Instance reflect_structure_field : ReflectEq structure_field := +{ eqb := eqb_structure_field ; eqb_spec := reflect_sf_mi_sb.1 }. + +#[global] Instance reflect_module_impl : ReflectEq module_implementation := +{ eqb := eqb_module_impl ; eqb_spec := reflect_sf_mi_sb.2.1 }. + +#[global] Instance reflect_structure_body : ReflectEq structure_body := +{ eqb := eqb_module_type_decl ; eqb_spec := reflect_sf_mi_sb.2.2 }. + +#[global] Instance reflect_module_type : ReflectEq module_type_decl := +{ eqb := eqb_module_type_decl ; eqb_spec := reflect_sf_mi_sb.2.2 }. + +Definition eqb_module_decl (m m': module_decl) := (m.1 ==? m'.1) && (m.2 ==? m'.2). + +#[global] Instance reflect_module_decl : ReflectEq module_decl. +Proof. + refine {| eqb := eqb_module_decl |}. + intros [] []. + unfold eqb_module_decl; cbn -[eqb]; finish_reflect. +Qed. + Definition eqb_global_decl x y := match x, y with | ConstantDecl cst, ConstantDecl cst' => eqb cst cst' | InductiveDecl mib, InductiveDecl mib' => eqb mib mib' + | ModuleDecl m, ModuleDecl m' => eqb m m' + | ModuleTypeDecl mt, ModuleTypeDecl mt' => eqb mt mt' | _, _ => false end. diff --git a/template-coq/theories/TemplateCheckWf.v b/template-coq/theories/TemplateCheckWf.v index 54de0453e..315696117 100644 --- a/template-coq/theories/TemplateCheckWf.v +++ b/template-coq/theories/TemplateCheckWf.v @@ -10,6 +10,37 @@ Open Scope bs_scope. Definition eta_expand p := EtaExpand.eta_expand_program p. +Definition check_const_decl_def kn const_decl : TemplateMonad unit := + match const_decl.(cst_body) with + | Some body => + tmMsg ("Unquoting eta-expanded " ++ string_of_kername kn)%bs ;; + tmUnquote body ;; + tmMsg ("Succeeded") + | None => ret tt + end. + +Fixpoint check_mod_impl_def kn impl {struct impl}:= + match impl with + | mi_struct sb => check_structure_body_def kn sb ;; ret tt + | _ => ret tt + end +with check_structure_field_def kn id sf := + let kn' := ((MPdot kn.1 kn.2), id) in + match sf with + | sfconst cb => check_const_decl_def kn' cb + | sfmind _ => ret tt + | sfmod impl modtype => check_mod_impl_def kn' impl ;; check_structure_body_def kn' modtype + | sfmodtype sb => check_structure_body_def kn' sb + end +with check_structure_body_def kn sb := + match sb with + | sb_nil => ret tt + | sb_cons id sf sb' => check_structure_field_def kn id sf ;; check_structure_body_def kn sb' + end. + +Definition check_modtype_def := check_structure_body_def. +Definition check_mod_decl_def kn m := check_mod_impl_def kn m.1 ;; check_modtype_def kn m.2. + Definition check_def (d : kername × global_decl) : TemplateMonad unit := match d.2 with | ConstantDecl cb => @@ -21,6 +52,8 @@ Definition check_def (d : kername × global_decl) : TemplateMonad unit := | None => ret tt end | InductiveDecl idecl => ret tt + | ModuleDecl m => check_mod_decl_def d.1 m + | ModuleTypeDecl sb => check_modtype_def d.1 sb end. Definition is_nil {A} (l : list A) := @@ -51,11 +84,37 @@ Fixpoint wfterm (t : term) : bool := From Coq Require Import ssrbool. +Definition wf_constant_body cb := wfterm cb.(cst_type) && option_default wfterm cb.(cst_body) true. + +Fixpoint wf_module_impl impl := + match impl with + | mi_struct sb => wf_structure_body sb + | _ => true + end +with wf_structure_field sf := + match sf with + | sfconst cb => wf_constant_body cb + | sfmind _ => true + | sfmod impl modtype => wf_module_impl impl && wf_structure_body modtype + | sfmodtype mt => wf_structure_body mt + end +with wf_structure_body sb := + match sb with + | sb_nil => true + | sb_cons kn sf sb' => wf_structure_field sf && wf_structure_body sb' + end. + +Definition wf_module_type := wf_structure_body. +Definition wf_module_decl m := wf_module_impl m.1 && wf_structure_body m.2. + Definition wf_global_decl d := match d with - | ConstantDecl cb => wfterm cb.(cst_type) && option_default wfterm cb.(cst_body) true + | ConstantDecl cb => wf_constant_body cb | InductiveDecl idecl => true + | ModuleDecl m => wf_module_decl m + | ModuleTypeDecl modtype => wf_module_type modtype end. + Definition wf_global_declarations : global_declarations -> bool := forallb (wf_global_decl ∘ snd). Definition wf_global_env (g : global_env) := wf_global_declarations g.(declarations). Definition wf_program p := wf_global_env p.1 && wfterm p.2. diff --git a/template-coq/theories/TemplateEnvMap.v b/template-coq/theories/TemplateEnvMap.v index 2ee0cf5c6..792f9aebc 100644 --- a/template-coq/theories/TemplateEnvMap.v +++ b/template-coq/theories/TemplateEnvMap.v @@ -15,8 +15,8 @@ Qed. Local Coercion declarations : global_env >-> global_declarations. Module GlobalEnvMap. - Record t := - { env :> global_env; + Record t := + { env :> global_env; map : EnvMap.t global_decl; repr : EnvMap.repr env.(declarations) map; wf : EnvMap.fresh_globals env.(declarations) }. @@ -24,16 +24,17 @@ Module GlobalEnvMap. Definition lookup_env Σ kn := EnvMap.lookup kn Σ.(map). Lemma lookup_env_spec (Σ : t) kn : lookup_env Σ kn = Env.lookup_env Σ kn. - Proof. + Proof. rewrite /lookup_env /Env.lookup_env. apply (EnvMap.lookup_spec Σ.(env).(declarations)); apply Σ. Qed. Definition lookup_minductive Σ kn : option mutual_inductive_body := - decl <- lookup_env Σ kn;; + decl <- lookup_env Σ kn;; match decl with | ConstantDecl _ => None | InductiveDecl mdecl => ret mdecl + | ModuleDecl _ | ModuleTypeDecl _ => None end. Lemma lookup_minductive_spec Σ kn : lookup_minductive Σ kn = Ast.lookup_minductive Σ kn. @@ -46,7 +47,7 @@ Module GlobalEnvMap. mdecl <- lookup_minductive Σ (inductive_mind kn) ;; idecl <- nth_error mdecl.(ind_bodies) (inductive_ind kn) ;; ret (mdecl, idecl). - + Lemma lookup_inductive_spec Σ kn : lookup_inductive Σ kn = Ast.lookup_inductive Σ kn. Proof. rewrite /lookup_inductive /Ast.lookup_inductive. @@ -56,7 +57,7 @@ Module GlobalEnvMap. Definition lookup_constructor Σ kn c : option (mutual_inductive_body * one_inductive_body * constructor_body) := '(mdecl, idecl) <- lookup_inductive Σ kn ;; cdecl <- nth_error idecl.(ind_ctors) c ;; - ret (mdecl, idecl, cdecl). + ret (mdecl, idecl, cdecl). Lemma lookup_constructor_spec Σ kn : lookup_constructor Σ kn = Ast.lookup_constructor Σ kn. Proof. diff --git a/template-coq/theories/Typing.v b/template-coq/theories/Typing.v index 88fb52508..29ba0a59a 100644 --- a/template-coq/theories/Typing.v +++ b/template-coq/theories/Typing.v @@ -1353,6 +1353,117 @@ Proof. apply (IH ((Σ', udecl); (wfΣ; _; _; _; Hs))). constructor 1. simpl. subst Σ' Σg; cbn; lia. + + cut ((forall (m : module_implementation), on_module_impl cumul_gen (lift_typing typing) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) m + -> on_module_impl cumul_gen (lift_typing P) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) m) + × (forall (p : structure_field), on_structure_field cumul_gen (lift_typing typing) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) p + -> on_structure_field cumul_gen (lift_typing P) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) p) + × (forall (s : structure_body), on_structure_body cumul_gen (lift_typing typing) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) s + -> on_structure_body cumul_gen (lift_typing P) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) s)). + * intros md_sf_sb. constructor; apply md_sf_sb; apply Xg. + (** start of mutual induction *) + * apply on_mi_sf_sb_mutrect; try now constructor. + -- constructor. destruct c; simpl in *. + destruct cst_body0; apply lift_typing_impl with (1 := o0); intros ? Hs. + all: specialize (IH ((Σ', udecl); wfΣ; _; _; _; Hs)). + all: forward IH; [constructor 1; simpl; subst Σ' Σg; cbn; lia|]. + all: apply IH. + -- intros kn0 inds o0. + apply on_sfmind with (kn:=kn0). destruct o0 as [onI onP onnp]; constructor; eauto. + --- unshelve eset (IH' := fun p => IH ((Σ', udecl); wfΣ; p) _). + constructor. cbn; subst Σ' Σg; lia. clearbody IH'. cbn in IH'. + clear IH; rename IH' into IH. + eapply Alli_impl; eauto. cbn in IH. clear onI onP onnp Xg. intros n x Xg. + refine {| ind_arity_eq := Xg.(ind_arity_eq); + ind_cunivs := Xg.(ind_cunivs) |}. + ** apply onArity in Xg. + apply lift_typing_impl with (1 := Xg); intros ? Hs. + apply (IH (_; _; _; Hs)). + ** pose proof Xg.(onConstructors) as Xg'. + eapply All2_impl; eauto. intros. + destruct X13 as [cass tyeq onctyp oncargs oncind]. + unshelve econstructor; eauto. + { apply lift_typing_impl with (1 := onctyp); intros ? Hs. + apply (IH (_; _; _; Hs)). } + { apply sorts_local_ctx_impl with (1 := oncargs); intros Γ' t' T' HT'. + apply lift_typing_impl with (1 := HT'); intros ? Hs. + apply (IH (_; _; _; Hs)). } + { clear -IH oncind. + revert oncind. + generalize (List.rev (lift_context #|cstr_args x0| 0 (ind_indices x))). + generalize (cstr_indices x0). induction 1; constructor; auto. + do 2 red in t0 |- *. + apply (IH (_; (_; (_; t0)))). } + ** pose proof (onProjections Xg); auto. + ** destruct Xg. simpl. unfold check_ind_sorts in *. + destruct Universe.is_prop; auto. + destruct Universe.is_sprop; auto. + split. apply ind_sorts0. destruct indices_matter; auto. + eapply type_local_ctx_impl. eapply ind_sorts0. intros ??? HT. + apply lift_typing_impl with (1 := HT); intros ? Hs. + apply (IH (_; _; _; Hs)). + ** apply (onIndices Xg). + --- red in onP |- *. + apply All_local_env_impl with (1 := onP); intros ??? HT. + apply lift_typing_impl with (1 := HT); intros ? Hs. + apply (IH ((Σ', udecl); (wfΣ; _; _; _; Hs))). + constructor 1. simpl. subst Σ' Σg; cbn; lia. + + + cut ((forall (m : module_implementation), on_module_impl cumul_gen (lift_typing typing) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) m + -> on_module_impl cumul_gen (lift_typing P) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) m) + × (forall (p : structure_field), on_structure_field cumul_gen (lift_typing typing) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) p + -> on_structure_field cumul_gen (lift_typing P) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) p) + × (forall (s : structure_body), on_structure_body cumul_gen (lift_typing typing) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) s + -> on_structure_body cumul_gen (lift_typing P) ({| universes := univs; declarations := Σ; retroknowledge := retroknowledge0 |}, Monomorphic_ctx) s)). + * intros md_sf_sb. apply md_sf_sb; apply Xg. + (** start of mutual induction *) + * apply on_mi_sf_sb_mutrect; try now constructor. + -- intros. apply on_sfconst. + destruct c; simpl in *. + destruct cst_body0; apply lift_typing_impl with (1 := o0); intros ? Hs. + all: specialize (IH ((Σ', udecl); wfΣ; _; _; _; Hs)). + all: forward IH; [constructor 1; simpl; subst Σ' Σg; cbn; lia|]. + all: apply IH. + -- intros kn0 inds o0. apply on_sfmind with (kn:=kn0). + destruct o0 as [onI onP onnp]; constructor; eauto. + --- unshelve eset (IH' := fun p => IH ((Σ', udecl); wfΣ; p) _). + constructor. cbn; subst Σ' Σg; lia. clearbody IH'. cbn in IH'. + clear IH; rename IH' into IH. + eapply Alli_impl; eauto. cbn in IH. clear onI onP onnp Xg. intros n x Xg. + refine {| ind_arity_eq := Xg.(ind_arity_eq); + ind_cunivs := Xg.(ind_cunivs) |}. + ** apply onArity in Xg. + apply lift_typing_impl with (1 := Xg); intros ? Hs. + apply (IH (_; _; _; Hs)). + ** pose proof Xg.(onConstructors) as Xg'. + eapply All2_impl; eauto. intros. + destruct X13 as [cass tyeq onctyp oncargs oncind]. + unshelve econstructor; eauto. + { apply lift_typing_impl with (1 := onctyp); intros ? Hs. + apply (IH (_; _; _; Hs)). } + { apply sorts_local_ctx_impl with (1 := oncargs); intros Γ' t' T' HT'. + apply lift_typing_impl with (1 := HT'); intros ? Hs. + apply (IH (_; _; _; Hs)). } + { clear -IH oncind. + revert oncind. + generalize (List.rev (lift_context #|cstr_args x0| 0 (ind_indices x))). + generalize (cstr_indices x0). induction 1; constructor; auto. + do 2 red in t0 |- *. + apply (IH (_; (_; (_; t0)))). } + ** pose proof (onProjections Xg); auto. + ** destruct Xg. simpl. unfold check_ind_sorts in *. + destruct Universe.is_prop; auto. + destruct Universe.is_sprop; auto. + split. apply ind_sorts0. destruct indices_matter; auto. + eapply type_local_ctx_impl. eapply ind_sorts0. intros ??? HT. + apply lift_typing_impl with (1 := HT); intros ? Hs. + apply (IH (_; _; _; Hs)). + ** apply (onIndices Xg). + --- red in onP |- *. + apply All_local_env_impl with (1 := onP); intros ??? HT. + apply lift_typing_impl with (1 := HT); intros ? Hs. + apply (IH ((Σ', udecl); (wfΣ; _; _; _; Hs))). + constructor 1. simpl. subst Σ' Σg; cbn; lia. + - assert (forall Γ t T (Hty : Σ ;;; Γ |- t : T), typing_size Hty < typing_size H -> on_global_env cumul_gen (lift_typing P) Σ.1 * P Σ Γ t T). diff --git a/template-coq/theories/TypingWf.v b/template-coq/theories/TypingWf.v index 47660f3b5..e128345d2 100644 --- a/template-coq/theories/TypingWf.v +++ b/template-coq/theories/TypingWf.v @@ -41,58 +41,12 @@ Lemma on_global_decl_impl `{checker_flags} Σ P Q kn d : (forall Σ Γ t T, on_global_env cumul_gen P Σ.1 -> P Σ Γ t T -> Q Σ Γ t T) -> on_global_env cumul_gen P Σ.1 -> on_global_decl cumul_gen P Σ kn d -> on_global_decl cumul_gen Q Σ kn d. -Proof. - unfold on_global_env. - intros X X0 o. - destruct d; simpl. - - destruct c; simpl. destruct cst_body0; simpl in *. - red in o |- *. simpl in *. now eapply X. - red in o |- *. simpl in *. now eapply X. - - simpl in *. - destruct o as [onI onP onNP]. - constructor; auto. - -- eapply Alli_impl. exact onI. eauto. intros. - - refine {| ind_arity_eq := X1.(ind_arity_eq); - ind_cunivs := X1.(ind_cunivs) |}. - --- apply onArity in X1. unfold on_type in *; simpl in *. - now eapply X. - --- pose proof X1.(onConstructors) as X11. red in X11. - eapply All2_impl; eauto. - simpl. intros. destruct X2 as [? ? ? ?]; unshelve econstructor; eauto. - * apply X; eauto. - * clear -X0 X on_cargs. revert on_cargs. - generalize (cstr_args x0), y. - induction c; destruct y0; simpl; auto; - destruct a as [na [b|] ty]; simpl in *; auto; - split; intuition eauto. - * clear -X0 X on_cindices. - revert on_cindices. - generalize (List.rev (lift_context #|cstr_args x0| 0 (ind_indices x))). - generalize (cstr_indices x0). - induction 1; simpl; constructor; auto. - --- simpl; intros. apply (onProjections X1). - --- destruct X1. simpl. unfold check_ind_sorts in *. - destruct Universe.is_prop; auto. - destruct Universe.is_sprop; auto. - split. apply ind_sorts. destruct indices_matter; auto. - eapply type_local_ctx_impl. eapply ind_sorts. auto. - --- apply (onIndices X1). - -- red in onP. red. - eapply All_local_env_impl. eauto. - intros. now apply X. -Qed. +Proof. intros; now eapply (on_global_decl_impl cumul_gen P). Qed. Lemma on_global_env_impl `{checker_flags} Σ P Q : (forall Σ Γ t T, on_global_env cumul_gen P Σ.1 -> P Σ Γ t T -> Q Σ Γ t T) -> on_global_env cumul_gen P Σ -> on_global_env cumul_gen Q Σ. -Proof. - destruct Σ as [univs Σ]; cbn. - intros X [cu X0]; split => /= //. cbn in *. - induction X0; try destruct o; constructor; auto; constructor; eauto. - clear IHX0. - eapply on_global_decl_impl; tea. split => //. -Qed. +Proof. intros; now eapply (on_global_env_impl cumul_gen P). Qed. Lemma All_local_env_wf_decl_inv Σ (a : context_decl) (Γ : list context_decl) (X : All_local_env (wf_decl_pred Σ) (a :: Γ)) : diff --git a/template-coq/theories/Universes.v b/template-coq/theories/Universes.v index 7fc5294cf..b0fe42b4e 100644 --- a/template-coq/theories/Universes.v +++ b/template-coq/theories/Universes.v @@ -125,7 +125,7 @@ Module Level. | Level.Var n1, Level.Var n2 => ReflectEq.eqb n1 n2 | _, _ => false end. - + #[global, program] Instance reflect_level : ReflectEq Level.t := { eqb := eq_level }. @@ -139,7 +139,7 @@ Module Level. - destruct (ReflectEq.eqb_spec n n0) ; nodec. constructor. subst. reflexivity. Defined. - + Global Instance eqb_refl : @Reflexive Level.t eqb. Proof. intros x. apply ReflectEq.eqb_refl. diff --git a/translations/translation_utils.v b/translations/translation_utils.v index bac74b33f..b9f7f3a2b 100644 --- a/translations/translation_utils.v +++ b/translations/translation_utils.v @@ -372,5 +372,8 @@ Definition TranslateRec {tsl : Translation} (ΣE : tsl_context) {A} (t : A) := ret (Σ', E') end end + (** FIXME:*) + | ModuleDecl _ => tmPrint "Module" ;; ret ΣE + | ModuleTypeDecl _ => tmPrint "Module Type" ;; ret ΣE end) (fst p).(declarations) ΣE.