5cef84709f
See Section "Other goodies" at https://github.com/leanprover/lean/wiki/Refactoring-structures This commit also improves the support for projections in the unifier/matcher. Now, we consider the extra case-split for projections. Given a projection `proj`, and the constraint `proj s =?= proj t`, we need to try first `s =?= t` and if it fails, then try to reduce. This is needed in the standard library because we now have constraints such as: ``` @has_le.le ?A ?s ?a ?b =?= @has_le.le nat nat.has_add x y ``` If we reduce the right hand side, we get the unsolvable constraint ``` @has_le.le ?A ?s ?a ?b =?= nat.le x y ``` Before this change, the constraint was `@le ?A ?s ?a ?b =?= @le nat nat.has_add x y`, and we already perform a case-split in this case. Moreover, projections were eagerly reduced whenever possible. The extra case-split generates a performance problem in several tests. For example `fib 8 = 34` was timing out. I worked around this issue by performing the case-split only when the constraint contains meta-variables. There are also minor issues. Example. `<` is notation for `has_lt.lt`, but `>` is for `gt`.
30 lines
887 B
Text
30 lines
887 B
Text
open tactic
|
|
|
|
def g : nat → nat := λ x, x + 5
|
|
|
|
example (a b : nat) (p : nat → Prop) (h : p (g (nat.succ (nat.succ a)))) : p (g (a + 2)) :=
|
|
begin
|
|
unfold g at h,
|
|
do { h ← get_local `h >>= infer_type, t ← to_expr `(p (nat.succ (nat.succ a) + 5)), guard (h = t) },
|
|
unfold has_add.add bit0 has_one.one nat.add,
|
|
unfold g,
|
|
do { t ← target, h ← get_local `h >>= infer_type, guard (t = h) },
|
|
assumption
|
|
end
|
|
|
|
meta def check_expected (p : pexpr) : tactic unit :=
|
|
do t ← target, ex ← to_expr p, guard (t = ex)
|
|
|
|
example (a b c : nat) (f : nat → nat → nat) (h : false) : f (g a) (g b) = (g c) :=
|
|
begin
|
|
unfold_occs g [2],
|
|
check_expected `(f (g a) (b + 5) = g c),
|
|
contradiction
|
|
end
|
|
|
|
example (a b c : nat) (f : nat → nat → nat) (h : false) : f (g a) (g b) = (g c) :=
|
|
begin
|
|
unfold_occs g [1, 3],
|
|
check_expected `(f (a + 5) (g b) = c + 5),
|
|
contradiction
|
|
end
|