The Coq mailing list

[Pierre Courtieu <Pierre.Courtieu AT cnam.fr>]

Hello,

Yes Function is still maintained and plans are made to merge it with
Program Fixpoint when there is time for the job. It is true that
Program Fixpoint is more powerful in a lot of cases, but to my
knoledge Program Fixpoint does not produce induction principles.

To answer your question, the "let in"s are reduced during the graph
analysis of the function (which then allows to generate the induction
principle). The trick showed by Cedric works because after reducing
the letins there is still an occurrence of the induction call you want
to add (since the call to dummy_trick is not reduced).

Let me add that you can do this kind of trick by defining *another
function*, as Cedric did by renaming go_right into go_right2, and
still use the induction principle to prove things on the initial
function. See below.

Moreover this second function does not need to be semantically
equivalent to the "real" one. It only needs to perform the "match" and
recursive calls you want to have in your induction scheme. I
particular, if you define dummy_trick like this:
Definition dummy_trick (H: Foo) (f2: Foo) := FooBase.
the induction scheme is almost the same and behaves the same. See
below for an example of a proof about go_right using the induction
scheme of go_right3 (with a modified dummy_trick).

Last remark: if you want to be able to reduce your function, you
should end your Function by "Defined". It is however generally better
to use the fix point equation of the function (also generated by
function) in proofs when terms are not closed. See the last proof
below for an example.

Best regards,
P.C.

-------------------------------8X-------------------------------

Require Import Arith.
Require Import Recdef.
Require Import Omega.

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 dummy_trick (H: Foo) (f2: Foo) := FooBase.

Function go_right3 (f : Foo) {measure size f} : Foo :=
  match f with
    | FooBase      => FooBase
    | FooTwo f1 f2 =>
        (*    let H: Foo := go_right3 f1 in
     go_right3 (dummy_trick H 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.
Defined.


Lemma foo : forall x, go_right x = FooBase.
Proof.
  intros x.
  functional induction (go_right3 x);simpl.
  unfold go_right;simpl; reflexivity.
  rewrite go_right_equation.
  assumption.
Qed.