recInduct fails for mutually recursive functions

[xrchz]

I want to be able to use recInduct for functions like test2/test3 below. Is that not supported?

open HolKernel boolLib bossLib lcsymtacs
val _ = new_theory"bug"

val test1_def = Define`(test1 (0,a) = a) ∧ (test1 (SUC n,a) = test1 (n,SUC a))`
val test1_ind = theorem"test1_ind";
val works = prove(
  `∀x y. test1 (x,y) = x + y`,
  recInduct test1_ind >> simp[test1_def])

val test2_def = tDefine"test2"
  `(test2 (0,0) = 1) ∧
   (test2 (0,SUC a) = test3 a) ∧
   (test2 (SUC n,a) = test2 (n,SUC a)) ∧
   (test3 0 = 0) ∧ (test3 (SUC n) = test2 (0,n))`
  (WF_REL_TAC`inv_image ($< LEX $<) (λx. case x of INL (a,b) => (a,b) | INR a => (0,a))`)
val test2_ind = theorem"test2_ind";

val fails = prove(
  `(∀x y. test2 (x,y) ≤ 1) ∧
   (∀x. test3 x ≤ 1)`,
  recInduct test2_ind

Exception raised at Induction.ndest_forall:
too few quantified variables in goal
Exception- HOL_ERR {message = "too few quantified variables in goal", origin_function = "ndest_forall", origin_structure = "Induction"} raised

---

Want to back this issue? Post a bounty on it! We accept bounties via Bountysource.

[konrad-slind]

I use HO_MATCH_MP_TAC for such things. --Konrad.

On Mon, Aug 31, 2015 at 8:11 PM, Ramana Kumar [email protected] wrote:

I want to be able to use recInduct for functions like test2/test3 below. Is that not supported?

open HolKernel boolLib bossLib lcsymtacs val _ = new_theory"bug"

val test1_def = Define(test1 (0,a) = a) ∧ (test1 (SUC n,a) = test1 (n,SUC a)) val test1_ind = theorem"test1_ind"; val works = prove( ∀x y. test1 (x,y) = x + y, recInduct test1_ind >> simp[test1_def])

val test2_def = tDefine"test2" (test2 (0,0) = 1) ∧ (test2 (0,SUC a) = test3 a) ∧ (test2 (SUC n,a) = test2 (n,SUC a)) ∧ (test3 0 = 0) ∧ (test3 (SUC n) = test2 (0,n)) (WF_REL_TACinv_image ($< LEX $<) (λx. case x of INL (a,b) => (a,b) | INR a => (0,a))) val test2_ind = theorem"test2_ind";

val fails = prove( (∀x y. test2 (x,y) ≤ 1) ∧ (∀x. test3 x ≤ 1), recInduct test2_ind

Exception raised at Induction.ndest_forall: too few quantified variables in goal Exception- HOL_ERR {message = "too few quantified variables in goal", origin_function = "ndest_forall", origin_structure = "Induction"} raised

— Reply to this email directly or view it on GitHub https://github.com/HOL-Theorem-Prover/HOL/issues/291.

[xrchz]

HO_MATCH_MP_TAC test2_ind won't work in this case because of the paired abstractions. Notice that HO_MATCH_MP_TAC test1_ind doesn't work either, but recInduct handles the paired abstractions correctly. I guess I'm asking for that functionality to be extended to support mutual recursion too.