d975e4302e
This is part of #3983. Fine-grained equational lemmas are useful even for non-recursive functions, so this adds them. The new option `eqns.nonrecursive` can be set to `false` to have the old behavior. ### Breaking channge This is a breaking change: Previously, `rw [Option.map]` would rewrite `Option.map f o` to `match o with … `. Now this rewrite will fail because the equational lemmas require constructors here (like they do for, say, `List.map`). Remedies: * Split on `o` before rewriting. * Use `rw [Option.map.eq_def]`, which rewrites any (saturated) application of `Option.map` * Use `set_option eqns.nonrecursive false` when *defining* the function in question. ### Interaction with simp The `simp` tactic so far had a special provision for non-recursive functions so that `simp [f]` will try to use the equational lemmas, but will also unfold `f` else, so less breakage here (but maybe performance improvements with functions with many cases when applied to a constructor, as the simplifier will no longer unfold to a large `match`-statement and then collapse it right away). For projection functions and functions marked `[reducible]`, `simp [f]` won’t use the equational theorems, and will only use its internal unfolding machinery. ### Implementation notes It uses the same `mkEqnTypes` function as for recursive functions, so we are close to a consistency here. There is still the wrinkle that for recursive functions we don't split matches without an interesting recursive call inside. Unifying that is future work.
146 lines
2.3 KiB
Text
146 lines
2.3 KiB
Text
/-!
|
||
This test should catch intentional or accidential changes to how projections are rewritten by
|
||
various tactics
|
||
-/
|
||
|
||
structure S where
|
||
proj : Nat
|
||
|
||
variable (P : Nat → Prop)
|
||
|
||
section structure_abstract
|
||
|
||
variable (s : S)
|
||
|
||
/--
|
||
error: tactic 'fail' failed
|
||
P : Nat → Prop
|
||
s : S
|
||
⊢ P s.1
|
||
-/
|
||
#guard_msgs in
|
||
example : P (s.proj) := by
|
||
rw [S.proj]
|
||
-- Cannot use
|
||
-- guard_target =ₛ P s.1
|
||
-- here as, as that elaborates as `P s.proj`
|
||
fail
|
||
|
||
/--
|
||
error: tactic 'fail' failed
|
||
P : Nat → Prop
|
||
s : S
|
||
⊢ P s.1
|
||
-/
|
||
#guard_msgs in
|
||
example : P (s.proj) := by
|
||
unfold S.proj
|
||
fail
|
||
|
||
/-- error: simp made no progress -/
|
||
#guard_msgs in
|
||
example : P (s.proj) := by
|
||
simp [S.proj]
|
||
fail
|
||
|
||
end structure_abstract
|
||
|
||
section structure_concrete
|
||
|
||
variable (n : Nat)
|
||
/--
|
||
error: tactic 'fail' failed
|
||
P : Nat → Prop
|
||
n : Nat
|
||
⊢ P { proj := n }.1
|
||
-/
|
||
#guard_msgs in
|
||
example : P (S.proj ⟨n⟩) := by rw [S.proj]; fail
|
||
-- Cannot use
|
||
-- guard_target =ₛ P s.1
|
||
-- here as, as that elaborates as `P s.proj`
|
||
|
||
/--
|
||
error: tactic 'fail' failed
|
||
P : Nat → Prop
|
||
n : Nat
|
||
⊢ P { proj := n }.1
|
||
-/
|
||
#guard_msgs in
|
||
example : P (S.proj ⟨n⟩) := by unfold S.proj; fail
|
||
|
||
/--
|
||
error: tactic 'fail' failed
|
||
P : Nat → Prop
|
||
n : Nat
|
||
⊢ P n
|
||
-/
|
||
#guard_msgs in
|
||
example : P (S.proj ⟨n⟩) := by simp [S.proj]; fail -- NB: reduces the projectino
|
||
|
||
end structure_concrete
|
||
|
||
class C (α : Type) where
|
||
meth : Nat
|
||
|
||
section class_abstract
|
||
|
||
instance : C Bool where
|
||
meth := 42
|
||
|
||
variable (α : Type) [C α]
|
||
|
||
/--
|
||
error: tactic 'fail' failed
|
||
P : Nat → Prop
|
||
α : Type
|
||
inst✝ : C α
|
||
⊢ P inst✝.1
|
||
-/
|
||
#guard_msgs in
|
||
example : P (C.meth α) := by rw [C.meth]; fail
|
||
|
||
/--
|
||
error: tactic 'fail' failed
|
||
P : Nat → Prop
|
||
α : Type
|
||
inst✝ : C α
|
||
⊢ P inst✝.1
|
||
-/
|
||
#guard_msgs in
|
||
example : P (C.meth α) := by unfold C.meth; fail
|
||
|
||
/-- error: simp made no progress -/
|
||
#guard_msgs in
|
||
example : P (C.meth α) := by simp [C.meth]; fail
|
||
|
||
end class_abstract
|
||
|
||
section class_concrete
|
||
|
||
/--
|
||
error: tactic 'fail' failed
|
||
P : Nat → Prop
|
||
⊢ P instCBool.1
|
||
-/
|
||
#guard_msgs in
|
||
example : P (C.meth Bool) := by rw [C.meth]; fail
|
||
|
||
/--
|
||
error: tactic 'fail' failed
|
||
P : Nat → Prop
|
||
⊢ P instCBool.1
|
||
-/
|
||
#guard_msgs in
|
||
example : P (C.meth Bool) := by unfold C.meth; fail
|
||
|
||
/--
|
||
error: tactic 'fail' failed
|
||
P : Nat → Prop
|
||
⊢ P 42
|
||
-/
|
||
#guard_msgs in
|
||
example : P (C.meth Bool) := by simp [C.meth]; fail -- NB: Unfolds the instance `instCBool`!
|
||
|
||
|
||
end class_concrete
|