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.
This commit is contained in:
Joachim Breitner
GitHub
parent
63ac27e9b9
commit
33baaccb20
3 changed files with 256 additions and 0 deletions
99
tests/lean/run/2961.lean
Normal file
99
tests/lean/run/2961.lean
Normal file
|
|
@ -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
|
||||
45
tests/lean/run/3219.lean
Normal file
45
tests/lean/run/3219.lean
Normal file
|
|
@ -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
|
||||
112
tests/lean/run/5667.lean
Normal file
112
tests/lean/run/5667.lean
Normal file
|
|
@ -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
|
||||
Loading…
Add table
Reference in a new issue