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.

Check count.

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


Theorem hello_decide : forall x : nat , count fret fret_dec x = 0.
Proof.
  intros.
  induction x.
  unfold count.
  replace (fret_dec 0) with false.
  
Qed.

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

(if fret_dec 0 then 1 else 0) = 0

Coq dose not automaticly 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:

Error: Terms do not have convertible types.

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

Anton Trunov Anton Trunov · Accepted Answer · 2018-06-07T06:08:40

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.
Proof.
  induction x as [| x IH].
  - unfold count. destruct (fret_dec 0) as [contra | _].
    + contradiction. 
    + reflexivity.
  - simpl. rewrite IH. destruct (fret_dec (S x)) as [contra | _].
    + contradiction.
    + 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 }.
Proof. right. intros contra. contradiction. Defined.

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

Compute if in a decideable prop in coq

1 Answers