Using if in Fixpoint

Question

I have this recursive function I am trying to define by way of Fixpoint, but the if condition is giving me trouble.

Require Import Arith.

Variables Cd : nat -> nat -> Prop.
Variables T : nat -> nat.

Fixpoint delay (t:nat) {struct t} : nat :=
  match t with
  | 0 => 0
  | S t => if ((T (S t)) = 0 /\ ((Cd ((S t) + (delay t) + 1 mod 2)) (S t))) then (delay t) + 1 else (delay t)
  end.

Coq complains that the if condition is of type Prop and not a coinductive type. I am not really sure what problem it is trying to tell me.

What I currently have instead is two hypotheses:

Hypothesis delay_def1 : forall t: nat, ((T (S t)) = 0 /\ ((Cd ((S t) + (delay t) + 1 mod 2)) (S t))) -> (delay (S t)) = (delay t) + 1.
Hypothesis delay_def2 : forall t: nat, ~((T (S t)) = 0 /\ ((Cd ((S t) + (delay t) + 1 mod 2)) (S t))) -> (delay (S t)) = (delay t).

---

More context to give a better idea of the problem I am working on. This is a hobby project to learn Coq where I am trying to prove certain properties of a selection function for weapons inside a game.

There are six sequences in total that depend on each other:

Require Import Arith.
Require Import Coq.Logic.Classical.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Structures.OrdersFacts.

Variables ATK0 Sd0 : Prop.
Variables Sel0 : nat -> Prop.

Variables Cd : nat -> nat -> Prop.
Variables T delay : nat -> nat.

Definition Sel (x t:nat): Prop :=
  match t with
  | 0 => (Sel0 x)
  | (S t) => ~(((T (S t)) = 2 /\ ~((Cd x) (S t)))
              \/ ((T (S t)) =  0 /\ ((Cd (1 - x)) (S t)) /\ ((Cd x) (S t)))
              ) /\ ((S t) + (delay t)) mod 2 = x
  end.

Definition ATK (t:nat) : Prop :=
  match t with
  | 0 => ATK0
  | S t => exists x: nat, ((Sel x) t) /\ ~ ((Cd x) t)
  end.

Fixpoint Sd (t:nat) : Prop :=
  match t with
  | 0 => (ATK t) \/ ((T t) > 0 /\ Sd0)
  | (S t) => (ATK (S t)) \/ ((T t) > 0 /\ (Sd t))
  end.

Hypothesis T_def1 : forall t : nat, (T t) = 2 \/ ((T t) = 0 /\ (Sd t)) -> (T (S t)) = 0.
Hypothesis T_def2 : forall t : nat, ~((T t) = 2 \/ ((T t) = 0 /\ (Sd t))) -> (T (S t)) = (S (T t)).
Hypothesis T_lt_3: forall t : nat, (lt (T t) 3).

Hypothesis Cd_def1 : forall t x : nat, ((Sel x) t) /\ ~((Cd x) t) -> ((Cd x) (S t)).
Hypothesis Cd_def2 : forall t x : nat, ((Sel x) t) /\ ((Cd x) t) -> ~((Cd x) (S t)).
Hypothesis Cd_def3 : forall t x : nat, ~((Sel x) t) -> (((Cd x) (S t)) <-> ((Cd x) t)).

Hypothesis delay_def1 : forall t: nat, ((T (S t)) = 0 /\ ((Cd ((S t) + (delay t) + 1 mod 2)) (S t))) -> (delay (S t)) = (delay t) + 1.
Hypothesis delay_def2 : forall t: nat, ~((T (S t)) = 0 /\ ((Cd ((S t) + (delay t) + 1 mod 2)) (S t))) -> (delay (S t)) = (delay t).

• ATK t is shorthand for whether an attack happened at time t. A Prop
• Sel x t is whether Weapon x is selected at time t. A Prop
• Cd x t is whether Weapon x is on cooldown at time t. A Prop
• delay t: On a basic level, Sel just switches back and forth between two weapons. In some cases I skip a frame, in which case delay is incremented so it changes which weapon comes next.
• Sd t Attacks influence the length of the cycle of T in a certain way that is captured by Sd. Sd is carried over between frames until T=0, at which point it is reset.
• T t captures a certain cycle in the game that essentially is a squence 0 1 2 0 0 1 2 0 0 ...

I was already able to prove two Lemmas, for one of which I had a proof on paper before I started.

Lemma only_2_weapons : forall t x : nat, t > 0 /\ ((Sel x) t) -> x < 2.
Lemma no_ATK_on_first_draw : forall t : nat, t > 0 /\ (T (t)) = 2 -> ~(ATK (S t)).

And the end goal is to prove or disprove

Theorem no_ATK_on_draw : forall t: nat, ((T t) = 0 /\ (ATK t)) -> forall t1: nat, ((t1 > t /\ (T t1) = 0) -> ~(ATK t1)).

The goal of my questions regarding Fixpoint, Definition etc. is to make the proof as smooth as possible. I started by defining all the sequences as Hypotheses.

Answer 1

As others have said, the reason Coq does not accept your definition is that, although classical logic stipulates forall P, P \/ ~P, it is an undecidable (non-computable) problem to decide whether P or ~P holds for any given P.* Think about it: If RiemannHypothesis : Prop is an encoding of its namesake, how in your favorite programming language would you compute the value if RiemannHypothesis then 0 else 1? Or even worse, if ContinuumHypothesis then 0 else 1? :)

Luckily, P \/ ~P is decidable for many P that programmers actually care about. Equality of natural numbers is one of them (your T (S t)) = 0), and we must assume that your Cd is also decidable. Thus, your part of the exercise is to instantiate Cd_dec in the following, and you will have the definition of delay that you (truly) want.

Require Import Arith.

Variables Cd : nat -> nat -> Prop.
Variables T : nat -> nat.

(* This isn't possible to define for all nat -> nat -> Prop, but 
   presumably this is possible for Cd specifically. *)
Definition Cd_dec : forall n m, { Cd n m } + { ~Cd n m }.
Admitted.

Fixpoint delay (t:nat) {struct t} : nat :=
  match t with
  | 0 => 0
  | S t => if Nat.eq_dec (T (S t)) 0 then
            if Cd_dec ((S t) + (delay t) + 1 mod 2) (S t)
            then delay t + 1
            else delay t
           else delay t
  end.

I've taken the liberty of splitting the conjunction into a nested if. You can use && and coercions into bool to write it with the conjunction intact in only a single if, but I think you'll find this simpler to work with in practice.

Also: You'll probably want to learn about this if you haven't already, and end Cq_dec with Defined. rather than Qed. if you want to actually compute with delay.

Finally: Meven's solution is also fine, although I would recommend working with functions into Prop together with their decidability functions rather than functions into bool with their correctness theorems. One reason is that when destructing on the outputs of decidability functions, you automatically get the proposition or its negation added to your context, whereas if you work with bools, you will have to use the destruct ... eqn: ... variant and then manually apply your correctness theorems to get the same effect.

* Because "P is true" in Coq better translates to "there exists a witness/proof of P," there are indeed propositions in base Coq for which neither it nor its negation has a witness.

Answer 2

Your issue is that you cannot use if statements with propositions (which is what you wrote), but only with booleans. The reason is that, by default, Coq only allows you to write functions which compute, and since not all propositions are decidable, you cannot use case-splits on arbitrary propositions to define a function. There are multiple things you can do, though, depending on the price you want to pay.

If you are content with classical logic, which in essence assumes that all propositions are decidable – but, by doing so, destroys hopes to have well-behaved computation –, you can do the following

Require Import ClassicalDescription.

Fixpoint delay (t:nat) {struct t} : nat :=
  match t with
  | 0 => 0
  | S t => if (excluded_middle_informative ((T (S t)) = 0 /\ ((Cd ((S t) + (delay t) + 1 mod 2)) (S t)))) then (delay t) + 1 else (delay t)
  end.

Otherwise, you will have to pay an extra price. The most natural is to re-express your logic in booleans. Luckily, equality between natural numbers is decidable, and so there is hope – at least, if you can express Cd as a decidable predicate:

Require Import Arith Bool.

Variables Cd : nat -> nat -> bool.
Variables T : nat -> nat.

Locate "=?". (* boolean equality test between natural numbers *)
Locate "&&". (* boolean conjuction *)

Fixpoint delay (t:nat) {struct t} : nat :=
  match t with
  | 0 => 0
  | S t => if (((T (S t)) =? 0) && ((Cd ((S t) + (delay t) + 1 mod 2)) (S t))) then (delay t) + 1 else (delay t)
  end.

Finally, you can also abandon the fact that delay is expressed as a function, and express it as a (functional) relation instead:

Require Import Arith.

Variables Cd : nat -> nat -> Prop.
Variables T : nat -> nat.

Inductive delay : nat -> nat -> Prop :=
  | delay_0 : delay 0 0
  | delay_S_true t r : delay t r -> (T (S t) = 0) /\ (Cd ((S t) + r + 1 mod 2) (S t)) -> delay (S t) (S r)
  | delay_S_false t r : delay t r -> ~ (T (S t) = 0 /\ (Cd ((S t) + r + 1 mod 2) (S t))) -> delay (S t) r.

In general, I would advise to use the boolean version over this one, which is a bit more annoying to use.