trouble with induction proof

Stream: new members

[Henkie67]

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.

import tactic


inductive form:Type
|Fvar:string->form
|Ftrue:form
|Ffalse:form
|Fand:form->form->form
|Ffor:form->form->form
|Fimpl:form->form->form
|Fneg:form->form


def valuation: Type := string->bool

def valid'(V : valuation): form->bool
  |(form.Fvar x):= V x
  |form.Ftrue := true
  |form.Ffalse := false
  |(form.Fand f1 f2):= (valid' f1) ∧ (valid' f2)
  |(form.Ffor f1 f2):= (valid' f1) ∨ (valid' f2)
  |(form.Fneg f1):= ¬(valid' f1)
  |(form.Fimpl f1 f2):= (valid' f1) -> (valid' f2)




def valid (V : valuation) (p : form) : Prop:= valid' V p
def norm_neg: form->form
|(form.Fneg(form.Fneg f1)):= norm_neg(f1)
|(form.Fneg(form.Fand f1 f2)):= form.Ffor(norm_neg(form.Fneg  f1))(norm_neg(form.Fneg  f2))
|(form.Fneg(form.Ffor f1 f2)):= form.Fand(norm_neg(form.Fneg  f1))(norm_neg(form.Fneg  f2))
|(form.Fneg(form.Fimpl f1 f2)):= form.Fand(norm_neg f1) (norm_neg (form.Fneg f2))
|(form.Fand f1 f2):= form.Fand (norm_neg f1) (norm_neg f2)
|(form.Ffor f1 f2):= form.Ffor (norm_neg f1) (norm_neg f2)
|(form.Fimpl (form.Fneg f1) f2):=form.Ffor (norm_neg f1) (norm_neg f2)
|(form.Fimpl (form.Fand f11 f12) f2):=form.Ffor (form.Ffor(norm_neg (form.Fneg f11)) (norm_neg(form.Fneg f12))) (norm_neg f2)
|(form.Fimpl (form.Ffor f11 f12) f2):=form.Ffor (form.Fand(norm_neg (form.Fneg f11)) (norm_neg(form.Fneg f12))) (norm_neg f2)
|(form.Fimpl (form.Fimpl f11 f12) f2):=form.Ffor (form.Fneg(form.Ffor (norm_neg (form.Fneg f11)) (norm_neg f12))) (norm_neg f2)
|(form.Fimpl f1 f2):= form.Ffor(form.Fneg  f1)(norm_neg  f2)
| x := x


lemma correct_norm(p:form)(V:valuation): valid V p -> valid V (norm_neg(p)):=
begin
induction p with a b c ih1 ih2 aa bb ih_aa ih_bb cc dd ih_cc ih_dd,
repeat{ --Var,True and False
  intro sat,
  simp[norm_neg],
  exact sat
},
{--And
  intro sat,
  simp[norm_neg],
  simp[valid',valid],
  simp[valid,valid'] at sat,
  apply and.intro,
  {apply ih1,
  rw valid,
  exact sat.left},
  {apply ih2,
  rw valid,
  exact sat.right}
},
{--Or
  intro sat,
  simp[norm_neg],
  simp[valid',valid],
  simp[valid,valid'] at sat,
  cases sat,
  {apply or.intro_left,
   apply ih_aa,
   rw valid,
   exact sat},
    {apply or.intro_right,
   apply ih_bb,
   rw valid,
   exact sat}
},
{--Implies
  sorry
},
{--Not
  sorry
}


end

[Patrick Johnson]

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]

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

[Henkie67]

ik keep getting this
image.png

[Patrick Johnson]

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