measureInduct_on

bossLib.measureInduct_on : term quotation -> tactic

Perform complete induction with a supplied measure function.

If q parses into a well-typed term M N, an invocation measureInduct_on q begins a proof by induction, using M to map N into a number. The term N should occur free in the current goal.

Failure

If M N does not parse into a term or if N does not occur free in the current goal.

Example

Suppose we wish to prove P (APPEND l1 l2) by induction on the length of l1. Then measureInduct_on `LENGTH ll` yields the goal

   { !y. LENGTH y < LENGTH l1 ==> P (APPEND y l2) } ?- P (APPEND l1 l2)

See also

bossLib.completeInduct_on, bossLib.Induct, bossLib.Induct_on