## Stream: Coq users

### Topic: Negative Normal Form as Inductive Proposition

#### Julia Dijkstra (Jan 10 2024 at 22:21):

I thought it might be nice to formalize what it means to be in negative normal form as an inductive proposition. However, when I try to use my definition I cannot seem to prove that it holds for my function `neg_norm`. Did I miss a way of constructing evidence?

``````Fixpoint neg_norm_aux (p: form) (b: bool): form :=
match b with
| true =>
(* Cases with a negation symbol in front. *)
match p with
| FVar sym => <{ ~sym }>
| <{ true }> => <{ false }>
| <{ false }> => <{ true }>
| <{ p /\ q }> => FOr (neg_norm_aux p true) (neg_norm_aux q true)
| <{ p \/ q }> => FAnd (neg_norm_aux p true) (neg_norm_aux q true)
| <{ p -> q }> => FAnd (neg_norm_aux p false) (neg_norm_aux q true)
| <{ ~p }> => neg_norm_aux p false
end
| false =>
(* Cases without a negation symbol in front. *)
match p with
| FVar sym => <{ sym }>
| <{ true }> => <{ true }>
| <{ false }> => <{ false }>
| <{ p /\ q }> => FAnd (neg_norm_aux p false) (neg_norm_aux q false)
| <{ p \/ q }> => FOr (neg_norm_aux p false) (neg_norm_aux q false)
| <{ p -> q }> => FImp (neg_norm_aux p false) (neg_norm_aux q false)
| <{ ~p }> => neg_norm_aux p true
end
end.

Definition neg_norm (p: form): form := neg_norm_aux p false.

Inductive in_neg_norm: form -> Prop :=
| in_neg_norm_var (sym: string): in_neg_norm <{ sym }>
| in_neg_norm_var_neg (sym: string): in_neg_norm <{ ~sym }>
| in_neg_norm_true: in_neg_norm <{ true }>
| in_neg_norm_false: in_neg_norm <{ false }>
| in_neg_norm_and (p q: form): in_neg_norm p /\ in_neg_norm q -> in_neg_norm <{ p /\ q }>
| in_neg_norm_or (p q: form): in_neg_norm p /\ in_neg_norm q -> in_neg_norm <{ p \/ q }>
| in_neg_norm_imp (p q: form): in_neg_norm p /\ in_neg_norm q -> in_neg_norm <{ p -> q }>.

Theorem neg_norm_in_neg_norm (p: form): in_neg_norm (neg_norm p).
Proof.
induction p.
- constructor.
- constructor.
- constructor.
- constructor. split; assumption.
- constructor. split; assumption.
- constructor. split; assumption.
(* Case <{ ~p }> *)
``````

#### Gaëtan Gilbert (Jan 10 2024 at 22:37):

with this sort of thing the proof usually resembles the definition, so you wouldn't directly prove `in_neg_norm (neg_norm p)` by induction
instead you would prove `forall b, in_neg_norm (neg_norm_aux b p)` by induction first

#### Gaëtan Gilbert (Jan 10 2024 at 22:39):

similarly when you want to prove `forall p, p <-> in_neg_form p` you would first prove `forall p b, (if b then ~ p else p) <-> in_neg_form_aux p b`

#### Julia Dijkstra (Jan 10 2024 at 22:42):

Gaëtan Gilbert said:

similarly when you want to prove `forall p, p <-> in_neg_form p` you would first prove `forall p b, (if b then ~ p else p) <-> in_neg_form_aux p b`

I don't quite understand the use of `<->` between formulas and the proposition of being in negative normal form.

Last updated: Jun 13 2024 at 21:01 UTC