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

Question

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.

Answer 1

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) *)