The Coq mailing list

[Julien Forest <forest AT ensiie.fr>]

Dear Ondrej, 
the problem here is the same as if you use (normal) induction on a local 
definition. 
The inductions tactics need to destruct their non constant arguments (in 
fact, functionnal induction tactic is mainly a wrapper onto the usual 
induction) and thus those arguments should be variables. By non constant, I 
mean here arguments which are not parameter of the induction principle used 
by the tactic. 

There are two ways to prevent that for Function. 
The first one is to copy the definition that will be destructed but this 
might not be what you want. 
The second one which is applicable to your example is to put constant 
argument of your function as first arguments of it. This way, they will be 
detected as parameters and won't be touched by functionnal induction. 

On your example, it suffice to change BigAnd definition as follows: 

Function BigAnd (P : nat-> bool) (i:nat){struct i} : bool :=   

  match i with 

  | O => P O

  | (S i') => andb (BigAnd P i') (P i)

  end.

to make Function detects that P is a parameter of BigAnd and obtain a much 
better principle. 

The proof of Lemma L is then 



Lemma L : forall (N : nat), (BigAnd (fun i => true) N = true).
Proof.
intros.
set (Q := fun i : nat => true).
functional induction (BigAnd Q N).
reflexivity.
rewrite IHb;reflexivity.
Qed.


Best regards, 
Julien. 

On Tue, 29 Jun 2010 19:38:55 +0200
Ondřej Ryšavý 
<rysavy AT fit.vutbr.cz>
 wrote:

> Greetings!
> 
>  
> 
> I am trying to prove lemma L (radically simplified to show the problem)
> using  "functional induction" tactic (the definition BigAnd is at the end of
> this email). 
> 
> However, after application of functional induction tactic, the definition Q
> disappears from the context and newly introduced 
> 
> hypothesis P0 cannot be used to prove the case.
> 
>  
> 
> Lemma L : forall (N : nat), (BigAnd N (fun i => true) = true).
> 
> Proof.
> 
> intros.
> 
> set (Q := fun i : nat => true).
> 
> functional induction (BigAnd N0 Q).
> 
>  
> 
> It is possible to workaround the problem by asserting the required property
> on Q, e.g. assert (forall i :nat, Q i = true):
> 
>  
> 
> Lemma L : forall (N : nat), (BigAnd N (fun i => true) = true).
> 
> Proof.
> 
> intros.
> 
> set (Q := fun i : nat => true).
> 
> assert (forall i :nat, Q i = true).
> 
> intro i.
> 
> unfold Q. reflexivity.
> 
> functional induction (BigAnd N0 Q).
> 
> apply H.
> 
> apply andb_true_intro.
> 
> split.
> 
> apply IHb. auto. auto.
> 
> Qed.
> 
>  
> 
> Nevertheless, is there any reason why this tactic does not keep this
> definition, or am I using this tactic in a wrong way?
> 
>  
> 
> Function BigAnd (i:nat)(P : nat-> bool){struct i} : bool :=   
> 
>   match i with 
> 
>   | O => P O
> 
>   | (S i') => andb (BigAnd i' P) (P i)
> 
>   end.
> 
>  
> 
> Thank you,
> 
>  
> 
> Ondrej Rysavy
> 
>  
>