Stream: Coq users

Topic: Negative Normal Form as Inductive Proposition


view this post on Zulip 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 }> *)
    - admit.
Admitted.

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

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

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