The Coq mailing list

[Ond�ej Ry�av� <rysavy AT fit.vutbr.cz>]

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