Documentation

Archive.Examples.IfNormalization.Result

A solution to the if normalization challenge in Lean. #

See Statement.lean for background.

source
def «tactic◾» :
Lean.ParserDescr
Equations
Instances For
    source
    def «term◾» :
    Lean.ParserDescr
    Equations
    Instances For

      We add some local simp lemmas so we can unfold the definitions of the normalization condition.

      Simp lemmas for eval. We don't want a simp lemma for (ite i t e).eval in general, only once we know the shape of i.

      source
      @[simp]
      theorem IfExpr.eval_lit {b : Bool} {f : ℕ → Bool} :
      eval f (lit b) = b
      source
      @[simp]
      theorem IfExpr.eval_var {f : ℕ → Bool} {i : ℕ} :
      eval f (var i) = f i
      source
      @[simp]
      theorem IfExpr.eval_ite_lit {b : Bool} {f : ℕ → Bool} {t e : IfExpr} :
      eval f ((lit b).ite t e) = bif b then eval f t else eval f e
      source
      @[simp]
      theorem IfExpr.eval_ite_var {f : ℕ → Bool} {i : ℕ} {t e : IfExpr} :
      eval f ((var i).ite t e) = bif f i then eval f t else eval f e
      source
      @[simp]
      theorem IfExpr.eval_ite_ite {f : ℕ → Bool} {a b c d e : IfExpr} :
      eval f ((a.ite b c).ite d e) = eval f (a.ite (b.ite d e) (c.ite d e))
      source
      def IfExpr.normSize :
      IfExpr → ℕ

      Custom size function for if-expressions, used for proving termination.

      Equations
      Instances For
        source
        @[irreducible]
        def IfExpr.normalize (l : AList fun (x : ℕ) => Bool) (e : IfExpr) :
        { e' : IfExpr // (∀ (f : ℕ → Bool), eval f e' = eval (fun (w : ℕ) => (AList.lookup w l).elim (f w) id) e) ∧ e'.normalized = true ∧ ∀ v ∈ e'.vars, AList.lookup v l = none }

        Normalizes the expression at the same time as assigning all variables in e to the literal booleans given by l

        Equations
        Instances For