Zulip Chat Archive

Stream: general

Topic: solve_by_elim


view this post on Zulip Scott Morrison (Mar 08 2018 at 23:54):

@Simon Hudon, the new solve_by_elim is really nice, and now I’d like it to do even more. I know that there is a mechanism to pass arbitrary assumptions, rather than using local context, and perhaps I should just use that.

view this post on Zulip Scott Morrison (Mar 08 2018 at 23:54):

But a particular thing I find myself using frequently now is applying eq.symm to various things in the context, before solve_by_elim can do its thing.

view this post on Zulip Simon Hudon (Mar 08 2018 at 23:59):

That's interesting. Maybe I could add cc to solve_by_elim. In terms of performance, I don't know what kind of slow down that would be but maybe this could be enabled by solve_by_elim!

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:00):

The other thing I'm finding I have to do is replace a hypothesis h : f = g with funext applied to it, to get h' : \forall x : X, f x = g x.

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:00):

Can you try something for me? Write:

meta def my_solve_by_elim (asms : option (list expr) := none)  : opt_param ℕ 3 → tactic unit
| 0 := done
| (succ n) :=
apply_assumption asms $ cc <|> my_solve_by_elim n

and tell me if that does the job

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:00):

Again, it would be nice to automate a bit.

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:01):

I'll investigate, thanks.

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:04):

For the second bit, maybe adding simp [function.funext_iff] at * before solve_by_elim would help.

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:05):

(function.funext_iff is a new theorem in mathlib)

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:08):

(ha, I'd actually just written funext_iff myself)

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:24):

No, cc doesn't seem to help here.

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:25):

Can you should me a situation where the issue arises?

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:26):

Oh -- a bug in solve_by_elim: the recursive call doesn't pass the arguments asms.

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:27):

Well, maybe this is too trivial ... :-)

lemma f {α} (a b : α) (p : a = b) : b = a :=
begin
  my_solve_by_elim
end

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:27):

It doesn't need to because it's declared on the left of :

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:27):

ah, great, sorry.

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:29):

This example could be handled by cc on its own

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:29):

I guess it's obviously not going to help here...

view this post on Zulip Kenny Lau (Mar 09 2018 at 00:32):

what does solve_by_elim do?

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:33):

repeatedly tries to apply hypotheses, discharging new goals created by apply by calling itself

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:33):

(i.e. discharging them by matching against other hypotheses)

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:35):

@Scott Morrison Can you show me something that cc doesn't solve?

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:37):

I'll have to look further. I'll try to see how much cc and solve_by_elim together let me automate, and get back to you if I find such an example.

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:37):

cool :)

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:38):

btw, have you tried tauto? Does it help?

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:39):

no, I haven't looked much at tauto yet. I already have tactics that do a lot of automatic cases, so I'm guessing it won't help much?

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:41):

The other pattern I have all the time is: a hypothesis p : x = y, where x and y are terms of some structure type S, then I go: have p' := congr_arg S.f p, solve_by_elim.

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:41):

It would be lovely to handle that automatically... that is, not just apply hypotheses, but apply structure fields congr_argd over hypotheses.

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:44):

That's an interesting case. It's a bit like funext_iff which we talked about earlier in that we infer the equality of the parts from the equality of the whole. I feel like there's probably a greek-letter-reduction for that

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:49):

I'm wondering if congr_arg / funext_iff / cc might be the best combination

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:51):

I'm not sure what you mean. I guess what I'm hoping for it some automation for finding the correct applications of congr_arg.

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:52):

(i.e. work out for itself what the field S.f should be in my example above: have p' := congr_arg S.f p.)

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:53):

If I see x = y where x and y are functions, I'd specialize ∀ i, x i = y i for every i such that x i appears in the context. Same thing y. I'd do the same with the fields of structure types

view this post on Zulip Simon Hudon (Mar 09 2018 at 00:54):

I'll write something, make a PR to mathlib and send you a link. How about that?

view this post on Zulip Scott Morrison (Mar 09 2018 at 00:55):

sounds amazing :-)

view this post on Zulip Simon Hudon (Mar 09 2018 at 01:14):

Do you have an example where that would be useful? All the examples I can think of can be handled directly by cc

view this post on Zulip Scott Morrison (Apr 13 2018 at 03:44):

cc successfully solves

example {α β : Type} (f g : α → β) (w : g = f) (y : α) : f y = g y := by cc

but not

example {α β : Type} (f g : α → β) (w : (λ x, g x) = (λ x, f x)) (y : α) : f y = g y := by cc

Does anyone see some slight generalisation of cc (and/or possibly solve_by_elim) that can handle the second case?

view this post on Zulip Scott Morrison (Apr 13 2018 at 03:56):

This example is unnecessarily complicated, sorry: even this pair:

example {α β : Type} (f g : α → β) (w : f = g) (y : α) : f y = g y := by cc -- success
example {α β : Type} (f g : α → β) (w : (λ x, f x) = (λ x, g x)) (y : α) : f y = g y := by cc -- FAIL

view this post on Zulip Scott Morrison (Apr 13 2018 at 03:56):

shows what's going on

view this post on Zulip Simon Hudon (Apr 13 2018 at 03:58):

What happens if you call simp on w before cc? If it does eta reduction, then cc should succeed

view this post on Zulip Scott Morrison (Apr 13 2018 at 03:59):

That does work, but only because my MWE is too M!

view this post on Zulip Scott Morrison (Apr 13 2018 at 04:01):

Maybe

example {α : Type} (f g : α → α) (w : (λ x, f (f x)) = (λ x, g (g x))) (y : α) : f (f y) = g (g y) :=

shows more of what I want.

view this post on Zulip Simon Hudon (Apr 13 2018 at 04:01):

That sounds like my conversations with my advisor: "- what are you looking at now? - Large scale software. - Cool, do you have a small example to illustrate your idea? - ..."

view this post on Zulip Mario Carneiro (Apr 13 2018 at 04:04):

scott, you are talking higher order matching here. It's very unlikely you will get something as powerful as what you are envisioning. Your best bet is to apply (reverse) funext on your hypotheses to turn it into a first order problem

view this post on Zulip Simon Hudon (Apr 13 2018 at 04:04):

By reverse funext, do you mean congr_fun?

view this post on Zulip Mario Carneiro (Apr 13 2018 at 04:05):

yes, with some beta postprocessing

view this post on Zulip Simon Hudon (Apr 13 2018 at 04:07):

Maybe @Scott Morrison would be satisfied with converting f (f x) to (f o f) x. Then simp, cc would be good enough.

view this post on Zulip Mario Carneiro (Apr 13 2018 at 04:25):

My point is that if \forall x, f (f x) = g (g x) was in the context instead of the lambda equality, I think cc would get it... maybe. (Honestly I don't understand how cc works, and I never trust it for anything significant.)

view this post on Zulip Simon Hudon (Apr 13 2018 at 04:27):

It seems to work a bit like the ematching feature of smt solvers, doesn't it? I wouldn't count on it to do any specialization

view this post on Zulip Scott Morrison (Apr 13 2018 at 04:31):

@Mario Carneiro, thanks, this had been my past solution, but I'd been a bit worried by it. I'll leave it in place for now.

view this post on Zulip Simon Hudon (Apr 13 2018 at 04:33):

@Scott Morrison Can you elaborate on why you prefer the equality between lambda terms?

view this post on Zulip Scott Morrison (Apr 13 2018 at 05:36):

It’s just that the earlier steps of my automation are giving my equalities
between lambdas as hypotheses, and I’m having trouble automatically always
getting these into a form that cc / solve_by_elim / rewrite_search can deal
with. I think just replacing hypotheses which are equations between
functions types with foralls will do the job, and doesn’t seem to cause
problems elsewhere.

view this post on Zulip Gabriel Ebner (Apr 13 2018 at 07:18):

Congruence closure (cc) performs purely equational reasoning via congruences. It can prove a=b, c=b |- f a = f c, but that's essentially it. One nice feature is that since it uses the congruence lemmas, it effectively ignores subsingleton arguments.

view this post on Zulip Gabriel Ebner (Apr 13 2018 at 07:20):

It definitely won't solve forall x, f x = g x |- f a = g a or fun x, f x = g x |- f a = g a. (They're clearly equivalent via funext, as you've observed.) If you solve such problems, then you have a first-order prover---and this is out of scope for cc. Congruence closure is supposed to be fast, predictable, and well, do congruence closure (and not general first-order proving).

view this post on Zulip Gabriel Ebner (Apr 13 2018 at 07:27):

Re: E-matching. Yes, you can solve the example with forall x, f x = g x using it (I think by[smt] eblast should do it). What E-matching does is that it heuristically generates instances of universally quantified formulas (I think the ematch tactic uses the local context and lemmas tagged [ematch]). In the example it would generate the instance f y = g y, and with this instance cc can solve the goal. The instance f y = g y is generated because the trigger f ?m_1 (in this example the lhs of the lemma) E-matches a currently known subterm, namely f y (the lhs of the target in the example).

view this post on Zulip Scott Morrison (Apr 17 2018 at 23:27):

@Simon Hudon, how would you feel about generalising the definition of solve_by_elim to

meta def solve_by_elim (asms : option (list expr) := none) (discharger : tactic unit := tactic.done) : opt_param  3  tactic unit
| 0     := tactic.done
| (n+1) := discharger <|> (tactic.interactive.apply_assumption asms $ solve_by_elim n)

I find myself using this as solve_by_elim none cc frequently and it's very helpful.

view this post on Zulip Mario Carneiro (Apr 17 2018 at 23:36):

Won't you have to write this as tactic.cc in an interactive tactic script?

view this post on Zulip Simon Hudon (Apr 17 2018 at 23:36):

I like it. Let's switch the order of asms and discharger though.

view this post on Zulip Simon Hudon (Apr 17 2018 at 23:38):

@Mario Carneiro Why? cc is also in tactic.interactive, no?

view this post on Zulip Mario Carneiro (Apr 17 2018 at 23:41):

but if it's not being parsed in interactive mode, you have to use the right namespace

view this post on Zulip Mario Carneiro (Apr 17 2018 at 23:42):

one option is to have an itactic for the discharger, then you can write {cc} or some other tactic block

view this post on Zulip Simon Hudon (Apr 17 2018 at 23:42):

Right. Alternatively, we can provide a variant such as solve_by_elim_with { cc } with a itactic argument (and a better name)

view this post on Zulip Mario Carneiro (Apr 17 2018 at 23:43):

I think you can still make it optional

view this post on Zulip Simon Hudon (Apr 17 2018 at 23:43):

No because itactic doesn't use the same parsing framework as everything else

view this post on Zulip Mario Carneiro (Apr 17 2018 at 23:43):

Have you used asms? I think it needs a parser

view this post on Zulip Simon Hudon (Apr 17 2018 at 23:44):

If we don't want multiple tactic names, we'd have to live with solve_by_elim { } when we don't use that feature.

view this post on Zulip Mario Carneiro (Apr 17 2018 at 23:45):

or stick with just passing a regular tactic and live with solve_by_elim `[cc]

view this post on Zulip Simon Hudon (Apr 17 2018 at 23:46):

Have you used asms? I think it needs a parser

I haven't used it in interactive mode. I think similarly to the options that you can feed simp (e.g. { single_pass := tt }) you can give it a literal as an expression

view this post on Zulip Scott Morrison (Apr 20 2018 at 01:53):

@Simon Hudon just checking -- should I PR this, or would you prefer to do it? I'm happy either way.

view this post on Zulip Scott Morrison (Jun 23 2018 at 02:22):

Hi @SimonHudon, I'm finding often solve_by_elim would succeed, except for the fact that an applicable equation needs to be wrapped in eq.symm first. In this case, {discharger := cc} works, but this tends to be very expensive and I'd really like to avoid it.

view this post on Zulip Scott Morrison (Jun 23 2018 at 02:23):

It's certainly possible to pass a more limited discharger, that just tries to apply hypotheses backwards, but I'm wondering what you think about building this behaviour in?

view this post on Zulip Scott Morrison (Jun 23 2018 at 02:24):

(e.g. by writing a version of apply that knows about symmetric relations, and then using that --- I'd be happy to implement if you thought this was reasonable behaviour)

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:25):

I think that's feasible. We could probably define it as sym_apply (r) := apply r <|> (symmetry >> apply r)

view this post on Zulip Scott Morrison (Jun 23 2018 at 02:26):

oh, that's much sneakier than what I had in mind

view this post on Zulip Scott Morrison (Jun 23 2018 at 02:26):

Currently in apply_assumption you do an initial filtering step by find_matching_head, and I guess this wouldn't be viable.

view this post on Zulip Scott Morrison (Jun 23 2018 at 02:27):

Do you know if this actually saves much time? I'd hope that apply returns very quickly on anything find_matching_head had discarded.

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:31):

You're right. I have a feeling we could get rid of the filtering. I'm not sure that testing the assumptions is any faster than just applying them

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:31):

It might actually be slower because we might be doing the same work twice

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:33):

I naively copied the behavior of assumption when I wrote that tactic. I didn't spend too much time thinking of the performances. It might be interesting to remove the filtering and measure the performances before adding the symmetry

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:41):

The other thing I'm wondering is if we should try every assumption directly first and only then try symmetry or try symmetry as we go. The upside of the first approach is that when you don't need symmetry, you get better performances. The downside is that you can't say that the tactic applies "the first assumption that matches" anymore. If assumption 11 matches directly and assumption 2 matches modulo symmetry, which one do we want the tactic to pick?

view this post on Zulip Scott Morrison (Jun 23 2018 at 02:41):

Hmm... my preference is to just make the change. :-) We do need some better tools for measuring performance. I know I neglect doing it, and then suffer for it later. (e.g. just now realising that letting solve_by_elim call cc can be very expensive)

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:43):

I would prefer just making the change too. I guess the rest is for extra credits :D

view this post on Zulip Scott Morrison (Jun 23 2018 at 02:43):

interesting... my inclination is to try symmetry as we go. When we're using apply, the semantic difference between a=b and b=a has pretty much disappeared.

view this post on Zulip Scott Morrison (Jun 23 2018 at 02:43):

In that case, https://github.com/leanprover/mathlib/pull/164

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:44):

I prefer that too. And my intuition is that the difference in performances will be unnoticeable

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:44):

That was fast!

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:45):

The added benefit is the code gets shorter and neater :)

view this post on Zulip Simon Hudon (Jun 23 2018 at 02:45):

Would you care to add a test case?

view this post on Zulip Scott Morrison (Jun 23 2018 at 02:46):

Sure!

view this post on Zulip Johan Commelin (Feb 13 2019 at 14:38):

Can I somehow tag certain lemmas with some attribute so that solve_by_elim picks them up?

local attibute [use_for_solving] foo bar xyzzy

view this post on Zulip Scott Morrison (Feb 14 2019 at 00:38):

Sorry... I better get on with 'back'.

view this post on Zulip Scott Morrison (Feb 14 2019 at 00:38):

This is one of the main features.

view this post on Zulip Johan Commelin (Feb 14 2019 at 05:55):

Well, my talk is next week, on Tuesday :thinking:


Last updated: May 16 2021 at 20:13 UTC