"Function {measure}" and induction principles

[Chris Casinghino]

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:

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_right (f : Foo) {measure size f} : Foo :=
match f with
| FooBase => FooBase
| FooTwo f1 f2 =>
let H := go_right f1 in
go_right 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

[AUGER Cedric]

(*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)" *)

[Pierre Courtieu]

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.

[Pierre Courtieu]

Hello Cedric,

I get the error

"Error: Nested recursive function are not allowed with Function"

this is indeed a nested recursive call since dummy_trick is not
unfolded. Nested recursive calls are currently not in the scope of
Function.

Bests,
Pierre

Post by AUGER Cedric
(* By the way, I get some very unexpected error if I replace
    "let H: Foo := go_right3 f1 in
     go_right3 (dummy_trick H f2)" *)

[David Pichardie]

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.

[Pierre Courtieu]

Hello David, this is needlessly complex. Generally you indeed need to
define a new function but it does not need to be equivalent to the
first one. It does not need to have the same type actually. the only
important thing is that the auxiliary function performs the good
math+fix graph.

Let me illustrate this point by simplifying your file drastically:
actually in your example you don't even need to define go_right' as
your size function already has the good scheme (though it does not
have the same type as go_right).

Bests,
Pierre

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

Require Import ZArith.
Require Import Recdef.

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

(* Use Function here *)
Function 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.

(* use size_ind directly to prove this *)
Lemma foo : forall x, go_right x = FooBase.
Proof.
intros x.
functional induction (size x);simpl.
rewrite go_right_equation.
reflexivity.
rewrite go_right_equation.
assumption.
Qed.


(* This is not needed anymore but can also be proved using size_ind *)
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 P X X0 f1.
functional induction (size f1).
rewrite go_right_equation.
eapply X;eauto.
rewrite go_right_equation.
eapply X0;eauto.
Qed.

Post by David Pichardie
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.

[Chris Casinghino]

Hi Cedric, David and Pierre,

Thanks for the wonderful responses! All three examples were very
helpful, and this simplifies my development dramatically.

--Chris