Stream: Coq users

Topic: Negation Normal Form as Inductive Proposition

Julia Dijkstra (Jan 10 2024 at 23:06):

I renamed `in_neg_norm` to `in_nnf` to be less confusing.

Julia Dijkstra (Jan 10 2024 at 23:09):

It would probably be better practice to return an `nnf_form` type instead that inherently shows only literals can have a negation sign now that I think a little more on it.

Julia Dijkstra (Jan 11 2024 at 00:01):

I rewrote it like I mentioned, but now I wonder if Coq allows me to make the notation a bit prettier. In particular it would be awesome if it could parse `<[ sym ]>` as `NVar sym false`. I only managed to get it working for the negated variant.

``````Inductive nnf_form: Type :=
| NVar (sym: string) (sign: bool)
| NTrue
| NFalse
| NAnd (p q: nnf_form)
| NOr (p q: nnf_form).

(* Declare notation to simplify working with nnf formulas. *)
Declare Custom Entry sat_nnf.
Declare Scope sat_nnf_scope.
Declare Custom Entry sat_nnf_aux.

Notation "<[ e ]>" := e (e custom sat_nnf_aux) : sat_nnf_scope.
Notation "e" := e (in custom sat_nnf_aux at level 0, e custom sat_nnf) : sat_nnf_scope.

Notation "( x )" := x (in custom sat_nnf, x at level 99) : sat_nnf_scope.
Notation "x" := x (in custom sat_nnf at level 0, x constr at level 0) : sat_nnf_scope.

Notation "'true'" := NTrue (in custom sat_nnf at level 0).
Notation "'false'" := NFalse (in custom sat_nnf at level 0).

Notation "~ x" := (NVar x true) (in custom sat_nnf at level 5, right associativity).
Notation "p /\ q" := (NAnd p q) (in custom sat_nnf at level 10, left associativity).
Notation "p \/ q" := (NOr p q) (in custom sat_nnf at level 15, left associativity).

Open Scope sat_nnf_scope.
``````

Last updated: Jun 13 2024 at 19:02 UTC