The Coq mailing list

[David Pichardie <david.pichardie AT inria.fr>]

Hi Chris,

Cedric already gives the trick.
If you want to obtain exactly the induction principle you want about go_right 
(and not its variation proposed by Cedric), here is a modest solution.

David.

Require Import ZArith.
Require Import Recdef.

 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.


Definition trick {A B:Type} (a:A) (b:B) := b.

Function go_right' (f : Foo) {measure size f} : Foo :=
  match f with
    | FooBase      => FooBase
    | FooTwo f1 f2 =>
      trick (go_right' f1) (go_right' f2)
  end.
intros; simpl; omega.
intros; simpl; omega.
Defined.

Lemma go_right'_is_go_right : forall f,
  go_right f = go_right' f.
Proof.
  intros f.
  functional induction (go_right f); rewrite go_right'_equation; auto.
Qed.


Lemma go_right_rect_v2
     : forall P : Foo -> Foo -> Type,
       (forall f : Foo, f = FooBase -> P FooBase FooBase) ->
       (forall f0 f1 f2 : Foo,
        f0 = FooTwo f1 f2 ->
        P f1 (go_right f1) ->
        P f2 (go_right f2) ->
        P (FooTwo f1 f2) (go_right f2)) ->
       forall f1 : Foo, P f1 (go_right f1).
Proof.
  intros.
  rewrite go_right'_is_go_right.
  apply go_right'_rect; auto.
  intros; 
    repeat rewrite <- go_right'_is_go_right;
    unfold trick; eapply X0;
    repeat rewrite go_right'_is_go_right; eauto.
Qed.