Autoinduct documentation improvement

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.
+
+
 </details>

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 :=

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

autoinduct/metacoq/theories/Autoinduct.v

@@ -38,8 +38,11 @@ Definition autoinduct (p : program) : term :=
         end
     | x => x
     end 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 (lambdas, rhd) := decompose_lam_assum [] hd' in
   let n := List.length lambdas in
+  (* lookup struct argument, extract from args *)
   match rhd with
   | tFix mfix idx =>
       match nth_error mfix idx with
@@ -65,6 +68,10 @@ Proof.
 Qed.
 
 (** * 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
@@ -85,6 +92,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
@@ -125,6 +133,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 :=

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