The Coq mailing list

[Jonathan <jonikelee AT gmail.com>]

On 10/10/2014 03:15 PM, Jason Gross wrote:
> Hi,
> Is there a way to make the following code work?  It currently says "Error:
> Not the right number of induction arguments." on the last line.
>
> Require Import List.
> Functional Scheme fold_right_rect := Induction for fold_right Sort Type.
> Goal forall x ls, fold_right and x ls -> x.
> Proof.
>    intros x ls H.
>    functional induction H using fold_right_rect.
>
>
> Thanks,
> Jason

I think functional induction takes a term, not a hypothesis as its argument:

Require Import List.
Functional Scheme fold_right_rect := Induction for fold_right Sort Type.
Goal forall x ls, fold_right and x ls -> x.
Proof.
  intros x ls H.
  functional induction (fold_right and x ls) using fold_right_rect.
  assumption.
  apply IHt.
  tauto.
Qed.

-- Jonathan