# Using if-then-else in Program Definition's obligation

Consider the following program (which is a simpler version of what I'm trying to do):

Require Import List Arith.

Program Definition test (l: list nat) : nat :=
if (existsb (fun x => Nat.eqb x 1) l) then
match l with
| a::_ => a
| nil => _
end
else 0.
Next Obligation.

Qed.

It should be simple to prove that the second case (nil) cannot happen because of the if-condition. However, in the obligation, I only see

Goal (1)
---
nat

The condition is not mentioned, so there is no way to derive a contradiction. (Of course I do not just want to provide a default value because this would not work in the more complex case).

How can I get hold of the if-condition and use it in fulfilling the obligation?

• Can you give a minimal working example? In particular, one that includes your imports, so that your example type-checks? Commented Jun 10 at 13:55
• Right. This should do it. Commented Jun 10 at 16:06
• You will probably have to use existsb_exists at some point. If this were Agda, I would tell you to use with ... in or the inspect idiom to get the required equality. Coq users apparently call this the convoy pattern? Commented Jun 10 at 16:36
• See also here, here and here. Commented Jun 10 at 16:42

I've found that if I want to use if-then-else facts later in a definition, I have to use decidable facts.

For example, in this case:

Definition has_one (l: list nat) :=
exists a, In a l /\ a = 1.

Definition has_one_dec (l: list nat): {has_one l} + {~ has_one l}.
Proof.
case (existsb (fun x => Nat.eqb x 1) l) eqn:A.
* left. apply existsb_exists in A. destruct A. exists x. intuition. now apply Nat.eqb_eq.
* right. intro. apply Bool.eq_true_false_abs in A. auto.
apply existsb_exists. destruct H. exists x. intuition. now apply Nat.eqb_eq.
Qed.

Now, doing if has_one_dec l will give me the fact one_dec l:

Program Definition test (l: list nat) : nat :=
if has_one_dec l then
match l with
| a::_ => a
| nil => _
end
else 0.

Next Obligation.
( Goal (1)
h : has_one nil
---
nat
)
apply constructive_indefinite_description in h. destruct h as [? []].
simpl in H. now exfalso.
Qed.

(N.B.: in this case I need constructive_indefinite_description to make use of has_one because test returns a nat instead of a Prop)