## Stream: general

### Topic: solve_by_elim

#### 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.

#### 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.

#### 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!

#### 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.

#### 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 #### Scott Morrison (Mar 09 2018 at 00:00): Again, it would be nice to automate a bit. #### Scott Morrison (Mar 09 2018 at 00:01): I'll investigate, thanks. #### 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. #### Simon Hudon (Mar 09 2018 at 00:05): (function.funext_iff is a new theorem in mathlib) #### Scott Morrison (Mar 09 2018 at 00:08): (ha, I'd actually just written funext_iff myself) #### Scott Morrison (Mar 09 2018 at 00:24): No, cc doesn't seem to help here. #### Simon Hudon (Mar 09 2018 at 00:25): Can you should me a situation where the issue arises? #### Scott Morrison (Mar 09 2018 at 00:26): Oh -- a bug in solve_by_elim: the recursive call doesn't pass the arguments asms. #### 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  #### Simon Hudon (Mar 09 2018 at 00:27): It doesn't need to because it's declared on the left of : #### Scott Morrison (Mar 09 2018 at 00:27): ah, great, sorry. #### Simon Hudon (Mar 09 2018 at 00:29): This example could be handled by cc on its own #### Scott Morrison (Mar 09 2018 at 00:29): I guess it's obviously not going to help here... #### Kenny Lau (Mar 09 2018 at 00:32): what does solve_by_elim do? #### Scott Morrison (Mar 09 2018 at 00:33): repeatedly tries to apply hypotheses, discharging new goals created by apply by calling itself #### Scott Morrison (Mar 09 2018 at 00:33): (i.e. discharging them by matching against other hypotheses) #### Simon Hudon (Mar 09 2018 at 00:35): @Scott Morrison Can you show me something that cc doesn't solve? #### 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. #### Simon Hudon (Mar 09 2018 at 00:37): cool :) #### Simon Hudon (Mar 09 2018 at 00:38): btw, have you tried tauto? Does it help? #### 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? #### 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. #### 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. #### 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 #### Simon Hudon (Mar 09 2018 at 00:49): I'm wondering if congr_arg / funext_iff / cc might be the best combination #### 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. #### 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.) #### 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 #### 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? #### Scott Morrison (Mar 09 2018 at 00:55): sounds amazing :-) #### 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 #### 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? #### 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  #### Scott Morrison (Apr 13 2018 at 03:56): shows what's going on #### 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 #### Scott Morrison (Apr 13 2018 at 03:59): That does work, but only because my MWE is too M! #### 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. #### 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? - ..." #### 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 #### Simon Hudon (Apr 13 2018 at 04:04): By reverse funext, do you mean congr_fun? #### Mario Carneiro (Apr 13 2018 at 04:05): yes, with some beta postprocessing #### 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. #### 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.) #### 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 #### 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. #### Simon Hudon (Apr 13 2018 at 04:33): @Scott Morrison Can you elaborate on why you prefer the equality between lambda terms? #### 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. #### 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. #### 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). #### 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). #### 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.

#### Mario Carneiro (Apr 17 2018 at 23:36):

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

#### Simon Hudon (Apr 17 2018 at 23:36):

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

#### Simon Hudon (Apr 17 2018 at 23:38):

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

#### 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

#### 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

#### 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)

#### Mario Carneiro (Apr 17 2018 at 23:43):

I think you can still make it optional

#### Simon Hudon (Apr 17 2018 at 23:43):

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

#### Mario Carneiro (Apr 17 2018 at 23:43):

Have you used asms? I think it needs a parser

#### 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.

#### Mario Carneiro (Apr 17 2018 at 23:45):

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

#### 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

#### 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.

#### 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.

#### 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?

#### 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)

#### 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)

#### Scott Morrison (Jun 23 2018 at 02:26):

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

#### 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.

#### 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.

#### 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

#### Simon Hudon (Jun 23 2018 at 02:31):

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

#### 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

#### 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?

#### 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)

#### 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

#### 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.

#### Scott Morrison (Jun 23 2018 at 02:43):

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

#### Simon Hudon (Jun 23 2018 at 02:44):

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

That was fast!

#### Simon Hudon (Jun 23 2018 at 02:45):

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

#### Simon Hudon (Jun 23 2018 at 02:45):

Would you care to add a test case?

Sure!

#### 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
`

#### Scott Morrison (Feb 14 2019 at 00:38):

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

#### Scott Morrison (Feb 14 2019 at 00:38):

This is one of the main features.

#### 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