test: more equational theorem generation tests (#6952)

This includes the examples from issues #2961, #3219 and #5667 in our
test suite, so that we know when (accidentially) fix them.

In fact this closes #3219, which (judging from the nightlies) was fixed
last week by #6901.

tests/lean/run/2961.lean

@@ -0,0 +1,99 @@
+def replace (f : Nat → Option Nat) (t : Nat) : Nat :=
+  match f t with
+  | some u => u
+  | none =>
+    match t with
+    | .zero => .zero
+    | .succ t' => replace f t'
+
+/--
+info: equations:
+theorem replace.eq_1 : ∀ (f : Nat → Option Nat),
+  replace f Nat.zero =
+    match f Nat.zero with
+    | some u => u
+    | none => Nat.zero
+theorem replace.eq_2 : ∀ (f : Nat → Option Nat) (t' : Nat),
+  replace f t'.succ =
+    match f t'.succ with
+    | some u => u
+    | none => replace f t'
+-/
+#guard_msgs in
+#print equations replace
+
+/--
+error: Failed to realize constant replace.eq_def:
+  failed to generate unfold theorem for 'replace'
+  case h_1
+  f : Nat → Option Nat
+  t : Nat
+  x : Option Nat
+  u : Nat
+  heq✝ : f t = some u
+  ⊢ replace f t = u
+---
+error: Failed to realize constant replace.eq_def:
+  failed to generate unfold theorem for 'replace'
+  case h_1
+  f : Nat → Option Nat
+  t : Nat
+  x : Option Nat
+  u : Nat
+  heq✝ : f t = some u
+  ⊢ replace f t = u
+---
+error: unknown identifier 'replace.eq_def'
+-/
+#guard_msgs in
+#check replace.eq_def
+
+def replace2 (f : Nat → Option Nat) (t1 t2 : Nat) : Nat :=
+  match f t1 with
+  | some u => u
+  | none =>
+    match t2 with
+    | .zero => .zero
+    | .succ t' => replace2 f t1 t'
+
+/--
+info: equations:
+theorem replace2.eq_1 : ∀ (f : Nat → Option Nat) (t1 : Nat),
+  replace2 f t1 Nat.zero =
+    match f t1 with
+    | some u => u
+    | none => Nat.zero
+theorem replace2.eq_2 : ∀ (f : Nat → Option Nat) (t1 t' : Nat),
+  replace2 f t1 t'.succ =
+    match f t1 with
+    | some u => u
+    | none => replace2 f t1 t'
+-/
+#guard_msgs in
+#print equations replace2
+
+/--
+error: Failed to realize constant replace2.eq_def:
+  failed to generate unfold theorem for 'replace2'
+  case h_1
+  f : Nat → Option Nat
+  t1 t2 : Nat
+  x : Option Nat
+  u : Nat
+  heq✝ : f t1 = some u
+  ⊢ replace2 f t1 t2 = u
+---
+error: Failed to realize constant replace2.eq_def:
+  failed to generate unfold theorem for 'replace2'
+  case h_1
+  f : Nat → Option Nat
+  t1 t2 : Nat
+  x : Option Nat
+  u : Nat
+  heq✝ : f t1 = some u
+  ⊢ replace2 f t1 t2 = u
+---
+error: unknown identifier 'replace2.eq_def'
+-/
+#guard_msgs in
+#check replace2.eq_def

tests/lean/run/3219.lean

@@ -0,0 +1,45 @@
+inductive Tree (α : Type u) : Nat → Type u
+  | leaf : Tree α 0
+  | branch :
+    (val : α)
+    → (left : Tree α n)
+    → (right : Tree α m)
+    → Tree α (n+m+1)
+
+def popLast {α : Type u} (heap : Tree α (o+1)) : (α × Tree α o) :=
+  match o, heap with
+  | (n+m), .branch a (left : Tree α n) (right : Tree α m)  =>
+    if r : m = 0 then
+      --remove left
+      match n, left with
+      | 0, _ => (a, (Eq.symm $ r.subst $ Nat.zero_add m : 0=0+m)▸Tree.leaf)
+      | (l+1), left =>
+        let (res, (newLeft : Tree α l)) := popLast left
+        (res, (Nat.add_right_comm l m 1)▸Tree.branch a newLeft right)
+    else
+      --remove right
+      match  m, right with
+      | (r+1), right =>
+        let (res, (newRight : Tree α r)) := popLast right
+        (res, Tree.branch a left newRight)
+
+def SomePredicate (_ : Tree α n) : Prop := True
+
+/--
+info: equations:
+theorem popLast.eq_1.{u} : ∀ {α : Type u} (n m : Nat) (a : α) (left : Tree α n) (right : Tree α m),
+  popLast (Tree.branch a left right) =
+    if r : m = 0 then
+      match n, left with
+      | 0, x => (a, ⋯ ▸ Tree.leaf)
+      | l.succ, left =>
+        match popLast left with
+        | (res, newLeft) => (res, ⋯ ▸ Tree.branch a newLeft right)
+    else
+      match m, right, r with
+      | r.succ, right, r_1 =>
+        match popLast right with
+        | (res, newRight) => (res, Tree.branch a left newRight)
+-/
+#guard_msgs in
+#print equations popLast

tests/lean/run/5667.lean

@@ -0,0 +1,112 @@
+inductive Expr where
+  | const (i : BitVec 32)
+  | op (op : Unit) (e1 : Expr)
+
+def optimize : Expr → Expr
+  | .const i => .const i
+  | .op bop e1 =>
+    match bop, optimize e1 with
+    | _, .const _ => .op bop (.const 0)
+    | _, _ => .const 0
+
+/--
+error: Failed to realize constant optimize.eq_def:
+  failed to generate equational theorem for 'optimize'
+  case h_2
+  e1 : Expr
+  i : BitVec 32
+  heq : optimize e1 = Expr.const i
+  bop✝ bop_1 : Unit
+  x : Expr
+  x_3 :
+    ∀ (i : BitVec 32),
+      (Expr.rec (fun i => ⟨Expr.const i, PUnit.unit⟩)
+              (fun op e1 e1_ih =>
+                ⟨match op, e1_ih.1 with
+                  | x, Expr.const i => Expr.op op (Expr.const 0)
+                  | x, x_1 => Expr.const 0,
+                  e1_ih⟩)
+              e1).1 =
+          Expr.const i →
+        False
+  ⊢ Expr.const 0 = Expr.op bop✝ (Expr.const 0)
+---
+error: Failed to realize constant optimize.eq_def:
+  failed to generate unfold theorem for 'optimize'
+  case h_2.h_1
+  x e1 : Expr
+  bop✝ bop_1 : Unit
+  x_1 : Expr
+  i : BitVec 32
+  heq✝ : optimize e1 = Expr.const i
+  ⊢ optimize (Expr.op bop✝ e1) = Expr.op bop✝ (Expr.const 0)
+---
+error: unknown identifier 'optimize.eq_def'
+-/
+#guard_msgs in
+#check optimize.eq_def
+
+/--
+error: failed to generate equational theorem for 'optimize'
+case h_2
+e1 : Expr
+i : BitVec 32
+heq : optimize e1 = Expr.const i
+bop✝ bop_1 : Unit
+x : Expr
+x_3 :
+  ∀ (i : BitVec 32),
+    (Expr.rec (fun i => ⟨Expr.const i, PUnit.unit⟩)
+            (fun op e1 e1_ih =>
+              ⟨match op, e1_ih.1 with
+                | x, Expr.const i => Expr.op op (Expr.const 0)
+                | x, x_1 => Expr.const 0,
+                e1_ih⟩)
+            e1).1 =
+        Expr.const i →
+      False
+⊢ Expr.const 0 = Expr.op bop✝ (Expr.const 0)
+-/
+#guard_msgs in
+#print equations optimize
+
+-- works:
+
+def optimize2 : Expr → Expr
+  | .const i => .const i
+  | .op bop e1 =>
+    match optimize2 e1 with
+    | .const _ => .op bop (.const 0)
+    | _ => .const 0
+
+/--
+info: equations:
+theorem optimize2.eq_1 : ∀ (i : BitVec 32), optimize2 (Expr.const i) = Expr.const i
+theorem optimize2.eq_2 : ∀ (bop : Unit) (e1 : Expr),
+  optimize2 (Expr.op bop e1) =
+    match optimize2 e1 with
+    | Expr.const i => Expr.op bop (Expr.const 0)
+    | x => Expr.const 0
+-/
+#guard_msgs in
+#print equations optimize2
+
+-- also works:
+
+def optimize3 : Expr → Expr
+  | .const i => .const i
+  | .op bop e1 =>
+    match bop, e1 with
+    | _, .const _ => .op bop (optimize3 e1)
+    | _, _ => .const 0
+
+/--
+info: equations:
+theorem optimize3.eq_1 : ∀ (i : BitVec 32), optimize3 (Expr.const i) = Expr.const i
+theorem optimize3.eq_2 : ∀ (bop : Unit) (i : BitVec 32),
+  optimize3 (Expr.op bop (Expr.const i)) = Expr.op bop (optimize3 (Expr.const i))
+theorem optimize3.eq_3 : ∀ (bop : Unit) (e1 : Expr),
+  (∀ (i : BitVec 32), e1 = Expr.const i → False) → optimize3 (Expr.op bop e1) = Expr.const 0
+-/
+#guard_msgs in
+#print equations optimize3