# Using if in Fixpoint

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.

• Can you provide a minimal working example that we can run? Probably, one where Cd and T are given as variables (if their content does not influence the question) or defined (if it does). Commented Jul 1 at 9:34
• @MevenLennon-Bertrand Added the variable declarations, there is nothing else relevant between those and the Fixpoint definition. Commented Jul 1 at 9:37
• Almost there: where does mod come from? (You probably want to add an import) Commented Jul 1 at 9:44
• @MevenLennon-Bertrand Fair, fixed. Commented Jul 1 at 9:46
• You do realize that x + 1 mod 2 is equal to x + (1 mod 2) = x + 1? Commented Jul 1 at 11:00

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 }.

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.

• Thanks, I understand now the issue with decidability, I think (although I am not certain why the proof system needs to care about decidability). All my stuff is trivially decidable though, I know the values at every t. Commented Jul 2 at 7:15
• Also, I don't understand what is going on with cd_dec here. It looks like a definition to tell that law of excluded middle holds for Cd (actually, that it's either provable or disprovable I guess), but then it's instantiated and supposed to be the decidable version of Cd? How does that work? Commented Jul 2 at 7:26
• To your first comment: It's not so much the proof system stopping you here, but rather the notion of computability. Compared to other theorem provers, Coq places a heavy emphasis on the ability to extract real, working code (by default, either OCaml or Haskell, with the Extraction command) from Definitions and Fixpoints. You cannot do this if you rely on noncomputable properties. Moreover, even noncomputably, how should you expect a definition like if ContinuumHypothesis then 1 else 0 to work? Neither ContinuumHypothesis nor ~ContinuumHypothesis holds in Coq! Commented Jul 2 at 7:59
• To your second: Compare the type of my Cd_dec above (which returns sumbool (Cd n m) (~Cd n m)) with the similar type forall m n, Cd n m \/ ~Cd n m, which is a Prop. Why does Coq like sumbools but not Props in definitions? The answer is that a sumbool P Q represents a boolean value paired with either a proof of P (if true) or a proof of Q (if false). The boolean part of Cd_dec is (must be) computable, while the proof of P or Q is literally stripped away during extraction. See softwarefoundations.cis.upenn.edu/draft/vfa-current/Decide.html for more! Commented Jul 2 at 8:09
• Good question: if X then Y else Z is just syntactic sugar for a match statement on any type with two constructors! So, there's nothing actually special here happening with sumbool, it's an entirely generic thing with if-then in Coq. You can also see how, for example, if (nil : list nat) then 1 else 0 = 1, where nil is the empty list. With that said, I've never seen real usage of it besides for bools and sumbools. Commented Jul 2 at 8:21

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.

• So, if I have excluded middle (this is what propositions being decidable means, right?), the easiest for reasoning is your first example? I just want a nicer replacement for the hypotheses I currently use to define delay, but if the replacement is more awkward I can also stick with those. Commented Jul 1 at 10:49
• @kutschkem: Once again, if you explain what you're trying to do, we can offer better advice. Without further information, the answer is "do not use excluded middle, you will regret it". Please describe the overall problem domain. What does T stand for? What sort of things is Cd? Commented Jul 1 at 10:56
• "classical logic ... destroys hopes to have well-behaved computation" is the least of the problems with classical logic and quite and understatement... Commented Jul 1 at 10:58
• @JulioDiEgidio I did not want to make this a holy war about classical logic. In this particular case, classical logic is one way to solve the issue, although I agree it might not be the best. But it is definitely a possibility worth mentioning, and for some purposes is good enough. Commented Jul 1 at 11:52
• "To not deny is to assert" I think is already a better characterization. I don't mean a holy war, indeed I only said yours was an understatement: IMO that is a critical point though, maybe even a crucial one, as for understanding what is what. -- Anyway, just an observation/remark on that specific point, indeed I have no qualms with your answer overall. Commented Jul 1 at 12:02