Documentation

Archive.Examples.IfNormalization.Statement

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 :

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

Instances For
    def instDecidableEqIfExpr.decEq (x✝ x✝¹ : IfExpr) :
    Decidable (x✝ = x✝¹)
    Equations
    Instances For
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

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

        Equations
        Instances For

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

          Equations
          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
            Instances For

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

              Equations
              Instances For
                def List.disjoint {α : Type u_1} [DecidableEq α] :
                List αList αBool

                A helper function to specify that two lists are disjoint.

                Equations
                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
                  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
                      def IfExpr.eval (f : NatBool) :

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

                      Equations
                      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
                        Instances For