max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: rename automatically generated equational theorems (#3661)

Browse source 
cc @nomeata
This commit is contained in:
Leonardo de Moura 2024-03-13 00:56:27 -07:00 • committed by GitHub
parent 317adf42e9
commit 2003814085
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
49 changed files with 321 additions and 255 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

27
RELEASES.md
View file

@ -31,6 +31,33 @@ v4.8.0 (development in progress)
(x x : Nat) : motive x x
```
Breaking changes:
* Automatically generated equational theorems are now named using suffix `.eq_<idx>` instead of `._eq_<idx>`, and `.def` instead of `._unfold`. Example:
```
def fact : Nat → Nat
| 0 => 1
| n+1 => (n+1) * fact n
theorem ex : fact 0 = 1 := by unfold fact; decide
#check fact.eq_1
-- fact.eq_1 : fact 0 = 1
#check fact.eq_2
-- fact.eq_2 (n : Nat) : fact (Nat.succ n) = (n + 1) * fact n
#check fact.def
/-
fact.def :
∀ (x : Nat),
fact x =
match x with
| 0 => 1
| Nat.succ n => (n + 1) * fact n
-/
```
v4.7.0
---------

2
src/Lean/Elab/PreDefinition/Eqns.lean
View file

@ -380,7 +380,7 @@ def mkUnfoldEq (declName : Name) (info : EqnInfoCore) : MetaM Name := withLCtx {
mkUnfoldProof declName goal.mvarId!
let type ← mkForallFVars xs type
let value ← mkLambdaFVars xs (← instantiateMVars goal)
let name := baseName ++ `_unfold
let name := baseName ++ `def
addDecl <| Declaration.thmDecl {
name, type, value
levelParams := info.levelParams

2
src/Lean/Elab/PreDefinition/Structural/Eqns.lean
View file

@ -68,7 +68,7 @@ def mkEqns (info : EqnInfo) : MetaM (Array Name) :=
for i in [: eqnTypes.size] do
let type := eqnTypes[i]!
trace[Elab.definition.structural.eqns] "{eqnTypes[i]!}"
let name := baseName ++ (`_eq).appendIndexAfter (i+1)
let name := baseName ++ (`eq).appendIndexAfter (i+1)
thmNames := thmNames.push name
let value ← mkProof info.declName type
let (type, value) ← removeUnusedEqnHypotheses type value

2
src/Lean/Elab/PreDefinition/WF/Eqns.lean
View file

@ -117,7 +117,7 @@ def mkEqns (declName : Name) (info : EqnInfo) : MetaM (Array Name) :=
for i in [: eqnTypes.size] do
let type := eqnTypes[i]!
trace[Elab.definition.wf.eqns] "{eqnTypes[i]!}"
let name := baseName ++ (`_eq).appendIndexAfter (i+1)
let name := baseName ++ (`eq).appendIndexAfter (i+1)
thmNames := thmNames.push name
let value ← mkProof declName type
let (type, value) ← removeUnusedEqnHypotheses type value

2
src/Lean/Meta/Tactic/Simp/Types.lean
View file

@ -285,7 +285,7 @@ def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
def recordSimpTheorem (thmId : Origin) : SimpM Unit := do
/-
If `thmId` is an equational theorem (e.g., `foo._eq_1`), we should record `foo` instead.
If `thmId` is an equational theorem (e.g., `foo.eq_1`), we should record `foo` instead.
See issue #3547.
-/
let thmId ← match thmId with

9
tests/lean/1026.lean.expected.out
View file

@ -1,9 +0,0 @@
1026.lean:1:4-1:7: warning: declaration uses 'sorry'
1026.lean:9:8-9:10: warning: declaration uses 'sorry'
foo._unfold (n : Nat) :
foo n =
if n = 0 then 0
else
let x := n - 1;
let_fun this := foo.proof_4;
foo x

4
tests/lean/1074a.lean.expected.out
View file

@ -1,4 +0,0 @@
Brx.interp._eq_1 (n z : Term) (H_2 : Brx (Term.id2 n z)) :
Brx.interp H_2 =
match ⋯ with
| ⋯ => Brx.interp Hz

20
tests/lean/974.lean
View file

@ -1,20 +0,0 @@
inductive Formula : Nat → Type u
| bot : Formula n
| imp (f₁ f₂ : Formula n ) : Formula n
| all (f : Formula (n+1)) : Formula n
def Formula.count_quantifiers : {n:Nat} → Formula n → Nat
| _, imp f₁ f₂ => f₁.count_quantifiers + f₂.count_quantifiers
| _, all f => f.count_quantifiers + 1
| _, _ => 0
attribute [simp] Formula.count_quantifiers
#check Formula.count_quantifiers._eq_1
#check Formula.count_quantifiers._eq_2
#check Formula.count_quantifiers._eq_3
@[simp] def Formula.count_quantifiers2 : Formula n → Nat
| imp f₁ f₂ => f₁.count_quantifiers2 + f₂.count_quantifiers2
| all f => f.count_quantifiers2 + 1
| _ => 0

9
tests/lean/974.lean.expected.out
View file

@ -1,9 +0,0 @@
Formula.count_quantifiers._eq_1.{u_1} :
∀ (x : Nat) (f₁ f₂ : Formula x),
Formula.count_quantifiers (Formula.imp f₁ f₂) = Formula.count_quantifiers f₁ + Formula.count_quantifiers f₂
Formula.count_quantifiers._eq_2.{u_1} :
∀ (x : Nat) (f : Formula (x + 1)), Formula.count_quantifiers (Formula.all f) = Formula.count_quantifiers f + 1
Formula.count_quantifiers._eq_3.{u_1} :
∀ (x : Nat) (x_1 : Formula x),
(∀ (f₁ f₂ : Formula x), x_1 = Formula.imp f₁ f₂ → False) →
(∀ (f : Formula (x + 1)), x_1 = Formula.all f → False) → Formula.count_quantifiers x_1 = 0

4
tests/lean/986.lean
View file

@ -1,4 +0,0 @@
attribute [simp] Array.insertionSort.swapLoop
#check Array.insertionSort.swapLoop._eq_1
#check Array.insertionSort.swapLoop._eq_2

9
tests/lean/986.lean.expected.out
View file

@ -1,9 +0,0 @@
Array.insertionSort.swapLoop._eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (h : 0 < Array.size a) :
Array.insertionSort.swapLoop lt a 0 h = a
Array.insertionSort.swapLoop._eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
(h : Nat.succ j' < Array.size a) :
Array.insertionSort.swapLoop lt a (Nat.succ j') h =
let_fun h' := ⋯;
if lt a[Nat.succ j'] a[j'] = true then
Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j' ⋯
else a

11
tests/lean/eqValue.lean
View file

@ -1,11 +0,0 @@
@[simp] def f (x : Nat) : Nat :=
match x with
| 0 => 1
| 100 => 2
| 1000 => 3
| x+1 => f x
#check f._eq_1
#check f._eq_2
#check f._eq_3
#check f._eq_4

4
tests/lean/eqValue.lean.expected.out
View file

@ -1,4 +0,0 @@
f._eq_1 : f 0 = 1
f._eq_2 : f 100 = 2
f._eq_3 : f 1000 = 3
f._eq_4 (x_2 : Nat) (x_3 : x_2 = 99 → False) (x_4 : x_2 = 999 → False) : f (Nat.succ x_2) = f x_2

17
tests/lean/heapSort.lean.expected.out
View file

@ -1,17 +0,0 @@
heapSort.lean:15:4-15:15: warning: declaration uses 'sorry'
heapSort.lean:15:4-15:15: warning: declaration uses 'sorry'
heapSort.lean:15:4-15:15: warning: declaration uses 'sorry'
heapSort.lean:43:4-43:10: warning: declaration uses 'sorry'
heapSort.lean:58:4-58:13: warning: declaration uses 'sorry'
heapSort.lean:58:4-58:13: warning: declaration uses 'sorry'
heapSort.lean:58:4-58:13: warning: declaration uses 'sorry'
heapSort.lean:102:4-102:13: warning: declaration uses 'sorry'
heapSort.lean:102:4-102:13: warning: declaration uses 'sorry'
Array.heapSort.loop._eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y)
(out : Array α) :
Array.heapSort.loop lt a out =
match e : BinaryHeap.max a with
| none => out
| some x =>
let_fun this := ⋯;
Array.heapSort.loop lt (BinaryHeap.popMax a) (Array.push out x)

15
tests/lean/namePatEqThm.lean
View file

@ -1,15 +0,0 @@
@[simp] def iota : Nat → List Nat
| 0 => []
| m@(n+1) => m :: iota n
#check iota._eq_1
#check iota._eq_2
@[simp] def f : List Nat → List Nat × List Nat
| xs@(x :: ys@(y :: [])) => (xs, ys)
| xs@(x :: ys@(y :: zs)) => f zs
| _ => ([], [])
#check f._eq_1
#check f._eq_2
#check f._eq_3

8
tests/lean/namePatEqThm.lean.expected.out
View file

@ -1,8 +0,0 @@
iota._eq_1 : iota 0 = []
iota._eq_2 (n : Nat) : iota (Nat.succ n) = Nat.succ n :: iota n
f._eq_1 (x_1 y : Nat) : f [x_1, y] = ([x_1, y], [y])
f._eq_2 (x_1 y : Nat) (zs : List Nat) (x_2 : zs = [] → False) : f (x_1 :: y :: zs) = f zs
f._eq_3 :
∀ (x : List Nat),
(∀ (x_1 y : Nat), x = [x_1, y] → False) →
(∀ (x_1 y : Nat) (zs : List Nat), x = x_1 :: y :: zs → False) → f x = ([], [])

12
tests/lean/1026.lean → tests/lean/run/1026.lean
View file

@ -10,4 +10,14 @@ theorem ex : foo 0 = 0 := by
unfold foo
sorry
#check foo._unfold
/--
info: foo.def (n : Nat) :
foo n =
if n = 0 then 0
else
let x := n - 1;
let_fun this := foo.proof_4;
foo x
-/
#guard_msgs in
#check foo.def

9
tests/lean/1074a.lean → tests/lean/run/1074a.lean
View file

@ -18,4 +18,11 @@ def Brx.interp_nil (H: Brx a): H.interp = H.interp
rfl
}
#check Brx.interp._eq_1
/--
info: Brx.interp.eq_1 (n z : Term) (H_2 : Brx (Term.id2 n z)) :
Brx.interp H_2 =
match ⋯ with
| ⋯ => Brx.interp Hz
-/
#guard_msgs in
#check Brx.interp.eq_1

4
tests/lean/run/1080.lean
View file

@ -17,8 +17,8 @@ def Bar.check: Bar f → Prop
attribute [simp] Bar.check
#check Bar.check._eq_1
#check Bar.check._eq_2
#check Bar.check.eq_1
#check Bar.check.eq_2
#check Bar.check.match_1.eq_1
#check Bar.check.match_1.eq_2
#check Bar.check.match_1.splitter

40
tests/lean/run/974.lean Normal file
View file

@ -0,0 +1,40 @@
inductive Formula : Nat → Type u where
| bot : Formula n
| imp (f₁ f₂ : Formula n ) : Formula n
| all (f : Formula (n+1)) : Formula n
def Formula.count_quantifiers : {n:Nat} → Formula n → Nat
| _, imp f₁ f₂ => f₁.count_quantifiers + f₂.count_quantifiers
| _, all f => f.count_quantifiers + 1
| _, _ => 0
attribute [simp] Formula.count_quantifiers
/--
info: Formula.count_quantifiers.eq_1.{u_1} :
∀ (x : Nat) (f₁ f₂ : Formula x),
Formula.count_quantifiers (Formula.imp f₁ f₂) = Formula.count_quantifiers f₁ + Formula.count_quantifiers f₂
-/
#guard_msgs in
#check Formula.count_quantifiers.eq_1
/--
info: Formula.count_quantifiers.eq_2.{u_1} :
∀ (x : Nat) (f : Formula (x + 1)), Formula.count_quantifiers (Formula.all f) = Formula.count_quantifiers f + 1
-/
#guard_msgs in
#check Formula.count_quantifiers.eq_2
/--
info: Formula.count_quantifiers.eq_3.{u_1} :
∀ (x : Nat) (x_1 : Formula x),
(∀ (f₁ f₂ : Formula x), x_1 = Formula.imp f₁ f₂ → False) →
(∀ (f : Formula (x + 1)), x_1 = Formula.all f → False) → Formula.count_quantifiers x_1 = 0
-/
#guard_msgs in
#check Formula.count_quantifiers.eq_3
@[simp] def Formula.count_quantifiers2 : Formula n → Nat
| imp f₁ f₂ => f₁.count_quantifiers2 + f₂.count_quantifiers2
| all f => f.count_quantifiers2 + 1
| _ => 0

19
tests/lean/run/986.lean
View file

@ -1 +1,20 @@
attribute [simp] Array.insertionSort.swapLoop
/--
info: Array.insertionSort.swapLoop.eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (h : 0 < Array.size a) :
Array.insertionSort.swapLoop lt a 0 h = a
-/
#guard_msgs in
#check Array.insertionSort.swapLoop.eq_1
/--
info: Array.insertionSort.swapLoop.eq_2.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : Array α) (j' : Nat)
(h : Nat.succ j' < Array.size a) :
Array.insertionSort.swapLoop lt a (Nat.succ j') h =
let_fun h' := ⋯;
if lt a[Nat.succ j'] a[j'] = true then
Array.insertionSort.swapLoop lt (Array.swap a { val := Nat.succ j', isLt := h } { val := j', isLt := h' }) j' ⋯
else a
-/
#guard_msgs in
#check Array.insertionSort.swapLoop.eq_2

2
tests/lean/run/byteSliceIssue.lean
View file

@ -42,4 +42,4 @@ def forIn.loop [Monad m] (f : UInt8 → β → m (ForInStep β))
termination_by _end - i
attribute [simp] ByteSlice.forIn.loop
#check @ByteSlice.forIn.loop._eq_1
#check @ByteSlice.forIn.loop.eq_1

21
tests/lean/run/eqValue.lean Normal file
View file

@ -0,0 +1,21 @@
@[simp] def f (x : Nat) : Nat :=
match x with
| 0 => 1
| 100 => 2
| 1000 => 3
| x+1 => f x
/-- info: f.eq_1 : f 0 = 1 -/
#guard_msgs in
#check f.eq_1
/-- info: f.eq_2 : f 100 = 2 -/
#guard_msgs in
#check f.eq_2
/-- info: f.eq_3 : f 1000 = 3 -/
#guard_msgs in
#check f.eq_3
/--
info: f.eq_4 (x_2 : Nat) (x_3 : x_2 = 99 → False) (x_4 : x_2 = 999 → False) : f (Nat.succ x_2) = f x_2
-/
#guard_msgs in
#check f.eq_4

4
tests/lean/run/eqnsAtSimp3.lean
View file

@ -38,7 +38,7 @@ theorem ex3 (x : Nat) (y : Nat) (h : y = 5 → False) : ∃ z, f (x+1) y = 2 * z
| x+1, y, z => 2 * f2 x y z
#check f2._eq_4
#check f2.eq_4
theorem ex4 (x y z : Nat) (h : y = 5 → z = 6 → False) : ∃ w, f2 (x+1) y z = 2 * w := by
simp [f2, h]
@ -64,7 +64,7 @@ theorem ex6 (x y z : Nat) (h2 : z ≠ 6) : ∃ w, f2 (x+1) y z = 2 * w := by
| x+1, 6, 4 => 3 * f3 x 0 1
| x+1, y, z => 2 * f3 x y z
#check f3._eq_5
#check f3.eq_5
theorem ex7 (x y z : Nat) (h2 : z ≠ 6) (h3 : y ≠ 6) : ∃ w, f3 (x+1) y z = 2 * w := by
simp [f3, h2, h3]

13
tests/lean/heapSort.lean → tests/lean/run/heapSort.lean
View file

@ -173,6 +173,17 @@ def Array.toBinaryHeap (lt : α → α → Bool) (a : Array α) : BinaryHeap α
loop (a.toBinaryHeap gt) #[]
attribute [simp] Array.heapSort.loop
#check Array.heapSort.loop._eq_1
/--
info: Array.heapSort.loop.eq_1.{u_1} {α : Type u_1} (lt : α → α → Bool) (a : BinaryHeap α fun y x => lt x y) (out : Array α) :
Array.heapSort.loop lt a out =
match e : BinaryHeap.max a with
| none => out
| some x =>
let_fun this := ⋯;
Array.heapSort.loop lt (BinaryHeap.popMax a) (Array.push out x)
-/
#guard_msgs in
#check Array.heapSort.loop.eq_1
attribute [simp] BinaryHeap.heapifyDown

4
tests/lean/run/instEtaIssue.lean
View file

@ -8,12 +8,12 @@ attribute [simp] filter
set_option pp.explicit true
/--
info: filter._eq_2.{u_1} {α : Type u_1} (p : α → Prop) [@DecidablePred α p] (x : α) (xs' : List α) :
info: filter.eq_2.{u_1} {α : Type u_1} (p : α → Prop) [@DecidablePred α p] (x : α) (xs' : List α) :
@Eq (List α) (@filter α p inst✝ (@List.cons α x xs'))
(@ite (List α) (p x) (inst✝ x) (@List.cons α x (@filter α p inst✝ xs')) (@filter α p inst✝ xs'))
-/
#guard_msgs in
#check filter._eq_2 -- We should not have terms of the form `@filter α p (fun x => inst✝ x) xs'`
#check filter.eq_2 -- We should not have terms of the form `@filter α p (fun x => inst✝ x) xs'`
def filter_length (p : α → Prop) [DecidablePred p] : (filter p xs).length ≤ xs.length := by

20
tests/lean/run/match_lit_fin_cover.lean
View file

@ -17,16 +17,16 @@ def boo (x : Fin 3) : Nat :=
| 2, y+1 => bla x y + 1
/--
info: bla._eq_1 (y : Nat) : bla 0 y = 10
info: bla.eq_1 (y : Nat) : bla 0 y = 10
-/
#guard_msgs in
#check bla._eq_1
#check bla.eq_1
/--
info: bla._eq_4 (y_2 : Nat) : bla 2 (Nat.succ y_2) = bla 2 y_2 + 1
info: bla.eq_4 (y_2 : Nat) : bla 2 (Nat.succ y_2) = bla 2 y_2 + 1
-/
#guard_msgs in
#check bla._eq_4
#check bla.eq_4
open BitVec
@ -56,19 +56,19 @@ def foo' (x : BitVec 3) (y : Nat) : Nat :=
attribute [simp] foo'
/--
info: foo'._eq_1 (y : Nat) : foo' (0#3) y = 7
info: foo'.eq_1 (y : Nat) : foo' (0#3) y = 7
-/
#guard_msgs in
#check foo'._eq_1
#check foo'.eq_1
/--
info: foo'._eq_2 (y : Nat) : foo' (1#3) y = 6
info: foo'.eq_2 (y : Nat) : foo' (1#3) y = 6
-/
#guard_msgs in
#check foo'._eq_2
#check foo'.eq_2
/--
info: foo'._eq_9 (y_2 : Nat) : foo' (7#3) (Nat.succ y_2) = foo' 7 y_2 + 1
info: foo'.eq_9 (y_2 : Nat) : foo' (7#3) (Nat.succ y_2) = foo' 7 y_2 + 1
-/
#guard_msgs in
#check foo'._eq_9
#check foo'.eq_9

20
tests/lean/run/match_lit_issues.lean
View file

@ -4,8 +4,8 @@
| _, 0 => b+1
| _, a+1 => f1 (i-1) a (b*2)
#check f1._eq_1
#check f1._eq_2
#check f1.eq_1
#check f1.eq_2
example : f1 (-1) a b = b := by simp -- should work
example : f1 (-2) 0 b = b+1 := by simp
@ -29,8 +29,8 @@ example (h : c ≠ 'a') : f2 c (a+1) b = f2 c a (b*2) := by simp
| _, 0 => b+1
| _, a+1 => f3 (i+1) a (b*2)
#check f3._eq_1
#check f3._eq_2
#check f3.eq_1
#check f3.eq_2
example : f3 2 a b = b := by simp -- should work
example : f3 3 0 b = b+1 := by simp
@ -43,8 +43,8 @@ example (h : i ≠ 2) : f3 i (a+1) b = f3 (i+1) a (b*2) := by simp; done -- shou
| _, 0 => b+1
| _, a+1 => f4 (i+1) a (b*2)
#check f4._eq_1
#check f4._eq_2
#check f4.eq_1
#check f4.eq_2
example : f4 2 a b = b := by simp -- should work
example : f4 3 0 b = b+1 := by simp
@ -57,8 +57,8 @@ example (h : i ≠ 2) : f4 i (a+1) b = f4 (i+1) a (b*2) := by simp -- should wor
| _, 0 => b+1
| _, a+1 => f5 (i+1) a (b*2)
#check f5._eq_1
#check f5._eq_2
#check f5.eq_1
#check f5.eq_2
open BitVec
@ -76,8 +76,8 @@ example (h : i ≠ 2#8) : f5 i (a+1) b = f5 (i+1) a (b*2) := by simp -- should w
| _, 0 => b+1
| _, a+1 => f6 (i+1) a (b*2)
#check f6._eq_1
#check f6._eq_2
#check f6.eq_1
#check f6.eq_2
example : f6 2#8 a b = b := by simp -- should work
example : f6 2#8 a b = b := by simp -- should work

35
tests/lean/run/namePatEqThm.lean Normal file
View file

@ -0,0 +1,35 @@
@[simp] def iota : Nat → List Nat
| 0 => []
| m@(n+1) => m :: iota n
/-- info: iota.eq_1 : iota 0 = [] -/
#guard_msgs in
#check iota.eq_1
/-- info: iota.eq_2 (n : Nat) : iota (Nat.succ n) = Nat.succ n :: iota n -/
#guard_msgs in
#check iota.eq_2
@[simp] def f : List Nat → List Nat × List Nat
| xs@(x :: ys@(y :: [])) => (xs, ys)
| xs@(x :: ys@(y :: zs)) => f zs
| _ => ([], [])
/-- info: f.eq_1 (x_1 y : Nat) : f [x_1, y] = ([x_1, y], [y]) -/
#guard_msgs in
#check f.eq_1
/--
info: f.eq_2 (x_1 y : Nat) (zs : List Nat) (x_2 : zs = [] → False) : f (x_1 :: y :: zs) = f zs
-/
#guard_msgs in
#check f.eq_2
/--
info: f.eq_3 :
∀ (x : List Nat),
(∀ (x_1 y : Nat), x = [x_1, y] → False) →
(∀ (x_1 y : Nat) (zs : List Nat), x = x_1 :: y :: zs → False) → f x = ([], [])
-/
#guard_msgs in
#check f.eq_3

4
tests/lean/run/nestedIssueMatch.lean
View file

@ -9,8 +9,8 @@ decreasing_by all_goals sorry
attribute [simp] g
#check g._eq_1
#check g._eq_2
#check g.eq_1
#check g.eq_2
theorem ex3 : g (n + 1) = match g n with
| 0 => 0

14
tests/lean/run/nestedWF.lean
View file

@ -28,12 +28,12 @@ attribute [simp] g
attribute [simp] h
attribute [simp] f
#check g._eq_1
#check g._eq_2
#check g.eq_1
#check g.eq_2
#check h._eq_1
#check h.eq_1
#check f._eq_1
#check f.eq_1
end Ex1
@ -51,14 +51,14 @@ decreasing_by all_goals sorry
theorem ex1 : g 0 = 0 := by
rw [g]
#check g._eq_1
#check g._eq_2
#check g.eq_1
#check g.eq_2
theorem ex2 : g 0 = 0 := by
unfold g
simp
#check g._unfold
#check g.def
end Ex2

2
tests/lean/run/overAndPartialAppsAtWF.lean
View file

@ -19,4 +19,4 @@ termination_by _ _ _ => a.size - i
(· + y)
termination_by x
#check f._eq_1
#check f.eq_1

14
tests/lean/run/printEqns.lean
View file

@ -1,7 +1,7 @@
/--
info: equations:
private theorem List.append._eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
private theorem List.append._eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
private theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
private theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
List.append (a :: l) x = a :: List.append l x
-/
#guard_msgs in
@ -9,8 +9,8 @@ private theorem List.append._eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α)
/--
info: equations:
private theorem List.append._eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
private theorem List.append._eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
private theorem List.append.eq_1.{u} : ∀ {α : Type u} (x : List α), List.append [] x = x
private theorem List.append.eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α) (l : List α),
List.append (a :: l) x = a :: List.append l x
-/
#guard_msgs in
@ -23,9 +23,9 @@ private theorem List.append._eq_2.{u} : ∀ {α : Type u} (x : List α) (a : α)
/--
info: equations:
private theorem ack._eq_1 : ∀ (x : Nat), ack 0 x = x + 1
private theorem ack._eq_2 : ∀ (x_2 : Nat), ack (Nat.succ x_2) 0 = ack x_2 1
private theorem ack._eq_3 : ∀ (x_2 y : Nat), ack (Nat.succ x_2) (Nat.succ y) = ack x_2 (ack (x_2 + 1) y)
private theorem ack.eq_1 : ∀ (x : Nat), ack 0 x = x + 1
private theorem ack.eq_2 : ∀ (x_2 : Nat), ack (Nat.succ x_2) 0 = ack x_2 1
private theorem ack.eq_3 : ∀ (x_2 y : Nat), ack (Nat.succ x_2) (Nat.succ y) = ack x_2 (ack (x_2 + 1) y)
-/
#guard_msgs in
#print eqns ack

8
tests/lean/run/robinson.lean
View file

@ -49,10 +49,10 @@ decreasing_by
attribute [simp] robinson
set_option pp.proofs true
#check robinson._eq_1
#check robinson._eq_2
#check robinson._eq_3
#check robinson._eq_4
#check robinson.eq_1
#check robinson.eq_2
#check robinson.eq_3
#check robinson.eq_4
theorem ex : (robinson (Term.Var 0) (Term.Var 0)).1 = some id := by
unfold robinson

6
tests/lean/run/rossel1.lean
View file

@ -21,9 +21,9 @@ def Lineage.container' {rtr i} : Lineage rtr i → (Option ID × Reactor)
attribute [simp] Lineage.container'
#check @Lineage.container'._eq_1
#check @Lineage.container'._eq_2
#check @Lineage.container'._eq_3
#check @Lineage.container'.eq_1
#check @Lineage.container'.eq_2
#check @Lineage.container'.eq_3
@[simp] def Lineage.container : Lineage rtr i → (Option ID × Reactor)
| nested l@h:(nested ..) _ => l.container

8
tests/lean/run/simpAtDefIssue.lean
View file

@ -5,7 +5,7 @@
| x+1, 5 => 2 * g x 0
| x+1, y => 2 * g x y
#check g._eq_1
#check g._eq_2
#check g._eq_3
#check g._eq_4
#check g.eq_1
#check g.eq_2
#check g.eq_3
#check g.eq_4

6
tests/lean/run/simp_eqn_bug.lean
View file

@ -5,6 +5,6 @@
| [] => a
| x::xs => x + f a xs
example : f 25 xs = 0 := by apply f._eq_1
example (h : a = 25 → False) : f a [] = a := by apply f._eq_2; assumption
example (h : a = 25 → False) : f a (x::xs) = x + f a xs := by apply f._eq_3; assumption
example : f 25 xs = 0 := by apply f.eq_1
example (h : a = 25 → False) : f a [] = a := by apply f.eq_2; assumption
example (h : a = 25 → False) : f a (x::xs) = x + f a xs := by apply f.eq_3; assumption

8
tests/lean/run/splitIssue.lean
View file

@ -19,9 +19,9 @@ theorem len_nil : len ([] : List α) = 0 := by
simp [len]
-- The `simp [len]` above generated the following equation theorems for len
#check @len._eq_1
#check @len._eq_2
#check @len._eq_3 -- It is conditional, and may be tricky to use.
#check @len.eq_1
#check @len.eq_2
#check @len.eq_3 -- It is conditional, and may be tricky to use.
theorem len_1 (a : α) : len [a] = 1 := by
simp [len]
@ -30,7 +30,7 @@ theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
conv => lhs; unfold len
-- The `unfold` tactic above generated the following theorem
#check @len._unfold
#check @len.def
theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
cases as with

16
tests/lean/run/splitList.lean
View file

@ -38,9 +38,9 @@ theorem len_nil : len ([] : List α) = 0 := by
simp [len]
-- The `simp [len]` above generated the following equation theorems for len
#check @len._eq_1
#check @len._eq_2
#check @len._eq_3
#check @len.eq_1
#check @len.eq_2
#check @len.eq_3
theorem len_1 (a : α) : len [a] = 1 := by
simp [len]
@ -49,7 +49,7 @@ theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
conv => lhs; unfold len
-- The `unfold` tactic above generated the following theorem
#check @len._unfold
#check @len.def
theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
cases as with
@ -88,9 +88,9 @@ theorem len_nil : len ([] : List α) = 0 := by
simp [len]
-- The `simp [len]` above generated the following equation theorems for len
#check @len._eq_1
#check @len._eq_2
#check @len._eq_3
#check @len.eq_1
#check @len.eq_2
#check @len.eq_3
theorem len_1 (a : α) : len [a] = 1 := by
simp [len]
@ -99,7 +99,7 @@ theorem len_2 (a b : α) (bs : List α) : len (a::b::bs) = 1 + len (b::bs) := by
conv => lhs; unfold len
-- The `unfold` tactic above generated the following theorem
#check @len._unfold
#check @len.def
theorem len_cons (a : α) (as : List α) : len (a::as) = 1 + len as := by
cases as with

6
tests/lean/run/streamEqIssue.lean
View file

@ -4,6 +4,6 @@
| n + 1, some (_, s') => hasLength n s'
| _, _ => false
#check @Stream.hasLength._eq_1
#check @Stream.hasLength._eq_2
#check @Stream.hasLength._eq_3
#check @Stream.hasLength.eq_1
#check @Stream.hasLength.eq_2
#check @Stream.hasLength.eq_3

23
tests/lean/structuralEqns.lean → tests/lean/run/structEqns.lean
View file

@ -15,11 +15,32 @@ def foo (xs ys zs : List Nat) : List Nat :=
| _ => [2]
#eval tst ``foo
#check foo._unfold
/--
info: foo.def (xs ys zs : List Nat) :
foo xs ys zs =
match (xs, ys) with
| (xs', ys') =>
match zs with
| z :: zs => foo xs ys zs
| x =>
match ys' with
| [] => [1]
| x => [2]
-/
#guard_msgs in
#check foo.def
def bar (xs ys : List Nat) : List Nat :=
match xs ++ [], ys ++ [] with
| xs', ys' => xs' ++ ys'
/--
info: def bar : List Nat → List Nat → List Nat :=
fun xs ys =>
match xs ++ [], ys ++ [] with
| xs', ys' => xs' ++ ys'
-/
#guard_msgs in
#print bar -- should not contain either `let _discr` aux binding

46
tests/lean/run/structuralEqns.lean
View file

@ -6,9 +6,9 @@ def tst (declName : Name) : MetaM Unit := do
IO.println (← getUnfoldEqnFor? declName)
#eval tst ``List.map
#check @List.map._eq_1
#check @List.map._eq_2
#check @List.map._unfold
#check @List.map.eq_1
#check @List.map.eq_2
#check @List.map.def
def foo (xs ys zs : List Nat) : List Nat :=
match (xs, ys) with
@ -21,9 +21,9 @@ def foo (xs ys zs : List Nat) : List Nat :=
#eval tst ``foo
#check foo._eq_1
#check foo._eq_2
#check foo._unfold
#check foo.eq_1
#check foo.eq_2
#check foo.def
#eval tst ``foo
@ -35,12 +35,12 @@ def g : List Nat → List Nat → Nat
| x::xs, [] => g xs []
#eval tst ``g
#check g._eq_1
#check g._eq_2
#check g._eq_3
#check g._eq_4
#check g._eq_5
#check g._unfold
#check g.eq_1
#check g.eq_2
#check g.eq_3
#check g.eq_4
#check g.eq_5
#check g.def
def h (xs : List Nat) (y : Nat) : Nat :=
match xs with
@ -51,9 +51,9 @@ def h (xs : List Nat) (y : Nat) : Nat :=
| y+1 => h xs y
#eval tst ``h
#check h._eq_1
#check h._eq_2
#check h._unfold
#check h.eq_1
#check h.eq_2
#check h.def
def r (i j : Nat) : Nat :=
i +
@ -65,10 +65,10 @@ def r (i j : Nat) : Nat :=
| Nat.succ j => r i j
#eval tst ``r
#check r._eq_1
#check r._eq_2
#check r._eq_3
#check r._unfold
#check r.eq_1
#check r.eq_2
#check r.eq_3
#check r.def
def bla (f g : α → α → α) (a : α) (i : α) (j : Nat) : α :=
f i <|
@ -80,7 +80,7 @@ def bla (f g : α → α → α) (a : α) (i : α) (j : Nat) : α :=
| Nat.succ j => bla f g a i j
#eval tst ``bla
#check @bla._eq_1
#check @bla._eq_2
#check @bla._eq_3
#check @bla._unfold
#check @bla.eq_1
#check @bla.eq_2
#check @bla.eq_3
#check @bla.def

12
tests/lean/run/structuralEqns2.lean
View file

@ -12,9 +12,9 @@ def g (i j : Nat) : Nat :=
| Nat.succ j => g i j
#eval tst ``g
#check g._eq_1
#check g._eq_2
#check g._unfold
#check g.eq_1
#check g.eq_2
#check g.def
def h (i j : Nat) : Nat :=
let z :=
@ -24,6 +24,6 @@ def h (i j : Nat) : Nat :=
z + z
#eval tst ``h
#check h._eq_1
#check h._eq_2
#check h._unfold
#check h.eq_1
#check h.eq_2
#check h.def

6
tests/lean/run/structuralEqns3.lean
View file

@ -15,6 +15,6 @@ def wk_comp : Wk n m → Wk m l → Wk n l
#eval tst ``wk_comp
#check @wk_comp._eq_1
#check @wk_comp._eq_2
#check @wk_comp._unfold
#check @wk_comp.eq_1
#check @wk_comp.eq_2
#check @wk_comp.def

6
tests/lean/run/wfEqns1.lean
View file

@ -22,6 +22,6 @@ end
#print isEven
#eval tst ``isEven
#check @isEven._eq_1
#check @isEven._eq_2
#check @isEven._unfold
#check @isEven.eq_1
#check @isEven.eq_2
#check @isEven.def

12
tests/lean/run/wfEqns2.lean
View file

@ -31,10 +31,10 @@ decreasing_by
end
#eval tst ``g
#check g._eq_1
#check g._eq_2
#check g._unfold
#check g.eq_1
#check g.eq_2
#check g.def
#eval tst ``h
#check h._eq_1
#check h._eq_2
#check h._unfold
#check h.eq_1
#check h.eq_2
#check h.def

4
tests/lean/run/wfEqns3.lean
View file

@ -15,5 +15,5 @@ decreasing_by
exact h
#eval tst ``f
#check f._eq_1
#check f._unfold
#check f.eq_1
#check f.def

12
tests/lean/run/wfEqns4.lean
View file

@ -37,12 +37,12 @@ end
#eval f 5 'a' 'b'
#eval tst ``f
#check @f._eq_1
#check @f._eq_2
#check @f._unfold
#check @f.eq_1
#check @f.eq_2
#check @f.def
#eval tst ``h
#check @h._eq_1
#check @h._eq_2
#check @h._unfold
#check @h.eq_1
#check @h.eq_2
#check @h.def

15
tests/lean/structuralEqns.lean.expected.out
View file

@ -1,15 +0,0 @@
(some _private.structuralEqns.0.foo._unfold)
foo._unfold (xs ys zs : List Nat) :
foo xs ys zs =
match (xs, ys) with
| (xs', ys') =>
match zs with
| z :: zs => foo xs ys zs
| x =>
match ys' with
| [] => [1]
| x => [2]
def bar : List Nat → List Nat → List Nat :=
fun xs ys =>
match xs ++ [], ys ++ [] with
| xs', ys' => xs' ++ ys'