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.
Equations
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.hasNestedIf (IfExpr.lit a) = false
- IfExpr.hasNestedIf (IfExpr.var a) = false
- IfExpr.hasNestedIf (IfExpr.ite (IfExpr.ite a a_1 a_2) a_3 a_4) = true
- IfExpr.hasNestedIf (IfExpr.ite a t e) = (IfExpr.hasNestedIf t || IfExpr.hasNestedIf e)
Instances For
An if-expression has a "constant if" if it contains an if-then-else where the "if" is itself a literal.
Equations
- IfExpr.hasConstantIf (IfExpr.lit a) = false
- IfExpr.hasConstantIf (IfExpr.var a) = false
- IfExpr.hasConstantIf (IfExpr.ite (IfExpr.lit a) a_1 a_2) = true
- IfExpr.hasConstantIf (IfExpr.ite i t e) = (IfExpr.hasConstantIf i || IfExpr.hasConstantIf t || IfExpr.hasConstantIf e)
Instances For
An if-expression has a "redundant if" if it contains an if-then-else where the then and else clauses are identical.
Equations
- IfExpr.hasRedundantIf (IfExpr.lit a) = false
- IfExpr.hasRedundantIf (IfExpr.var a) = false
- IfExpr.hasRedundantIf (IfExpr.ite a a_1 a_2) = (a_1 == a_2 || IfExpr.hasRedundantIf a || IfExpr.hasRedundantIf a_1 || IfExpr.hasRedundantIf a_2)
Instances For
All the variables appearing in an if-expressions, read left to right, without removing duplicates.
Equations
- IfExpr.vars (IfExpr.lit a) = []
- IfExpr.vars (IfExpr.var a) = [a]
- IfExpr.vars (IfExpr.ite a a_1 a_2) = IfExpr.vars a ++ IfExpr.vars a_1 ++ IfExpr.vars a_2
Instances For
A helper function to specify that two lists are disjoint.
Equations
- List.disjoint [] x = true
- List.disjoint (x_2 :: xs) x = (decide ¬x_2 ∈ x && List.disjoint xs x)
Instances For
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
- One or more equations did not get rendered due to their size.
- IfExpr.disjoint (IfExpr.lit a) = true
- IfExpr.disjoint (IfExpr.var a) = true
Instances For
An if expression is "normalized" if it has not nested, constant, or redundant ifs, and it evaluates each variable at most once.
Equations
Instances For
The evaluation of an if expresssion at some assignment of variables.
Equations
- IfExpr.eval f (IfExpr.lit a) = a
- IfExpr.eval f (IfExpr.var a) = f a
- IfExpr.eval f (IfExpr.ite a a_1 a_2) = bif IfExpr.eval f a then IfExpr.eval f a_1 else IfExpr.eval f a_2
Instances For
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
- One or more equations did not get rendered due to their size.