ImandraX derives induction schemes from recursive function definitions. When the
default choice (heuristic, or the recursion of a function in your goal) gives the
wrong cases or an unusable induction hypothesis, you don't fight it — you supply
the scheme. These techniques appear in essentially every hard expert proof.
induction ~id:[%id f] () inducts along the recursion structure of function f
(similarly induct ~on_fun:[%id f] ()). Point it at whichever recursive function
shapes the goal — including imported ones (~id:[%id Binomial.choose]) and
recognizer predicates:
(* geometric_sequence recurses singleton / cons-with-ratio-check, giving exactly the two cases the sum theorem needs *)theorem geo_sum_mult seq r = geometric_sequence seq r ==> ...[@@by induction ~id:[%id geometric_sequence] () @>| [ <base>; <step> ]]
Use ~vars:["v"] to pin the induction variable for structural induction, and
[@@adm x, y] on definitions to control which arguments drive admission (and
hence the derived scheme).
If no existing function has the right recursion, define a function whose only
purpose is its recursion structure — the body value is irrelevant:
(* Plain natural-number induction on an int parameter *)let rec nat_ind n = if n <= 0 then true else nat_ind (n - 1)[@@measure Ordinal.of_int (max 0 n)]lemma choose_1 n = n >= 0 ==> choose n 1 = n[@@by induction ~id:[%id nat_ind] () @>>| auto]
Richer schemes bake in exactly the IH you need:
(* IH on (tl s, xs), (s, tl xs), AND (tl s, tl xs) simultaneously *)let rec fun_induct (s : real list) (xs : real list) = if s = [] || xs = [] then 0 else fun_induct (List.tl s) xs + fun_induct s (List.tl xs) + fun_induct (List.tl s) (List.tl xs)[@@adm s, xs](* "ys shrinks by remove h" — structural induction on xs would never give this *)let rec ppe_ind xs ys n = match xs with [] -> true | h :: t -> ppe_ind t (remove h ys) n
A common special case: to prove a loop descent_loop correct, define a
descent_ind mirroring its exact recursion and drive the invariant proof with
induction ~id:[%id descent_ind] () @>>| close_tac.
For ~id to apply, the scheme function must relate to the goal. Two standard
ways to force it, both followed by deriving a clean lemma:
(* (a) vacuous hypothesis anchor *)lemma subseq_tail_weak_h s xs = fun_induct s xs = fun_induct s xs && subseqp s xs ==> ...[@@by induction ~id:[%id fun_induct] () @>| [...]]lemma subseq_tail_weak s xs = subseqp s xs ==> ...[@@by [%use subseq_tail_weak_h s xs] @> auto](* (b) conjoin into the conclusion, strip with an "always true" lemma *)lemma pa_scheme_always c p = pa_scheme c p = true [@@by auto]lemma ballot_gen_h ... = ... ==> (P ... && pa_scheme candidates p) [@@by ...]
The anchor also solves a polymorphism wrinkle: a scheme over 'a list list
may need a dummy (x : 'a) argument so the type variable is anchored
(nmc_ind x l k = nmc_ind x l k (* anchor for polymorphism workaround *)).
When your target fixes an argument that the recursion varies (e.g. you care about
small_divisor_from 2 n but the function recurses by incrementing that 2):
Generalize (_aux pattern): prove the lemma for a variable cursor k with
range hypotheses, then specialize:
lemma sd_divides_aux n k = 2 <= k && k <= max 2 n ==> ...lemma sd_divides n = ... [@@by [%use sd_divides_aux n 2] @> auto]
Pin: keep the argument a variable constrained by hypothesis j = 2, so
induction can still follow the recursion on j:
lemma sd_minimal_key n k j = n > 1 && 2 <= k && j = 2 && k < small_divisor_from j n ==> ...
Stating it directly with the constant 2 would make the IH unusable.
Argument order also matters — ImandraX's heuristics prefer certain positions,
and experts annotate reorderings: (* s first so induction picks it *) lemma foo_h s u = ... then restate as foo u s via [%use foo_h ...].
Don't fight a hard inductive step in place. Extract it as a non-inductive
lemma whose hypotheses are exactly the IH instances, over fresh variables:
(* takes both IH equalities as premises; needs no induction itself *)lemma choose_fact_interior_from_IH n k ihl ihr = 0 < k && k < n && ihl = ... (* IH at (n-1, k-1) *) && ihr = ... (* IH at (n-1, k) *) ==> choose n k * fact k * fact (n - k) = fact n[@@by ... @> nonlin ()]
Then the inductive proof's step branch is just
[%use choose_fact_interior_from_IH ...] @> auto, instantiated at the
destructor terms the induction leaves you (n - 1, List.hd xs, List.tl xs).
Only the main lemma inducts; every helper is plain algebra.
[@@by induction () @>| [ <base tactic> ; <step tactic> ]] (* per-subgoal *)[@@by induction ~id:[%id f] () @>>| auto] (* same tactic on all *)
@>| is positional — it depends on subgoal order. Keep each branch to a short
chain; if a branch grows past a few steps, extract a step lemma (§6).
Inside branches the surgical kit applies: [%cases cond] to split
interior/boundary, [%expand f args] to unfold exactly one call (a bare
expand may also hit the IH occurrence — prefer the applied form),
[%replace x] to commit an equation, lift_ifs @>>| auto to split residual
conditionals.
A reusable closer can be named:
let close_sub = intros @> [%subgoal ...] @>| [...] in induction ... @>>| close_sub.