Stream: Coq users

Topic: Negation Normal Form as Inductive Proposition


view this post on Zulip Julia Dijkstra (Jan 10 2024 at 23:06):

I renamed in_neg_norm to in_nnf to be less confusing.

view this post on Zulip 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.

view this post on Zulip 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