From 33baaccb20616b2c0c7a59ea655238afae373c73 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Tue, 4 Feb 2025 23:18:35 +0100 Subject: [PATCH] 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 | 99 ++++++++++++++++++++++++++++++++++ tests/lean/run/3219.lean | 45 ++++++++++++++++ tests/lean/run/5667.lean | 112 +++++++++++++++++++++++++++++++++++++++ 3 files changed, 256 insertions(+) create mode 100644 tests/lean/run/2961.lean create mode 100644 tests/lean/run/3219.lean create mode 100644 tests/lean/run/5667.lean diff --git a/tests/lean/run/2961.lean b/tests/lean/run/2961.lean new file mode 100644 index 0000000000..e55dbb80af --- /dev/null +++ b/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 diff --git a/tests/lean/run/3219.lean b/tests/lean/run/3219.lean new file mode 100644 index 0000000000..cf96cffbc1 --- /dev/null +++ b/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 diff --git a/tests/lean/run/5667.lean b/tests/lean/run/5667.lean new file mode 100644 index 0000000000..0ea0d09bb7 --- /dev/null +++ b/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