Inductive predicates vs Fixpoints

[radeusgd]

The first intuition when defining some property, like 'isvalue' is to use an Inductive predicate.

For example:

Inductive isvalue : typedterm -> Prop :=
| Val_Nat : forall n T, isvalue (Nat n : T)
| Val_Lam : forall t T1 T, isvalue (Lam T1 t : T)
| Val_Box : forall t T, isplain t -> isvalue (Quote t : T).

This makes it easy to use in theorem statements (just use isvalue t) and looks nice. However it proves troublesome when we need to prove and assume negation, I haven't analysed deeply the core reasons for that, but I think it is because Coq uses constructive/intuitionistic logic and negation has sometimes unusual properties there.

So in case of such predicates it may be better to use a fixpoint definition (it's not always possible but works ok for simple properties) - it's advantage is that we get a boolean value and it works with negation without issues.

For example:

Fixpoint decide_isvalue (t : typedterm) : bool :=
  match t with
  | TypedTerm t' _ =>
    match t' with
    | Nat _ => true
    | Lam _ ebody => true
    | Quote t => decide_isplain t
    | _ => false
    end
  end.

A disadvantage is that some proofs that were trivial with the inductive predicate (using inversion tactic) now may not work, but usually they can usually be fixed with clever usage cbn and cbv.