Replace all uses of todo and Admitted by axioms (MetaCoq#717)

* remove all todos, all Admitteds and add a checktodos make target

* Squash the axioms to avoid introducing useless dependencies in extracted code

Co-authored-by: Matthieu Sozeau <[email protected]>

INSTALL.md

@@ -72,12 +72,12 @@ To setup a fresh `opam` installation, you might want to create a
 one yet. You need to use **opam 2** to obtain the right version of
 `Equations`.
 
-    # opam switch create coq.8.14 4.07.1
+    # opam switch create coq.8.16 --packages=ocaml-variants.4.13.1+options,ocaml-option-flambda
     # eval $(opam env)
 
-This creates the `coq.8.14` switch which initially contains only the
-basic `OCaml` `4.07.1` compiler, and puts you in the right environment
-(check with `ocamlc -v`).
+This creates the `coq.8.16` switch which initially contains only the
+basic `OCaml` `4.13.1` compiler with the `flambda` option enabled,
+and puts you in the right environment (check with `ocamlc -v`).
 
 Once in the right switch, you can install `Coq` and the `Equations` package using:
 

Makefile

@@ -119,7 +119,7 @@ ci-local-noclean:
 	./configure.sh local
 	$(MAKE) all test-suite TIMED=pretty-timed
 
-ci-local: ci-local-noclean
+ci-local: ci-local-noclean 
 	$(MAKE) clean
 
 ci-quick:
@@ -130,3 +130,6 @@ ci-opam:
 # Use -v so that regular output is produced
 	opam install -v -y .
 	opam remove -y coq-metacoq coq-metacoq-template
+
+checktodos:
+	sh checktodos.sh

README.md

@@ -54,9 +54,14 @@ Template-Coq with additional features. Each extension is in dedicated folder.
 
 Template-Coq is a quoting library for [Coq](http://coq.inria.fr). It
 takes `Coq` terms and constructs a representation of their syntax tree as
-a `Coq` inductive data type. The representation is based on the kernel's
+an inductive data type. The representation is based on the kernel's
 term representation.
 
+After importing `MetaCoq.Template.Loader` there are commands `MetaCoq Test Quote t.`, 
+`MetaCoq Quote Definition name := (t).` and `MetaCoq Quote Recursively Definition name := (t).` as 
+well as a tactic `quote_term t k`,
+where in all cases `t` is a term and `k` a continuation tactic.
+
 In addition to this representation of terms, Template Coq includes:
 
 - Reification of the environment structures, for constant and inductive
@@ -66,9 +71,9 @@ In addition to this representation of terms, Template Coq includes:
 
 - A monad for manipulating global declarations, calling the type
   checker, and inserting them in the global environment, in
-  the style of MTac.
+  the style of MTac. Monadic programs `p : TemplateMonad A` can be run using `MetaCoq Run p`.
 
-- A formalisation of the expected typing rules reflecting the ones of Coq
+- A formalisation of the typing rules reflecting the ones of Coq, not covering eta-expansion and template polymorphism.
 
 ### [PCUIC](https://github.com/MetaCoq/metacoq/tree/coq-8.11/pcuic)
 
@@ -92,6 +97,13 @@ calculus has proofs of standard metatheoretical results:
   that singleton elimination (from Prop to Type) is only allowed
   on singleton inductives in Prop.
 
+- Canonicity: The weak head normal form of erms of inductive type is a constructor application.
+
+- Consistency under the assumption of strong normalization
+
+- Weak call-by-value standardization: Normal forms of terms of first-order inductive type
+can be found via weak call-by-value evaluation.
+
 ### [Safe Checker](https://github.com/MetaCoq/metacoq/tree/coq-8.16/safechecker)
 
 Implementation of a fuel-free and verified reduction machine, conversion
@@ -108,12 +120,11 @@ type-checker, one can use:
 
     MetaCoq CoqCheck <term>
 
-
 ### [Erasure](https://github.com/MetaCoq/metacoq/tree/coq-8.16/erasure)
 
 An erasure procedure to untyped lambda-calculus accomplishing the
-same as the Extraction plugin of Coq. The extracted safe erasure is
-available in Coq through a new vernacular command:
+same as the type and proof erasure phase of the Extraction plugin of Coq.
+The extracted safe erasure is available in Coq through a new vernacular command:
 
     MetaCoq Erase <term>
 
@@ -138,8 +149,6 @@ Examples of translations built on top of this:
   and [test-suite/safechecker_test.v](https://github.com/MetaCoq/metacoq/tree/coq-8.16/test-suite/safechecker_test.v) show example
   uses (and current limitations of) the verified checker and erasure.
 
-
-
 ## Papers
 
 - ["Coq Coq Correct! Verification of Type Checking and Erasure for Coq, in Coq"](https://metacoq.github.io/coqcoqcorrect)

RELEASING.md

@@ -1 +1,2 @@
 - Change the "version:" fields in opam files.
+

checktodos.sh

@@ -0,0 +1,21 @@
+#!/bin/sh
+
+if [[ $(git grep -c todo | grep theories) = template-coq/theories/utils/MCUtils.v:3 ]]
+then
+    echo "No todos found"
+    if [[ $(git grep -c Admitted | grep theories) = "" ]]
+    then
+        echo "No Admitted results found"
+        exit 0
+    else
+        echo "Found Admitted results:"
+        git grep -c Admitted | grep theories
+        exit 1
+    fi
+else
+    echo "Found todos:"
+    git grep -c todo | grep theories
+    exit 1
+fi
+endef
+

erasure/theories/EArities.v

@@ -22,7 +22,7 @@ Local Existing Instance extraction_checker_flags.
 
 Implicit Types (cf : checker_flags) (Σ : global_env_ext).
 
-(* todo move *)
+(* TODO move *)
 #[global] Existing Instance extends_refl.
 
 Lemma isErasable_Proof Σ Γ t :

erasure/theories/Erasure.v

@@ -108,20 +108,32 @@ Definition run_erase_program_fast {guard : abstract_guard_impl} := run erasure_p
 
 Local Open Scope string_scope.
 
+Axiom fake_guard_impl_properties : 
+forall (fix_cofix: PCUICTyping.FixCoFix)
+       (Σ: PCUICAst.PCUICEnvironment.global_env_ext)
+       (Γ: PCUICAst.PCUICEnvironment.context)
+       (mfix: BasicAst.mfixpoint PCUICAst.term),
+PCUICTyping.guard fix_cofix Σ Γ mfix <-> fake_guard_impl fix_cofix Σ Γ mfix.
+
+
 Global Program Instance fake_guard_impl : abstract_guard_impl :=
 {| guard_impl := fake_guard_impl |}.
-Next Obligation. Admitted.  
+Next Obligation. apply fake_guard_impl_properties. Qed.
 
 (** This uses the retyping-based erasure and assumes that the global environment and term 
   are welltyped (for speed). As such this should only be used for testing, or when we know that 
   the environment is wellformed and the term well-typed (e.g. when it comes directly from a 
   Coq definition). *)
+
+
+Axiom assume_that_we_only_erase_on_welltyped_programs :
+  forall (p : Ast.Env.program), squash (TemplateProgram.wt_template_program p).
 Definition erase_and_print_template_program {cf : checker_flags} (p : Ast.Env.program)
   : string :=
-  let p' := run_erase_program p (sq (todo "assuming quoted environment and term are well-typed")) in
+  let p' := run_erase_program p (assume_that_we_only_erase_on_welltyped_programs p) in
   time "Pretty printing" EPretty.print_program p'.
 
 Program Definition erase_fast_and_print_template_program {cf : checker_flags} (p : Ast.Env.program)
   : string :=
-  let p' := run_erase_program_fast p (sq (todo "wf_env and welltyped term")) in
+  let p' := run_erase_program_fast p (assume_that_we_only_erase_on_welltyped_programs p) in
   time "pretty-printing" EPretty.print_program p'.

pcuic/theories/PCUICEquality.v

@@ -1291,7 +1291,7 @@ Proof.
   eapply eq_term_upto_univ_trans; exact _.
 Qed.
 
-(* todo: rename *)
+(* TODO: rename *)
 (* Definition nleq_term t t' := *)
 (*   eqb_term_upto_univ eqb eqb t t'. *)
 

pcuic/theories/PCUICInversion.v

@@ -6,7 +6,7 @@ From MetaCoq.PCUIC Require Import PCUICAst PCUICCases PCUICLiftSubst PCUICUnivSu
      PCUICOnFreeVars PCUICClosedTyp PCUICWellScopedCumulativity.
 
 Require Import Equations.Prop.DepElim.
-(* todo: make wf arguments implicit *)
+(* TODO: make wf arguments implicit *)
 Section Inversion.
 
   Context {cf : checker_flags}.

pcuic/theories/PCUICSafeLemmata.v

@@ -346,7 +346,7 @@ Section Lemmata.
     destruct h; depelim wf; simpl in *.
     all: destruct l; econstructor; eauto.
   Qed.
-  (* todo: rename alpha_eq *)
+  (* TODO: rename alpha_eq *)
   Lemma compare_decls_conv Γ Γ' :
     eq_context_upto_names Γ Γ' ->
     conv_context cumulAlgo_gen Σ Γ Γ'.

pcuic/theories/utils/PCUICAstUtils.v

@@ -205,7 +205,7 @@ Fixpoint remove_arity (n : nat) (t : term) : term :=
   | O => t
   | S n => match t with
           | tProd _ _ B => remove_arity n B
-          | _ => t (* todo *)
+          | _ => t (* TODO *)
           end
   end.
 
@@ -282,7 +282,7 @@ Fixpoint decompose_prod_n_assum (Γ : context) n (t : term) : option (context *
     end
   end.
 
-(* todo move *)
+(* TODO move *)
 Lemma it_mkLambda_or_LetIn_app l l' t :
   it_mkLambda_or_LetIn (l ++ l') t = it_mkLambda_or_LetIn l' (it_mkLambda_or_LetIn l t).
 Proof. induction l in l', t |- *; simpl; auto. Qed.
@@ -402,7 +402,7 @@ Ltac merge_All :=
 #[global]
 Hint Rewrite @map_def_id @map_id : map.
 
-(* todo move *)
+(* TODO move *)
 Ltac close_All :=
   match goal with
   | H : Forall _ _ |- Forall _ _ => apply (Forall_impl H); clear H; simpl

safechecker/theories/Extraction.v

@@ -37,12 +37,19 @@ Extraction Inline Equations.Prop.Logic.True_rect_dep Equations.Prop.Logic.False_
 Extraction Inline PCUICPrimitive.prim_val_reflect_eq.
 
 Cd "src".
+Axiom fake_abstract_guard_impl_properties:
+  forall (fix_cofix : PCUICTyping.FixCoFix)
+    (Σ : PCUICAst.PCUICEnvironment.global_env_ext)
+    (Γ : PCUICAst.PCUICEnvironment.context)
+    (mfix : BasicAst.mfixpoint PCUICAst.term),
+    PCUICTyping.guard fix_cofix Σ Γ mfix <->
+      PCUICWfEnvImpl.fake_guard_impl fix_cofix Σ Γ mfix.
 
 #[local,program] Instance fake_abstract_guard_impl : PCUICWfEnvImpl.abstract_guard_impl := 
   {
     guard_impl := PCUICWfEnvImpl.fake_guard_impl
   }.
-Next Obligation. Admitted. 
+Next Obligation. eapply fake_abstract_guard_impl_properties. Qed.
 
 Definition infer_and_print_template_program_with_guard {cf} {nor} := 
   @SafeTemplateChecker.infer_and_print_template_program cf nor fake_abstract_guard_impl.

safechecker/theories/PCUICEqualityDec.v

@@ -13,7 +13,7 @@ Local Set Keyed Unification.
 
 Set Default Goal Selector "!".
 
-(*todo move*)
+(* TODO move*)
 
 Lemma consistent_instance_wf_universe `{checker_flags} Σ uctx u :
   consistent_instance_ext Σ uctx u ->

safechecker/theories/PCUICSafeConversion.v

@@ -5850,13 +5850,13 @@ match
              (LevelSet.add Level.lzero LevelSet.empty, ConstraintSet.empty);
            declarations := []
          |}, Monomorphic_ctx);
-      referenced_impl_ext_wf := todo "foo"
+      referenced_impl_ext_wf := TODO "foo"
     |} [] Cumul (tSort (Universe.lType (Universe.make' (Level.lzero, 0))))
-    (todo "") (tSort (Universe.lType (Universe.make' (Level.lzero, 0))))
-    (todo "")
+    (TODO "") (tSort (Universe.lType (Universe.make' (Level.lzero, 0))))
+    (TODO "")
 with
 | ConvSuccess => "success"
-| ConvError _ => todo "foo"
+| ConvError _ => TODO "foo"
 end = "success".
 Proof.
   lazy. reflexivity.

safechecker/theories/PCUICTypeChecker.v

@@ -1769,7 +1769,7 @@ Section Typecheck.
   Qed.
 
   Next Obligation.
-    (*todo: factor*)
+    (*TODO: factor*)
     cbn in *. pose proof (heΣ _ wfΣ) as [heΣ]. specialize_Σ wfΣ ; sq. 
     apply eqb_eq in i. subst I.
     eapply eqb_eq in i0.

template-coq/theories/AstUtils.v

@@ -192,7 +192,7 @@ Fixpoint remove_arity (n : nat) (t : term) : term :=
   | O => t
   | S n => match t with
           | tProd _ _ B => remove_arity n B
-          | _ => t (* todo *)
+          | _ => t (* TODO *)
           end
   end.
 

template-coq/theories/Checker.v

@@ -614,25 +614,6 @@ Definition check_conv `{checker_flags} {F:Fuel} := check_conv_gen Conv.
 Definition is_graph_of_global_env_ext `{checker_flags} Σ G :=
   is_graph_of_uctx G (global_ext_uctx Σ).
 
-Lemma conv_spec : forall `{checker_flags} {F:Fuel} Σ G Γ t u,
-    is_graph_of_global_env_ext Σ G ->
-    Σ ;;; Γ |- t = u <~> check_conv (fst Σ) G Γ t u = Checked ().
-Proof.
-  intros. todo "Checker.conv_spec".
-Defined.
-
-Lemma cumul_spec : forall `{checker_flags} {F:Fuel} Σ G Γ t u,
-    is_graph_of_global_env_ext Σ G ->
-    Σ ;;; Γ |- t <= u <~> check_conv_leq (fst Σ) G Γ t u = Checked ().
-Proof.
-  intros. todo "Checker.cumul_spec".
-Defined.
-
-Lemma reduce_cumul :
-  forall `{checker_flags} Σ Γ n t, Σ ;;; Γ |- try_reduce (fst Σ) Γ n t <= t.
-Proof. intros. todo "Checker.reduce_cumul". Defined.
-
-
 Section Typecheck.
   Context {F : Fuel}.
   Context (Σ : global_env).

template-coq/theories/EnvMap.v

@@ -293,7 +293,7 @@ Context {A : Type}.
   Lemma pos_of_string_cont_inj s s' p : pos_of_string_cont s p = pos_of_string_cont s' p -> s = s'.
   Proof.
     induction s; destruct s' => /= //.
-  Admitted.
+  Qed.                          (* TODO *)
   
   Fixpoint pos_of_dirpath_cont (d : dirpath) (cont : positive) : positive := 
     match d with
@@ -324,7 +324,7 @@ Context {A : Type}.
     induction a; destruct m => /= //.
 
     cbn.
-  Admitted.
+  Qed.                          (* TODO *)
 
   Definition empty : t := PTree.empty _.
 

template-coq/theories/LiftSubst.v

@@ -461,7 +461,7 @@ Qed.
 Lemma noccur_between_subst k n t : noccur_between k n t -> 
   closedn (n + k) t -> closedn k t.
 Proof.
-Admitted. *)
+Qed.  *)                        (* TODO *)
 
 Lemma strip_casts_lift n k t : 
   strip_casts (lift n k t) = lift n k (strip_casts t).
@@ -524,4 +524,4 @@ Proof.
   pose (subst_context_snoc n k ctx a). unfold snoc in e. rewrite e. clear e.
   simpl. rewrite -> IHctx.
   pose (subst_context_snoc n k ctx a). simpl. now destruct a as [na [b|] ty].
-Qed.
+Qed.

template-coq/theories/TemplateCheckWf.v

@@ -9,8 +9,11 @@ Open Scope bs_scope.
 
 Definition run_eta_program := Transform.run template_eta_expand.
 
+Axiom assume_welltypedness_of_input : forall p, ∥ wt_template_program p ∥.
 Definition eta_expand p := 
-  run_eta_program p (todo "assume well-typedness").
+  run_eta_program p (assume_welltypedness_of_input p).
+
+Compute (Transform.pre template_eta_expand _).
 
 Definition check_def (d : kername × global_decl) : TemplateMonad unit :=
   match d.2 with
@@ -72,4 +75,4 @@ Definition check_wf_eta (g : Ast.Env.program) : TemplateMonad unit :=
 
 (* To test that a program's eta-expansion is indeed well-typed according to Coq's kernel use: 
  
-  MetaCoq Run (tmQuoteRec wf_program >>= check_wf_eta). *)
+  MetaCoq Run (tmQuoteRec wf_program >>= check_wf_eta). *)