Trigger CI for leanprover/lean4#2749

.github/workflows/bors.yml

@@ -256,10 +256,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker

.github/workflows/build.yml

@@ -16,6 +16,7 @@ on:
       - 'nolints'
       # ignore staging branch used by bors, this is handled by bors.yml
       - 'staging'
+  merge_group:
 
 name: continuous integration
 
@@ -262,10 +263,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker

.github/workflows/build.yml.in

@@ -242,10 +242,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker

.github/workflows/build_fork.yml

@@ -260,10 +260,7 @@ jobs:
         run: |
           git clone https://github.com/leanprover/lean4checker
           cd lean4checker
-          # Because `Lean4Checker/Tests/ReduceBool.lean` is non-deterministic (compiles only 1/4 of the time),
-          # we just keep rebuilding until it works!
-          # I'll try to come up with something better.
-          until lake build > /dev/null 2>&1; do :; done
+          lake build
           ./test.sh
           cd ..
           lake env lean4checker/build/bin/lean4checker

.github/workflows/mk_build_yml.sh

@@ -28,6 +28,7 @@ on:
       - 'nolints'
       # ignore staging branch used by bors, this is handled by bors.yml
       - 'staging'
+  merge_group:
 
 name: continuous integration
 EOF

Archive.lean

@@ -1,4 +1,7 @@
 import Archive.Arithcc
+import Archive.Examples.IfNormalization.Result
+import Archive.Examples.IfNormalization.Statement
+import Archive.Examples.IfNormalization.WithoutAesop
 import Archive.Examples.MersennePrimes
 import Archive.Examples.PropEncodable
 import Archive.Imo.Imo1959Q1

Archive/Examples/IfNormalization/Result.lean

@@ -0,0 +1,122 @@
+/-
+Copyright (c) 2023 Chris Hughes. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Chris Hughes
+-/
+import Archive.Examples.IfNormalization.Statement
+import Mathlib.Data.List.AList
+import Mathlib.Tactic.Recall
+
+/-!
+# A solution to the if normalization challenge in Lean.
+
+See `Statement.lean` for background.
+-/
+
+set_option autoImplicit true
+
+macro "◾" : tactic => `(tactic| aesop)
+macro "◾" : term => `(term| by aesop)
+
+namespace IfExpr
+
+/-!
+We add some local simp lemmas so we can unfold the definitions of the normalization condition.
+-/
+attribute [local simp] normalized hasNestedIf hasConstantIf hasRedundantIf disjoint vars
+  List.disjoint
+
+/-!
+Adding these lemmas to the simp set allows Lean to handle the termination proof automatically.
+-/
+attribute [local simp] Nat.lt_add_one_iff le_add_of_le_right
+
+/-!
+Some further simp lemmas for handling if-then-else statements.
+-/
+attribute [local simp] apply_ite ite_eq_iff'
+
+-- A copy of Lean's `decide_eq_true_eq` which unifies the `Decidable` instance
+-- rather than finding it by typeclass search.
+-- See https://github.com/leanprover/lean4/pull/2816
+@[simp] theorem decide_eq_true_eq {i : Decidable p} : (@decide p i = true) = p :=
+  _root_.decide_eq_true_eq
+
+
+/-!
+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`.
+-/
+@[simp] theorem eval_lit : (lit b).eval f  = b := rfl
+@[simp] theorem eval_var : (var i).eval f  = f i := rfl
+@[simp] theorem eval_ite_lit :
+    (ite (.lit b) t e).eval f = bif b then t.eval f else e.eval f := rfl
+@[simp] theorem eval_ite_var :
+    (ite (.var i) t e).eval f = bif f i then t.eval f else e.eval f := rfl
+@[simp] theorem eval_ite_ite :
+    (ite (ite a b c) d e).eval f = (ite a (ite b d e) (ite c d e)).eval f := by
+  cases h : eval f a <;> simp_all [eval]
+
+/-- Custom size function for if-expressions, used for proving termination. -/
+@[simp] def normSize : IfExpr → Nat
+  | lit _ => 0
+  | var _ => 1
+  | .ite i t e => 2 * normSize i + max (normSize t) (normSize e) + 1
+
+/-- Normalizes the expression at the same time as assigning all variables in
+`e` to the literal booleans given by `l` -/
+def normalize (l : AList (fun _ : ℕ => Bool)) :
+    (e : IfExpr) → { e' : IfExpr //
+        (∀ f, e'.eval f = e.eval (fun w => (l.lookup w).elim (f w) (fun b => b)))
+        ∧ e'.normalized
+        ∧ ∀ (v : ℕ), v ∈ vars e' → l.lookup v = none }
+  | lit b => ⟨lit b, ◾⟩
+  | var v =>
+    match h : l.lookup v with
+    | none => ⟨var v, ◾⟩
+    | some b => ⟨lit b, ◾⟩
+  | .ite (lit true)   t e => have t' := normalize l t; ⟨t'.1, ◾⟩
+  | .ite (lit false)  t e => have e' := normalize l e; ⟨e'.1, ◾⟩
+  | .ite (.ite a b c) t e => have i' := normalize l (.ite a (.ite b t e) (.ite c t e)); ⟨i'.1, ◾⟩
+  | .ite (var v)      t e =>
+    match h : l.lookup v with
+    | none =>
+      have ⟨t', ht₁, ht₂, ht₃⟩ := normalize (l.insert v true) t
+      have ⟨e', he₁, he₂, he₃⟩ := normalize (l.insert v false) e
+      ⟨if t' = e' then t' else .ite (var v) t' e', by
+        refine ⟨fun f => ?_, ?_, fun w b => ?_⟩
+        · -- eval = eval
+          simp
+          cases hfv : f v
+          · simp_all
+            congr
+            ext w
+            by_cases w = v <;> ◾
+          · simp [h, ht₁]
+            congr
+            ext w
+            by_cases w = v <;> ◾
+        · -- normalized
+          have := ht₃ v
+          have := he₃ v
+          ◾
+        · -- lookup = none
+          have := ht₃ w
+          have := he₃ w
+          by_cases w = v <;> ◾⟩
+    | some b =>
+      have i' := normalize l (.ite (lit b) t e); ⟨i'.1, ◾⟩
+  termination_by normalize e => e.normSize
+  decreasing_by { decreasing_with simp (config := { arith := true }) [Zero.zero]; done }
+
+/-
+We recall the statement of the if-normalization problem.
+
+We want a function from if-expressions to if-expressions,
+that outputs normalized if-expressions and preserves meaning.
+-/
+recall IfNormalization :=
+  { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized ∧ (Z e).eval = e.eval }
+
+example : IfNormalization :=
+  ⟨_, fun e => ⟨(IfExpr.normalize ∅ e).2.2.1, by simp [(IfExpr.normalize ∅ e).2.1]⟩⟩

Archive/Examples/IfNormalization/Statement.lean

@@ -0,0 +1,107 @@
+/-
+Copyright (c) 2023 Lean FRO LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Scott Morrison
+-/
+
+/-!
+# 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.
+-/
+
+/-- An if-expression is either boolean literal, a numbered variable,
+or an if-then-else expression where each subexpression is an if-expression. -/
+inductive IfExpr
+  | lit : Bool → IfExpr
+  | var : Nat → IfExpr
+  | ite : IfExpr → IfExpr → IfExpr → IfExpr
+deriving DecidableEq, Repr
+
+namespace IfExpr
+
+/--
+An if-expression has a "nested if" if it contains
+an if-then-else where the "if" is itself an if-then-else.
+-/
+def hasNestedIf : IfExpr → Bool
+  | lit _ => false
+  | var _ => false
+  | ite (ite _ _ _) _ _ => true
+  | ite _ t e => t.hasNestedIf || e.hasNestedIf
+
+/--
+An if-expression has a "constant if" if it contains
+an if-then-else where the "if" is itself a literal.
+-/
+def hasConstantIf : IfExpr → Bool
+  | lit _ => false
+  | var _ => false
+  | ite (lit _) _ _ => true
+  | ite i t e => i.hasConstantIf || t.hasConstantIf || e.hasConstantIf
+
+/--
+An if-expression has a "redundant if" if it contains
+an if-then-else where the then and else clauses are identical.
+-/
+def hasRedundantIf : IfExpr → Bool
+  | lit _ => false
+  | var _ => false
+  | ite i t e => t == e || i.hasRedundantIf || t.hasRedundantIf || e.hasRedundantIf
+
+/--
+All the variables appearing in an if-expressions, read left to right, without removing duplicates.
+-/
+def vars : IfExpr → List Nat
+  | lit _ => []
+  | var i => [i]
+  | ite i t e => i.vars ++ t.vars ++ e.vars
+
+/--
+A helper function to specify that two lists are disjoint.
+-/
+def _root_.List.disjoint {α} [DecidableEq α] : List α → List α → Bool
+  | [], _ => true
+  | x::xs, ys => x ∉ ys && xs.disjoint ys
+
+/--
+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.
+-/
+def disjoint : IfExpr → 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
+
+/--
+An if expression is "normalized" if it has not nested, constant, or redundant ifs,
+and it evaluates each variable at most once.
+-/
+def normalized (e : IfExpr) : Bool :=
+  !e.hasNestedIf && !e.hasConstantIf && !e.hasRedundantIf && e.disjoint
+
+/--
+The evaluation of an if expresssion at some assignment of variables.
+-/
+def eval (f : Nat → Bool) : IfExpr → Bool
+  | lit b => b
+  | var i => f i
+  | ite i t e => bif i.eval f then t.eval f else e.eval f
+
+end IfExpr
+
+/--
+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.
+-/
+def IfNormalization : Type := { Z : IfExpr → IfExpr // ∀ e, (Z e).normalized ∧ (Z e).eval = e.eval }