## Stream: general

### Topic: forward implication from an iff, with typeclasses

#### Scott Morrison (Apr 14 2019 at 09:05):

I've discovered a gap in library_search, and am having trouble fixing it.

#### Scott Morrison (Apr 14 2019 at 09:06):

The essential problem is that many library lemmas are iff, and we have to construct the forward and backward implications separately, so they can be applyd.

#### Scott Morrison (Apr 14 2019 at 09:06):

It's very important that this construction step is fast, because we're repeating this step over every relevant imported lemma in the library.

#### Scott Morrison (Apr 14 2019 at 09:08):

My current approach is to use
iff_mp_core in tactic/basic.lean. This takes an expression along with its known type, and builds the corresponding .mp after dropping down through all the arguments.

#### Scott Morrison (Apr 14 2019 at 09:09):

As an example, on le_mul_iff_one_le_left this creates the expression

λ {α : Type u} [_inst_1 : linear_ordered_semiring α] {a b : α} (hb : b > 0), (le_mul_iff_one_le_left hb).mp


#### Scott Morrison (Apr 14 2019 at 09:10):

and at this point you can see my problem... The instance [_inst_1] is not available in the later arguments or body of the lambda, so we get errors:

#### Scott Morrison (Apr 14 2019 at 09:10):

e.g.

failed to synthesize type class instance for
α : Type u,
_inst_1 : linear_ordered_semiring α,
a b : α
⊢ has_zero αLean


at b > 0.

... help?!

#### Mario Carneiro (Apr 14 2019 at 09:27):

Why don't you skip the apply altogether and use unify instead?

#### Mario Carneiro (Apr 14 2019 at 09:29):

actually I can't see the problem as you have articulated it. The iff_mp_core expression already has the instances filled in

#### Scott Morrison (Apr 14 2019 at 09:42):

The problem is that the expression that iff_mp_core produces doesn't even typecheck

#### Scott Morrison (Apr 14 2019 at 09:42):

Because when we put all the lambdas back in place, the instances don't enter the instance cache

#### Scott Morrison (Apr 14 2019 at 09:43):

Note that iff_mp_core is not using to_expr or anything, it's just building expr objects by hand.

#### Scott Morrison (Apr 14 2019 at 09:45):

Sorry, I'll try to make a MWE.

#### Mario Carneiro (Apr 14 2019 at 10:02):

It is exactly because it is building exprs by hand that it doesn't have to worry about typeclass inference or to_expr or anything

#### Mario Carneiro (Apr 14 2019 at 10:02):

it's just a fully elaborated and type correct expression

#### Scott Morrison (Apr 14 2019 at 10:22):

Okay, I agree, my diagnosis of the problem was completely wrong. Nevertheless, I can't get apply to work here. Here's a self-contained instance of the problem:

import algebra.ordered_ring

#print le_mul_iff_one_le_left
-- theorem le_mul_iff_one_le_left : ∀ {α : Type u} [_inst_1 : linear_ordered_semiring α] {a b : α}, b > 0 → (b ≤ a * b ↔ 1 ≤ a) :=

-- This works fine:
def oom {a b : ℕ} (h : 0 < b) (w : 1 ≤ a) : b ≤ a * b :=
(le_mul_iff_one_le_left h).mpr w

open tactic
meta def f : tactic unit :=
do d ← get_decl le_mul_iff_one_le_left,
let n := d.to_name,
let t := d.type,
e ← mk_const n,
mp ← iff_mpr_core e t,
apply mp,
skip

example {a b : ℕ} : b ≤ a * b :=
begin
f,
/-
invalid apply tactic, failed to unify
b ≤ a * b
with
?m_3 ≤ ?m_4 * ?m_3
-/
end


#### Scott Morrison (Apr 14 2019 at 10:23):

oh, crap, it's universes:

set_option pp.all true

example {a b : ℕ} : b ≤ a * b :=
begin
f,
/-
invalid apply tactic, failed to unify
@has_le.le.{0} nat nat.has_le b (@has_mul.mul.{0} nat nat.has_mul a b)
with
@has_le.le.{u} ?m_1
(@preorder.to_has_le.{u} ?m_1
(@partial_order.to_preorder.{u} ?m_1
(@ordered_comm_monoid.to_partial_order.{u} ?m_1
(@ordered_cancel_comm_monoid.to_ordered_comm_monoid.{u} ?m_1
(@ordered_semiring.to_ordered_cancel_comm_monoid.{u} ?m_1
(@linear_ordered_semiring.to_ordered_semiring.{u} ?m_1 ?m_2))))))
?m_3
(@has_mul.mul.{u} ?m_1
(@mul_zero_class.to_has_mul.{u} ?m_1
(@semiring.to_mul_zero_class.{u} ?m_1
(@ordered_semiring.to_semiring.{u} ?m_1 (@linear_ordered_semiring.to_ordered_semiring.{u} ?m_1 ?m_2))))
?m_4
?m_3)
-/
end


#### Scott Morrison (Apr 14 2019 at 10:25):

Or is it? I guess I don't know how apply deals with those us.

#### Scott Morrison (Apr 14 2019 at 10:36):

Oooh... I think I see. The type coming out of d.type has a fixed universe already plugged in. The type for e coming out of mk_const (correctly) has fresh universe metavariables.

Wah!

#### Scott Morrison (Apr 14 2019 at 10:37):

I think this means I have to run infer_type e instead of just using d.type.
:+1:

#### Scott Morrison (Apr 14 2019 at 10:37):

Unfortunately this is slow, and will kill library_search, I think. :-(

#### Mario Carneiro (Apr 14 2019 at 10:39):

just create a bunch of metavariables for the declaration's universe variables and substitute

#### Scott Morrison (Apr 14 2019 at 10:41):

It seems infer_type is not actually a problem (this is strange, as previously it seemed it was).

#### Scott Morrison (Apr 14 2019 at 10:41):

Let me actually profile before deciding whether to do the universe substitution.

#### Scott Morrison (Apr 14 2019 at 10:42):

In any case:

example {a b : ℕ} (h : a ≥ 1): b ≤ a * b :=
by library_search -- exact le_mul_of_ge_one_left' (by norm_num) h


#### Scott Morrison (Apr 14 2019 at 10:42):

(well, not quite --- it does run norm_num to discharge the arithmetic goals, but for now it prints the term norm_num produces, which is no good)

#### Mario Carneiro (Apr 14 2019 at 10:42):

the expr substitution functions should be very fast, faster than apply since apply does that among many other things

#### Scott Morrison (Apr 14 2019 at 10:42):

I know how to fix this, but need to work out how to do substring replacement. :-)

#### Mario Carneiro (Apr 14 2019 at 10:43):

what's the issue / what are you aiming for?

#### Scott Morrison (Apr 14 2019 at 10:43):

The problem has just been the library_search has to date been failing to apply any iff lemmas that involved universes!

#### Scott Morrison (Apr 14 2019 at 10:43):

Which is a lot of them

#### Mario Carneiro (Apr 14 2019 at 10:43):

you shouldn't be running norm_num as part of a library search, that will kill your performance

hmm..

#### Scott Morrison (Apr 14 2019 at 10:44):

it seems okay on my example set

#### Mario Carneiro (Apr 14 2019 at 10:44):

I'm really confused on your goals now though

oh, sorry

#### Scott Morrison (Apr 14 2019 at 10:44):

the norm_num issue is separate

#### Mario Carneiro (Apr 14 2019 at 10:44):

It should be a really simple dumb search to be performant on the whole library

#### Scott Morrison (Apr 14 2019 at 10:45):

okay... let's now change topics to norm_num. :-)

#### Mario Carneiro (Apr 14 2019 at 10:45):

if you can't afford to substitute metavariables you certainly can't afford norm_num

#### Scott Morrison (Apr 14 2019 at 10:45):

I really want to be able to solve problems like this:

example {a b : ℕ} (h : a * 2 ≤ b) : a ≤ b / 2 :=
by library_search -- exact (nat.le_div_iff_mul_le a b XXX).mpr h


#### Scott Morrison (Apr 14 2019 at 10:46):

where XXX should be dec_trivial or (by norm_num)

#### Scott Morrison (Apr 14 2019 at 10:46):

The problem is that too many library lemmas have arithmetic side conditions.

#### Mario Carneiro (Apr 14 2019 at 10:46):

You should note the initial success to shortlist it and come back to it later

#### Mario Carneiro (Apr 14 2019 at 10:47):

Or just give them back as subgoals

#### Scott Morrison (Apr 14 2019 at 10:48):

no, giving back subgoals won't work --- there are way too many lemmas that successfully apply, but the hypotheses are just completely irrelevant to the problem you're actually working on

#### Mario Carneiro (Apr 14 2019 at 10:48):

I think a useful and general approach is to try to rank successes by how similar they are to the goal

#### Mario Carneiro (Apr 14 2019 at 10:49):

i.e. don't necessarily close the goal outright but give some possible matching lemmas

#### Scott Morrison (Apr 14 2019 at 10:49):

Sorry -- do you mean how similar the newly generated goals (after the initial apply) are to the original goal?

#### Scott Morrison (Apr 14 2019 at 10:50):

The problem is there are many lemmas whose conclusion is just a \leq b, and they only really differ in their hypotheses.

#### Mario Carneiro (Apr 14 2019 at 10:50):

I mean how "deeply" the goal and hypotheses match with the target and things in the context

Ok.

#### Scott Morrison (Apr 14 2019 at 10:51):

So at the moment I only report lemmas that match so deeply that solve_by_elim can solve all the newly generated goals, from local hypotheses

#### Mario Carneiro (Apr 14 2019 at 10:51):

I'm still thinking one step proofs here, but it's not an immediate fail if some hypotheses can't be found in the context

Okay.

#### Mario Carneiro (Apr 14 2019 at 10:53):

If you like, you could try splitting into two tactics, one that finds likely candidates and another more tidy-like tactic that tries to kill the subgoals of the candidates

#### Scott Morrison (Apr 14 2019 at 10:53):

Even just: "Apply a library lemma, and then as many as possible local hypotheses. Return the library lemma for which some combination of [number of applied hypotheses]/[number of remaining goals] is 'best'".

#### Scott Morrison (Apr 14 2019 at 10:53):

This follows your description of trying to get good "matching" with the local goals/hypotheses

#### Mario Carneiro (Apr 14 2019 at 10:55):

Especially if you can't close the goal, though, I think you should consider reporting multiple matches. If you can display the subgoals for each case I could quickly look through them to see things like "this one needs 0 > 2, no good, that one needs 2 | x, no good, that one says x < x + 1, ok let's try that"

#### Scott Morrison (Apr 14 2019 at 10:58):

Hmm... this sounds great, but realistically I can't work on that anytime soon.

#### Scott Morrison (Apr 14 2019 at 10:58):

I will PR a fix that deals with the universe issue.

#### Mario Carneiro (Apr 14 2019 at 10:59):

okay, just thought I would give some ideas

#### Scott Morrison (Apr 14 2019 at 10:59):

No, they are great ideas. I will attempt to write up a description of some things someone should do, and shop it around here/to students. :-)

#### Scott Morrison (Apr 14 2019 at 11:00):

(on that note, we should keep thinking about how to make/maintain lists of "things someone should do")

#### Mario Carneiro (Apr 14 2019 at 11:00):

The metamath IDE I use has a "step search" function that allows you to type a statement and then it searches the library and reports all matches. Many are silly matches but they are mostly organized in groups so you can still scroll through them to find the one you are after

#### Mario Carneiro (Apr 14 2019 at 11:01):

that feature would be much improved if the matches were organized by relevance in terms of number of matched constants in the unify, so that things like "\all p, bla -> bla -> p" don't appear in every match

#### Scott Morrison (Apr 14 2019 at 11:09):

So... in copying the universe metavariables over from e <- mk_const n into d.type... how do I know which universes correspond to which?

#### Scott Morrison (Apr 14 2019 at 11:16):

I can call expr.collect_univ_params d.type to collect universes out of the type I get from the declaration, but I have no idea what order this list is in.

#### Scott Morrison (Apr 14 2019 at 11:17):

Is it certain to be in the same order as in ls when I match mk_const n against expr.const _ ls?

#### Mario Carneiro (Apr 14 2019 at 11:21):

declaration has a list name field for this

#### Mario Carneiro (Apr 14 2019 at 11:21):

it lists the universe names used in d.type in the order they appear in expr.const

#### Scott Morrison (Apr 14 2019 at 11:27):

It looks like running infer_type costs about a 10% increase in runtime in the library_search tests, so I'll avoid it, I guess.

#### Scott Morrison (May 03 2019 at 11:07):

@Mario Carneiro I never got this working, but I've made a [WIP] PR that shows the problem I ran into. #967 I'm attempt to update the universe levels in d.type use the new universes from e <- mk_const d.to_name, but apparently I'm not getting them all.

#### Scott Morrison (May 03 2019 at 11:07):

Possibly I'm just doing something dumb as I traverse the expr.

#### Mario Carneiro (May 03 2019 at 11:29):

you wrote your own instantiate_univ_params?

#### Mario Carneiro (May 03 2019 at 11:29):

meta def decl_mk_const (d : declaration) : tactic (expr × expr) :=
do subst ← d.univ_params.mmap $λ u, prod.mk u <$> mk_meta_univ,
`