Zulip Chat Archive

Stream: new members

Topic: trouble with induction proof


Henkie67 (Jan 31 2023 at 17:31):

Hello there, I have a function norm_neg which transforms a boolean formula into its negation normal form(only have negations on variables) and a function valid which evaluates formulas. both functions use the inductive form which represents its formula. As a final assignment i need to prove the correctness of norm_neg which I figured I would do by proving that valid V p -> valid V norm_neg(p) or if formula p is valid it is also valid in negation normal form. I have managed to solver the first 5 cases (var,true,false,and,or) but the last ones require more effort due to the fact they have multiple cases in norm_neg. I have tried both induction and cases but still fail to see a way to prove it with the given induction hypothesis so I am wondering if there is a different way to handle this.

Patrick Johnson (Jan 31 2023 at 18:03):

You need to prove other theorems about valid that let you rewrite the terms. For example, you may need

example {V : valuation} {a b : form} : valid V (a.Ffor b)  valid V (a.Fneg.Fimpl b) := sorry

and

example {V : valuation} {a : form} : valid V a.Fneg.Fneg  valid V a := sorry

and similar theorems, so that you can transform the goal state by rewriting using those theorems. Try to write your proof on paper and then translate it to Lean. That's usually the best approach.

Henkie67 (Jan 31 2023 at 19:32):

I am trying but for some cases I am having trouble deducing them

Henkie67 (Jan 31 2023 at 19:50):

ik keep getting this
image.png

Patrick Johnson (Jan 31 2023 at 20:32):

That goal can be solved by rwa [or_iff_not_imp_left, eq_tt_eq_not_eq_ff]


Last updated: Dec 20 2023 at 11:08 UTC