solve_by_elim

Stream: general

[Scott Morrison]

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

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]

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]

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]

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]

Again, it would be nice to automate a bit.

[Scott Morrison]

I'll investigate, thanks.

[Simon Hudon]

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

[Simon Hudon]

(function.funext_iff is a new theorem in mathlib)

[Scott Morrison]

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

[Scott Morrison]

No, cc doesn't seem to help here.

[Simon Hudon]

Can you should me a situation where the issue arises?

[Scott Morrison]

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

[Scott Morrison]

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

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

[Simon Hudon]

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

[Scott Morrison]

ah, great, sorry.

[Simon Hudon]

This example could be handled by cc on its own

[Scott Morrison]

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

[Kenny Lau]

what does solve_by_elim do?

[Scott Morrison]

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

[Scott Morrison]

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

[Simon Hudon]

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

[Scott Morrison]

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]

cool :)

[Simon Hudon]

btw, have you tried tauto? Does it help?

[Scott Morrison]

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]

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]

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

[Simon Hudon]

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]

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

[Scott Morrison]

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]

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

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]

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

[Scott Morrison]

sounds amazing :-)

[Simon Hudon]

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]

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]

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]

shows what's going on

[Simon Hudon]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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]

By reverse funext, do you mean congr_fun?

[Mario Carneiro]

yes, with some beta postprocessing

[Simon Hudon]

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]

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]

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]

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

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

[Scott Morrison]

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]

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]

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]

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]

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

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

[Simon Hudon]

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

[Simon Hudon]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Mario Carneiro]

I think you can still make it optional

[Simon Hudon]

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

[Mario Carneiro]

Have you used asms? I think it needs a parser

[Simon Hudon]

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]

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

[Simon Hudon]

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]

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

[Scott Morrison]

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]

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]

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

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

[Scott Morrison]

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

[Scott Morrison]

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

[Scott Morrison]

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]

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]

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

[Simon Hudon]

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]

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]

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]

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

[Scott Morrison]

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]

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

[Simon Hudon]

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

[Simon Hudon]

That was fast!

[Simon Hudon]

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

[Simon Hudon]

Would you care to add a test case?

[Scott Morrison]

Sure!

[Johan Commelin]

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]

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

[Scott Morrison]

This is one of the main features.

[Johan Commelin]

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