forward implication from an `iff`, with typeclasses

Stream: general

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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]

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]

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]

e.g.

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

at b > 0.

[Scott Morrison]

... help?!

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

Sorry, I'll try to make a MWE.

[Mario Carneiro]

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]

it's just a fully elaborated and type correct expression

[Scott Morrison]

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]

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]

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

[Scott Morrison]

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.

[Scott Morrison]

Wah!

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

(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]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

Which is a lot of them

[Mario Carneiro]

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

[Scott Morrison]

hmm..

[Scott Morrison]

it seems okay on my example set

[Mario Carneiro]

I'm really confused on your goals now though

[Scott Morrison]

oh, sorry

[Scott Morrison]

the norm_num issue is separate

[Mario Carneiro]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Scott Morrison]

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]

where XXX should be dec_trivial or (by norm_num)

[Scott Morrison]

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

[Mario Carneiro]

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

[Mario Carneiro]

Or just give them back as subgoals

[Scott Morrison]

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]

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

[Mario Carneiro]

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

[Scott Morrison]

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

[Scott Morrison]

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

[Mario Carneiro]

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

[Scott Morrison]

Ok.

[Scott Morrison]

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]

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

[Scott Morrison]

Okay.

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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]

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

[Scott Morrison]

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

[Mario Carneiro]

okay, just thought I would give some ideas

[Scott Morrison]

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]

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

[Mario Carneiro]

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]

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]

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]

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]

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

[Mario Carneiro]

declaration has a list name field for this

[Mario Carneiro]

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

[Scott Morrison]

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]

@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]

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

[Mario Carneiro]

you wrote your own instantiate_univ_params?

[Mario Carneiro]

try this instead:

meta def decl_mk_const (d : declaration) : tactic (expr × expr) :=
do subst ← d.univ_params.mmap $ λ u, prod.mk u <$> mk_meta_univ,
   let e : expr := expr.const d.to_name (prod.snd <$> subst),
   return (e, d.type.instantiate_univ_params subst)