From ffbe532cc4050107365d3f46f4d32dc1063324a7 Mon Sep 17 00:00:00 2001 From: Marcel Ullrich Date: Sat, 21 Oct 2023 21:58:26 +0200 Subject: [PATCH 1/4] extend general documentation in ltac1 --- autoinduct/ltac1/Autoinduct.v | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/autoinduct/ltac1/Autoinduct.v b/autoinduct/ltac1/Autoinduct.v index 8782a17..bc94a4e 100644 --- a/autoinduct/ltac1/Autoinduct.v +++ b/autoinduct/ltac1/Autoinduct.v @@ -3,8 +3,12 @@ * proof automation intially. * * The biggest limitation of the Ltac approach is that we must limit - * the number of arguments we can apply it to. We can't easily build + * the number of arguments we can apply it to (we limit them to 3). We can't easily build * a version of this tactic that works on arbitrarily many arguments. + * + * We limit ourselves to the `autoinduct on (f a b)` form. + * With our tactic, we descend into the applications, forwarding the arguments. + * We chain the tactics using continuation passing style. * * We'll build on some tactics from StructTact, and also build a new tactic * in the style of StructTact. This imports the StructTact library so we can do that: @@ -47,6 +51,7 @@ Module V1. (* * The first version of autoinduct makes some extra assumptions, but doesn't rely on * StructTact or anything else. + * Namely, we assume that the recursive argument is a variable to perform induction on. *) Ltac autoinduct1 f := in_reduced_f f ltac:(fun x f => @@ -84,6 +89,8 @@ Module V2. (* * Our tactic makes a whole bunch of assumptions. With StructTact we can get rid of * some of them. + * We first remember constants and generalize the goal. + * Doing so, we arrive at a suitable form of the recursive argument for induction. *) Ltac autoinduct1 f := From 33e41da28a7b85329194bad73ce3654246252ce1 Mon Sep 17 00:00:00 2001 From: Marcel Ullrich Date: Sat, 21 Oct 2023 22:05:01 +0200 Subject: [PATCH 2/4] document ltac2 procedure --- autoinduct/ltac2/Autoinduct.v | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) diff --git a/autoinduct/ltac2/Autoinduct.v b/autoinduct/ltac2/Autoinduct.v index c658e6a..2a0d87f 100644 --- a/autoinduct/ltac2/Autoinduct.v +++ b/autoinduct/ltac2/Autoinduct.v @@ -1,9 +1,18 @@ Require Import Ltac2.Ltac2. +(* +We match the definition of the fixpoint to find the index of the +structural argument. +Afterward, we extract the corresponding arguments from the applied form. +For tactic 2 and 3, we search for a suitable function application. +*) + + (* stdlib fail does enter so has type unit (indeed it doesn't fail if there are no focused goals) *) Ltac2 fail s := Control.backtrack_tactic_failure s. +(* Computes the index of the structural index *) (* If you don't want to use Unsafe.kind, but can only handle fixpoints with 2 arguments *) Ltac2 naive_struct_arg (f : constr) : int := lazy_match! f with @@ -19,11 +28,18 @@ Ltac2 rec struct_arg (f : constr) : int := | _ => fail "not a fixpoint" end. +(* +Find an application of f in the goal. +Returns the structural argument of the applied form. +If f is None, acts on the first suitable function found. +If f is Some, it has to be be a fair of the function and the index of the structural argument. +*) Ltac2 find_applied (f : (constr * int) option) : constr := match! goal with | [ |- context [ ?t ] ] => match Constr.Unsafe.kind t with | Constr.Unsafe.App g args => + (* index of the structural argument of g *) let farg := match f with | Some (f,farg) => @@ -45,6 +61,7 @@ Ltac2 find_applied (f : (constr * int) option) : constr := end end. +(* Combination of the three autoinduct tactics. *) Ltac2 autoinduct0 (f: constr option) : unit := let arg := match f with From acd429b55fabd13bba4a53bd1a89898d888eb456 Mon Sep 17 00:00:00 2001 From: Marcel Ullrich Date: Sat, 21 Oct 2023 22:05:20 +0200 Subject: [PATCH 3/4] add documents to MetaCoq code --- autoinduct/metacoq/theories/Autoinduct.v | 11 +++++++++++ autoinduct/metacoq/theories/Autoinduct_Template.v | 10 ++++++++++ 2 files changed, 21 insertions(+) diff --git a/autoinduct/metacoq/theories/Autoinduct.v b/autoinduct/metacoq/theories/Autoinduct.v index e8afe61..3f49e62 100644 --- a/autoinduct/metacoq/theories/Autoinduct.v +++ b/autoinduct/metacoq/theories/Autoinduct.v @@ -16,6 +16,8 @@ Definition autoinduct (p : program) : term := let (Σ, t) := p in (* decompose into head and arguments *) let (hd, args) := decompose_app t in + (* binder count, inner term (for a constant in environment) *) + (* allows for `autoinduct (f 3 5)` with `f := (fun a => e)` (e has to be a fixpoint) *) let (n, hd') := match hd with | tConst kn _ => match lookup_constant Σ kn with | Some b => match b.(cst_body) with @@ -27,6 +29,7 @@ Definition autoinduct (p : program) : term := end | x => (0, x) end in + (* lookup struct argument, extract from args *) match hd' with | tFix mfix idx => match nth_error mfix idx with @@ -48,6 +51,10 @@ Tactic Notation "autoinduct1" "on" constr(f) := induction t). (** * Step 2 *) +(* +Go through the goal and find an application of f. +Then proceed as with Step 1. +*) Definition eq_const (c1 c2: term) : bool := match c1, c2 with @@ -68,6 +75,7 @@ Fixpoint find_cnst_in_args (f : term) (args : list term): term := end. (* From a list of terms returns all the tApp nodes, including the ones appearing as arguments *) +(* Nested recursion through lists are not natively recognized. Therefore, we need to disable the guard check. *) #[bypass_check(guard)] Fixpoint split_apps (ts : list term) : list term := match ts with @@ -108,6 +116,9 @@ Tactic Notation "autoinduct" "on" constr(f) := end. (** * Step 3 *) +(* +Find any fixpoint, and proceed as with Step 1. +*) (* Looks in the goal applications of fixpoints *) Definition find_fixpoints (ctx : program) : list term := diff --git a/autoinduct/metacoq/theories/Autoinduct_Template.v b/autoinduct/metacoq/theories/Autoinduct_Template.v index 4b55be7..911265b 100644 --- a/autoinduct/metacoq/theories/Autoinduct_Template.v +++ b/autoinduct/metacoq/theories/Autoinduct_Template.v @@ -5,12 +5,22 @@ Require Import List. Import MCMonadNotation ListNotations. Open Scope bs. +(* +We implement the form 1 autoinduct tactic by looking up the recursive argument +in the fixpoint definition and extracting it from the applied term. +*) + +(* +Retrives the structural argument of an applied function `(f a b) -> b` +We return a typed_term (a dependent pair of type and term). +*) Definition autoinduct {A} (a : A) : TemplateMonad typed_term := a' <- tmEval cbv a ;; (* get the inductive representation of a *) t <- tmQuote a' ;; (* decompose into head and arguments *) let (hd, args) := decompose_app t in + (* lookup the recursive argument from the definition and extract it from args *) match hd with | tFix mfix idx => match nth_error mfix idx with From 76c27db3ac4a0da7fada0465bf84eefe61bbfa67 Mon Sep 17 00:00:00 2001 From: Marcel Ullrich Date: Sat, 21 Oct 2023 22:05:49 +0200 Subject: [PATCH 4/4] general remarks and explanation of MetaCoq files --- autoinduct/README.md | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/autoinduct/README.md b/autoinduct/README.md index 064872a..60d6759 100644 --- a/autoinduct/README.md +++ b/autoinduct/README.md @@ -3,6 +3,8 @@ This exercise amounts to implementing a tactic which performs induction on the right argument of a recursive function. The tactic was originally used in a course by T. Ringer, more information is [here](https://dependenttyp.es/classes/fa2022/artifacts/12-custom.html). +A more detailed explanation and motivation is given in `ltac1`. + ## Steps 1. `autoinduct on (f a b).` should run `induction` on the recursive argument of `f`, in this case either `a` or `b`. 1. `f` unfolds to a `fix`, like `Nat.plus` does @@ -133,4 +135,14 @@ Requires: `coq-metacoq-template` Some details specific to the MetaCoq code. +MetaCoq provides the structural argument in the fixpoint definition. +We use this to extract the structural argument from the applied arguments. + +For tactic 2 and 3, we recursive through the quoted goal to find a suitable term. + +- `Autoinduct_Template` is the simplified version for tactic 1. +- `Autoinduct` uses the same approach but considers additional cases and +implements all three tactics. + +