# Best practices: Should I prefer definitions or iff when defining predicates?

I am a beginner in Coq, and I have a proposition I defined in this way:

Variables PA : nat -> Prop.
Variables PB PC : nat -> nat -> Prop.

Hypothesis A_def : forall t : nat, (PA (S t)) <-> exists x: nat, ((PC x) t) /\ ~ ((PB x) t).


I feel like I may have made a mistake here in not using a definition instead, but I don't really know. One issue I have here is that PA 0 is intentionally undefined, so if I were to write a definition instead, would I have to use an unbound variable for PA 0 or how would that look?

I'd like some advice on whether definitions are preferable to this type of "definition" with iff, and how to write the defintion with an undefined PA 0.

• For us to intelligently answer this question, please explain what you're doing. Is this part of a formalization project, and if so what? What is the role of PB and PC, where do they come from? Commented Jun 28 at 9:42
• @AndrejBauer I am analyzing the behavior of a time sequence that doesn't have a clearly defined beginning, PB and PC are other Predicates/Sequences that are defined similarly. There are 6 such sequences in total that are defined in terms of each other. So I have similar iff constructions that relate the sequences value at time (S t) to the value of the other sequences at time t. But the value of the sequence at t= 0 is deliberately undefined, I want to reason regardless of starting conditions. Commented Jun 28 at 10:10
• You can just have an additional parameter that specifies the value of the time series in the beginning, see my answer. Commented Jun 28 at 13:39

Without knowing more, I will say that you should use a definition because Coq will use it automatically.

How you want to treat PB and PC depends on what you are doing. Below I am showing that you can use the Section mechanism to introduce PB and PC as (undefined) free parameters inside a section. These become parameters to PA once the section is closed. It's a common technique.

We also intrpuce a parameter P0 : Prop which is used as the undetermined value of P 0.

Section MySection.
Variable P0 : Prop.

Variable PB PC : nat -> nat -> Prop.

Definition PA (t : nat) : Prop :=
match t with
| 0 => P0
| S t => exists x : nat, (PC x t /\ ~ PB x t)
end.

(* Inside the section, the type of PA is nat -> Prop. *)
Check PA. (* outputs nat -> Prop *)

Eval compute in (PA 0).
(* outputs: P0 *)

Eval compute in (PA 3).
(* output: exists x : nat, PC x 2 /\ (PB x 2 -> False) *)

Check PB. (* outputs nat -> nat -> Prop *)

End MySection.

(* When we closed the section, the free variables PB, PC and P0 disappeared. *)
(* Does not work: Check PB. *)

(* PB and PC have become parameteres to PA,
so if we check the type of PA again, we see it changed. *)
Check PA.  (* outputs: Prop -> (nat -> nat -> Prop) -> (nat -> nat -> Prop) -> nat -> Prop *)

(* Consequently, PA 0 does not work anymore because PA now wants three arguments. *)
(* Does not work: Check PA 0. *)

(* But we can provide specific P0, PB and PC. Here we instantiate P0 := True,
PB (m, n) := (m < n + 13) and PC (m, n) := (n + 3 = m). *)
Check PA True (fun m n => m < n + 13) (fun m n => n + 3 = m) 0.

Eval compute in PA True (fun m n => m < n + 13) (fun m n => n + 3 = m) 3.
(* outputs: exists x : nat, 5 = x /\ (S x <= 15 -> False) *)

• The problem I have with that is that I need to relate (PA (S t)) and (PB t), (PC t). It's a time series. Commented Jun 28 at 10:13
• Oops, sorry, I missed the S in S t. Commented Jun 28 at 13:31
• I amended the answer so that PA 0 is undetermined, and PA (S t) is what you wanted to have. Whether this solution works for you depends on what you want to do with your time series. It would really help if you explained your wider goals (not here, but by editing your original question). Commented Jun 28 at 13:38