If normalization

Rustan Leino, Stephan Merz, and Natarajan Shankar have recently been discussing challenge problems to compare proof assistants. (See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Rustan's.20challenge)

Their first suggestion was "if-normalization".

This file contains a Lean formulation of the problem. See Result.lean for a Lean solution.

inductive IfExpr : Type

An if-expression is either boolean literal, a numbered variable, or an if-then-else expression where each subexpression is an if-expression.

• lit: Bool → IfExpr
• var: Nat → IfExpr
• ite: IfExpr → IfExpr → IfExpr → IfExpr

instance instDecidableEqIfExpr : DecidableEq IfExpr

Equations

• instDecidableEqIfExpr = decEqIfExpr✝

instance instReprIfExpr : Repr IfExpr

Equations

• instReprIfExpr = { reprPrec := reprIfExpr✝ }

def IfExpr.hasNestedIf : IfExpr → Bool

An if-expression has a "nested if" if it contains an if-then-else where the "if" is itself an if-then-else.

Equations

• (IfExpr.lit a).hasNestedIf = false
• (IfExpr.var a).hasNestedIf = false
• ((a.ite a_1 a_2).ite a_3 a_4).hasNestedIf = true
• (a.ite t e).hasNestedIf = (t.hasNestedIf || e.hasNestedIf)

def IfExpr.hasConstantIf : IfExpr → Bool

An if-expression has a "constant if" if it contains an if-then-else where the "if" is itself a literal.

Equations

• (IfExpr.lit a).hasConstantIf = false
• (IfExpr.var a).hasConstantIf = false
• ((IfExpr.lit a).ite a_1 a_2).hasConstantIf = true
• (i.ite t e).hasConstantIf = (i.hasConstantIf || t.hasConstantIf || e.hasConstantIf)

def IfExpr.hasRedundantIf : IfExpr → Bool

An if-expression has a "redundant if" if it contains an if-then-else where the then and else clauses are identical.

Equations

• (IfExpr.lit a).hasRedundantIf = false
• (IfExpr.var a).hasRedundantIf = false
• (a.ite a_1 a_2).hasRedundantIf = (a_1 == a_2 || a.hasRedundantIf || a_1.hasRedundantIf || a_2.hasRedundantIf)

def IfExpr.vars : IfExpr → List Nat

All the variables appearing in an if-expressions, read left to right, without removing duplicates.

Equations

• (IfExpr.lit a).vars = []
• (IfExpr.var a).vars = [a]
• (a.ite a_1 a_2).vars = a.vars ++ a_1.vars ++ a_2.vars

def List.disjoint {α : Type u_1} [DecidableEq α] : List α → List α → Bool

A helper function to specify that two lists are disjoint.

Equations

• [].disjoint x = true
• (x_2 :: xs).disjoint x = (decide ¬x_2 ∈ x && xs.disjoint x)

def IfExpr.disjoint : IfExpr → Bool

An if expression evaluates each variable at most once if for each if-then-else the variables in the if clause are disjoint from the variables in the then clause, and the variables in the if clause are disjoint from the variables in the else clause.

Equations

• (IfExpr.lit a).disjoint = true
• (IfExpr.var a).disjoint = true
• (a.ite a_1 a_2).disjoint = (a.vars.disjoint a_1.vars && a.vars.disjoint a_2.vars && a.disjoint && a_1.disjoint && a_2.disjoint)

def IfExpr.normalized (e : IfExpr) : Bool

An if expression is "normalized" if it has not nested, constant, or redundant ifs, and it evaluates each variable at most once.

Equations

• e.normalized = (!e.hasNestedIf && !e.hasConstantIf && !e.hasRedundantIf && e.disjoint)

def IfExpr.eval (f : Nat → Bool) : IfExpr → Bool

The evaluation of an if expression at some assignment of variables.

Equations

• IfExpr.eval f (IfExpr.lit a) = a
• IfExpr.eval f (IfExpr.var a) = f a
• IfExpr.eval f (a.ite a_1 a_2) = bif IfExpr.eval f a then IfExpr.eval f a_1 else IfExpr.eval f a_2

def IfNormalization : Type

This is the statement of the if normalization problem.

We require a function from that transforms if expressions to normalized if expressions, preserving all evaluations.

Equations

• IfNormalization = { Z : IfExpr → IfExpr // ∀ (e : IfExpr), (Z e).normalized = true ∧ (fun (f : Nat → Bool) => IfExpr.eval f (Z e)) = fun (f : Nat → Bool) => IfExpr.eval f e }