The Coq mailing list

[Matthieu Sozeau <matthieu.sozeau AT gmail.com>]

Hi,

  You can use the 'dec' combinator from Program's Coq library to get the 
equality
corresponding to the if statement in each branch. E.g. "if dec (eq_nat n 3) 
then _ else _"

-- Matthieu

On 1 oct. 2013, at 10:06, Fabien Renaud 
<fafounet AT gmail.com>
 wrote:

> 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