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`.
16 lines
673 B
Text
16 lines
673 B
Text
private definition S := Σ a : nat, nat
|
|
private definition R : S → S → Prop := sigma.skip_left nat (<)
|
|
private definition Rwf : well_founded R :=
|
|
sigma.skip_left_wf nat nat.lt_wf
|
|
private definition f_aux : ∀ (p₁ : S), (∀ p₂ : S, R p₂ p₁ → nat) → nat
|
|
| (sigma.mk n (m+1)) F := F (sigma.mk (n+10) (m - n)) (sigma.mk_skip_left _ _ (nat.sub_lt_succ _ _))
|
|
| (sigma.mk n 0) F := n
|
|
|
|
definition f (n m : nat) : nat :=
|
|
well_founded.fix Rwf f_aux (sigma.mk n m)
|
|
|
|
lemma f.eq_1 (n m : nat) : f n (m+1) = f (n+10) (m - n) :=
|
|
well_founded.fix_eq Rwf f_aux (sigma.mk n (m+1))
|
|
|
|
lemma f.eq_2 (n m : nat) : f n 0 = n :=
|
|
well_founded.fix_eq Rwf f_aux (sigma.mk n 0)
|