Compute if in a decideable prop in Coq

Question

I want to write a function that calculate count of true values of p 0 .. p t in a nat -> prop function.

Section count_sc.

  Variable p : nat -> Prop.
  Hypothesis p_dec : forall x : nat, {p x} + {~ p x}.

  Fixpoint count (x : nat) :=
    match x with
    | 0 => if p_dec 0 then 1 else 0
    | S y => if p_dec x then 1 + count y else count y
    end.

End count_sc.

Definition fret (x : nat) := False.

Axiom fret_dec : forall x : nat, { fret x } + { ~ fret x }.

Theorem hello_decide : forall x : nat, count fret fret_dec x = 0.
forall x : nat, count fret fret_dec x = 0
Proof.
forall x : nat, count fret fret_dec x = 0
  intros.
x: nat
count fret fret_dec x = 0 induction x.
count fret fret_dec 0 = 0
x: nat
IHx: count fret fret_dec x = 0
count fret fret_dec (S x) = 0 unfold count.
(if fret_dec 0 then 1 else 0) = 0
x: nat
IHx: count fret fret_dec x = 0
count fret fret_dec (S x) = 0
  -
(if fret_dec 0 then 1 else 0) = 0 replace (fret_dec 0) with false.
Tactic failure: Terms do not have convertible types.
(if fret_dec 0 then 1 else 0) = 0

Before the replace tactic I should proof some goal like this:

(if fret_dec 0 then 1 else 0) = 0

Coq does not automatically compute the value of the if statement. and if I try to replace the fret_dec with it's value, I will get this error:

Tactic failure: Terms do not have convertible types.

How I can write count function that I can unfold and use it in theorems?

Answer

You have declared fret_dec as an axiom. But that means it does not have a definition, or implementation in other words. Thus, Coq cannot compute with it.

You can still prove your theorem like so, using the destruct tactic:

Theorem hello_decide : forall x : nat, count fret fret_dec x = 0.
forall x : nat, count fret fret_dec x = 0
Proof.
forall x : nat, count fret fret_dec x = 0
  induction x as [| x IH].
count fret fret_dec 0 = 0
x: nat
IH: count fret fret_dec x = 0
count fret fret_dec (S x) = 0
  -
count fret fret_dec 0 = 0 unfold count.
(if fret_dec 0 then 1 else 0) = 0 destruct (fret_dec 0) as [contra | _].
contra: fret 0
1 = 0
0 = 0
    +
contra: fret 0
1 = 0 contradiction.
    +
0 = 0 reflexivity.
  -
x: nat
IH: count fret fret_dec x = 0
count fret fret_dec (S x) = 0 simpl.
x: nat
IH: count fret fret_dec x = 0
(if fret_dec (S x)
 then S (count fret fret_dec x)
 else count fret fret_dec x) = 0 rewrite IH.
x: nat
IH: count fret fret_dec x = 0
(if fret_dec (S x) then 1 else 0) = 0 destruct (fret_dec (S x)) as [contra | _].
x: nat
IH: count fret fret_dec x = 0
contra: fret (S x)
1 = 0
x: nat
IH: count fret fret_dec x = 0
0 = 0
    +
x: nat
IH: count fret fret_dec x = 0
contra: fret (S x)
1 = 0 contradiction.
    +
x: nat
IH: count fret fret_dec x = 0
0 = 0 reflexivity.
Qed.

But, in this case it is really easy to provide such a decision procedure instead of postulating it. And this simplifies the proof a lot:

Definition fret_dec' (x : nat) : { fret x } + { ~ fret x }.
x: nat
{fret x} + {~ fret x}
Proof.
x: nat
{fret x} + {~ fret x} now right. Defined.

Theorem hello_decide' : forall x : nat, count fret fret_dec' x = 0.
forall x : nat, count fret fret_dec' x = 0
Proof.
forall x : nat, count fret fret_dec' x = 0
  induction x as [|x IH]; simpl.
0 = 0
x: nat
IH: count fret fret_dec' x = 0
count fret fret_dec' x = 0
  -
0 = 0 reflexivity.
  -
x: nat
IH: count fret fret_dec' x = 0
count fret fret_dec' x = 0 exact IH.
Qed.