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

feat: guard_msgs to treat trace messages separate (#8267)

Browse source 
This PR makes `#guard_msgs` to treat `trace` messages separate from
`info`, `warning` and `error`. It also introduce the ability to say
`#guard_msgs (pass info`, like `(drop info)` so far, and also adds
`(check info)` as the explicit form of `(info)`, for completeness.

Fixes #8266
This commit is contained in:
Joachim Breitner 2025-05-09 07:44:34 +02:00 • committed by GitHub
parent 33afaa061e
commit 0e49576fe4
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
139 changed files with 817 additions and 724 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

46
src/Init/Notation.lean
View file

@ -621,9 +621,6 @@ This is the same as `#eval show MetaM Unit from do discard doSeq`.
-/
syntax (name := runMeta) "run_meta " doSeq : command
set_option linter.missingDocs false in
syntax guardMsgsFilterSeverity := &"info" <|> &"warning" <|> &"error" <|> &"all"
/--
`#reduce <expression>` reduces the expression `<expression>` to its normal form. This
involves applying reduction rules until no further reduction is possible.
@ -640,15 +637,27 @@ of expressions.
-/
syntax (name := reduceCmd) "#reduce " (atomic("(" &"proofs" " := " &"true" ")"))? (atomic("(" &"types" " := " &"true" ")"))? term : command
set_option linter.missingDocs false in
syntax guardMsgsFilterAction := &"check" <|> &"drop" <|> &"pass"
set_option linter.missingDocs false in
syntax guardMsgsFilterSeverity := &"trace" <|> &"info" <|> &"warning" <|> &"error" <|> &"all"
/--
A message filter specification for `#guard_msgs`.
- `info`, `warning`, `error`: capture messages with the given severity level.
- `all`: capture all messages (the default).
- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level.
- `drop all`: drop every message.
These filters are processed in left-to-right order.
- `info`, `warning`, `error`: capture (non-trace) messages with the given severity level.
- `trace`: captures trace messages
- `all`: capture all messages.
The filters can be prefixed with
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
-/
syntax guardMsgsFilter := &"drop"? guardMsgsFilterSeverity
syntax guardMsgsFilter := guardMsgsFilterAction ? guardMsgsFilterSeverity
set_option linter.missingDocs false in
syntax guardMsgsWhitespaceArg := &"exact" <|> &"normalized" <|> &"lax"
@ -719,13 +728,20 @@ In general, `#guard_msgs` accepts a comma-separated list of configuration clause
```
#guard_msgs (configElt,*) in cmd
```
By default, the configuration list is `(all, whitespace := normalized, ordering := exact)`.
By default, the configuration list is `(check all, whitespace := normalized, ordering := exact)`.
Message filters (processed in left-to-right order):
- `info`, `warning`, `error`: capture messages with the given severity level.
- `all`: capture all messages (the default).
- `drop info`, `drop warning`, `drop error`: drop messages with the given severity level.
- `drop all`: drop every message.
Message filters select messages by severity:
- `info`, `warning`, `error`: (non-trace) messages with the given severity level.
- `trace`: trace messages
- `all`: all messages.
The filters can be prefixed with the action to take:
- `check` (the default): capture and check the message
- `drop`: drop the message
- `pass`: let the message pass through
If no filter is specified, `check all` is assumed. Otherwise, these filters are processed in
left-to-right order, with an implicit `pass all` at the end.
Whitespace handling (after trimming leading and trailing whitespace):
- `whitespace := exact` requires an exact whitespace match.

51
src/Lean/Elab/GuardMsgs.lean
View file

@ -31,10 +31,13 @@ private def messageToStringWithoutPos (msg : Message) : BaseIO String := do
unless msg.caption == "" do
str := msg.caption ++ ":\n" ++ str
if !("\n".isPrefixOf str) then str := " " ++ str
match msg.severity with
| MessageSeverity.information => str := "info:" ++ str
| MessageSeverity.warning => str := "warning:" ++ str
| MessageSeverity.error => str := "error:" ++ str
if msg.isTrace then
str := "trace:" ++ str
else
match msg.severity with
| MessageSeverity.information => str := "info:" ++ str
| MessageSeverity.warning => str := "warning:" ++ str
| MessageSeverity.error => str := "error:" ++ str
if str.isEmpty || str.back != '\n' then
str := str ++ "\n"
return str
@ -46,7 +49,7 @@ inductive SpecResult
/-- Drop the message and delete it. -/
| drop
/-- Do not capture the message. -/
| passthrough
| pass
/-- The method to use when normalizing whitespace, after trimming. -/
inductive WhitespaceMode
@ -64,6 +67,25 @@ inductive MessageOrdering
/-- Sort the produced messages. -/
| sorted
def parseGuardMsgsFilterAction (action? : Option (TSyntax ``guardMsgsFilterAction)) :
CommandElabM SpecResult := do
if let some action := action? then
match action with
| `(guardMsgsFilterAction| check) => pure .check
| `(guardMsgsFilterAction| drop) => pure .drop
| `(guardMsgsFilterAction| pass) => pure .pass
| _ => throwUnsupportedSyntax
else
pure .check
def parseGuardMsgsFilterSeverity : TSyntax ``guardMsgsFilterSeverity → CommandElabM (Message → Bool)
| `(guardMsgsFilterSeverity| trace) => pure fun msg => msg.isTrace
| `(guardMsgsFilterSeverity| info) => pure fun msg => !msg.isTrace && msg.severity == .information
| `(guardMsgsFilterSeverity| warning) => pure fun msg => !msg.isTrace && msg.severity == .warning
| `(guardMsgsFilterSeverity| error) => pure fun msg => !msg.isTrace && msg.severity == .error
| `(guardMsgsFilterSeverity| all) => pure fun _ => true
| _ => throwUnsupportedSyntax
/-- Parses a `guardMsgsSpec`.
- No specification: check everything.
- With a specification: interpret the spec, and if nothing applies pass it through. -/
@ -79,24 +101,23 @@ def parseGuardMsgsSpec (spec? : Option (TSyntax ``guardMsgsSpec)) :
let mut whitespace : WhitespaceMode := .normalized
let mut ordering : MessageOrdering := .exact
let mut p? : Option (Message → SpecResult) := none
let pushP (s : MessageSeverity) (drop : Bool) (p? : Option (Message → SpecResult))
let pushP (action : SpecResult) (msgP : Message → Bool) (p? : Option (Message → SpecResult))
(msg : Message) : SpecResult :=
let p := p?.getD fun _ => .passthrough
if msg.severity == s then if drop then .drop else .check
else p msg
if msgP msg then
action
else
(p?.getD fun _ => .pass) msg
for elt in elts.reverse do
match elt with
| `(guardMsgsSpecElt| $[drop%$drop?]? info) => p? := pushP .information drop?.isSome p?
| `(guardMsgsSpecElt| $[drop%$drop?]? warning) => p? := pushP .warning drop?.isSome p?
| `(guardMsgsSpecElt| $[drop%$drop?]? error) => p? := pushP .error drop?.isSome p?
| `(guardMsgsSpecElt| $[drop%$drop?]? all) => p? := some fun _ => if drop?.isSome then .drop else .check
| `(guardMsgsSpecElt| $[$action?]? $sev) => p? := pushP (← parseGuardMsgsFilterAction action?) (← parseGuardMsgsFilterSeverity sev) p?
| `(guardMsgsSpecElt| whitespace := exact) => whitespace := .exact
| `(guardMsgsSpecElt| whitespace := normalized) => whitespace := .normalized
| `(guardMsgsSpecElt| whitespace := lax) => whitespace := .lax
| `(guardMsgsSpecElt| ordering := exact) => ordering := .exact
| `(guardMsgsSpecElt| ordering := sorted) => ordering := .sorted
| _ => throwUnsupportedSyntax
return (whitespace, ordering, p?.getD fun _ => .check)
let defaultP := fun _ => .check
return (whitespace, ordering, p?.getD defaultP)
/-- An info tree node corresponding to a failed `#guard_msgs` invocation,
used for code action support. -/
@ -157,7 +178,7 @@ def MessageOrdering.apply (mode : MessageOrdering) (msgs : List String) : List S
match specFn msg with
| .check => toCheck := toCheck.add msg
| .drop => pure ()
| .passthrough => toPassthrough := toPassthrough.add msg
| pass => toPassthrough := toPassthrough.add msg
let strings ← toCheck.toList.mapM (messageToStringWithoutPos ·)
let strings := ordering.apply strings
let res := "---\n".intercalate strings |>.trim

10
src/Lean/Message.lean
View file

@ -147,6 +147,13 @@ def kind : MessageData → Name
| tagged n _ => n
| _ => .anonymous
def isTrace : MessageData → Bool
| withContext _ msg => msg.isTrace
| withNamingContext _ msg => msg.isTrace
| tagged _ msg => msg.isTrace
| .trace _ _ _ => true
| _ => false
/-- An empty message. -/
def nil : MessageData :=
ofFormat Format.nil
@ -424,6 +431,9 @@ namespace Message
@[inherit_doc MessageData.kind] abbrev kind (msg : Message) :=
msg.data.kind
def isTrace (msg : Message) : Bool :=
msg.data.isTrace
/-- Serializes the message, converting its data into a string and saving its kind. -/
@[inline] def serialize (msg : Message) : BaseIO SerialMessage := do
return {msg with kind := msg.kind, data := ← msg.data.toString}

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

@ -10,7 +10,7 @@ set_option Elab.async false -- for stable message ordering in #guard_msgs
/--
warning: declaration uses 'sorry'
---
info: [Meta.Tactic.simp.rewrite] h₁:1000:
trace: [Meta.Tactic.simp.rewrite] h₁:1000:
k ≤ v - 1
==>
True
@ -47,7 +47,7 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v):
/--
warning: declaration uses 'sorry'
---
info: [Meta.Tactic.simp.rewrite] h₁:1000:
trace: [Meta.Tactic.simp.rewrite] h₁:1000:
k ≤ v - 1
==>
True
@ -82,7 +82,7 @@ example (h₁: k ≤ v - 1) (h₂: 0 < v):
/--
warning: declaration uses 'sorry'
---
info: [Meta.Tactic.simp.rewrite] h₁:1000:
trace: [Meta.Tactic.simp.rewrite] h₁:1000:
k ≤ v - 1
==>
True

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

@ -3,7 +3,7 @@ variable (n v₁ v₂) (hv₁: v₁ < n + 1) (hv₂: v₂ < n + 1)
theorem foo (_: ¬ Fin.mk v₂ hv₂ = Fin.mk v₁ hv₁ ): True := trivial
/--
info: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
trace: [Meta.Tactic.simp.unify] eq_self:1000, failed to unify
?a = ?a
with
⟨v₂, hv₂⟩ = ⟨v₁, hv₁⟩

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

@ -7,7 +7,7 @@ theorem mul_comm (a b : α) : a * b = b * a := sorry
set_option trace.Meta.Tactic.simp true
/--
info: [Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected Left a ==> default * a
trace: [Meta.Tactic.simp.rewrite] mul_comm:1000:perm, perm rejected Left a ==> default * a
[Meta.Tactic.simp.rewrite] mul_comm:1000:perm:
Right a
==>

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

@ -94,7 +94,7 @@ end
Rewrote forall, remains a forall, since domain is `Nat`.
-/
/--
info: P : Nat → Prop
trace: P : Nat → Prop
q : Prop
h : ∀ (n : Nat), P n = q
hq : q
@ -111,7 +111,7 @@ example (P : Nat → Prop) (q : Prop) (h : ∀ n, P n = q) (hq : q) :
When `pp.foralls` is false, uses non-dependent `→`.
-/
/--
info: P : Nat → Prop
trace: P : Nat → Prop
q : Prop
h : (n : Nat) → P n = q
hq : q
@ -129,7 +129,7 @@ example (P : Nat → Prop) (q : Prop) (h : ∀ n, P n = q) (hq : q) :
Rewrote forall, turns into an implication, since domain is a proposition.
-/
/--
info: p : Prop
trace: p : Prop
P : p → Prop
q : Prop
h : ∀ (n : p), P n = q

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

@ -2,7 +2,7 @@
2 * a
/--
info: case h
trace: case h
x : Nat
⊢ 2 * x = x + x
-/
@ -19,7 +19,7 @@ by
| a => 2 * a
/--
info: case h
trace: case h
x : Nat
⊢ 2 * x = x + x
-/

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

@ -1,7 +1,7 @@
/--
info: ⊢ 1.2 < 2
trace: ⊢ 1.2 < 2
---
info: ⊢ 1.2 < 2
trace: ⊢ 1.2 < 2
---
warning: declaration uses 'sorry'
-/

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

@ -8,17 +8,17 @@ inductive Forall (P : α → Prop) : List α → Prop
| nil : Forall P []
| cons : {x : α} → P x → Forall P l → Forall P (x::l)
inductive Tree : Type :=
inductive Tree : Type where
| leaf : Nat → Tree
| node : List Tree → Tree
set_option trace.Meta.IndPredBelow true in
/-- info: [Meta.IndPredBelow] Nested or not recursive -/
/-- trace: [Meta.IndPredBelow] Nested or not recursive -/
#guard_msgs in
/-- Despite not having `.below` and `.brecOn`,
the type is still usable thanks to well-founded recursion. -/
inductive OnlyZeros : Tree → Prop :=
inductive OnlyZeros : Tree → Prop where
| leaf : OnlyZeros (.leaf 0)
| node (l : List Tree): Forall OnlyZeros l → OnlyZeros (.node l)

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

@ -1,7 +1,7 @@
set_option pp.coercions false -- Show `OfNat.ofNat` when present for clarity
/--
info: x : Nat
trace: x : Nat
⊢ OfNat.ofNat 2 = x
---
warning: declaration uses 'sorry'
@ -13,7 +13,7 @@ example : nat_lit 2 = x := by
sorry
/--
info: x : Nat
trace: x : Nat
⊢ OfNat.ofNat 2 = x
---
warning: declaration uses 'sorry'
@ -25,7 +25,7 @@ example : nat_lit 2 = x := by
sorry
/--
info: α : Nat → Type
trace: α : Nat → Type
f : (n : Nat) → α n
x : α (OfNat.ofNat 2)
⊢ f (OfNat.ofNat 2) = x
@ -39,12 +39,12 @@ example (α : Nat → Type) (f : (n : Nat) → α n) (x : α 2) : f (nat_lit 2)
sorry
/--
info: x : Nat
trace: x : Nat
f : Nat → Nat
h : f (OfNat.ofNat 2) = x
⊢ f (OfNat.ofNat 2) = x
---
info: x : Nat
trace: x : Nat
f : Nat → Nat
h : f (OfNat.ofNat 2) = x
⊢ f 2 = x
@ -57,12 +57,12 @@ example (f : Nat → Nat) (h : f 2 = x) : f 2 = x := by
assumption
/--
info: α : Nat → Type
trace: α : Nat → Type
f : (n : Nat) → α n
x : α (OfNat.ofNat 2)
⊢ f (OfNat.ofNat 2) = x
---
info: α : Nat → Type
trace: α : Nat → Type
f : (n : Nat) → α n
x : α (OfNat.ofNat 2)
⊢ f 2 = x

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

@ -6,7 +6,7 @@
The function `g` is "over-applied". Previously, conv-mode `congr` failed.
-/
/--
info: case a
trace: case a
a b : Nat
g : {α : Type} → α → α
f : Nat → Nat
@ -40,19 +40,19 @@ While we are here, test `arg` too via `enter`.
-/
/--
info: a b : Nat
trace: a b : Nat
g : {α : Type} → α → α
f : Nat → Nat
h : a = b
| a
---
info: a b : Nat
trace: a b : Nat
g : {α : Type} → α → α
f : Nat → Nat
h : a = b
| f
---
info: a b : Nat
trace: a b : Nat
g : {α : Type} → α → α
f : Nat → Nat
h : a = b

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

@ -14,7 +14,7 @@ example : U := by
simp [foo, T.mk]
/--
info: [Meta.Tactic.simp.discharge] bar discharge ✅️
trace: [Meta.Tactic.simp.discharge] bar discharge ✅️
autoParam T _auto✝
[Meta.Tactic.simp.rewrite] T.mk:1000:
T

24
tests/lean/run/3467.lean
View file

@ -13,13 +13,13 @@ Basic diamond
set_option structure.strictResolutionOrder true
set_option trace.Elab.structure.resolutionOrder true
/-- info: [Elab.structure.resolutionOrder] computed resolution order: [A] -/
/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [A] -/
#guard_msgs in structure A
/-- info: [Elab.structure.resolutionOrder] computed resolution order: [B, A] -/
/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [B, A] -/
#guard_msgs in structure B extends A
/-- info: [Elab.structure.resolutionOrder] computed resolution order: [C, A] -/
/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [C, A] -/
#guard_msgs in structure C extends A
/-- info: [Elab.structure.resolutionOrder] computed resolution order: [D, B, C, A] -/
/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [D, B, C, A] -/
#guard_msgs in structure D extends B, C
def A.x (a : A) : Bool := default
@ -55,7 +55,7 @@ Example resolution order failure
warning: failed to compute strict resolution order:
- parent 'B' must come after parent 'D'
---
info: [Elab.structure.resolutionOrder] computed resolution order: [D', B, D, C, A]
trace: [Elab.structure.resolutionOrder] computed resolution order: [D', B, D, C, A]
-/
#guard_msgs in
structure D' extends B, D
@ -67,17 +67,17 @@ Example from issue 3467.
namespace Issue3467
/-- info: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.X] -/
/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.X] -/
#guard_msgs in
structure X where
base : Nat
/-- info: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.A, Issue3467.X] -/
/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.A, Issue3467.X] -/
#guard_msgs in
structure A extends X where
countA : Nat
/-- info: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.B, Issue3467.X] -/
/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.B, Issue3467.X] -/
#guard_msgs in
structure B extends X where
countB : Nat
@ -95,7 +95,7 @@ def getTwiceCountB (b : B) := b.countB * 2
end B
/--
info: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.C, Issue3467.A, Issue3467.B, Issue3467.X]
trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue3467.C, Issue3467.A, Issue3467.B, Issue3467.X]
-/
#guard_msgs in
structure C extends A, B
@ -112,20 +112,20 @@ end Issue3467
namespace Issue1881
/-- info: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo1] -/
/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo1] -/
#guard_msgs in
structure Foo1 where
a : Nat
b : Nat
/-- info: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo2] -/
/-- trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo2] -/
#guard_msgs in
structure Foo2 where
a : Nat
c : Nat
/--
info: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo3, Issue1881.Foo1, Issue1881.Foo2]
trace: [Elab.structure.resolutionOrder] computed resolution order: [Issue1881.Foo3, Issue1881.Foo1, Issue1881.Foo2]
-/
#guard_msgs in
structure Foo3 extends Foo1, Foo2 where

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

@ -12,8 +12,8 @@ example : p 0 0 := by
simp [foo 1] -- will not simplify
simp [foo 0]
/-- info: ⊢ p 0 0 -/
#guard_msgs in
/-- trace: ⊢ p 0 0 -/
#guard_msgs (trace) in
example : p 0 0 ∧ p 1 1 := by
simp [foo 1]
trace_state

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

@ -13,7 +13,7 @@ universe v u
variable (α : Sort u)
structure Opposite :=
structure Opposite where
op ::
unop : α
@ -714,7 +714,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
/--
info: [simp] Diagnostics
trace: [simp] Diagnostics
[simp] theorems with bad keys
[simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
@ -735,7 +735,7 @@ example (M : Comon_ (Mon_ C)) : Mon_ (Comon_ C) where
attribute [simp] foo
/--
info: [simp] Diagnostics
trace: [simp] Diagnostics
[simp] theorems with bad keys
[simp] foo, key: @Quiver.Hom.unop _ _ _ _ (@Opposite.op (@Quiver.Hom _ _ _.1 _.1) _)
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters

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

@ -7,7 +7,7 @@ structure HH (A B : Nat) where
set_option pp.explicit true
/--
info: S T f : Nat
trace: S T f : Nat
⊢ @Eq (HH S T) (@HH.mk S T f trivial) (@id (HH S T) (@HH.mk S T f trivial))
-/
#guard_msgs in
@ -18,7 +18,7 @@ example {S T : Nat} (f : Nat) :
rfl
/--
info: S T f : Nat
trace: S T f : Nat
⊢ @Eq (HH S T) (@HH.mk S T f trivial) (@id (HH S T) (@HH.mk S T f trivial))
-/
#guard_msgs in
@ -29,7 +29,7 @@ example {S T : Nat} (f : Nat) :
rfl
/--
info: S T f : Nat
trace: S T f : Nat
⊢ @Eq (HH S T) (@HH.mk S T f trivial) (@id (HH S T) (@HH.mk S T f trivial))
-/
#guard_msgs in

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

@ -1,5 +1,5 @@
/--
info: case h
trace: case h
d g : Nat
H1 : d = g
⊢ ?w = g

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

@ -24,7 +24,7 @@ p :
p =
state
---
info: [split.failure] `split` tactic failed to generalize discriminant(s) at
trace: [split.failure] `split` tactic failed to generalize discriminant(s) at
match h : step state with
| none => [state]
| some newState => state :: countdown newState

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

@ -13,7 +13,7 @@ def thingy : List (Nat ⊕ Nat) → List Bool
| _ => []
termination_by l => l.length
/-- info: ⊢ [] = [] -/
/-- trace: ⊢ [] = [] -/
#guard_msgs in
theorem thingy_empty : thingy [] = [] := by
unfold thingy

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

@ -16,7 +16,7 @@ instance : Vec' Nat := ⟨⟩
set_option trace.Meta.Tactic.simp true
/--
info: [Meta.Tactic.simp.rewrite] differential_of_linear:1000:
trace: [Meta.Tactic.simp.rewrite] differential_of_linear:1000:
differential f x dx
==>
f dx

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

@ -25,13 +25,11 @@ elab "test" : tactic => do
levelParams := []
}
/--
info: [Elab.debug] traced
-/
/-- trace: [Elab.debug] traced -/
#guard_msgs in
theorem f1 : True := by test; trivial
/-- info: [Elab.debug] traced -/
/-- trace: [Elab.debug] traced -/
#guard_msgs in
def f2 : True := by test; trivial

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

@ -15,7 +15,7 @@ def cseSizeTest : PassInstaller :=
set_option trace.Compiler.test true in
/--
info: [Compiler.test] Starting wrapper test cseSizeLeq for cse occurrence 0
trace: [Compiler.test] Starting wrapper test cseSizeLeq for cse occurrence 0
[Compiler.test] Wrapper test cseSizeLeq for cse occurrence 0 successful
[Compiler.test] Starting post condition test cseFix for cse occurrence 0
[Compiler.test] Post condition test cseFix for cse occurrence 0 successful

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

@ -15,7 +15,7 @@ def cseSizeTest : PassInstaller :=
set_option trace.Compiler.test true in
/--
info: [Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0
trace: [Compiler.test] Starting wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0
[Compiler.test] Wrapper test findJoinPointsSizeLeq for findJoinPoints occurrence 0 successful
[Compiler.test] Starting post condition test findJoinPointsFix for findJoinPoints occurrence 0
[Compiler.test] Post condition test findJoinPointsFix for findJoinPoints occurrence 0 successful

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

@ -16,7 +16,7 @@ def floatLetInSizeTest : PassInstaller :=
set_option trace.Compiler.test true in
/--
info: [Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occurrence 0
trace: [Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occurrence 0
[Compiler.test] Wrapper test floatLetInSizeEq for floatLetIn occurrence 0 successful
[Compiler.test] Starting wrapper test floatLetInSizeEq for floatLetIn occurrence 1
[Compiler.test] Wrapper test floatLetInSizeEq for floatLetIn occurrence 1 successful

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

@ -15,7 +15,7 @@ def pullInstancesSizeTest : PassInstaller :=
set_option trace.Compiler.test true in
/--
info: [Compiler.test] Starting wrapper test pullInstancesSizeEq for pullInstances occurrence 0
trace: [Compiler.test] Starting wrapper test pullInstancesSizeEq for pullInstances occurrence 0
[Compiler.test] Wrapper test pullInstancesSizeEq for pullInstances occurrence 0 successful
[Compiler.test] Starting post condition test pullInstancesFix for pullInstances occurrence 0
[Compiler.test] Post condition test pullInstancesFix for pullInstances occurrence 0 successful

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

@ -15,7 +15,7 @@ def simpReaderTest : PassInstaller :=
set_option trace.Compiler.test true in
/--
info: [Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 0
trace: [Compiler.test] Starting post condition test simpInlinesBinds for simp occurrence 0
[Compiler.test] Post condition test simpInlinesBinds for simp occurrence 0 successful
[Compiler.test] Starting post condition test simpFix for simp occurrence 0
[Compiler.test] Post condition test simpFix for simp occurrence 0 successful

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

@ -5,21 +5,21 @@ def ack : Nat → Nat → Nat
termination_by a b => (a, b)
/--
info: [diag] Diagnostics
trace: [diag] Diagnostics
[kernel] unfolded declarations (max: 147, num: 3):
[kernel] OfNat.ofNat ↦ 147
[kernel] Add.add ↦ 61
[kernel] HAdd.hAdd ↦ 61
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
---
info: [simp] Diagnostics
trace: [simp] Diagnostics
[simp] used theorems (max: 59, num: 1):
[simp] ack.eq_3 ↦ 59
[simp] tried theorems (max: 59, num: 1):
[simp] ack.eq_3 ↦ 59, succeeded: 59
use `set_option diagnostics.threshold <num>` to control threshold for reporting counters
---
info: [diag] Diagnostics
trace: [diag] Diagnostics
[kernel] unfolded declarations (max: 147, num: 3):
[kernel] OfNat.ofNat ↦ 147
[kernel] Add.add ↦ 61

18
tests/lean/run/allGoals.lean
View file

@ -12,7 +12,7 @@ open Lean Elab Tactic
Tactics may assign other goals. There are three goals, but the tactic is run twice.
-/
/--
info: case a
trace: case a
⊢ 1 ≤ ?m
case a
@ -21,7 +21,7 @@ case a
case m
⊢ Nat
---
info: running tac
trace: running tac
running tac
-/
#guard_msgs in
@ -94,7 +94,7 @@ case refine_1
b : Bool
⊢ Unit
---
info: case refine_2.false
trace: case refine_2.false
v : Unit := ?_ false
⊢ True
@ -149,7 +149,7 @@ error: Case tag 'true' not found.
The only available case tag is 'refine_1'.
---
info: case refine_2.false
trace: case refine_2.false
v : Unit := ()
this : () = v
⊢ True
@ -160,7 +160,7 @@ case refine_1
b : Bool
⊢ Unit
---
info: in true
trace: in true
-/
#guard_msgs in
example (b : Bool) : True := by
@ -200,7 +200,7 @@ This is the responsibility of `first`, but `all_goals` coordinates by being sure
-/
/--
info: rfl
trace: rfl
rfl
-/
#guard_msgs in
@ -311,7 +311,7 @@ theorem idEq (a : α) : id a = a :=
rfl
/--
info: case sunday
trace: case sunday
⊢ sunday.previous.next = id sunday
case monday
@ -332,7 +332,7 @@ case friday
case saturday
⊢ saturday.previous.next = id saturday
---
info: case sunday
trace: case sunday
⊢ sunday.previous.next = sunday
case monday
@ -362,7 +362,7 @@ theorem Weekday.test (d : Weekday) : next (previous d) = id d := by
all_goals rfl
/--
info: case sunday
trace: case sunday
⊢ sunday.previous.next = sunday
case monday

10
tests/lean/run/apply_tac.lean
View file

@ -5,7 +5,7 @@ open Lean.Meta
open Lean.Elab.Tactic
/--
info: a b c : Nat
trace: a b c : Nat
h₁ : a = b
h₂ : b = c
⊢ a = b
@ -17,7 +17,7 @@ example (a b c : Nat) (h₁ : a = b) (h₂ : b = c) : a = c := by
exact h₁
/--
info: case h
trace: case h
a : Nat
⊢ ?w = a
@ -38,7 +38,7 @@ elab "eapply " e:term : tactic =>
evalApplyLikeTactic (MVarId.apply (cfg := {newGoals := ApplyNewGoals.nonDependentOnly})) e
/--
info: case h
trace: case h
a : Nat
⊢ ?w = a
-/
@ -49,7 +49,7 @@ example (a : Nat) : ∃ x, x = a := by
rfl
/--
info: case w
trace: case w
a : Nat
⊢ Nat
@ -57,7 +57,7 @@ case h
a : Nat
⊢ ?w = a
---
info: case h
trace: case h
a : Nat
⊢ a = a
-/

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

@ -39,7 +39,7 @@ The auto-bound implicit creates a new variable `A✝`, which comes from the argu
(This has been the case well before the creation of this test.)
-/
/--
info: A✝ : Sort u_1
trace: A✝ : Sort u_1
a : A✝
_x : constUnit a
⊢ True
@ -66,7 +66,7 @@ The duplication was because `runTermElabM` wasn't resetting the local context.
The poor variable name was due to using `mkForallFVars` instead of `mkForallFVars'`.
-/
/--
info: A✝ : Sort _
trace: A✝ : Sort _
a : A✝
x : constUnit a
⊢ True
@ -82,7 +82,7 @@ Checking that `#check` also has the improvement.
/--
info: 1 : Nat
---
info: A✝ : Sort _
trace: A✝ : Sort _
a : A✝
x : constUnit a
⊢ ?_

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

@ -84,7 +84,7 @@ error: unsolved goals
names : List String
⊢ (!names.any fun x => !"Waldo".isPrefixOf x) = true
---
info: names : List String
trace: names : List String
⊢ (!names.any fun x => binderNameHint x (fun name => "Waldo".isPrefixOf name) !"Waldo".isPrefixOf x) = true
-/
#guard_msgs in

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

@ -12,7 +12,7 @@ def z : Nat := 0
set_option trace.Meta.Tactic.simp.rewrite true
/--
info: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000:
trace: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000:
binderNameHint x y z
==>
z
@ -24,7 +24,7 @@ example : binderNameHint x y z = 0 := by
simp [x, y, z]
/--
info: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000:
trace: [Meta.Tactic.simp.rewrite] ↓ binderNameHint.eq_1:1000:
binderNameHint x y z
==>
z

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

@ -12,7 +12,7 @@ elab "foo" t:term : tactic => do
#check (∃ f : Nat → Nat, ∀ x, f x = 0) -- works fine
/--
info: [debug] canonicalizing ∃ f, ∀ (x : Nat), f x = 0
trace: [debug] canonicalizing ∃ f, ∀ (x : Nat), f x = 0
[debug] canonicalized it to ∃ f, ∀ (x : Nat), f x = 0
-/
#guard_msgs in

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

@ -6,7 +6,7 @@ example : ¬ true = false := by
/-! Test `binop%` -/
/--
info: y x : Nat
trace: y x : Nat
h : y = 0
⊢ Add.add x y = x
-/
@ -19,7 +19,7 @@ example (h : y = 0) : x + y = x := by
done
/--
info: y x : Nat
trace: y x : Nat
h : y = 0
⊢ Add.add x y = x
-/

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

@ -85,7 +85,7 @@ is not definitionally equal to target
`change` can create new metavariables and assign them
-/
/--
info: x y z : Nat
trace: x y z : Nat
w : Nat := x + y
⊢ x + y = z
-/
@ -114,7 +114,7 @@ example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 :
`change` reorders hypotheses if necessary
-/
/--
info: x y z w : Nat
trace: x y z w : Nat
a : Nat := x + y
h : a = z + w
⊢ True
@ -199,7 +199,7 @@ example (m n : Nat) : m + 2 = n := by
conv `change` to create a metavariable
-/
/--
info: a b c d : Nat
trace: a b c d : Nat
e : Nat := a + b
⊢ a + b + c = d
-/

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

@ -41,7 +41,7 @@ printDef `foo1
set_option pp.mvars false in
/--
info: [Meta.debug] foo1 α f b ?_ ?_
trace: [Meta.debug] foo1 α f b ?_ ?_
[Meta.debug] fun α f b _x_1 _x_2 => _x_2 (f b)
-/
#guard_msgs in
@ -63,7 +63,7 @@ printDef `foo2
set_option pp.mvars false in
/--
info: [Meta.debug] foo2 α v1 v2 p ?_
trace: [Meta.debug] foo2 α v1 v2 p ?_
[Meta.debug] fun α v1 v2 p _x_1 => v1 = v2 ∧ (_x_1 v2 ∨ p)
-/
#guard_msgs in

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

@ -4,7 +4,7 @@
-- With the option off (default)
/--
info: n : Nat
trace: n : Nat
h : n = 0
⊢ ↑n = 0
-/
@ -15,7 +15,7 @@ example (n : Nat) (h : n = 0) : (↑n : Int) = 0 := by
-- With the option on
/--
info: n : Nat
trace: n : Nat
h : n = 0
⊢ (↑n : Int) = 0
-/

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

@ -3,7 +3,7 @@ set_option pp.analyze false
def p (x y : Nat) := x = y
/--
info: x y : Nat
trace: x y : Nat
⊢ x + y = y.add x
-/
#guard_msgs in
@ -18,7 +18,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
rfl
/--
info: x y : Nat
trace: x y : Nat
⊢ x + y = y.add x
-/
#guard_msgs in
@ -32,7 +32,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
rfl
/--
info: x y : Nat
trace: x y : Nat
⊢ x.add y = y.add x
-/
#guard_msgs in
@ -48,7 +48,7 @@ example (x y : Nat) : p (x + y) (y + x + 0) := by
apply Nat.add_comm x y
/--
info: x y : Nat
trace: x y : Nat
| x + y
-/
#guard_msgs in
@ -109,14 +109,14 @@ example (h₁ : f x = x + 1) (h₂ : x > 0) : f x = f x := by
exact h₁
/--
info: x y : Nat
trace: x y : Nat
f : Nat → Nat → Nat
g : Nat → Nat
h₁ : ∀ (z : Nat), f z z = z
h₂ : ∀ (x y : Nat), f (g x) (g y) = y
⊢ f (g (0 + y)) (f (g x) (g x)) = x
---
info: x y : Nat
trace: x y : Nat
f : Nat → Nat → Nat
g : Nat → Nat
h₁ : ∀ (z : Nat), f z z = z
@ -133,7 +133,7 @@ example (x y : Nat) (f : Nat → Nat → Nat) (g : Nat → Nat) (h₁ : ∀ z, f
set_option linter.unusedVariables false
/--
info: x y : Nat
trace: x y : Nat
f : Nat → Nat → Nat
g : Nat → Nat
h₁ : ∀ (z : Nat), f z z = z
@ -141,7 +141,7 @@ h₂ : ∀ (x y : Nat), f (g x) (g y) = y
h₃ : f (g x) (g x) = 0
⊢ g x = 0
---
info: x y : Nat
trace: x y : Nat
f : Nat → Nat → Nat
g : Nat → Nat
h₁ : ∀ (z : Nat), f z z = z

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

@ -30,10 +30,10 @@ example (p q₁ q₂ : Prop) (h : q₁ ↔ q₂) : (p → q₁) ↔ (p → q₂)
-- Dependent implications
/--
info: i✝ : Nat
trace: i✝ : Nat
| i✝ < 10
---
info: a✝¹ : Nat
trace: a✝¹ : Nat
a✝ : a✝¹ < 10
| ↑⟨a✝¹, ⋯⟩ = a✝¹
-/

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

@ -29,7 +29,7 @@ testing...
---
info: 10
---
info: [Elab] trace message
trace: [Elab] trace message
-/
#guard_msgs in
#eval f

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

@ -1,6 +1,6 @@
set_option trace.Elab true
/--
info: α✝ : Sort u_1
trace: α✝ : Sort u_1
a b : α✝
h : a = b
⊢ (fun x => x) a = b

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

@ -8,7 +8,7 @@ termination_by n
/--
info: 89
---
info: [diag] Diagnostics
trace: [diag] Diagnostics
[reduction] unfolded declarations (max: 407, num: 3):
[reduction] Nat.rec ↦ 407
[reduction] Or.rec ↦ 144

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

@ -9,7 +9,7 @@ theorem f_eq : f (x + 1) = q (f x) := rfl
set_option trace.Meta.debug true
/--
info: [diag] Diagnostics
trace: [diag] Diagnostics
[reduction] unfolded declarations (max: 15, num: 6):
[reduction] Nat.rec ↦ 15
[reduction] Add.add ↦ 10
@ -30,7 +30,7 @@ example : f (x + 5) = q (q (q (q (q (f x))))) :=
rfl
/--
info: [diag] Diagnostics
trace: [diag] Diagnostics
[reduction] unfolded declarations (max: 15, num: 6):
[reduction] Nat.rec ↦ 15
[reduction] Add.add ↦ 10

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

@ -7,7 +7,7 @@ axiom P : Bool → Prop
axiom P_false : P false
/--
info: x : Nat
trace: x : Nat
⊢ P (1 + x).isZero
-/
#guard_msgs in

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

@ -10,7 +10,7 @@ theorem write_simplify_test_0 (a x y : BitVec 64)
simp only [setWidth_eq, BitVec.cast_eq]
/--
info: write : (n : Nat) → BitVec 64 → BitVec (n * 8) → Type → Type
trace: write : (n : Nat) → BitVec 64 → BitVec (n * 8) → Type → Type
s aux : Type
a x y : BitVec 64
h : 128 = 128

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

@ -26,7 +26,7 @@ elab "try" t:tactic : tactic => do
set_option linter.unusedVariables false
/--
info: case h₁
trace: case h₁
x y z : Nat
h1 : y = z
h2 : x = x
@ -47,7 +47,7 @@ h2 : x = x
h3 : x = y
⊢ Nat
---
info: case h₂
trace: case h₂
x y z : Nat
h1 : y = z
h2 : x = x

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

@ -7,7 +7,7 @@ def f (x : MyEmpty) : Nat :=
set_option trace.Compiler.result true
/--
info: [Compiler.result] size: 0
trace: [Compiler.result] size: 0
def f x : Nat :=
⊥
-/

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

@ -6,7 +6,7 @@ def f (x y : Nat) : Nat :=
| x+1, y => 2 * f x y
/--
info: x y : Nat
trace: x y : Nat
h : y ≠ 5
⊢ ∃ z, 2 * f x y = 2 * z
-/
@ -25,7 +25,7 @@ theorem ex1 (x : Nat) (y : Nat) (h : y ≠ 5) : ∃ z, f (x+1) y = 2 * z := by
| x+1, y => 2 * g x y
/--
info: x y : Nat
trace: x y : Nat
h : y ≠ 5
⊢ ∃ z, 2 * g x y = 2 * z
-/
@ -37,7 +37,7 @@ theorem ex2 (x : Nat) (y : Nat) (h : y ≠ 5) : ∃ z, g (x+1) y = 2 * z := by
rfl
/--
info: x y : Nat
trace: x y : Nat
h : y = 5 → False
⊢ ∃ z, 2 * f x y = 2 * z
-/
@ -59,7 +59,7 @@ theorem ex3 (x : Nat) (y : Nat) (h : y = 5 → False) : ∃ z, f (x+1) y = 2 * z
#check f2.eq_4
/--
info: x y z : Nat
trace: x y z : Nat
h : y = 5 → z = 6 → False
⊢ ∃ w, 2 * f2 x y z = 2 * w
-/

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

@ -20,7 +20,7 @@ set_option pp.funBinderTypes true
set_option pp.letVarTypes true
set_option trace.Compiler.result true
/--
info: [Compiler.result] size: 1
trace: [Compiler.result] size: 1
def Erased.mk (α : lcErased) (a : lcAny) : PSigma lcErased lcAny :=
let _x.1 : PSigma lcErased lcAny := PSigma.mk lcErased ◾ ◾ ◾;
return _x.1

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

@ -1,5 +1,5 @@
/--
info: α : Type u_1
trace: α : Type u_1
inst : DecidableEq α
inst_1 : Add α
a_1 b_1 : α
@ -9,14 +9,14 @@ h_1 : b = a_2
a : α
⊢ a = b
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example [DecidableEq α] [Add α] (a b : α) (_ : a = b) (a : α) (b : α) (_ : b = a) (a : α) : a = b := by
expose_names
trace_state
sorry
/--
info: α : Sort u_1
trace: α : Sort u_1
a b : α
h_1 : a = b
h_2 : True
@ -24,14 +24,14 @@ h_3 : True ∨ False
h : b = a
⊢ b = a
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b : α) (h : a = b) (_ : True) (_ : True ∨ False) (h : b = a) : b = a := by
expose_names
trace_state
rw [h]
/--
info: α : Sort u_1
trace: α : Sort u_1
a b : α
h : a = b
h_3 : True
@ -41,7 +41,7 @@ h_5 : True
h_2 : b = a
⊢ b = a
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b : α) (h : a = b) (_ : True) (_ : False) (h_1 : True ∨ False) (_ : True) (h_2 : b = a) : b = a := by
expose_names
trace_state

98
tests/lean/run/extract_lets.lean
View file

@ -10,7 +10,7 @@ axiom test_sorry {α : Sort _} : α
Extract a top-level let, no names given.
-/
/--
info: x✝ : Nat := 2
trace: x✝ : Nat := 2
⊢ x✝ = 2
-/
#guard_msgs in
@ -23,7 +23,7 @@ example : let x := 2; x = 2 := by
Extract a top-level let, name given.
-/
/--
info: z : Nat := 2
trace: z : Nat := 2
⊢ z = 2
-/
#guard_msgs in
@ -36,7 +36,7 @@ example : let x := 2; x = 2 := by
Extract a top-level let, placeholder name given.
-/
/--
info: x✝ : Nat := 2
trace: x✝ : Nat := 2
⊢ x✝ = 2
-/
#guard_msgs in
@ -49,7 +49,7 @@ example : let x := 2; x = 2 := by
Extract an embedded let, name given.
-/
/--
info: z : Nat := 2
trace: z : Nat := 2
⊢ z = 2
-/
#guard_msgs in
@ -62,7 +62,7 @@ example : (let x := 2; x) = 2 := by
Extract multiple embedded lets, no names given.
-/
/--
info: x✝ : Nat := 2
trace: x✝ : Nat := 2
y✝ : Nat := 1 + 1
⊢ x✝ = y✝
-/
@ -76,7 +76,7 @@ example : (let x := 2; x) = (let y := 1 + 1; y) := by
Names extracted lets in order, but keeps extracting even after list is exhausted.
-/
/--
info: z : Nat := 2
trace: z : Nat := 2
y✝ : Nat := 1 + 1
⊢ z = y✝
-/
@ -93,7 +93,7 @@ Too many names, linter warning.
warning: unused name
note: this linter can be disabled with `set_option linter.tactic.unusedName false`
---
info: z : Nat := 2
trace: z : Nat := 2
z' : Nat := 1 + 1
⊢ z = z'
-/
@ -107,7 +107,7 @@ example : (let x := 2; x) = (let y := 1 + 1; y) := by
Length of name list controls number of lets in `+onlyGivenNames` mode.
-/
/--
info: z : Nat := 2
trace: z : Nat := 2
⊢ z =
let y := 1 + 1;
y
@ -118,7 +118,7 @@ example : (let x := 2; x) = (let y := 1 + 1; y) := by
trace_state
rfl
/--
info: z : Nat := 2
trace: z : Nat := 2
w : Nat := 1 + 1
⊢ z = w
-/
@ -132,7 +132,7 @@ example : (let x := 2; x) = (let y := 1 + 1; y) := by
Merging.
-/
/--
info: x✝ : Nat := 2
trace: x✝ : Nat := 2
⊢ x✝ = x✝
-/
#guard_msgs in
@ -145,7 +145,7 @@ example : (let x := 2; x) = (let y := 2; y) := by
Merging, even if we run out of names.
-/
/--
info: z : Nat := 2
trace: z : Nat := 2
⊢ z = z
-/
#guard_msgs in
@ -158,7 +158,7 @@ example : (let x := 2; x) = (let y := 2; y) := by
Merging reuses pre-existing declarations
-/
/--
info: z : Nat := 2
trace: z : Nat := 2
⊢ z = z
-/
#guard_msgs in
@ -172,7 +172,7 @@ example : (let x := 2; x) = (let y := 2; y) := by
Merging doesn't reuse pre-existing declarations when `-useContext`.
-/
/--
info: z : Nat := 2
trace: z : Nat := 2
x✝ : Nat := 2
⊢ x✝ = x✝
-/
@ -187,7 +187,7 @@ example : (let x := 2; x) = (let y := 2; y) := by
Works with `have` (`let_fun`)
-/
/--
info: a✝ : Nat := 2
trace: a✝ : Nat := 2
x✝ : Nat := a✝
y✝ : Nat := a✝ + 0
⊢ x✝ = y✝
@ -202,7 +202,7 @@ example : have a := 2; (have x := a; x) = (have y := a + 0; y) := by
Extracts at both the type and the value of a local definition.
-/
/--
info: α✝ : Type := Nat
trace: α✝ : Type := Nat
y✝ : Nat := 2
x : α✝ := 2
⊢ x = x
@ -215,7 +215,7 @@ example : let x : (let α := Nat; α) := (let y := 2; 2); x = x := by
rfl
-- Essentially same state:
/--
info: α✝ : Type := Nat
trace: α✝ : Type := Nat
y✝ : Nat := 2
x✝ : α✝ := 2
⊢ x✝ = x✝
@ -230,7 +230,7 @@ example : let x : (let α := Nat; α) := (let y := 2; 2); x = x := by
Basic `descend := false` test.
-/
/--
info: x✝ : Nat := 2
trace: x✝ : Nat := 2
⊢ x✝ = 2
-/
#guard_msgs in
@ -243,7 +243,7 @@ example : let x := 2; x = 2 := by
Make sure `descend := false` is not obstructed by metadata.
-/
/--
info: this : True
trace: this : True
x✝ : Nat := 2
⊢ x✝ = 2
-/
@ -271,7 +271,7 @@ example : (let x := 2; x) = 2 := by
In `-descend` mode, merges using pre-existing declarations.
-/
/--
info: w : Nat := 2
trace: w : Nat := 2
y✝ : Nat := 3
⊢ w = 2 + y✝ - y✝
-/
@ -286,7 +286,7 @@ example : let x := 2; let y := 3; let z := 3; x = 2 + y - z := by
`-descend` works with `have` (`let_fun`)
-/
/--
info: a✝ : Nat := 2
trace: a✝ : Nat := 2
⊢ (let_fun x := a✝;
x) =
let_fun y := a✝ + 0;
@ -302,7 +302,7 @@ example : have a := 2; (have x := a; x) = (have y := a + 0; y) := by
Extracting at a hypothesis
-/
/--
info: x✝ : Nat := 1
trace: x✝ : Nat := 1
h : x✝ = x✝
⊢ True
-/
@ -317,7 +317,7 @@ example (h : let x := 1; x = x) : True := by
Extracting at a hypothesis, with names
-/
/--
info: y : Nat := 1
trace: y : Nat := 1
h : y = y
⊢ True
-/
@ -332,7 +332,7 @@ example (h : let x := 1; x = x) : True := by
Extracting at a hypothesis, reorders hypotheses
-/
/--
info: h' : Nat
trace: h' : Nat
y : Nat := 1
h : y = y
⊢ True
@ -348,7 +348,7 @@ example (h : let x := 1; x = x) (h' : Nat) : True := by
Extracting at a hypothesis, not all top level.
-/
/--
info: x✝ : Nat := 1
trace: x✝ : Nat := 1
y✝ : Nat := 2
h : x✝ + 1 = y✝
⊢ True
@ -363,7 +363,7 @@ example (h : let x := 1; x + 1 = let y := 2; y) : True := by
Extracting at a hypothesis, not all top level, in `-descend` mode.
-/
/--
info: x✝ : Nat := 1
trace: x✝ : Nat := 1
h :
x✝ + 1 =
let y := 2;
@ -380,7 +380,7 @@ example (h : let x := 1; x + 1 = let y := 2; y) : True := by
At multiple locations with `merge := true`.
-/
/--
info: _z✝ : Nat := 3
trace: _z✝ : Nat := 3
x✝ : Nat := 1
h : x✝ + 2 = _z✝
⊢ ∀ (x : Nat), True
@ -396,7 +396,7 @@ example (h : let x := 1; let y := 3; x + 2 = y) : let _z := 3; ∀ (_ : Nat), Tr
At multiple locations with `merge := false`.
-/
/--
info: _z✝ : Nat := 3
trace: _z✝ : Nat := 3
x✝ : Nat := 1
y✝ : Nat := 3
h : x✝ + 2 = y✝
@ -413,7 +413,7 @@ example (h : let x := 1; let y := 3; x + 2 = y) : let _z := 3; ∀ (_ : Nat), Tr
Merging can chain. This tests how extracted let declarations are recalled and can handle dependence.
-/
/--
info: x✝ : Nat := 2
trace: x✝ : Nat := 2
y✝ : Nat := x✝
⊢ y✝ = y✝
-/
@ -427,7 +427,7 @@ example : (let x := 2; let y := x; y) = (let x' := 2; let y' := x'; y') := by
Same merging example, but with `-merge`.
-/
/--
info: x✝ : Nat := 2
trace: x✝ : Nat := 2
y✝ : Nat := x✝
x'✝ : Nat := 2
y'✝ : Nat := x'✝
@ -445,21 +445,21 @@ Reported at https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topi
Unused lets are handled properly.
-/
/--
info: ok✝ : Prop := True
trace: ok✝ : Prop := True
h :
let _not_ok := False;
ok✝
⊢ let _also_ok := 3;
True
---
info: ok✝ : Prop := True
trace: ok✝ : Prop := True
h :
let _not_ok := False;
ok✝
_also_ok✝ : Nat := 3
⊢ True
---
info: ok✝ : Prop := True
trace: ok✝ : Prop := True
_also_ok✝ : Nat := 3
_not_ok✝ : Prop := False
h : ok✝
@ -479,12 +479,12 @@ example (h : let ok := True; let _not_ok := False; ok) : let _also_ok := 3; True
Testing `+usedOnly`
-/
/--
info: ok✝ : Prop := True
trace: ok✝ : Prop := True
h : ok✝
⊢ let _also_ok := 3;
True
---
info: ok✝ : Prop := True
trace: ok✝ : Prop := True
h : ok✝
⊢ True
-/
@ -500,12 +500,12 @@ example (h : let ok := True; let _not_ok := False; ok) : let _also_ok := 3; True
Testing `+usedOnly` with `-descend`
-/
/--
info: ok✝ : Prop := True
trace: ok✝ : Prop := True
h : ok✝
⊢ let _also_ok := 3;
True
---
info: ok✝ : Prop := True
trace: ok✝ : Prop := True
h : ok✝
⊢ True
-/
@ -521,7 +521,7 @@ example (h : let ok := True; let _not_ok := False; ok) : let _also_ok := 3; True
`+proofs`
-/
/--
info: this✝ : (some true).isSome = true := of_eq_true (eq_self true)
trace: this✝ : (some true).isSome = true := of_eq_true (eq_self true)
⊢ (some true).get this✝ = true
-/
#guard_msgs in
@ -535,7 +535,7 @@ example : Option.get (some true) (have := (by simp); this) = true := by
`+implicits`
-/
/--
info: α✝ : Type := Nat
trace: α✝ : Type := Nat
⊢ id 2 = 2
-/
#guard_msgs in
@ -570,7 +570,7 @@ example : ∀ n : Nat, let x := n; x = x := by
Can extract from underneath another `let`.
-/
/--
info: y✝ : Nat := 2
trace: y✝ : Nat := 2
⊢ ∀ (n : Nat),
let x := n;
x + y✝ = x + y✝
@ -638,7 +638,7 @@ See also the `lift_lets.lean` test file.
Lifts, does not make use of name generator.
-/
/--
info: ⊢ ∀ (n : Nat),
trace: ⊢ ∀ (n : Nat),
let x := n;
n = x
-/
@ -654,7 +654,7 @@ example : ∀ n : Nat, n = (let x := n; x) := by
Same example, but testing `letFun`.
-/
/--
info: ⊢ ∀ (n : Nat),
trace: ⊢ ∀ (n : Nat),
let_fun x := n;
n = x
-/
@ -671,7 +671,7 @@ Merging of merely-lifted lets. Four cases to this test, depending on whether a `
and whether the second is a `have` or `let`.
-/
/--
info: ⊢ ∀ (n : Nat),
trace: ⊢ ∀ (n : Nat),
let_fun x := n;
x = x
-/
@ -683,7 +683,7 @@ example : ∀ n : Nat, (have x := n; x) = (have x' := n; x') := by
intros
rfl
/--
info: ⊢ ∀ (n : Nat),
trace: ⊢ ∀ (n : Nat),
let x := n;
x = x
-/
@ -695,7 +695,7 @@ example : ∀ n : Nat, (let x := n; x) = (have x' := n; x') := by
intros
rfl
/--
info: ⊢ ∀ (n : Nat),
trace: ⊢ ∀ (n : Nat),
let x := n;
x = x
-/
@ -707,7 +707,7 @@ example : ∀ n : Nat, (have x := n; x) = (let x' := n; x') := by
intros
rfl
/--
info: ⊢ ∀ (n : Nat),
trace: ⊢ ∀ (n : Nat),
let x := n;
x = x
-/
@ -723,7 +723,7 @@ example : ∀ n : Nat, (let x := n; x) = (let x' := n; x') := by
Without merging
-/
/--
info: ⊢ ∀ (n : Nat),
trace: ⊢ ∀ (n : Nat),
let_fun x := n;
let_fun x' := n;
x = x'
@ -748,7 +748,7 @@ example : ∀ n : Nat, let x := n; let y := x; y = n := by
Extracting `let`s in proofs in `+proof` mode.
-/
/--
info: m : Nat
trace: m : Nat
h : ∃ n, n + 1 = m
x : Fin m
y : Fin (h.choose + 1)
@ -771,10 +771,10 @@ example (m : Nat) (h : ∃ n, n + 1 = m) (x : Fin m) (y : Fin _) :
Limitation: we can use `extract_lets` within `conv`, but the let bindings do not persist.
-/
/--
info: y : Type := Nat
trace: y : Type := Nat
| y = Int
---
info: ⊢ Nat = Int
trace: ⊢ Nat = Int
-/
#guard_msgs in
example : let x := Nat; x = Int := by

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

@ -7,7 +7,7 @@ namespace Ex1
/--
error: well-founded recursion cannot be used, 'Ex1.foo' does not take any (non-fixed) arguments
---
info: [Elab.definition.fixedParams] getFixedParams:
trace: [Elab.definition.fixedParams] getFixedParams:
• ⏎
•
-/
@ -25,7 +25,7 @@ namespace Ex2
/--
error: well-founded recursion cannot be used, 'Ex2.foo' does not take any (non-fixed) arguments
---
info: [Elab.definition.fixedParams] getFixedParams:
trace: [Elab.definition.fixedParams] getFixedParams:
• [#1 #1]
• [#1 #1]
-/
@ -41,7 +41,7 @@ namespace Ex3
/--
error: well-founded recursion cannot be used, 'Ex3.foo' does not take any (non-fixed) arguments
---
info: [Elab.definition.fixedParams] getFixedParams:
trace: [Elab.definition.fixedParams] getFixedParams:
• [#1 #2] [#2 #1]
• [#2 #1] [#1 #2]
-/
@ -56,7 +56,7 @@ end Ex3
namespace Ex4
/--
info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 3:
trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 3:
In foo c n b m
m not matched
[Elab.definition.fixedParams] getFixedParams: • [#1 #3] ❌ [#3 #1] ❌ • [#3 #1] ❌ [#1 #3] ❌
@ -73,7 +73,7 @@ end Ex4
namespace Append1
/--
info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
In app as bs
x✝¹ =/= as
[Elab.definition.fixedParams] getFixedParams: notFixed 0 2:
@ -81,18 +81,18 @@ info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
x✝ =/= bs
[Elab.definition.fixedParams] getFixedParams: • [#1] ❌ ❌
-/
#guard_msgs(info) in
#guard_msgs(trace) in
def app : List α → List α → List α
| [], bs => bs
| a::as, bs => a :: app as bs
/--
info: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
trace: [Elab.definition.fixedParams] getFixedParams: notFixed 0 1:
In app' as bs
as✝ =/= as
[Elab.definition.fixedParams] getFixedParams: • [#1] ❌ [#3]
-/
#guard_msgs(info) in
#guard_msgs(trace) in
def app' (as : List α) (bs : List α) : List α :=
match as with
| [] => bs

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

@ -86,11 +86,11 @@ elab "seq" s:tacticSeq : tactic => do
evalTactic tac
/--
info: x y : Nat
trace: x y : Nat
h : x = y
⊢ 0 + x = y
---
info: x y : Nat
trace: x y : Nat
h : x = y
⊢ 0 + y = y
-/
@ -100,11 +100,11 @@ example (h : x = y) : 0 + x = y := by
done
/--
info: x y : Nat
trace: x y : Nat
h : x = y
⊢ 0 + x = y
---
info: x y : Nat
trace: x y : Nat
h : x = y
⊢ 0 + y = y
-/
@ -115,11 +115,11 @@ example (h : x = y) : 0 + x = y := by
done
/--
info: x y : Nat
trace: x y : Nat
h : x = y
⊢ 0 + x = y
---
info: x y : Nat
trace: x y : Nat
h : x = y
⊢ 0 + y = y
-/

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

@ -1,7 +1,7 @@
set_option pp.analyze false
/--
info: p : (n : Nat) → Fin n → Prop
trace: p : (n : Nat) → Fin n → Prop
n : Nat
v : Fin n
n' : Nat

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

@ -22,7 +22,7 @@ let t ← mkLambdaFVars ys ys.back!
trace[Meta.debug] t
pure ()
/-- info: [Meta.debug] fun x x => x -/
/-- trace: [Meta.debug] fun x x => x -/
#guard_msgs in
#eval tst1
@ -39,7 +39,7 @@ let t ← mkLambdaFVars ys ys.back!
trace[Meta.debug] t
pure ()
/-- info: [Meta.debug] fun (x : Nat) (x_1 : Vec Nat x) (x : @Eq.{1} (Vec Nat x) x_1 x_1) => x -/
/-- trace: [Meta.debug] fun (x : Nat) (x_1 : Vec Nat x) (x : @Eq.{1} (Vec Nat x) x_1 x_1) => x -/
#guard_msgs in
#eval tst2
@ -61,6 +61,6 @@ failIfSuccess do
pure ()
trace[Meta.debug] "failed as expected"
/-- info: [Meta.debug] failed as expected -/
/-- trace: [Meta.debug] failed as expected -/
#guard_msgs in
#eval tst3

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

@ -25,7 +25,7 @@ pure ()
set_option trace.Elab true
/--
info: [Elab] ⊢ ∀ (α : Type u) (xs : List (List α)) (h : Pred (List α) xs), xs ≠ [] → xs = xs
trace: [Elab] ⊢ ∀ (α : Type u) (xs : List (List α)) (h : Pred (List α) xs), xs ≠ [] → xs = xs
[Elab] α✝ : Type u
xs✝ : List (List α✝)
h✝ : Pred (List α✝) xs✝

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

@ -27,20 +27,20 @@ opaque Expr.eval : Expr → State → Nat
axiom Expr.constProp : Expr → State → Expr
/-- info: [grind.ematch.pattern] eval_constProp_of_sub: [State.le #3 #2, constProp #1 #3] -/
#guard_msgs (info) in
/-- trace: [grind.ematch.pattern] eval_constProp_of_sub: [State.le #3 #2, constProp #1 #3] -/
#guard_msgs (trace) in
set_option trace.grind.ematch.pattern true in
@[grind =>] theorem Expr.eval_constProp_of_sub (e : Expr) (h : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ :=
sorry
/-- info: [grind.ematch.pattern] eval_constProp_of_eq_of_sub: [State.le #3 #2, constProp #1 #3] -/
#guard_msgs (info) in
/-- trace: [grind.ematch.pattern] eval_constProp_of_eq_of_sub: [State.le #3 #2, constProp #1 #3] -/
#guard_msgs (trace) in
set_option trace.grind.ematch.pattern true in
@[grind =>] theorem Expr.eval_constProp_of_eq_of_sub {e : Expr} (h₂ : State.le σ' σ) : (e.constProp σ').eval σ = e.eval σ :=
sorry
/-- info: [grind.ematch.pattern] update_le_update: [le #4 #3, update #4 #2 #1] -/
#guard_msgs (info) in
/-- trace: [grind.ematch.pattern] update_le_update: [le #4 #3, update #4 #2 #1] -/
#guard_msgs (trace) in
set_option trace.grind.ematch.pattern true in
@[grind =>] theorem State.update_le_update (h : State.le σ' σ) : State.le (σ'.update x v) (σ.update x v) :=
sorry

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

@ -30,10 +30,10 @@ example (f : Nat → Nat → Nat) : f 2 3 ≠ 5 → f = (fun x y : Nat => x + y)
opaque bla : Nat → Nat → Nat → Nat
/--
info: [grind.beta] f 2 3 = bla 2 3 2, using fun x y => bla x y x
trace: [grind.beta] f 2 3 = bla 2 3 2, using fun x y => bla x y x
[grind.beta] f 2 3 = 2 + 3, using fun x y => x + y
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.beta true in
example (g h f : Nat → Nat → Nat) :
f 2 3 ≠ 5 →

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

@ -52,8 +52,8 @@ def fallback : Fallback := do
set_option trace.Meta.debug true
/-- info: [Meta.debug] [a * (b * c), b * c, d * (b * c)] -/
#guard_msgs (info) in
/-- trace: [Meta.debug] [a * (b * c), b * c, d * (b * c)] -/
#guard_msgs (trace) in
example (a b c d : Nat) : b * (a * c) = d * (b * c) → False := by
rw [left_comm] -- Introduces a new (non-canonical) instance for `Mul Nat`
grind on_failure fallback -- State should have only 3 `*`-applications
@ -62,14 +62,14 @@ example (a b c d : Nat) : b * (a * c) = d * (b * c) → False := by
set_option pp.notation false in
set_option pp.explicit true in
/--
info: [Meta.debug] [@HMul.hMul Int Int Int (@instHMul Int Int.instMul) (@NatCast.natCast Int instNatCastInt b)
trace: [Meta.debug] [@HMul.hMul Int Int Int (@instHMul Int Int.instMul) (@NatCast.natCast Int instNatCastInt b)
(@NatCast.natCast Int instNatCastInt a),
@HMul.hMul Int Int Int (@instHMul Int Int.instMul) (@NatCast.natCast Int instNatCastInt b)
(@NatCast.natCast Int instNatCastInt d),
@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b a,
@HMul.hMul Nat Nat Nat (@instHMul Nat instMulNat) b d]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d : Nat) : b * a = d * b → False := by
rw [CommMonoid.mul_comm d b] -- Introduces a new (non-canonical) instance for `Mul Nat`
-- See target here

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

@ -12,9 +12,9 @@ def fallback : Fallback := do
set_option trace.Meta.debug true
set_option pp.explicit true
/--
info: [Meta.debug] [@f Nat a, @f Nat b]
trace: [Meta.debug] [@f Nat a, @f Nat b]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d : Nat) : @f Nat a = b → @f (g Nat) a = c → @f (g Nat) b = d → a = b → False := by
-- State should have only two `f`-applications: `@f Nat a`, `@f Nat b`
-- Note that `@f (g Nat) b` has been canonicalized to `@f Nat b`.

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

@ -15,28 +15,28 @@ def f (v : Vec α n) : Bool :=
| .cons .. => false
/--
info: n : Nat
trace: n : Nat
v : Vec Nat n
h : f v ≠ false
⊢ n + 1 = 0 → HEq (Vec.cons 10 v) Vec.nil → False
---
info: n : Nat
trace: n : Nat
v : Vec Nat n
h : f v ≠ false
⊢ ∀ {n_1 : Nat} (a : Nat) (a_1 : Vec Nat n_1), n + 1 = n_1 + 1 → HEq (Vec.cons 10 v) (Vec.cons a a_1) → False
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (v : Vec Nat n) (h : f v ≠ false) : False := by
cases' (Vec.cons 10 v)
next => trace_state; sorry
next => trace_state; sorry
/--
info: ⊢ False → False
trace: ⊢ False → False
---
info: ⊢ True → False
trace: ⊢ True → False
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : False := by
cases' (Or.inr (a := False) True.intro)
next => trace_state; sorry

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

@ -1,3 +1,5 @@
set_option grind.warning false
universe v v₁ v₂ v₃ u u₁ u₂ u₃
namespace CategoryTheory

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

@ -16,29 +16,29 @@ set_option grind.debug true
set_option grind.debug.proofs true
/--
info: [Meta.debug] [d, f b, c, f a]
trace: [Meta.debug] [d, f b, c, f a]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d : Nat) : a = b → f a = c → f b = d → False := by
grind on_failure fallback
/--
info: [Meta.debug] [d, f b, c, f a]
trace: [Meta.debug] [d, f b, c, f a]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d : Nat) : f a = c → f b = d → a = b → False := by
grind on_failure fallback
/--
info: [Meta.debug] [d, f (g b), c, f (g a)]
trace: [Meta.debug] [d, f (g b), c, f (g a)]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d e : Nat) : f (g a) = c → f (g b) = d → a = e → b = e → False := by
grind on_failure fallback
/--
info: [Meta.debug] [d, f (g b), c, f v]
trace: [Meta.debug] [d, f (g b), c, f v]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d e v : Nat) : f v = c → f (g b) = d → a = e → b = e → v = g a → False := by
grind on_failure fallback

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

@ -30,13 +30,13 @@ abbrev problem (x y z w v : Int) : Prop :=
(y ≥ -10)
/--
info: [grind.cutsat.model] x := 121
trace: [grind.cutsat.model] x := 121
[grind.cutsat.model] y := -10
[grind.cutsat.model] z := -34
[grind.cutsat.model] w := 0
[grind.cutsat.model] v := 1
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (x y z w v : Int) : problem x y z w v → False := by
fail_if_success grind

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

@ -19,17 +19,17 @@ abbrev problem₁ [∀ n, OfNat α n] [Neg α] [Mul α] [Sub α] [Add α] [LE α
7*x - 9*y ≤ 4
/--
info: [grind.cutsat.model] x := 241/154
trace: [grind.cutsat.model] x := 241/154
[grind.cutsat.model] y := 1
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (x y : Int) : problem₁ x y → False := by
fail_if_success grind +qlia -- Rational counterexamples allowed
sorry
/-- info: true -/
#guard_msgs (info) in
#guard_msgs in
open Std.Internal in
#eval problem₁ (241/154 : Rat) (1 : Rat)

36
tests/lean/run/grind_cutsat_diseq_1.lean
View file

@ -5,80 +5,80 @@ open Int.Linear
set_option trace.grind.cutsat.assert true
/--
info: [grind.cutsat.assert] a + b + 1 ≤ 0
trace: [grind.cutsat.assert] a + b + 1 ≤ 0
[grind.cutsat.assert] a + -1*b ≠ 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b : Int) : a + b < 0 → a ≠ b → False := by
(fail_if_success grind); sorry
#guard_msgs (info) in -- `a` and `b` are not relevant to cutsat in the following example
#guard_msgs (trace) in -- `a` and `b` are not relevant to cutsat in the following example
example (a b : Int) : a ≠ b → False := by
(fail_if_success grind); sorry
/--
info: [grind.cutsat.assert] a + -1*b ≠ 0
trace: [grind.cutsat.assert] a + -1*b ≠ 0
[grind.cutsat.assert] a + b + 1 ≤ 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b : Int) : a ≠ b → a + b < 0 → False := by
(fail_if_success grind); sorry
/--
info: [grind.cutsat.assert] a + -1*b ≠ 0
trace: [grind.cutsat.assert] a + -1*b ≠ 0
[grind.cutsat.assert] a + b + 1 ≤ 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c : Int) : a ≠ c → c = b → a + b < 0 → False := by
(fail_if_success grind); sorry
/--
info: [grind.cutsat.assert] a + -1*b ≠ 0
trace: [grind.cutsat.assert] a + -1*b ≠ 0
[grind.cutsat.assert] a + b + 1 ≤ 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d : Int) : d ≠ c → c = b → a = d → a + b < 0 → False := by
(fail_if_success grind); sorry
/--
info: [grind.cutsat.assert] a + b + 1 ≤ 0
trace: [grind.cutsat.assert] a + b + 1 ≤ 0
[grind.cutsat.assert] a + -1*b ≠ 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d : Int) : d ≠ c → a = d → a + b < 0 → c = b → False := by
(fail_if_success grind); sorry
/--
info: [grind.cutsat.assert] a + b + 1 ≤ 0
trace: [grind.cutsat.assert] a + b + 1 ≤ 0
[grind.cutsat.assert] a + -1*b ≠ 0
[grind.cutsat.assert] e + -1*b = 0
[grind.cutsat.assert] -1*e + 1 ≤ 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d e : Int) : d ≠ c → a = d → a + b < 0 → c = b → c = e → e > 0 → False := by
(fail_if_success grind); sorry
/--
info: [grind.cutsat.assert] -1*e + 1 ≤ 0
trace: [grind.cutsat.assert] -1*e + 1 ≤ 0
[grind.cutsat.assert] b + -1*e = 0
[grind.cutsat.assert] a + -1*e ≠ 0
[grind.cutsat.assert] a + b + 1 ≤ 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d e : Int) : d ≠ c → a = d → c = b → c = e → e > 0 → a + b < 0 → False := by
(fail_if_success grind); sorry
/--
info: [grind.cutsat.assert] -1*e + 1 ≤ 0
trace: [grind.cutsat.assert] -1*e + 1 ≤ 0
[grind.cutsat.assert] b + -1*e = 0
[grind.cutsat.assert] a + b + 1 ≤ 0
[grind.cutsat.assert] a + -1*e ≠ 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d e : Int) : a = d → c = b → c = e → e > 0 → a + b < 0 → d ≠ c → False := by
(fail_if_success grind); sorry
#guard_msgs (info) in -- no propagation to cutsat
#guard_msgs (trace) in -- no propagation to cutsat
example (a b c d e : Int) : a = d → c = b → c = e → a = 1 → d ≠ c → False := by
(fail_if_success grind); sorry

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

@ -12,14 +12,14 @@ theorem ex₃ (a b c : Int) : a + b + c = 0 → a = c → b = 4 → c = -2 := by
grind
/--
info: [grind.cutsat.assert] -1*「a + -2 * b + -2 * c」 + a + -2*b + -2*c = 0
trace: [grind.cutsat.assert] -1*「a + -2 * b + -2 * c」 + a + -2*b + -2*c = 0
[grind.cutsat.assert] 「a + -2 * b + -2 * c」 = 0
[grind.cutsat.assert] -1*「a + -2 * b + -2 * d」 + a + -2*b + -2*d = 0
[grind.cutsat.assert] 「a + -2 * b + -2 * d」 ≠ 0
[grind.cutsat.assert] -1*d + c = 0
[grind.cutsat.assert] 0 ≠ 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.assert true in
theorem ex₄ (a b c d : Int) : a = 2*b + 2*c → a - 2*b - 2*d ≠ 0 → c ≠ d := by
grind

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

@ -21,22 +21,22 @@ theorem ex₄ (f : Int → Int) (a b : Int) (_ : 2 ∣ f (f a) + 1) (h₁ : 3
#print ex₄
/--
info: [grind.debug.cutsat.search.assign] a := 1
trace: [grind.debug.cutsat.search.assign] a := 1
[grind.debug.cutsat.search.assign] b := 0
-/
#guard_msgs (info) in -- finds the model without any backtracking
#guard_msgs (trace) in -- finds the model without any backtracking
set_option trace.grind.debug.cutsat.search.assign true in
example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) : False := by
fail_if_success grind
sorry
/--
info: [grind.cutsat.assert] 2 ∣ a + 3
trace: [grind.cutsat.assert] 2 ∣ a + 3
[grind.cutsat.assert] 3 ∣ a + 3*b + -4
[grind.debug.cutsat.search.assign] a := 1
[grind.debug.cutsat.search.assign] b := 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.assert true in
set_option trace.grind.debug.cutsat.search.assign true in
example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + 3*b - 4) : False := by
@ -44,30 +44,30 @@ example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + 3*b - 4) : False := by
sorry
/--
info: [grind.debug.cutsat.search.assign] a := 1
trace: [grind.debug.cutsat.search.assign] a := 1
[grind.debug.cutsat.search.assign] b := 15
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.debug.cutsat.search.assign true in
example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b < 18): False := by
fail_if_success grind
sorry
/--
info: [grind.debug.cutsat.search.assign] a := 1
trace: [grind.debug.cutsat.search.assign] a := 1
[grind.debug.cutsat.search.assign] b := 12
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.debug.cutsat.search.assign true in
example (a b : Int) (_ : 2 ∣ a + 3) (_ : 3 ∣ a + b - 4) (_ : b ≥ 11): False := by
fail_if_success grind
sorry
/--
info: [grind.debug.cutsat.search.assign] f 0 := 11
trace: [grind.debug.cutsat.search.assign] f 0 := 11
[grind.debug.cutsat.search.assign] f 1 := 2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.debug.cutsat.search.assign true in
example (f : Int → Int) (_ : 2 ∣ f 0 + 3) (_ : 3 ∣ f 0 + f 1 - 4) (_ : f 0 ≥ 11): False := by
fail_if_success grind

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

@ -13,10 +13,10 @@ example (x y : Int) : x % 2 + y = 3 → x = 5 → y = 2 := by
grind
/--
info: [grind.cutsat.model] x := 5
trace: [grind.cutsat.model] x := 5
[grind.cutsat.model] y := 2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (x y : Int) : x % 2 + y = 3 → x ≤ 5 → x > 4 → y = 1 := by
fail_if_success grind

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

@ -3,10 +3,10 @@ set_option grind.debug true
open Int.Linear
/--
info: [grind.cutsat.assert] -1*「b + f a + 1」 + b + f a + 1 = 0
trace: [grind.cutsat.assert] -1*「b + f a + 1」 + b + f a + 1 = 0
[grind.cutsat.assert] 「b + f a + 1」 = 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.assert true in
example (a b : Int) (f : Int → Int) (h₁ : f a + b + 3 = 2) : False := by
fail_if_success grind

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

@ -2,10 +2,10 @@ set_option grind.warning false
set_option grind.debug true
/--
info: [grind.debug.cutsat.search.assign] b := -1
trace: [grind.debug.cutsat.search.assign] b := -1
[grind.debug.cutsat.search.assign] a := 3
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.debug.cutsat.search.assign true in
example (a b : Int) (h₁ : a ≤ 3) (h₂ : a > 2) (h₃ : a + b < 3) : False := by
fail_if_success grind

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

@ -11,12 +11,12 @@ example (a b c d e : Int) :
set_option trace.grind.cutsat.model true
/--
info: [grind.cutsat.model] a := 7
trace: [grind.cutsat.model] a := 7
[grind.cutsat.model] b := 0
[grind.cutsat.model] c := 3
[grind.cutsat.model] d := 2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c d e : Int) :
a + b ≥ 0 →
a = 2*c + 1 →
@ -25,11 +25,11 @@ example (a b c d e : Int) :
(fail_if_success grind); sorry
/--
info: [grind.cutsat.model] a := 17
trace: [grind.cutsat.model] a := 17
[grind.cutsat.model] b := -9
[grind.cutsat.model] c := -9
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (a b c : Int) :
2*a + 3*b = 7 →
4*a + 7*c = 5 →

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

@ -70,21 +70,21 @@ example (a b : Int) : (a - b).toNat = 0 ↔ a ≤ b := by
grind
/--
info: [grind.cutsat.model] x := 3
trace: [grind.cutsat.model] x := 3
[grind.cutsat.model] y := 1
[grind.cutsat.model] z := 4
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (x y z : Nat) : x ≥ 3 → x ≠ z → x > y → z ≤ 6 → x + y = z → False := by
fail_if_success grind
sorry
/--
info: [grind.cutsat.model] x := 13
trace: [grind.cutsat.model] x := 13
[grind.cutsat.model] y := 9
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (x y : Nat) : x > 8 → y > 8 → x ≠ y → (x - y) % 4 = 1 := by
fail_if_success grind
@ -115,10 +115,10 @@ example (x y : Nat) : x ^ 0 + y = 0 → False := by
grind
/--
info: [grind.cutsat.model] x := 4
trace: [grind.cutsat.model] x := 4
[grind.cutsat.model] y := 1
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (x y : Nat) : x = y + 3 → y > 0 → False := by
fail_if_success grind

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

@ -29,7 +29,7 @@ example (a b : Int) : a + b = Int.ofNat 2 → a - 2 = -b := by
grind
/--
info: [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
trace: [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
[grind.cutsat.assert] -1*↑c ≤ 0
[grind.cutsat.assert] -1*↑c + 「↑a * ↑b」 + 1 ≤ 0
[grind.cutsat.assert] ↑c = 0
@ -37,7 +37,7 @@ info: [grind.cutsat.assert] -1*「↑a * ↑b」 ≤ 0
[grind.cutsat.assert] 「↑a * ↑b」 + 1 ≤ 0
[grind.cutsat.assert] 1 ≤ 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.assert true in
example (a b c : Nat) : c > a * b → c >= 1 := by
grind

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

@ -15,13 +15,13 @@ abbrev test1 (a b c d e : Int) :=
a ≤ 100
/--
info: [grind.cutsat.model] a := 101
trace: [grind.cutsat.model] a := 101
[grind.cutsat.model] b := 0
[grind.cutsat.model] c := 5335
[grind.cutsat.model] d := 0
[grind.cutsat.model] e := 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (a b c d e : Int) : test1 a b c d e := by
(fail_if_success grind); sorry

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

@ -1,5 +1,5 @@
/-- info: [grind.cutsat.model] a := 2 -/
#guard_msgs (info) in
/-- trace: [grind.cutsat.model] a := 2 -/
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (a b : Int) : a ≤ 5 → a ≠ 4 → 2 ∣ a → False := by
(fail_if_success grind); sorry

40
tests/lean/run/grind_diseq_api.lean
View file

@ -23,58 +23,58 @@ def fallback : Fallback := do
set_option trace.Meta.debug true
/--
info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1)) : a ≠ b
trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1)) : a ≠ b
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (x y : Nat) : a = x → y ≠ x → b = y → False := by
grind on_failure fallback
/--
info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h h_1) : a ≠ b
trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_2 (Lean.Grind.ne_of_ne_of_eq_left h h_1) : a ≠ b
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (x y : Nat) : a = x → x ≠ y → b = y → False := by
grind on_failure fallback
/--
info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_3 (Lean.Grind.ne_of_ne_of_eq_left (Eq.trans h (Eq.symm h_1)) h_2) : a ≠ b
trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h_3 (Lean.Grind.ne_of_ne_of_eq_left (Eq.trans h (Eq.symm h_1)) h_2) : a ≠ b
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (x y z : Nat) : a = x → z = x → z ≠ y → b = y → False := by
grind on_failure fallback
/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/
#guard_msgs (info) in
/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/
#guard_msgs (trace) in
example (x : Nat) : a = x → b ≠ x → False := by
grind on_failure fallback
/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h h_1 : a ≠ b -/
#guard_msgs (info) in
/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h h_1 : a ≠ b -/
#guard_msgs (trace) in
example (x : Nat) : a = x → x ≠ b → False := by
grind on_failure fallback
/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h h_1 : a ≠ b -/
#guard_msgs (info) in
/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h h_1 : a ≠ b -/
#guard_msgs (trace) in
example (x : Nat) : b = x → a ≠ x → False := by
grind on_failure fallback
/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h (Ne.symm h_1) : a ≠ b -/
#guard_msgs (info) in
/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_right h (Ne.symm h_1) : a ≠ b -/
#guard_msgs (trace) in
example (x : Nat) : b = x → x ≠ a → False := by
grind on_failure fallback
/-- info: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/
#guard_msgs (info) in
/-- trace: [Meta.debug] Lean.Grind.ne_of_ne_of_eq_left h (Ne.symm h_1) : a ≠ b -/
#guard_msgs (trace) in
example (x : Nat) : a = x → b ≠ x → False := by
grind on_failure fallback
/-- info: [Meta.debug] h : ¬a = b -/
#guard_msgs (info) in
/-- trace: [Meta.debug] h : ¬a = b -/
#guard_msgs (trace) in
example : a ≠ b → False := by
grind on_failure fallback
/-- info: [Meta.debug] Ne.symm h : a ≠ b -/
#guard_msgs (info) in
/-- trace: [Meta.debug] Ne.symm h : a ≠ b -/
#guard_msgs (trace) in
example : b ≠ a → False := by
grind on_failure fallback

48
tests/lean/run/grind_ematch1.lean
View file

@ -27,10 +27,10 @@ set_option trace.grind.ematch.instance true
attribute [grind =] Array.getElem_set_ne
/--
info: [grind.ematch.instance] Array.size_set: (as.set i v ⋯).size = as.size
trace: [grind.ematch.instance] Array.size_set: (as.set i v ⋯).size = as.size
[grind.ematch.instance] Array.getElem_set_ne: ∀ (pj : j < as.size), i ≠ j → (as.set i v ⋯)[j] = as[j]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (as bs cs : Array α) (v : α)
(i : Nat)
(h₁ : i < as.size)
@ -49,15 +49,15 @@ theorem Rtrans (a b c : Nat) : R a b → R b c → R a c := sorry
grind_pattern Rtrans => R a b, R b c
/--
info: [grind.ematch.instance] Rtrans: R a b → R b c → R a c
trace: [grind.ematch.instance] Rtrans: R a b → R b c → R a c
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : R a b → R b c → R a c := by
grind
/--
info: [grind.ematch.instance] Rtrans: R a d → R d e → R a e
trace: [grind.ematch.instance] Rtrans: R a d → R d e → R a e
[grind.ematch.instance] Rtrans: R c d → R d e → R c e
[grind.ematch.instance] Rtrans: R b c → R c d → R b d
[grind.ematch.instance] Rtrans: R a b → R b c → R a c
@ -67,7 +67,7 @@ info: [grind.ematch.instance] Rtrans: R a d → R d e → R a e
[grind.ematch.instance] Rtrans: R a b → R b d → R a d
[grind.ematch.instance] Rtrans: R b c → R c e → R b e
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : R a b → R b c → R c d → R d e → R a d := by
grind
@ -85,7 +85,7 @@ error: `@[grind →] theorem using_grind_fwd.StransBad` failed to find patterns
set_option trace.grind.debug.ematch.pattern true in
/--
info: [grind.debug.ematch.pattern] place: S a b ∨ R a b
trace: [grind.debug.ematch.pattern] place: S a b ∨ R a b
[grind.debug.ematch.pattern] collect: S a b ∨ R a b
[grind.debug.ematch.pattern] arg: S a b, support: false
[grind.debug.ematch.pattern] collect: S a b
@ -104,13 +104,13 @@ info: [grind.debug.ematch.pattern] place: S a b ∨ R a b
[grind.debug.ematch.pattern] found full coverage
[grind.ematch.pattern] Strans: [S #4 #3, S #3 #2]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
@[grind→] theorem Strans (a b c : Nat) : S a b ∨ R a b → S b c → S a c := sorry
/--
info: [grind.ematch.instance] Strans: S a b ∨ R a b → S b c → S a c
trace: [grind.ematch.instance] Strans: S a b ∨ R a b → S b c → S a c
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : S a b → S b c → S a c := by
grind
@ -122,14 +122,14 @@ opaque P : Nat → Prop
opaque Q : Nat → Prop
opaque f : Nat → Nat → Nat
/-- info: [grind.ematch.pattern] pqf: [f #2 #1] -/
#guard_msgs (info) in
/-- trace: [grind.ematch.pattern] pqf: [f #2 #1] -/
#guard_msgs (trace) in
@[grind←] theorem pqf : Q x → P (f x y) := sorry
/--
info: [grind.ematch.instance] pqf: Q a → P (f a b)
trace: [grind.ematch.instance] pqf: Q a → P (f a b)
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : Q 0 → Q 1 → Q 2 → Q 3 → ¬ P (f a b) → a = 1 → False := by
grind
@ -148,18 +148,18 @@ error: `@[grind →] theorem using_grind_fwd2.pqfBad` failed to find patterns in
@[grind→] theorem pqfBad : Q x → P (f x y) := sorry
/--
info: [grind.ematch.pattern] pqf: [Q #1]
trace: [grind.ematch.pattern] pqf: [Q #1]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
@[grind→] theorem pqf : Q x → P (f x x) := sorry
/--
info: [grind.ematch.instance] pqf: Q 3 → P (f 3 3)
trace: [grind.ematch.instance] pqf: Q 3 → P (f 3 3)
[grind.ematch.instance] pqf: Q 2 → P (f 2 2)
[grind.ematch.instance] pqf: Q 1 → P (f 1 1)
[grind.ematch.instance] pqf: Q 0 → P (f 0 0)
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : Q 0 → Q 1 → Q 2 → Q 3 → ¬ P (f a a) → a = 1 → False := by
grind
@ -184,9 +184,9 @@ error: `@[grind ←] theorem using_grind_mixed.pqBad2` failed to find patterns i
/--
info: [grind.ematch.pattern] pqBad: [Q #3 #1, P #3 #2]
trace: [grind.ematch.pattern] pqBad: [Q #3 #1, P #3 #2]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
@[grind] theorem pqBad : P x y → Q x z := sorry
example : P a b → Q a c := by
@ -201,9 +201,9 @@ opaque f : Nat → Nat
opaque g : Nat → Nat → Nat
/--
info: [grind.ematch.pattern] fq: [g #0 (f #0)]
trace: [grind.ematch.pattern] fq: [g #0 (f #0)]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
@[grind =_]
theorem fq : f x = g x (f x) := sorry
@ -215,10 +215,10 @@ opaque f : Nat → Nat
opaque g : Nat → Nat → Nat
/--
info: [grind.ematch.pattern] fq: [f #0]
trace: [grind.ematch.pattern] fq: [f #0]
[grind.ematch.pattern] fq: [g #0 (g #0 #0)]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
@[grind _=_]
theorem fq : f x = g x (g x x) := sorry

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

@ -43,14 +43,14 @@ example (as bs cs : Array α) (v₁ v₂ : α)
grind
/--
info: [grind.ematch.instance] Array.size_set: (cs.set i₃ v₃ ⋯).size = cs.size
trace: [grind.ematch.instance] Array.size_set: (cs.set i₃ v₃ ⋯).size = cs.size
[grind.ematch.instance] Array.size_set: (bs.set i₂ v₂ ⋯).size = bs.size
[grind.ematch.instance] Array.size_set: (as.set i₁ v₁ ⋯).size = as.size
[grind.ematch.instance] Array.getElem_set_ne: ∀ (pj : j < cs.size), i₃ ≠ j → (cs.set i₃ v₃ ⋯)[j] = cs[j]
[grind.ematch.instance] Array.getElem_set_ne: ∀ (pj : j < bs.size), i₂ ≠ j → (bs.set i₂ v₂ ⋯)[j] = bs[j]
[grind.ematch.instance] Array.getElem_set_ne: ∀ (pj : j < as.size), i₁ ≠ j → (as.set i₁ v₁ ⋯)[j] = as[j]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (as bs cs ds : Array α) (v₁ v₂ v₃ : α)
(i₁ i₂ i₃ j : Nat)
(h₁ : i₁ < as.size)
@ -69,8 +69,8 @@ opaque f (a b : α) : α := a
@[grind =] theorem fx : f x (f x x) = x := sorry
/--
info: [grind.ematch.instance] fx: f a (f a a) = a
trace: [grind.ematch.instance] fx: f a (f a a) = a
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : a = b₁ → c = f b₁ b₂ → f a c ≠ a → a = b₂ → False := by
grind

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

@ -3,10 +3,10 @@ def replicate : (n : Nat) → (a : α) → List α
| n+1, a => a :: replicate n a
/--
info: [grind.ematch.pattern] replicate.eq_1: [@replicate #1 `[0] #0]
trace: [grind.ematch.pattern] replicate.eq_1: [@replicate #1 `[0] #0]
[grind.ematch.pattern] replicate.eq_2: [@replicate #2 (#0 + 1) #1]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.ematch.pattern true in
attribute [grind] replicate

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

@ -14,12 +14,12 @@ set_option trace.grind.ematch.instance true
set_option trace.grind.assert true
/--
info: [grind.assert] f (y + 1) = a
trace: [grind.assert] f (y + 1) = a
[grind.assert] ¬a = g (f y)
[grind.ematch.instance] f.eq_2: f y.succ = g (f y)
[grind.assert] f (y + 1) = g (f y)
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f (y + 1) = a → a = g (f y):= by
grind
@ -29,7 +29,7 @@ example : f (y + 1) = a → a = g (f y):= by
| x::xs => x :: app xs ys
/--
info: [grind.assert] app [1, 2] ys = xs
trace: [grind.assert] app [1, 2] ys = xs
[grind.assert] ¬xs = 1 :: 2 :: ys
[grind.ematch.instance] app.eq_2: app [1, 2] ys = 1 :: app [2] ys
[grind.assert] app [1, 2] ys = 1 :: app [2] ys
@ -38,7 +38,7 @@ info: [grind.assert] app [1, 2] ys = xs
[grind.ematch.instance] app.eq_1: app [] ys = ys
[grind.assert] app [] ys = ys
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : app [1, 2] ys = xs → xs = 1::2::ys := by
grind
@ -48,12 +48,12 @@ opaque q : Nat → Prop
@[grind =] theorem pq : p x x ↔ q x := by sorry
/--
info: [grind.assert] p a a
trace: [grind.assert] p a a
[grind.assert] ¬q a
[grind.ematch.instance] pq: p a a ↔ q a
[grind.assert] p a a = q a
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : p a a → q a := by
grind
@ -65,7 +65,7 @@ theorem appV_assoc (a : Vector α n) (b : Vector α m) (c : Vector α n') :
HEq (appV a (appV b c)) (appV (appV a b) c) := sorry
/--
info: [grind.assert] x1 = appV a_2 b
trace: [grind.assert] x1 = appV a_2 b
[grind.assert] x2 = appV x1 c
[grind.assert] x3 = appV b c
[grind.assert] x4 = appV a_2 x3
@ -73,6 +73,6 @@ info: [grind.assert] x1 = appV a_2 b
[grind.ematch.instance] appV_assoc: HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
[grind.assert] HEq (appV a_2 (appV b c)) (appV (appV a_2 b) c)
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : x1 = appV a b → x2 = appV x1 c → x3 = appV b c → x4 = appV a x3 → HEq x2 x4 := by
grind

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

@ -1,3 +1,5 @@
set_option grind.warning false
theorem dummy (x : Nat) : x = x :=
rfl
@ -17,7 +19,7 @@ def one : α := sorry
theorem inv_eq {a b : α} (w : mul a b = one) : inv a = b := sorry
/--
info: [grind.ematch.pattern] inv_eq: [@Lean.Grind.eqBwdPattern `[α] (inv #2) #1]
trace: [grind.ematch.pattern] inv_eq: [@Lean.Grind.eqBwdPattern `[α] (inv #2) #1]
-/
#guard_msgs in
set_option trace.grind.ematch.pattern true in
@ -52,10 +54,10 @@ example (s : S) : a ≠ s.f false → a = inv (s.f true) → False := by
grind
/--
info: [grind.ematch.instance] inv_eq: mul (s.f true) (s.f false) = one → inv (s.f true) = s.f false
trace: [grind.ematch.instance] inv_eq: mul (s.f true) (s.f false) = one → inv (s.f true) = s.f false
[grind.ematch.instance] S.h: mul (s.f true) (s.f false) = one
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.ematch.instance true in
example (s : S) : inv (s.f true) = s.f false := by
grind

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

@ -1,32 +1,32 @@
reset_grind_attrs%
/--
info: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #2 #0]
trace: [grind.ematch.pattern] List.append_ne_nil_of_left_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #2 #0]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.ematch.pattern true in
attribute [grind] List.append_ne_nil_of_left_ne_nil
/--
info: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #1 #2]
trace: [grind.ematch.pattern] List.append_ne_nil_of_right_ne_nil: [@HAppend.hAppend (List #3) (List _) (List _) _ #1 #2]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.ematch.pattern true in
attribute [grind] List.append_ne_nil_of_right_ne_nil
/-- info: [grind.ematch.pattern] List.getLast?_eq_some_iff: [@List.getLast? #2 #1, @some _ #0] -/
#guard_msgs (info) in
/-- trace: [grind.ematch.pattern] List.getLast?_eq_some_iff: [@List.getLast? #2 #1, @some _ #0] -/
#guard_msgs (trace) in
set_option trace.grind.ematch.pattern true in
attribute [grind =] List.getLast?_eq_some_iff
/--
info: [grind.assert] xs.getLast? = b?
trace: [grind.assert] xs.getLast? = b?
[grind.assert] b? = some 10
[grind.assert] xs = []
[grind.assert] (xs.getLast? = some 10) = ∃ ys, xs = ys ++ [10]
[grind.assert] xs = w ++ [10]
[grind.assert] ¬w ++ [10] = []
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.assert true in
example (xs : List Nat) : xs.getLast? = b? → b? = some 10 → xs ≠ [] := by
grind

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

@ -13,10 +13,10 @@ attribute [-grind] fthm'
set_option trace.grind.assert true
/--
info: [grind.assert] ¬f (f (f a)) = f a
trace: [grind.assert] ¬f (f (f a)) = f a
[grind.assert] f (f a) = f a
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f (f (f a)) = f a := by
grind
@ -27,9 +27,9 @@ error: unsolved goals
a : Nat
⊢ f (f (f a)) = f a
---
info: [grind.assert] ¬f (f (f a)) = f a
trace: [grind.assert] ¬f (f (f a)) = f a
-/
#guard_msgs (info, error) in
#guard_msgs (trace, error) in
example : f (f (f a)) = f a := by
fail_if_success grind
@ -61,11 +61,11 @@ error: unsolved goals
a b : Nat
⊢ g a = b → a = 0 → b = 1
---
info: [grind.assert] g a = b
trace: [grind.assert] g a = b
[grind.assert] a = 0
[grind.assert] ¬b = 1
-/
#guard_msgs (info, error) in
#guard_msgs (trace, error) in
example : g a = b → a = 0 → b = 1 := by
fail_if_success grind

24
tests/lean/run/grind_implies.lean
View file

@ -2,7 +2,7 @@ set_option trace.grind.eqc true
set_option trace.grind.internalize true
/--
info: [grind.internalize] p → q
trace: [grind.internalize] p → q
[grind.internalize] p
[grind.internalize] q
[grind.eqc] (p → q) = True
@ -10,12 +10,12 @@ info: [grind.internalize] p → q
[grind.eqc] (p → q) = q
[grind.eqc] q = False
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (p q : Prop) : (p → q) → p → q := by
grind
/--
info: [grind.internalize] p → q
trace: [grind.internalize] p → q
[grind.internalize] p
[grind.internalize] q
[grind.eqc] (p → q) = True
@ -23,12 +23,12 @@ info: [grind.internalize] p → q
[grind.eqc] p = False
[grind.eqc] p = True
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (p q : Prop) : (p → q) → ¬q → ¬p := by
grind
/--
info: [grind.internalize] (p → q) = r
trace: [grind.internalize] (p → q) = r
[grind.internalize] Prop
[grind.internalize] p → q
[grind.internalize] p
@ -40,13 +40,13 @@ info: [grind.internalize] (p → q) = r
[grind.eqc] (p → q) = True
[grind.eqc] r = False
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (p q : Prop) : (p → q) = r → ¬p → r := by
grind
/--
info: [grind.internalize] (p → q) = r
trace: [grind.internalize] (p → q) = r
[grind.internalize] Prop
[grind.internalize] p → q
[grind.internalize] p
@ -58,12 +58,12 @@ info: [grind.internalize] (p → q) = r
[grind.eqc] (p → q) = True
[grind.eqc] r = False
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (p q : Prop) : (p → q) = r → q → r := by
grind
/--
info: [grind.internalize] (p → q) = r
trace: [grind.internalize] (p → q) = r
[grind.internalize] Prop
[grind.internalize] p → q
[grind.internalize] p
@ -76,12 +76,12 @@ info: [grind.internalize] (p → q) = r
[grind.eqc] p = False
[grind.eqc] p = True
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (p q : Prop) : (p → q) = r → ¬q → r → ¬p := by
grind
/--
info: [grind.internalize] (p → q) = r
trace: [grind.internalize] (p → q) = r
[grind.internalize] Prop
[grind.internalize] p → q
[grind.internalize] p
@ -94,6 +94,6 @@ info: [grind.internalize] (p → q) = r
[grind.eqc] p = True
[grind.eqc] p = False
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (p q : Prop) : (p → q) = r → ¬q → ¬r → p := by
grind

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

@ -5,16 +5,16 @@ def f (n : Nat) (m : Nat) :=
n
/--
info: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5
trace: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.ematch.instance true in
example : f 5 m > 0 := by
fail_if_success grind (splits := 0) [f.eq_def]
sorry
/-- info: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5 -/
#guard_msgs (info) in
/-- trace: [grind.ematch.instance] f.eq_def: f 5 m = if 5 < m then f (5 + 1) m + 5 else 5 -/
#guard_msgs (trace) in
set_option trace.grind.ematch.instance true in
example : f 5 m > 0 := by
grind (splits := 1) [f.eq_def]

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

@ -11,7 +11,7 @@ set_option trace.grind.split.candidate true
set_option trace.grind.split.resolved true
/--
info: [grind.assert] (match as, bs with
trace: [grind.assert] (match as, bs with
| [], x => bs
| head :: head_1 :: tail, [] => []
| x :: xs, ys => x :: g xs ys) =
@ -34,7 +34,7 @@ info: [grind.assert] (match as, bs with
| head :: head_1 :: tail, [] => []
| x :: xs, ys => x :: g xs ys
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (f : Nat → List Nat) : g as bs = d → bs = [] → a₁ :: f 0 = as → f 0 = a₂ :: f 1 → d = [] := by
unfold g
grind

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

@ -17,11 +17,11 @@ def h (as : List Nat) :=
| _::_::_ => 3
/--
info: [grind] closed `grind.1`
trace: [grind] closed `grind.1`
[grind] closed `grind.2`
[grind] closed `grind.3`
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind true in
example : h as ≠ 0 := by
grind [h.eq_def]

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

@ -9,11 +9,11 @@ example (f : Int → Int) (x : Int)
-- and we have an invalid counterexample where `x := 1`,
-- but `f x` and `f 1` have different assignments.
/--
info: [grind.cutsat.model] x := 1
trace: [grind.cutsat.model] x := 1
[grind.cutsat.model] f x := 2
[grind.cutsat.model] f 1 := 5
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (f : Int → Int) (x : Int)
: 0 ≤ x → x ≠ 0 → x ≤ 1 → f x = 2 → f 1 = 2 := by
@ -21,11 +21,11 @@ example (f : Int → Int) (x : Int)
sorry
/--
info: [grind.cutsat.model] x := 2
trace: [grind.cutsat.model] x := 2
[grind.cutsat.model] f x := 2
[grind.cutsat.model] f 1 := 5
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (f : Int → Int) (x : Int)
: 0 ≤ x → x ≠ 0 → x ≤ 3 → f x = 2 → f 1 = 2 := by
@ -46,21 +46,21 @@ example (f : Nat → Nat → Nat) (x y : Nat)
-- `b` must not be `2`. Otherwise, `f (b+1)` and `f 3` must be equal.
/-- info: [grind.cutsat.model] b := 3 -/
#guard_msgs (info) in
/-- trace: [grind.cutsat.model] b := 3 -/
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (f : Int → α) (a b : Int) : b > 1 → f (b + 1) = x → f 3 = y → x = y := by
(fail_if_success grind); sorry
-- `b` must not be `2`. Otherwise, `f (b+1)` and `f 3` must be equal.
/--
info: [grind.cutsat.model] x := 7
trace: [grind.cutsat.model] x := 7
[grind.cutsat.model] y := 8
[grind.cutsat.model] b := 3
[grind.cutsat.model] f 3 := 8
[grind.cutsat.model] f (b + 1) := 7
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.cutsat.model true in
example (f : Int → Int) (a b : Int) : b > 1 → f (b + 1) = x → f 3 = y → x = y := by
(fail_if_success grind); sorry

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

@ -5,7 +5,7 @@ set_option grind.warning false
attribute [grind →] Array.eq_empty_of_append_eq_empty eq_nil_of_length_eq_zero
attribute [grind] Vector.getElem?_append getElem?_dropLast
#guard_msgs (info) in -- should not report any issues
#guard_msgs (trace) in -- should not report any issues
set_option trace.grind.issues true
theorem dropLast_concat : dropLast (l₁ ++ [b]) = l₁ := by
fail_if_success grind (gen := 6)

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

@ -22,17 +22,17 @@ detect equalities between array access terms.
-/
/--
info: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›]
trace: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›]
[Meta.debug] [a[i], b[j], a[j]]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i ≤ j) : a[i] < a[j] + b[j] → i = j → a = b → False := by
grind -mbtc on_failure fallback
/--
info: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›]
trace: [Meta.debug] [‹i < a.toList.length›, ‹j < a.toList.length›, ‹j < b.toList.length›]
[Meta.debug] [a[i], a[j]]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (i j : Nat) (a b : Array Nat) (h1 : j < a.size) (h : j < b.size) (h2 : i ≤ j) : a[i] < a[j] + b[j] → i = j → False := by
grind -mbtc on_failure fallback

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

@ -11,8 +11,8 @@ def fallback : Fallback := do
-- `grind` final state must contain only two `g`-applications
set_option trace.Meta.debug true in
/--
info: [Meta.debug] [g (a, b), g (g (a, b))]
trace: [Meta.debug] [g (a, b), g (g (a, b))]
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example {β : Type v} {α : Type u} (a c : α) (b d : β) : g.{max u v + 1} (a, b) = (c, d) → g (g.{max (u+1) (v+1)} (a, b)) = (c, d) → False := by
grind on_failure fallback

48
tests/lean/run/grind_offset.lean
View file

@ -9,52 +9,52 @@ set_option trace.grind.ematch.pattern true
set_option trace.grind.ematch.instance true
set_option trace.grind.assert true
/-- info: [grind.ematch.pattern] f.eq_2: [f (#0 + 1)] -/
/-- trace: [grind.ematch.pattern] f.eq_2: [f (#0 + 1)] -/
#guard_msgs in
grind_pattern f.eq_2 => f (x + 1)
/--
info: [grind.assert] f (y + 1) = a
trace: [grind.assert] f (y + 1) = a
[grind.assert] ¬a = g (f y)
[grind.ematch.instance] f.eq_2: f y.succ = g (f y)
[grind.assert] f (y + 1) = g (f y)
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f (y + 1) = a → a = g (f y) := by
grind
/--
info: [grind.assert] f 1 = a
trace: [grind.assert] f 1 = a
[grind.assert] ¬a = g (f 0)
[grind.ematch.instance] f.eq_2: f (Nat.succ 0) = g (f 0)
[grind.assert] f 1 = g (f 0)
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f 1 = a → a = g (f 0) := by
grind
/--
info: [grind.assert] f 10 = a
trace: [grind.assert] f 10 = a
[grind.assert] ¬a = g (f 9)
[grind.ematch.instance] f.eq_2: f (Nat.succ 8) = g (f 8)
[grind.ematch.instance] f.eq_2: f (Nat.succ 9) = g (f 9)
[grind.assert] f 9 = g (f 8)
[grind.assert] f 10 = g (f 9)
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f 10 = a → a = g (f 9) := by
grind
/--
info: [grind.assert] f (c + 2) = a
trace: [grind.assert] f (c + 2) = a
[grind.assert] ¬a = g (g (f c))
[grind.ematch.instance] f.eq_2: f (c + 1).succ = g (f (c + 1))
[grind.assert] f (c + 2) = g (f (c + 1))
[grind.ematch.instance] f.eq_2: f c.succ = g (f c)
[grind.assert] f (c + 1) = g (f c)
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f (c + 2) = a → a = g (g (f c)) := by
grind
@ -64,86 +64,86 @@ example : f (c + 2) = a → a = g (g (f c)) := by
| 1 => 10
| a+2 => g (foo a)
/-- info: [grind.ematch.pattern] foo.eq_3: [foo (#0 + 2)] -/
/-- trace: [grind.ematch.pattern] foo.eq_3: [foo (#0 + 2)] -/
#guard_msgs in
grind_pattern foo.eq_3 => foo (a_2 + 2)
-- The instance is correctly found in the following example.
-- TODO: to complete the proof, we need linear arithmetic support to prove that `b + 2 = c + 1`.
/--
info: [grind.assert] foo (c + 1) = a
trace: [grind.assert] foo (c + 1) = a
[grind.assert] c = b + 1
[grind.assert] ¬a = g (foo b)
[grind.ematch.instance] foo.eq_3: foo b.succ.succ = g (foo b)
[grind.assert] foo (b + 2) = g (foo b)
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : foo (c + 1) = a → c = b + 1 → a = g (foo b) := by
grind
set_option trace.grind.assert false
/--
info: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
trace: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
[grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98))
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f (x + 100) = a → a = b := by
fail_if_success grind (ematch := 2)
sorry
/--
info: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
trace: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
[grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98))
[grind.ematch.instance] f.eq_2: f (x + 97).succ = g (f (x + 97))
[grind.ematch.instance] f.eq_2: f (x + 96).succ = g (f (x + 96))
[grind.ematch.instance] f.eq_2: f (x + 95).succ = g (f (x + 95))
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f (x + 100) = a → a = b := by
fail_if_success grind (ematch := 5)
sorry
/--
info: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
trace: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
[grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98))
[grind.ematch.instance] f.eq_2: f (x + 97).succ = g (f (x + 97))
[grind.ematch.instance] f.eq_2: f (x + 96).succ = g (f (x + 96))
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f (x + 100) = a → a = b := by
fail_if_success grind (ematch := 100) (instances := 4)
sorry
/--
info: [grind.ematch.instance] f.eq_2: f (y + 9).succ = g (f (y + 9))
trace: [grind.ematch.instance] f.eq_2: f (y + 9).succ = g (f (y + 9))
[grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
[grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98))
[grind.ematch.instance] f.eq_2: f (y + 8).succ = g (f (y + 8))
[grind.ematch.instance] f.eq_2: f (y + 7).succ = g (f (y + 7))
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f (x + 100) = a → f (y + 10) = c → a = b := by
fail_if_success grind (ematch := 100) (instances := 5)
sorry
/--
info: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
trace: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
[grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98))
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f (x + 100) = a → a = b := by
fail_if_success grind (gen := 2)
sorry
/--
info: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
trace: [grind.ematch.instance] f.eq_2: f (x + 99).succ = g (f (x + 99))
[grind.ematch.instance] f.eq_2: f (x + 98).succ = g (f (x + 98))
[grind.ematch.instance] f.eq_2: f (x + 97).succ = g (f (x + 97))
[grind.ematch.instance] f.eq_2: f (x + 96).succ = g (f (x + 96))
[grind.ematch.instance] f.eq_2: f (x + 95).succ = g (f (x + 95))
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example : f (x + 100) = a → a = b := by
fail_if_success grind (gen := 5)
sorry

89
tests/lean/run/grind_offset_cnstr.lean
View file

@ -1,7 +1,8 @@
set_option grind.warning false
set_option grind.debug true
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.internalize] a1 + 1 ≤ a2 ↦ #0 + 1 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
@ -9,7 +10,7 @@ info: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a4 ↦ #3
[grind.offset.internalize] a3 ≤ a4 ↦ #2 ≤ #3
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize true in
example (a1 a2 a3) :
a1 + 1 ≤ a2 → a2 ≤ a3 + 2 → a3 ≤ a4 → False := by
@ -17,14 +18,14 @@ example (a1 a2 a3) :
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 + 1 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2
[grind.offset.dist] #0 + 1 ≤ #2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
@ -34,14 +35,14 @@ example (a1 a2 a3 : Nat) :
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 + 1 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 + 2 ≤ #2
[grind.offset.dist] #0 + 3 ≤ #2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
@ -50,14 +51,14 @@ example (a1 a2 a3 : Nat) :
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 + 1 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2 + 2
[grind.offset.dist] #0 ≤ #2 + 1
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
@ -66,14 +67,14 @@ example (a1 a2 a3 : Nat) :
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2
[grind.offset.dist] #0 ≤ #2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
@ -82,14 +83,14 @@ example (a1 a2 a3 : Nat) :
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 + 2 ≤ #2
[grind.offset.dist] #0 + 2 ≤ #2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
@ -98,14 +99,14 @@ example (a1 a2 a3 : Nat) :
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2 + 5
[grind.offset.dist] #0 ≤ #2 + 5
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
@ -114,14 +115,14 @@ example (a1 a2 a3 : Nat) :
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1 + 5
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2
[grind.offset.dist] #0 ≤ #2 + 5
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
@ -130,14 +131,14 @@ example (a1 a2 a3 : Nat) :
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1 + 5
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 + 2 ≤ #2
[grind.offset.dist] #0 ≤ #2 + 3
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
@ -146,14 +147,14 @@ example (a1 a2 a3 : Nat) :
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1 + 5
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 ≤ #2 + 2
[grind.offset.dist] #0 ≤ #2 + 7
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) :
@ -169,14 +170,14 @@ example (a1 a2 a3 : Nat) :
sorry
/--
info: [grind.offset.internalize.term] a1 ↦ #0
trace: [grind.offset.internalize.term] a1 ↦ #0
[grind.offset.internalize.term] a2 ↦ #1
[grind.offset.dist] #0 ≤ #1 + 2
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #1 + 3 ≤ #2
[grind.offset.dist] #0 + 1 ≤ #2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (a1 a2 a3 : Nat) : a1 ≤ a2 + 2 → a2 + 3 ≤ a3 → False := by
@ -184,14 +185,14 @@ example (a1 a2 a3 : Nat) : a1 ≤ a2 + 2 → a2 + 3 ≤ a3 → False := by
sorry
/--
info: [grind.offset.internalize.term] a2 ↦ #0
trace: [grind.offset.internalize.term] a2 ↦ #0
[grind.offset.internalize.term] a1 ↦ #1
[grind.offset.dist] #1 + 3 ≤ #0
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #0 + 3 ≤ #2
[grind.offset.dist] #1 + 6 ≤ #2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1 + 2) → ¬p → a2 + 3 ≤ a3 → False := by
@ -199,14 +200,14 @@ example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1 + 2) → ¬p → a2 + 3
sorry
/--
info: [grind.offset.internalize.term] a2 ↦ #0
trace: [grind.offset.internalize.term] a2 ↦ #0
[grind.offset.internalize.term] a1 ↦ #1
[grind.offset.dist] #1 ≤ #0 + 1
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #0 + 3 ≤ #2
[grind.offset.dist] #1 + 2 ≤ #2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by
@ -214,14 +215,14 @@ example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 2 ≤ a1) → ¬p → a2 + 3
sorry
/--
info: [grind.offset.internalize.term] a2 ↦ #0
trace: [grind.offset.internalize.term] a2 ↦ #0
[grind.offset.internalize.term] a1 ↦ #1
[grind.offset.dist] #1 + 1 ≤ #0
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #0 + 3 ≤ #2
[grind.offset.dist] #1 + 4 ≤ #2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by
@ -229,14 +230,14 @@ example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 ≤ a1) → ¬p → a2 + 3 ≤ a
sorry
/--
info: [grind.offset.internalize.term] a2 ↦ #0
trace: [grind.offset.internalize.term] a2 ↦ #0
[grind.offset.internalize.term] a1 ↦ #1
[grind.offset.dist] #1 ≤ #0
[grind.offset.internalize.term] a3 ↦ #2
[grind.offset.dist] #0 + 3 ≤ #2
[grind.offset.dist] #1 + 3 ≤ #2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.internalize.term true in
set_option trace.grind.offset.dist true in
example (p : Prop) (a1 a2 a3 : Nat) : (p ↔ a2 + 1 ≤ a1) → ¬p → a2 + 3 ≤ a3 → False := by
@ -275,45 +276,45 @@ fun {a4} p a1 a2 a3 =>
(Nat.lo_lo a2 a3 a4 3 3 h_2 (Nat.of_ro_eq_false a4 a3 2 (Eq.trans (Eq.symm h_3) (eq_false h_1)))))))
True.intro)
-/
#guard_msgs (info) in
#guard_msgs in
open Lean Grind in
#print ex1._proof_1
/-! Propagate `cnstr = False` tests -/
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p q r s : Prop) (a b : Nat) : a ≤ b → b + 2 ≤ c → (a + 1 ≤ c ↔ p) → (a + 2 ≤ c ↔ s) → (a ≤ c ↔ q) → (a ≤ c + 4 ↔ r) → p ∧ q ∧ r ∧ s := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p q : Prop) (a b : Nat) : a ≤ b → b ≤ c → (a ≤ c ↔ p) → (a ≤ c + 1 ↔ q) → p ∧ q := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p q : Prop) (a b : Nat) : a ≤ b → b ≤ c + 1 → (a ≤ c + 1 ↔ p) → (a ≤ c + 2 ↔ q) → p ∧ q := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p r s : Prop) (a b : Nat) : a ≤ b → b + 2 ≤ c → (c ≤ a ↔ p) → (c ≤ a + 1 ↔ s) → (c + 1 ≤ a ↔ r) → ¬p ∧ ¬r ∧ ¬s := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p r : Prop) (a b : Nat) : a ≤ b → b ≤ c → (c + 1 ≤ a ↔ p) → (c + 2 ≤ a + 1 ↔ r) → ¬p ∧ ¬r := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p r : Prop) (a b : Nat) : a ≤ b → b ≤ c + 3 → (c + 5 ≤ a ↔ p) → (c + 4 ≤ a ↔ r) → ¬p ∧ ¬r := by
grind (splits := 0)
@ -321,37 +322,37 @@ example (p r : Prop) (a b : Nat) : a ≤ b → b ≤ c + 3 → (c + 5 ≤ a ↔
/-! Propagate `cnstr = False` tests, but with different internalization order -/
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p q r s : Prop) (a b : Nat) : (a + 1 ≤ c ↔ p) → (a + 2 ≤ c ↔ s) → (a ≤ c ↔ q) → (a ≤ c + 4 ↔ r) → a ≤ b → b + 2 ≤ c → p ∧ q ∧ r ∧ s := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p q : Prop) (a b : Nat) : (a ≤ c ↔ p) → (a ≤ c + 1 ↔ q) → a ≤ b → b ≤ c → p ∧ q := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p q : Prop) (a b : Nat) : (a ≤ c + 1 ↔ p) → (a ≤ c + 2 ↔ q) → a ≤ b → b ≤ c + 1 → p ∧ q := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p r s : Prop) (a b : Nat) : (c ≤ a ↔ p) → (c ≤ a + 1 ↔ s) → (c + 1 ≤ a ↔ r) → a ≤ b → b + 2 ≤ c → ¬p ∧ ¬r ∧ ¬s := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p r : Prop) (a b : Nat) : (c + 1 ≤ a ↔ p) → (c + 2 ≤ a + 1 ↔ r) → a ≤ b → b ≤ c → ¬p ∧ ¬r := by
grind (splits := 0)
-- The following example is solved by `grind` using constraint propagation and 0 case-splits.
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.split true in
example (p r : Prop) (a b : Nat) : (c + 5 ≤ a ↔ p) → (c + 4 ≤ a ↔ r) → a ≤ b → b ≤ c + 3 → ¬p ∧ ¬r := by
grind (splits := 0)
@ -398,7 +399,7 @@ example (a : Nat) : a < 2 → a = 5 → False := by
example (a : Nat) : a < 2 → a = b → b = c → c = 5 → False := by
grind
#guard_msgs (info) in -- none of the numerals should be internalized by the offset module
#guard_msgs (trace) in -- none of the numerals should be internalized by the offset module
set_option trace.grind.offset.internalize true in
example (a b c d e : Nat) : a = 1 → b = 2 → c = 3 → d = 4 → e = 5 → a ≠ e := by
grind

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

@ -5,54 +5,54 @@ set_option grind.debug.proofs true
set_option trace.grind.offset.model true
/--
info: [grind.offset.model] i := 1
trace: [grind.offset.model] i := 1
[grind.offset.model] j := 0
[grind.offset.model] 「0」 := 0
[grind.offset.model] 「i + 1」 := 2
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = i + 1 := by
fail_if_success grind
sorry
/--
info: [grind.offset.model] i := 101
trace: [grind.offset.model] i := 101
[grind.offset.model] 「0」 := 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (i : Nat) : i ≤ 100 := by
fail_if_success grind
sorry
/--
info: [grind.offset.model] i := 99
trace: [grind.offset.model] i := 99
[grind.offset.model] 「0」 := 0
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (i : Nat) : 100 ≤ i := by
fail_if_success grind
sorry
/--
info: [grind.offset.model] n := 0
trace: [grind.offset.model] n := 0
[grind.offset.model] j := 0
[grind.offset.model] i := 99
[grind.offset.model] 「0」 := 0
[grind.offset.model] 「n + 1」 := 1
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (i : Nat) : g (n + 1) m = a → 100 + j ≤ i := by
fail_if_success grind
sorry
/--
info: [grind.offset.model] n := 0
trace: [grind.offset.model] n := 0
[grind.offset.model] j := 101
[grind.offset.model] i := 0
[grind.offset.model] 「0」 := 0
[grind.offset.model] 「n + 1」 := 1
-/
#guard_msgs (info) in
#guard_msgs (trace) in
example (i : Nat) : g (n + 1) m = a → j ≤ i + 100 := by
fail_if_success grind
sorry

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

@ -1,20 +1,20 @@
set_option trace.grind.ematch.pattern true
/--
info: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem (Array #4) `[Nat] _ _ _ (@Array.push _ #3 #2) #1 _]
trace: [grind.ematch.pattern] Array.getElem_push_lt: [@getElem (Array #4) `[Nat] _ _ _ (@Array.push _ #3 #2) #1 _]
-/
#guard_msgs in
grind_pattern Array.getElem_push_lt => (xs.push x)[i]
/--
info: [grind.ematch.pattern] List.getElem_attach: [@getElem (List (@Subtype #3 _)) `[Nat] (@Subtype _ _) _ _ (@List.attach _ #2) #1 _]
trace: [grind.ematch.pattern] List.getElem_attach: [@getElem (List (@Subtype #3 _)) `[Nat] (@Subtype _ _) _ _ (@List.attach _ #2) #1 _]
-/
#guard_msgs in
grind_pattern List.getElem_attach => xs.attach[i]
/--
info: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 (List _) _ (@HAppend.hAppend (List _) (List _) (List _) _ #1 (@List.cons _ #0 (@List.nil _))) #0]
trace: [grind.ematch.pattern] List.mem_concat_self: [@Membership.mem #2 (List _) _ (@HAppend.hAppend (List _) (List _) (List _) _ #1 (@List.cons _ #0 (@List.nil _))) #0]
-/
#guard_msgs in
grind_pattern List.mem_concat_self => a ∈ xs ++ [a]
@ -32,7 +32,7 @@ the following theorem parameters cannot be instantiated:
i : Nat
h : i < xs.size
---
info: [grind.ematch.pattern] Array.getElem_push_lt: [@Array.push #4 #3 #2]
trace: [grind.ematch.pattern] Array.getElem_push_lt: [@Array.push #4 #3 #2]
-/
#guard_msgs in
grind_pattern Array.getElem_push_lt => (xs.push x)
@ -54,13 +54,13 @@ instance [Boo α β] : Boo (List α) (Array β) where
theorem fEq [Foo α β] [Boo α β] (a : List α) : (f a).1 = a := rfl
/-- info: [grind.ematch.pattern] fEq: [@f (List #4) (Array #3) _ _ #0] -/
/-- trace: [grind.ematch.pattern] fEq: [@f (List #4) (Array #3) _ _ #0] -/
#guard_msgs in
grind_pattern fEq => f a
theorem fEq2 [Foo α β] [Boo α β] (a : List α) (_h : a.length > 5) : (f a).1 = a := rfl
/-- info: [grind.ematch.pattern] fEq2: [@f (List #5) (Array #4) _ _ #1] -/
/-- trace: [grind.ematch.pattern] fEq2: [@f (List #5) (Array #4) _ _ #1] -/
#guard_msgs in
grind_pattern fEq2 => f a
@ -76,7 +76,7 @@ the following theorem parameters cannot be instantiated:
β : Type
inst✝ : Boo α β
---
info: [grind.ematch.pattern] gEq: [@g (List #3) _ _ #0]
trace: [grind.ematch.pattern] gEq: [@g (List #3) _ _ #0]
-/
#guard_msgs in
grind_pattern gEq => g a
@ -92,7 +92,7 @@ error: invalid pattern(s) for `hThm1`
the following theorem parameters cannot be instantiated:
c : Nat
---
info: [grind.ematch.pattern] hThm1: [plus #2 #3]
trace: [grind.ematch.pattern] hThm1: [plus #2 #3]
-/
#guard_msgs in
grind_pattern hThm1 => plus a b
@ -104,12 +104,12 @@ the following theorem parameters cannot be instantiated:
b : Nat
h : b > 10
---
info: [grind.ematch.pattern] hThm1: [plus #2 #1]
trace: [grind.ematch.pattern] hThm1: [plus #2 #1]
-/
#guard_msgs in
grind_pattern hThm1 => plus a c
/-- info: [grind.ematch.pattern] hThm1: [plus #2 #1, plus #2 #3] -/
/-- trace: [grind.ematch.pattern] hThm1: [plus #2 #1, plus #2 #3] -/
#guard_msgs in
grind_pattern hThm1 => plus a c, plus a b

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

@ -16,14 +16,14 @@ grind_pattern contains_insert => contains (insertElem s a) a
set_option trace.grind.ematch true
set_option trace.grind.ematch.pattern true
/-- info: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/
#guard_msgs (info) in
/-- trace: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/
#guard_msgs (trace) in
example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
s₂ = insertElem s₁ a₁ → a₁ = a₂ → contains s₂ a₂ := by
grind
/-- info: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/
#guard_msgs (info) in
/-- trace: [grind.ematch] activated `contains_insert`, [@contains #3 (@insertElem _ #2 #1 #0) #0] -/
#guard_msgs (trace) in
example [DecidableEq α] (s₁ s₂ : Set α) (a₁ a₂ : α) :
¬ contains s₂ a₂ → s₂ = insertElem s₁ a₁ → a₁ = a₂ → False := by
grind
@ -34,13 +34,13 @@ def foo (x : List Nat) (y : List Nat) := x ++ y ++ x
theorem fooThm : foo x [a, b] = x ++ [a, b] ++ x := rfl
/-- info: [grind.ematch.pattern] fooThm: [foo #0 `[[a, b]]] -/
/-- trace: [grind.ematch.pattern] fooThm: [foo #0 `[[a, b]]] -/
#guard_msgs in
grind_pattern fooThm => foo x [a, b]
/--
info: [grind.internalize] foo x y
trace: [grind.internalize] foo x y
[grind.internalize] [a, b]
[grind.internalize] Nat
[grind.internalize] a
@ -52,7 +52,7 @@ info: [grind.internalize] foo x y
[grind.internalize] y
[grind.internalize] z
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.internalize true in
example : foo x y = z → False := by
fail_if_success grind
@ -62,7 +62,7 @@ theorem arrEx [Add α] (as : Array α) (h₁ : i < as.size) (h₂ : i = j) : as[
/--
info: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 _ _ _ (@getElem (Array _) `[Nat] _ _ _ #2 #5 _) (@getElem (Array _) `[Nat] _ _ _ #2 #4 _)]
trace: [grind.ematch.pattern] arrEx: [@HAdd.hAdd #6 _ _ _ (@getElem (Array _) `[Nat] _ _ _ #2 #5 _) (@getElem (Array _) `[Nat] _ _ _ #2 #4 _)]
-/
#guard_msgs in
grind_pattern arrEx => as[i]+as[j]'(h₂▸h₁)

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

@ -35,13 +35,13 @@ structure Functor (C : Type u₁) [Category.{v₁} C] (D : Type u₂) [Category.
set_option trace.grind.ematch.pattern true
/--
info: [grind.ematch.pattern] Functor.map_id: [@Prefunctor.map #5 _ #3 _ (@Functor.toPrefunctor _ #4 _ #2 #1) #0 #0 (@CategoryStruct.id _ _ #0)]
trace: [grind.ematch.pattern] Functor.map_id: [@Prefunctor.map #5 _ #3 _ (@Functor.toPrefunctor _ #4 _ #2 #1) #0 #0 (@CategoryStruct.id _ _ #0)]
-/
#guard_msgs in
grind_pattern Functor.map_id => self.map (𝟙 X)
/--
info: [grind.ematch.pattern] Functor.map_comp: [@Prefunctor.map #9 _ #7 _ (@Functor.toPrefunctor _ #8 _ #6 #5) #4 #2 (@CategoryStruct.comp _ _ #4 #3 #2 #1 #0)]
trace: [grind.ematch.pattern] Functor.map_comp: [@Prefunctor.map #9 _ #7 _ (@Functor.toPrefunctor _ #8 _ #6 #5) #4 #2 (@CategoryStruct.comp _ _ #4 #3 #2 #1 #0)]
-/
#guard_msgs in
grind_pattern Functor.map_comp => self.map (f ≫ g)

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

@ -79,14 +79,14 @@ end
def g (i : Nat) (j : Nat) (_ : i > j := by omega) := i + j
/--
info: [grind.offset.model] i := 1
trace: [grind.offset.model] i := 1
[grind.offset.model] j := 0
[grind.offset.model] 「0」 := 0
[grind.offset.model] 「i + j」 := 0
[grind.offset.model] 「i + 1」 := 2
[grind.offset.model] 「i + j + 1」 := 1
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.offset.model true in
example (i j : Nat) (h : i + 1 > j + 1) : g (i+1) j = f ((fun x => x) i) + f j + 1 := by
fail_if_success grind
@ -173,13 +173,13 @@ example (a : α) (p q r : Prop) : (h₁ : HEq p a) → (h₂ : HEq q a) → (h
grind
/--
info: [grind.issues] found congruence between
trace: [grind.issues] found congruence between
g b
and
f a
but functions have different types
-/
#guard_msgs (info) in
#guard_msgs (trace) in
set_option trace.grind.issues true in
set_option trace.grind.debug.proof false in
example (f : Nat → Bool) (g : Int → Bool) (a : Nat) (b : Int) : HEq f g → HEq a b → f a = g b := by

Some files were not shown because too many files have changed in this diff Show more