Zulip Chat Archive

Stream: general

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


view this post on Zulip Scott Morrison (Apr 14 2019 at 09:05):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 14 2019 at 09:10):

... help?!

view this post on Zulip Mario Carneiro (Apr 14 2019 at 09:27):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 14 2019 at 09:42):

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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 14 2019 at 09:45):

Sorry, I'll try to make a MWE.

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 14 2019 at 10:02):

it's just a fully elaborated and type correct expression

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:25):

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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:36):

Wah!

view this post on Zulip 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:

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:37):

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

view this post on Zulip Mario Carneiro (Apr 14 2019 at 10:39):

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

view this post on Zulip 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).

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:41):

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

view this post on Zulip 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

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:42):

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

view this post on Zulip Mario Carneiro (Apr 14 2019 at 10:43):

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

view this post on Zulip 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!

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:43):

Which is a lot of them

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:44):

hmm..

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:44):

it seems okay on my example set

view this post on Zulip Mario Carneiro (Apr 14 2019 at 10:44):

I'm really confused on your goals now though

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:44):

oh, sorry

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:44):

the norm_num issue is separate

view this post on Zulip Mario Carneiro (Apr 14 2019 at 10:44):

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

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:45):

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

view this post on Zulip Mario Carneiro (Apr 14 2019 at 10:45):

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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:46):

where XXX should be dec_trivial or (by norm_num)

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:46):

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

view this post on Zulip Mario Carneiro (Apr 14 2019 at 10:46):

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

view this post on Zulip Mario Carneiro (Apr 14 2019 at 10:47):

Or just give them back as subgoals

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 14 2019 at 10:49):

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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:51):

Ok.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:52):

Okay.

view this post on Zulip 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

view this post on Zulip 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'".

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:53):

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

view this post on Zulip 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"

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:58):

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

view this post on Zulip Scott Morrison (Apr 14 2019 at 10:58):

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

view this post on Zulip Mario Carneiro (Apr 14 2019 at 10:59):

okay, just thought I would give some ideas

view this post on Zulip 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. :-)

view this post on Zulip 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")

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip Mario Carneiro (Apr 14 2019 at 11:21):

declaration has a list name field for this

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Scott Morrison (May 03 2019 at 11:07):

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

view this post on Zulip Mario Carneiro (May 03 2019 at 11:29):

you wrote your own instantiate_univ_params?

view this post on Zulip Mario Carneiro (May 03 2019 at 11:29):

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)

Last updated: May 11 2021 at 23:11 UTC