termination of conversion to negation normal form

Stream: general

[Paige Thomas]

I was wondering if someone might have a suggestion for how to go about proving that this terminates:

import Mathlib.Util.CompileInductive

inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  | forall_ : String → Formula_ → Formula_
  | exists_ : String → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Repr

compile_inductive% Formula_

open Formula_

def to_nnf :
  Formula_ → Formula_
  | and_ phi psi => and_ (to_nnf phi) (to_nnf psi)
  | or_ phi psi => or_ (to_nnf phi) (to_nnf psi)
  | imp_ phi psi => or_ (to_nnf (not_ phi)) (to_nnf psi)
  | iff_ phi psi => or_ (and_ (to_nnf phi) (to_nnf psi)) (and_ (to_nnf (not_ phi)) (to_nnf (not_ psi)))
  | not_ (not_ phi) => to_nnf phi
  | not_ (and_ phi psi) => or_ (to_nnf (not_ phi)) (to_nnf (not_ psi))
  | not_ (or_ phi psi) => and_ (to_nnf (not_ phi)) (to_nnf (not_ psi))
  | not_ (imp_ phi psi) => and_ (to_nnf phi) (to_nnf (not_ psi))
  | not_ (iff_ phi psi) => or_ (and_ (to_nnf phi) (to_nnf (not_ psi))) (and_ (to_nnf (not_ phi)) (to_nnf psi))
  | phi => phi

[Paige Thomas]

The issue seems to be the calls of the form to_nnf (not_ phi) and to_nnf (not_ psi) on the rhs.

[Joachim Breitner]

Right, these aren't obviously smaller, are they?
If you specify termination_by f => f then you should get better error messagea about what could not be solved here. Maybe you need a custom measure that really is decreasing.

[Joachim Breitner]

Alternatively and maybe cleaner: write two mutually recursive functions, to_nnf and to_nnf_neg. Then you might even get away with structural recursion!

[Joachim Breitner]

Oh, yes, the imp case will clearly make it hard to get your current definition through, at least without a very carefully crafted measure that makes not cheap and imp expensive. Try the mutual variant!

[Joachim Breitner]

And read https://lean-lang.org/blog/2024-1-11-recursive-definitions-in-lean/ if you haven't already!

[Paige Thomas]

Do you mean one that translates a formula F and another that translates not F?

[Paige Thomas]

I see. I'll give it a try. Thank you!

[Joachim Breitner]

Right. This way you should never have to make bigger arguments in the recursive calls

[Paige Thomas]

This seems to type check. I'll have to prove some properties to make sure it means the same thing.

import Mathlib.Util.CompileInductive

inductive Formula_ : Type
  | false_ : Formula_
  | true_ : Formula_
  | atom_ : String → Formula_
  | not_ : Formula_ → Formula_
  | and_ : Formula_ → Formula_ → Formula_
  | or_ : Formula_ → Formula_ → Formula_
  | imp_ : Formula_ → Formula_ → Formula_
  | iff_ : Formula_ → Formula_ → Formula_
  | forall_ : String → Formula_ → Formula_
  | exists_ : String → Formula_ → Formula_
  deriving Inhabited, DecidableEq, Repr

compile_inductive% Formula_

open Formula_

mutual
def to_nnf :
  Formula_ → Formula_
  | and_ phi psi => and_ (to_nnf phi) (to_nnf psi)
  | or_ phi psi => or_ (to_nnf phi) (to_nnf psi)
  | imp_ phi psi => or_ (to_nnf_neg phi) (to_nnf psi)
  | iff_ phi psi => or_ (and_ (to_nnf phi) (to_nnf psi)) (and_ (to_nnf_neg phi) (to_nnf_neg psi))
  | not_ (not_ phi) => to_nnf phi
  | not_ (and_ phi psi) => or_ (to_nnf_neg phi) (to_nnf_neg psi)
  | not_ (or_ phi psi) => and_ (to_nnf_neg phi) (to_nnf_neg psi)
  | not_ (imp_ phi psi) => and_ (to_nnf phi) (to_nnf_neg psi)
  | not_ (iff_ phi psi) => or_ (and_ (to_nnf phi) (to_nnf_neg psi)) (and_ (to_nnf_neg phi) (to_nnf psi))
  | phi => phi

def to_nnf_neg :
  Formula_ → Formula_
  | (not_ phi) => to_nnf phi
  | (and_ phi psi) => or_ (to_nnf_neg phi) (to_nnf_neg psi)
  | (or_ phi psi) => and_ (to_nnf_neg phi) (to_nnf_neg psi)
  | (imp_ phi psi) => and_ (to_nnf phi) (to_nnf_neg psi)
  | (iff_ phi psi) => or_ (and_ (to_nnf phi) (to_nnf_neg psi)) (and_ (to_nnf_neg phi) (to_nnf psi))
  | phi => not_ phi
end

#eval to_nnf false_
#eval to_nnf (not_ false_)
#eval to_nnf (not_ (not_ false_))
#eval to_nnf (not_ (not_ (not_ false_)))
#eval to_nnf (not_ (not_ (not_ (not_ false_))))

[Joachim Breitner]

I’d replace

  | not_ (not_ phi) => to_nnf phi
  | not_ (and_ phi psi) => or_ (to_nnf_neg phi) (to_nnf_neg psi)
  | not_ (or_ phi psi) => and_ (to_nnf_neg phi) (to_nnf_neg psi)
  | not_ (imp_ phi psi) => and_ (to_nnf phi) (to_nnf_neg psi)
  | not_ (iff_ phi psi) => or_ (and_ (to_nnf phi) (to_nnf_neg psi)) (and_ (to_nnf_neg phi) (to_nnf psi))

with

  | not_ phi => to_nnf_not phi

no need to duplicate that logic!

[Paige Thomas]

That did seem to be odd to me.

[Joachim Breitner]

Hmm, why? Seems natural to me. After all, to_nnf_not phi is meant to be the helper to implement to_nnf (not phi)

[Paige Thomas]

No, I mean it seemed odd to have the same logic twice.

[Paige Thomas]

Cool. Thank you!