Stream: Coq users

Topic: ✔ Cannot Rewrite and Unsure Why


view this post on Zulip Notification Bot (Jan 07 2024 at 14:09):

Julia Dijkstra has marked this topic as resolved.

view this post on Zulip Julia Dijkstra (Jan 08 2024 at 12:11):

I still had to resort to doing this to rewrite , since the tactic did not work.

Theorem norm_neg_correct: forall (p: form) (V: valuation), valid' V (norm_neg p) = valid' V p.

Lemma norm_neg_correct_fun: forall (p: form),
    (fun V => valid' V (norm_neg p)) = (fun V => valid' V p).
Proof.
    intros. apply functional_extensionality. intros. apply norm_neg_correct.
Qed.

Last updated: Jun 23 2024 at 04:03 UTC