08eb78a5b2
This PR sets up the new integrated test/bench suite. It then migrates all benchmarks and some related tests to the new suite. There's also some documentation and some linting. For now, a lot of the old tests are left alone so this PR doesn't become even larger than it already is. Eventually, all tests should be migrated to the new suite though so there isn't a confusing mix of two systems.
214 lines
4.6 KiB
Text
214 lines
4.6 KiB
Text
|
||
private axiom test_sorry : ∀ {α}, α
|
||
|
||
set_option linter.missingDocs false
|
||
set_option pp.mvars false
|
||
|
||
example : n + 2 = m := by
|
||
change n + 1 + 1 = _
|
||
guard_target =ₛ n + 1 + 1 = m
|
||
exact test_sorry
|
||
|
||
example (h : n + 2 = m) : False := by
|
||
change _ + 1 = _ at h
|
||
guard_hyp h :ₛ n + 1 + 1 = m
|
||
exact test_sorry
|
||
|
||
example : n + 2 = m := by
|
||
fail_if_success change true
|
||
fail_if_success change _ + 3 = _
|
||
fail_if_success change _ * _ = _
|
||
change (_ : Nat) + _ = _
|
||
exact test_sorry
|
||
|
||
-- `change ... at ...` allows placeholders to mean different things at different hypotheses
|
||
example (h : n + 3 = m) (h' : n + 2 = m) : False := by
|
||
change _ + 1 = _ at h h'
|
||
guard_hyp h :ₛ n + 2 + 1 = m
|
||
guard_hyp h' :ₛ n + 1 + 1 = m
|
||
exact test_sorry
|
||
|
||
-- `change ... at ...` preserves dependencies
|
||
example (p : n + 2 = m → Type) (h : n + 2 = m) (x : p h) : false := by
|
||
change _ + 1 = _ at h
|
||
guard_hyp x :ₛ p h
|
||
exact test_sorry
|
||
|
||
noncomputable example : Nat := by
|
||
fail_if_success change Type 1
|
||
exact test_sorry
|
||
|
||
def foo (a b c : Nat) := if a < b then c else 0
|
||
|
||
/-!
|
||
The first `change` would fail with `typeclass instance problem is stuck` if we did not have
|
||
the `Term.synthesizeSyntheticMVars (postpone := .partial); discard <| isDefEq p e` hint
|
||
-/
|
||
example : foo 1 2 3 = 3 := by
|
||
change (if _ then _ else _) = _
|
||
change ite _ _ _ = _
|
||
change (if _ < _ then _ else _) = _
|
||
change _ = (if true then 3 else 4)
|
||
rfl
|
||
|
||
example (h : foo 1 2 3 = 4) : True := by
|
||
change ite _ _ _ = _ at h
|
||
guard_hyp h :ₛ ite (1 < 2) 3 0 = 4
|
||
trivial
|
||
|
||
example (h : foo 1 2 3 = 4) : True := by
|
||
change (if _ then _ else _) = _ at h
|
||
guard_hyp h : (if 1 < 2 then 3 else 0) = 4
|
||
trivial
|
||
|
||
example (α : Type) [LT α] (x : α) (h : x < x) : x < id x := by
|
||
change _ < _ -- can defer LT typeclass lookup, just like `show`
|
||
change _ < _ at h -- can defer LT typeclass lookup at h too
|
||
guard_target =ₛ x < id x
|
||
change _ < x
|
||
guard_target =ₛ x < x
|
||
exact h
|
||
|
||
/-!
|
||
basic failure
|
||
-/
|
||
/--
|
||
error: 'change' tactic failed, pattern
|
||
m = ?_
|
||
is not definitionally equal to target
|
||
n = m
|
||
-/
|
||
#guard_msgs in example : n = m := by
|
||
change m = _
|
||
|
||
/-!
|
||
`change` can create new metavariables and assign them
|
||
-/
|
||
/--
|
||
trace: x y z : Nat
|
||
w : Nat := x + y
|
||
⊢ x + y = z
|
||
-/
|
||
#guard_msgs in
|
||
example (x y z : Nat) : x + y = z := by
|
||
change ?a = _
|
||
let w := ?a
|
||
trace_state
|
||
exact test_sorry
|
||
|
||
/-!
|
||
`change` is allowed to create new goals.
|
||
Motivation: sometimes there are proof arguments that need to be filled in, and it is easier to do so as a new goal.
|
||
-/
|
||
example (x y : Nat) (h : x = y) : True := by
|
||
change (if 1 < 2 then x else ?z) = y at h
|
||
· trivial
|
||
· exact 22
|
||
|
||
example : let x := 22; let y : Nat := x; let z : Fin (y + 1) := 0; z.1 < y + 1 := by
|
||
intro x y z -- `z` was previously erroneously marked as unused
|
||
change _ at y
|
||
exact z.2
|
||
|
||
/-!
|
||
`change` reorders hypotheses if necessary
|
||
-/
|
||
/--
|
||
trace: x y z w : Nat
|
||
a : Nat := x + y
|
||
h : a = z + w
|
||
⊢ True
|
||
-/
|
||
#guard_msgs in
|
||
example (x y z w : Nat) (h : x + y = z + w) : True := by
|
||
let a := x + y
|
||
change a = _ at h
|
||
trace_state
|
||
trivial
|
||
|
||
/-!
|
||
`change` inserts a coercion when types are incompatible.
|
||
-/
|
||
example (ty : {α : Prop // Nonempty α}) : ty.val := by
|
||
change ty
|
||
guard_target =ₛ ty.val
|
||
exact test_sorry
|
||
|
||
/-!
|
||
Fails, type hint can't hint enough since `.some _` is postponed.
|
||
-/
|
||
/--
|
||
error: Invalid dotted identifier notation: The expected type of `.some` could not be determined
|
||
|
||
Hint: Using one of these would be unambiguous:
|
||
[apply] `some`
|
||
[apply] `Option.Rel.some`
|
||
-/
|
||
#guard_msgs in example : some true = (some true).map id := by
|
||
change _ = .some _
|
||
|
||
/-!
|
||
That works with a mild type hint.
|
||
-/
|
||
example : some true = (some true).map id := by
|
||
change _ = (.some _ : Option _)
|
||
rfl
|
||
|
||
|
||
/-!
|
||
## Conv `change`
|
||
-/
|
||
|
||
/-!
|
||
conv `change` test
|
||
-/
|
||
example (m n : Nat) : m + 2 = n := by
|
||
conv => enter [1]; change m + (1 + 1)
|
||
guard_target =ₛ m + (1 + 1) = n
|
||
exact test_sorry
|
||
|
||
/-!
|
||
conv `change` test failure
|
||
-/
|
||
/--
|
||
error: 'change' tactic failed, pattern
|
||
m + n
|
||
is not definitionally equal to target
|
||
m + 2
|
||
-/
|
||
#guard_msgs in
|
||
example (m n : Nat) : m + 2 = n := by
|
||
conv => enter [1]; change m + n
|
||
|
||
/-!
|
||
conv `change` unsolved metavariables
|
||
-/
|
||
/--
|
||
error: don't know how to synthesize placeholder for argument `e`
|
||
context:
|
||
case a
|
||
m n : Nat
|
||
⊢ Nat
|
||
---
|
||
error: unsolved goals
|
||
m n : Nat
|
||
⊢ m + 2 = n
|
||
-/
|
||
#guard_msgs in
|
||
example (m n : Nat) : m + 2 = n := by
|
||
conv => enter [1]; change if True then m + 2 else ?a
|
||
|
||
/-!
|
||
conv `change` to create a metavariable
|
||
-/
|
||
/--
|
||
trace: a b c d : Nat
|
||
e : Nat := a + b
|
||
⊢ a + b + c = d
|
||
-/
|
||
#guard_msgs in
|
||
example (a b c d : Nat) : a + b + c = d := by
|
||
conv => enter [1,1]; change ?mvar
|
||
let e := ?mvar
|
||
trace_state
|
||
exact test_sorry
|