Example of using `refine` to build up a proof term for induction principle.

InductionRefine.v

Inductive ev : nat -> Prop :=
  | ev_0 : ev 0
  | ev_SS : forall n, ev n -> ev (S (S n)).

Hint Constructors ev.

Inductive test : (nat -> nat) -> nat -> Prop :=
  | TestCase : forall f i,
      (forall k,
        0 <= k < f i ->
        exists r,
          ev r /\ test f (k + r)) ->
      test f i.

Definition sample_f (n : nat) : nat :=
  match n with
  | 2 => 0
  | 3 => 0
  | 6 => 2
  | _ => 6
  end.

Require Import Omega.

Example test_sample_f : test sample_f 6.
Proof.
  apply TestCase.
  intros.
  destruct k.
  - exists 2. split; eauto.
    apply TestCase.
    intros.
    exists 2. split; eauto.
    simpl in *.
    omega.
  - destruct k.
    + exists 2. split; eauto.
      apply TestCase.
      intros.
      simpl in *.
      omega.
    + simpl in *.
      omega.
Qed.

Check test_ind.

(* test_ind
     : forall P : (nat -> nat) -> nat -> Prop,
       (forall (f : nat -> nat) (i : nat),
        (forall k : nat, 0 <= k < f i -> exists r : nat, ev r /\ test f (k + r)) -> P f i) ->
  forall (n : nat -> nat) (n0 : nat), test n n0 -> P n n0 *)


Lemma test_ind' :
  forall P : (nat -> nat) -> nat -> Prop,
    (forall (f : nat -> nat) (i : nat),
        (forall k : nat, 0 <= k < f i ->
                         exists r : nat,
                           ev r /\ test f (k + r) /\ P f (k + r)) ->
        P f i) ->
    forall (f : nat -> nat) (n : nat), test f n -> P f n.
Proof.
  intros P H.
  refine (fix F f n t :=
            match t with
            | TestCase f i Hrec =>
              H f i (fun k Hk =>
                       match Hrec k Hk with
                       | ex_intro _ r Hr =>
                         match Hr with
                         | conj Hev Hrest => 
                           ex_intro _ r (conj Hev (conj Hrest (F f (k + r) Hrest)))
                         end
                       end)
            end).
Qed.