Rustan's challenge

Stream: general

[Leonardo de Moura]

Rustan Leino is a famous computer scientist and a long time friend of mine. In a recent trip, he talked with Shankar and Stephan Merz about some challenge problem that could be used to compare proof assistants. Surely, one would need to have many different kinds of problems for a good comparison. Still, Shankar was excited to suggest “if normalization”, so the 3 of them have been discussing versions to solve this in PVS, Isabelle, and Dafny. Today, Rustan asked me if the Lean community would be interested in the challenge :)
Here is the summary he shared with me:
The data structure is an Expression with boolean literals, variables, and if-then-else expressions.
The goal is to normalize such expressions into a form where:
a) No nested ifs: That is, the condition part of an if-expression is not itself an if-expression
b) No constant tests: That is, the condition part of an if-expression is not a constant
c) No redundant if’s: That is, the then and else branches of an if are not the same
d) Each variable is evaluated at most once: That is, the free variables of the condition are disjoint from those in the then branch, and also disjoint from those in the else branch.
One should show that a normalization function produces an expression satisfying (a,b,c,d), and one should also prove that the normalization function preserves the meaning of the given expression.

[Jason Rute]

Is it just a programming problem, i.e. converting the input data structure to the desired output? Or is the goal to produce a formally verified algorithm? Or is the goal to use Lean's framework more directly in the solution (say producing a tactic that reduces on a Lean term of the right form, i.e. a shallow embedding of the input data structure)?

[Jason Rute]

Oh, I didn't read the last line. :face_palm:

[Jineon Baek]

So no boolean operations between literals and variables are made?

[Joe Hendrix]

Seems like a request for verified BDD algorithm.

[Scott Morrison]

I think this is the problem statement, if you prefer your statements pre-formalized. :-)

inductive E
| lit : Bool → E
| var : Nat → E
| ite : E → E → E → E
deriving BEq

def E.hasNestedIf : E → Bool
| lit _ => false
| var _ => false
| ite (ite _ _ _) _ _ => true
| ite _ t e => t.hasNestedIf || e.hasNestedIf

def E.hasConstantIf : E → Bool
| lit _ => false
| var _ => false
| ite (lit _) _ _ => true
| ite i t e => i.hasConstantIf || t.hasConstantIf || e.hasConstantIf

def E.hasRedundantIf : E → Bool
| lit _ => false
| var _ => false
| ite i t e => t == e || i.hasRedundantIf || t.hasRedundantIf || e.hasRedundantIf

def E.vars : E → List Nat
| lit _ => []
| var i => [i]
| ite i t e => i.vars ++ t.vars ++ e.vars

def List.disjoint : List Nat → List Nat → Bool
| [], _ => true
| (x::xs), ys => x ∉ ys && xs.disjoint ys

def E.disjoint : E → Bool
| lit _ => true
| var _ => true
| ite i t e =>
    i.vars.disjoint t.vars && i.vars.disjoint e.vars && i.disjoint && t.disjoint && e.disjoint

def E.normalized (e : E) : Bool :=
  !e.hasNestedIf && !e.hasConstantIf && !e.hasRedundantIf && e.disjoint

def E.eval (f : Nat → Bool) : E → Bool
| lit b => b
| var i => f i
| ite i t e => bif i.eval f then t.eval f else e.eval f

def IfNormalization : Type := { Z : E → E // ∀ e, (Z e).normalized ∧ ∀ f, (Z e).eval f = e.eval f }

example : IfNormalization := sorry

-- Bonus points for functions `E → Syntax` and `Syntax → E`
-- and a code action that runs normalization! :-)

[Andrés Goens]

@Scott Morrison I'm curious why you formalize the properties in Bool and not Prop, is there a concrete reason or was it just faster to write it that way for the example?

[Scott Morrison]

We're talking to some computer scientists here. They might want to run the code! :-)

[Scott Morrison]

(Of course, we could provide Decidable instances, but Bool from the beginning is easier?)

[Andrés Goens]

yeah, that makes sense, but if you're proving that the normalization function does its job you'll have to go there anyway! I guess showing E.hasNestedIf = false, etc works too (I was just checking whether there was another underlying reason)

[Nathaniel Burke]

For point c), is "the same" considering the truth table or the exact syntactic structure of the sub-expressions?

For example, using xn for variables, would if x0 then (if x1 then x2 else x3) else false be considered "the same" as if x1 then (if x0 then x2 else false) else (if x0 then x3) else false

[Chris Hughes]

I proved you can produce a disjoint expression with the same semantics. I think I will stop for today now, but anyone can feel free to take over. https://gist.github.com/ChrisHughes24/f278f2b22474c001565b672ab2d7f1d0 It's done in a way that does not introduce nestedIfs, so it should be possible to remove the nestedIfs first, and then remove constantIfs and redundantIfs afterwards I think.

[Chris Hughes]

Okay, I finished. Not the most beautiful code right now, maybe I will tidy it up https://gist.github.com/ChrisHughes24/f278f2b22474c001565b672ab2d7f1d0

[Eric Wieser]

Can you rename the file to .lean so that it syntax-highlights?

[Scott Morrison]

This is really great, Chris! The fast turnaround time on challenges is becoming a hallmark of Lean. :-)

[Scott Morrison]

It would be amazing if Chris and/or others want to continue working on this, and producing something polished!

(And maybe even performant? I haven't looked at Chris's code.)

We suspect the other systems that Leo mentions in the top post are going to try to come up with very clean solutions, and it would be great if we look at least as nice. :-)

[Kevin Buzzard]

I am reminded of Larry Paulson's remark in a talk at a conference, saying that cubing the cube had never been formalised, and me announcing @Floris van Doorn 's formalisation in my talk two days later :-)

[Wojciech Nawrocki]

And here is another solution :) I define a normalization relation in the style of big-step operational semantics, a predicate for normal forms, prove that normal forms have the desired properties, prove that the results of normalization are normal, and then implement the normalization relation as a computable function with some slightly weird termination measure. Mostly its lots and lots of repetitive inductions which I wish I knew how to make shorter: e.g. in Norm.preservation, the cases differ only in where in the context some variable that I want to give a name to is, but named variable syntax in induction doesn't seem to be supported (induction h with | pat (x := x) => ..). Also the norm function technically has two sorries in it due to (kernel) invalid projection (perhaps this?).

[Wojciech Nawrocki]

(And maybe even performant? I haven't looked at Chris's code.)

If you want to actually normalize large Boolean formulas in practice, BDDs are the way to go. But it would be rather more work to verify a BDD package.

[Scott Morrison]

@Wojciech Nawrocki, what did you want to write at your sorrys? The thing you have commented out gives invalid field 'ite_inversion'.

[Wojciech Nawrocki]

Scott Morrison said:

Wojciech Nawrocki, what did you want to write at your sorrys? The thing you have commented out gives invalid field 'ite_inversion'.

Oops! Fixed.

[Chris Hughes]

I have a much cleaner, shorter, and faster version here

[Wojciech Nawrocki]

Wow, this is really short! I'm amazed the default tactic can prove all the termination goals.

[Chris Hughes]

The default tactic includes simp and I strategically added some simp lemmas on line 51

[Scott Morrison]

@Chris Hughes, I hope you won't mind that I took the liberty of polishing this slightly further, and really trying to show off aesop.

I made a PR at #8035. If you'd like to make further changes please do so, of course!!

[Chris Hughes]

I have too say as well, that although mine is very short, it maybe goes against the mathlib principle of building up the correct API. I suspect if you really wanted the fastest procedure, then the code would be more complicated and you'd need a better API, and something like Wojciech's Norm relation might be very useful.