The Coq mailing list

[AUGER Cedric <Cedric.Auger AT lri.fr>]

(*Hi all,

I have a situation where Function is not generating an induction
principle for me when using "measure" or "wf".  What follows is a
reduced example.  As explanation, here is a similar definition that
Coq accepts and for which it generates a sensible induction principle:
*)
Require Import Arith.
Require Import Recdef.
Require Import Omega.
(* Please, add the previous 3 lines when post. *)

  Inductive Foo : Type :=
    | FooBase : Foo
    | FooTwo  : Foo -> Foo -> Foo.

  Fixpoint size (f : Foo) : nat :=
    match f with
    | FooBase      => 0
    | FooTwo f1 f2 => 1 + (size f1) + (size f2)
    end.

  Function go_right (f : Foo) {measure size f} : Foo :=
    match f with
    | FooBase      => FooBase
    | FooTwo f1 f2 =>
      go_right f2
    end.

    intros; simpl; omega.
  Defined.
(*
Coq generates the following perfectly sensible induction principle
for go_right:

  go_right_rect
       : forall P : Foo -> Foo -> Type,
         (forall f : Foo, f = FooBase -> P FooBase FooBase) ->
         (forall f0 f1 f2 : Foo,
          f0 = FooTwo f1 f2 ->
          P f2 (go_right f2) -> P (FooTwo f1 f2) (go_right f2)) ->
         forall f1 : Foo, P f1 (go_right f1)

My problem is that, for the theorems I want to prove, I need an IH for
both f1 and f2 in the FooTwo case.  Coq quite sensibly doesn't give me
one for f1, since I didn't make a recursive call on it and I didn't
prove f1 is smaller acccording to the metric.  (In the real example f1
is added to a context in the conclusion, perhaps to be mentioned
later, but I don't recurse on it).

So, I tried "tricking" coq into giving me an extra IH by changing the
definiton of go_right to this:
*)
  Function go_right2 (f : Foo) {measure size f} : Foo :=
    match f with
    | FooBase      => FooBase
    | FooTwo f1 f2 =>
      let H: Foo := go_right2 f1 in
      go_right2 f2
    end.

    intros; simpl; omega.
  Qed.
(*
Coq "accepts" this definition, but as you can see it does not ask me
to prove that f1 is smaller (despite the recursion) and it will
not generate an induction principle for this definition.  Instead,
it warns:

  "Warning: Cannot define principle(s) for go_right"

Can anyone explain this behavior?  It seems like a sensible
definition, even if f1 is not mentioned in the conclusion.  Is there
some other trick I can play to get the IH I want?  Thanks for your
help!

--Chris
*)

(*
 I can't explain why; I may be completely wrong,
 but I think that "Function" is no longer well maintained,
 as "Program" seems to be more powerfull than Function.

 Here is a variant of your trick (although I don't understand
 why you need induction on f1)
*)

Definition dummy_trick (H: Foo) (f2: Foo) := f2.

  Function go_right3 (f : Foo) {measure size f} : Foo :=
    match f with
    | FooBase      => FooBase
    | FooTwo f1 f2 =>
      let H: Foo := go_right3 f1 in
      let I := go_right3 f2 in
      dummy_trick H I
    end.

    intros; simpl; omega.
    intros; simpl; omega.
  Qed.

(* By the way, I get some very unexpected error if I replace
   the critical part with :
     "let H: Foo := go_right3 f1 in
      go_right3 (dummy_trick H f2)" *)