cf3e7de143
after this change, `simp` will be able to discharge side-goals that, after simplification, are of the form `∀ …, a = b` with `a =?= b`. Usually these side-goals are solved by simplification using `eq_self`, but that does not work when there are metavariables involved. This enables us to have rewrite rules like ``` theorem List.foldl_subtype (p : α → Prop) (l : List (Subtype p)) (f : β → Subtype p → β) (g : β → α → β) (b : β) (hf : ∀ b x h, f b ⟨x, h⟩ = g b x) : l.foldl f b = (l.map (·.val)).foldl g b := by ``` where the parameter `g` does not appear on the lhs, but can be solved for using the `hf` equation. See `tests/lean/run/simpHigherOrder.lean` for more examples. The motivating use-case is that `simp` should be able to clean up the usual ``` l.attach.map (fun <x, _> => x) ``` idiom often seen in well-founded recursive functions with nested recursion. Care needs to be taken with adding such rules to the default simp set if the lhs is very general, and thus causes them to be tried everywhere. Performance impact of just this PR (no additional simp rules) on mathlib is unsuspicious: http://speed.lean-fro.org/mathlib4/compare/b5bc44c7-e53c-4b6c-9184-bbfea54c4f80/to/ae1d769b-2ff2-4894-940c-042d5a698353 I tried a few alternatives, e.g. letting `simp` apply `eq_self` without bumping the mvar depth, or just solve equalities directly, but that broke too much things, and adding code to the default discharger seemed simpler.
69 lines
2.2 KiB
Text
69 lines
2.2 KiB
Text
/-!
|
||
This test checks that simp is able to instantiate the parameter `g` below. It does not
|
||
appear on the lhs of the rule, but solving `hf` fully determines it.
|
||
-/
|
||
|
||
theorem List.foldl_subtype (p : α → Prop) (l : List (Subtype p)) (f : β → Subtype p → β)
|
||
(g : β → α → β) (b : β)
|
||
(hf : ∀ b x h, f b ⟨x, h⟩ = g b x) :
|
||
l.foldl f b = (l.map (·.val)).foldl g b := by
|
||
induction l generalizing b with
|
||
| nil => simp
|
||
| cons a l ih => simp [hf, ih]
|
||
|
||
example (l : List Nat) :
|
||
l.attach.foldl (fun acc t => max acc (t.val)) 0 = l.foldl (fun acc t => max acc t) 0 := by
|
||
simp [List.foldl_subtype]
|
||
|
||
example (l : List Nat) :
|
||
l.attach.foldl (fun acc ⟨t, _⟩ => max acc t) 0 = l.foldl (fun acc t => max acc t) 0 := by
|
||
simp [List.foldl_subtype]
|
||
|
||
|
||
theorem foldr_to_sum (l : List Nat) (f : Nat → Nat → Nat) (g : Nat → Nat)
|
||
(h : ∀ acc x, f x acc = g x + acc) :
|
||
l.foldr f 0 = Nat.sum (l.map g) := by
|
||
rw [Nat.sum, List.foldr_map]
|
||
congr
|
||
funext x acc
|
||
apply h
|
||
|
||
-- this works:
|
||
example (l : List Nat) :
|
||
l.foldr (fun x a => x*x + a) 0 = Nat.sum (l.map (fun x => x * x)) := by
|
||
simp [foldr_to_sum]
|
||
|
||
-- this does not, so such a pattern is still quite fragile
|
||
|
||
/-- error: simp made no progress -/
|
||
#guard_msgs in
|
||
example (l : List Nat) :
|
||
l.foldr (fun x a => a + x*x) 0 = Nat.sum (l.map (fun x => x * x)) := by
|
||
simp [foldr_to_sum]
|
||
|
||
-- but with stronger simp normal forms, it would work:
|
||
|
||
@[simp]
|
||
theorem add_eq_add_cancel (a x y : Nat) : (a + x = y + a) ↔ (x = y) := by omega
|
||
|
||
example (l : List Nat) :
|
||
l.foldr (fun x a => a + x*x) 0 = Nat.sum (l.map (fun x => x * x)) := by
|
||
simp [foldr_to_sum]
|
||
|
||
|
||
-- An example with zipWith
|
||
|
||
theorem zipWith_ignores_right
|
||
(l₁ : List α) (l₂ : List β) (f : α → β → γ) (g : α → γ)
|
||
(h : ∀ a b, f a b = g a) :
|
||
List.zipWith f l₁ l₂ = List.map g (l₁.take l₂.length) := by
|
||
induction l₁ generalizing l₂ with
|
||
| nil => simp
|
||
| cons x xs ih =>
|
||
cases l₂
|
||
· simp
|
||
· simp [List.zipWith, h, ih]
|
||
|
||
example (l₁ l₂ : List Nat) (hlen: l₁.length = l₂.length):
|
||
List.zipWith (fun x y => x*x) l₁ l₂ = l₁.map (fun x => x * x) := by
|
||
simp only [zipWith_ignores_right, hlen.symm, List.take_length]
|