The Coq mailing list

[Fabien Renaud <fafounet AT gmail.com>]

Hi,

Here is a simplification of my problem:


Fixpoint eq_nat (m n : nat) : bool :=
match m, n with
| 0, 0 => true
| S m', S n' => eq_nat m' n'
| _,_ => false
end.

Program Fixpoint test (n: nat) :=
match n with
| 0 => 0::nil
| S n => if (eq_nat n 3) then _ else _
end.

Program asks me to fill 2 obligations. In this case this is fine. I know which obligation is asked in which order.

However sometimes the situation is a bit more complex and I have to perform a proof, and not only refine.

And the problem is that I lack the information about in which branch of the "if" I am. And thus I cannot conclude my proof since

I cannot remove some contradictory cases.

Does someone have an idea?

Thanks!

Fabien