Zulip Chat Archive

Stream: general

Topic: apply with new equality goals


view this post on Zulip Reid Barton (Apr 23 2018 at 07:56):

Is there a tactic which works like apply f except that, if unifying the goal with the result type of f fails, it introduces new goals stating that the terms which don't unify are equal?
Example: I want to prove a statement like f ⁻¹' (u ∩ v) = ∅. Suppose I know I want to use preimage_empty : f ⁻¹' ∅ = ∅. I would like to obtain u ∩ v = ∅ as a new goal without spelling it out explicitly (in a have or similar).

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:00):

An interesting idea. You can effectively get the result by refine cast _ f and then congr

view this post on Zulip Patrick Massot (Apr 23 2018 at 08:04):

I'm interested in this question but I don't understand the answer at all. @Reid Barton do your have a MWE so that Mario (or you) could be more explicit about to do this?

view this post on Zulip Reid Barton (Apr 23 2018 at 08:05):

Let me try to cook one up and try out Mario's suggestion

view this post on Zulip Reid Barton (Apr 23 2018 at 08:11):

OK, here's an example:

import data.set
open set

variables {α β : Type}
@[simp] lemma singleton_inter_singleton_eq_empty {x y : α} :
  ({x}  {y} = ( : set α))  x  y :=
by simp [singleton_inter_eq_empty]

example {f : β  α} {x y : α} (h : x  y) : f ⁻¹' {x}  f ⁻¹' {y} =  :=
begin
  rw preimage_inter,
-- ⊢ f ⁻¹' ({x} ∩ {y}) = ∅
  have : {x}  {y} = ( : set α) := by simpa using h,
  rw this, exact preimage_empty
end

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:12):

If p has type f ⁻¹' ∅ = ∅ and the goal is f ⁻¹' (u ∩ v) = ∅, then refine cast _ p will give the goal (f ⁻¹' (u ∩ v) = ∅) = (f ⁻¹' ∅ = ∅) and congr will skip all the same stuff to get to u ∩ v = ∅. Of course this has the usual congr caveats about going too far, but it seems like the right idea for Reid's problem

view this post on Zulip Reid Barton (Apr 23 2018 at 08:14):

refine cast _ preimage_empty guessed to replace the wrong part, though, leaving ⊢ ?m_3 ⁻¹' ∅ = ∅ = (f ⁻¹' ({x} ∩ {y}) = ∅)

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:16):

no that's correct

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:16):

what happens after congr?

view this post on Zulip Reid Barton (Apr 23 2018 at 08:18):

congr errors with "tactic failed, there are no goals to be solved" (even though there were 4 goals)

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:18):

what is the first goal?

view this post on Zulip Reid Barton (Apr 23 2018 at 08:19):

the goals are ⊢ Type ?, ⊢ Type ?, ⊢ ?m_1 → ?m_2, and what I wrote above

view this post on Zulip Reid Barton (Apr 23 2018 at 08:19):

I assume they are describing the type of ?m_3

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:19):

yes

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:19):

You don't want to run congr on those goals

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:20):

you have to cycle through them or set up the refine right, I guess

view this post on Zulip Reid Barton (Apr 23 2018 at 08:20):

I'm confused though because I thought it was the {x} ∩ {y} part I wanted to replace

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:22):

The goal is to do it in two stages. The first stage replaces your goal with an equality between the "apply" theorem and the goal, and the second stage simplifies the equality by congruence until you just have the part(s) that aren't defeq

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

cast has the type A = B -> A -> B, so cast _ p where p : A yields the goal A = B

view this post on Zulip Reid Barton (Apr 23 2018 at 08:23):

Oh I see

view this post on Zulip Reid Barton (Apr 23 2018 at 08:23):

I need to tell it to solve the third goal with f

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

You could also try specifying f for the sake of the example

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:24):

i.e. refine cast _ (@preimage_empty _ _ f)

view this post on Zulip Reid Barton (Apr 23 2018 at 08:25):

I just did exact β, exact α, exact f, congr,, and that also works, and leaves me with ⊢ ∅ = {x} ∩ {y} like I wanted

view this post on Zulip Reid Barton (Apr 23 2018 at 08:26):

Well, I would have preferred ⊢ {x} ∩ {y} = ∅ :simple_smile:

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:26):

I'm not sure if congr will automatically unify when it can, but that would fix these metavars without your intervention

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:26):

I think eq.mp and eq.mpr are the same as cast and allow you to get the orientation right

view this post on Zulip Reid Barton (Apr 23 2018 at 08:29):

Yes, refine cast _ preimage_empty, swap 4, congr also worked

view this post on Zulip Reid Barton (Apr 23 2018 at 08:29):

and eq.mpr eliminates the need for symmetry

view this post on Zulip Reid Barton (Apr 23 2018 at 08:30):

Final version is to replace the last two lines with

  refine eq.mpr _ preimage_empty, swap 4, congr,
-- ⊢ {x} ∩ {y} = ∅
  simpa using h

view this post on Zulip Reid Barton (Apr 23 2018 at 08:31):

This is helpful, I haven't used congr before

view this post on Zulip Reid Barton (Apr 23 2018 at 08:33):

The swap business reminds me of those pairs of tactics which differ only in how the resulting goals get ordered; I guess refine has no such companion?

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:34):

no, it just creates all metavars in the order it finds them

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:35):

There is enough going on here that it would not be unreasonable to have a tactic for it. Keep in mind though that it's not like apply in that it can't guess how many args to apply

view this post on Zulip Patrick Massot (Apr 23 2018 at 08:36):

@Simon Hudon we need you!

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

if you don't get the args right your equality will be some statement like (\forall x. ...) = (f 0 = 0) and congr will not do anything useful

view this post on Zulip Reid Barton (Apr 23 2018 at 08:36):

Right, I realized as I was asking the question that I don't really know how apply figures out how many args to insert

view this post on Zulip Mario Carneiro (Apr 23 2018 at 08:38):

I think it just applies as many as it can, or maybe counts how many nested pi are in the theorem type vs the target type and applies the difference

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

@Patrick Massot What would you imagine a tactic doing?

view this post on Zulip Patrick Massot (Apr 23 2018 at 13:23):

Ideally, the first message of this thread

view this post on Zulip Simon Hudon (Apr 23 2018 at 15:01):

Something like this?

meta def bridge_gap (r : parse texpr) : parse ("using" *> smallnat)? -> tactic unit
| none := refine ``(cast _ %%r) >> congr
| (some n) := refine ``(cast _ %%r) >> congr_n n

This way you can do bridge_gap rule using n to limit the depth of congr or just bridge_gap rule

view this post on Zulip Simon Hudon (Apr 23 2018 at 15:02):

I'm not sure of the name though. Maybe something like fit or adapt_to would be better

view this post on Zulip Simon Hudon (Apr 23 2018 at 15:03):

I don't get why you need swap though

view this post on Zulip Patrick Massot (Apr 23 2018 at 15:12):

Can you do the example with it?

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

I'm giving it a try. My computer is not helping today

view this post on Zulip Simon Hudon (Apr 23 2018 at 15:51):

Ok I think I see why swap was necessary. Here's a proof and a tactic that work:

view this post on Zulip Simon Hudon (Apr 23 2018 at 15:52):

example {f : β  α} {x y : α} (h : x  y) : f ⁻¹' {x}  f ⁻¹' {y} =  :=
begin
  have : {x}  {y} = ( : set α) := by simpa using h,
  bridge_gap preimage_empty,
  rw [preimage_inter,this],
end
namespace tactic
namespace interactive

open interactive interactive.types lean.parser
local postfix `?`:9001 := optional
local postfix *:9001 := many

meta def bridge_gap (sym : parse (tk "←")?) (r : parse texpr) (n : parse (tk "using" *> small_nat)?) : tactic unit :=
do v  mk_mvar,
   if sym.is_none
     then refine ``(eq.mp %%v %%r)
     else refine ``(eq.mpr %%v %%r),
   gs  get_goals,
   set_goals [v],
   (option.cases_on n congr congr_n : tactic unit),
   gs'  get_goals,
   set_goals $ gs' ++ gs

end interactive
end tactic

view this post on Zulip Simon Hudon (Apr 23 2018 at 15:58):

I added an option to allow bridge_gap ← preimage_empty but the parser doesn't seem to like it

view this post on Zulip Simon Hudon (Apr 23 2018 at 16:20):

Ok, it's now working. I put it here https://gist.github.com/cipher1024/0d3328135367269cc35f74f43ecbb302 if you want to use it.

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:24):

Let's get to 20! (I mean 20, not 20!)

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:24):

noooo

view this post on Zulip Mario Carneiro (Apr 23 2018 at 16:25):

my backlog is so long...

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:25):

(deleted)

view this post on Zulip Kevin Buzzard (Apr 23 2018 at 16:25):

He'll go hermit

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:28):

(deleted)

view this post on Zulip Simon Hudon (Apr 23 2018 at 16:34):

Let's get to 20! (I mean 20, not 20!)

20 what?

view this post on Zulip Patrick Massot (Apr 23 2018 at 16:35):

20 opened PR to mathlib

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

Ah! I didn't open a PR. I don't know if it's generally useful

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

Or rather, I don't know if there's interest for this tactic to be in mathlib rather than in one particular project

view this post on Zulip Sebastien Gouezel (Apr 23 2018 at 20:16):

20 :)

view this post on Zulip Patrick Massot (Apr 24 2018 at 00:28):

@Simon Hudon Is this really a problem to have too many tactics in mathlib?

view this post on Zulip Simon Hudon (Apr 24 2018 at 00:33):

I think it's good to prioritize the tactics that will have the most positive impact for the users of mathlib. On one hand, that makes better use of Mario's time and on the other hand, it minimizes the effort required to understand mathlib's features

view this post on Zulip Patrick Massot (Apr 24 2018 at 00:33):

I have a new idea for you (which would simplify my current work). Assume (*) : R → R → R and [is_associative (*))]. I have an expression like (a₁*(a₂*a₃)*a₄)*((a₅*a₆)*a₇) (maybe I'm in conv mode so I only see this expression). I'd like to write simon_new_magic_trick 4 5 and get an expression where parentheses are rearranged so that I see (a₄*a₅) in the middle.

view this post on Zulip Patrick Massot (Apr 24 2018 at 00:34):

And I'm going to sleep (2:33 am here)

view this post on Zulip Simon Hudon (Apr 24 2018 at 00:37):

We can talk about it some more tomorrow. Do you want it as a preparation for something in particular (e.g. rw) or do you foresee using it in combination with multiple other tactics?

view this post on Zulip Simon Hudon (Apr 24 2018 at 00:38):

As for syntax, I could think of calling it ac_zoom a₄*a₅ (in case we want to consider commutativity too) in conv mode.

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 00:40):

that does seem useful. I guess the algebraic normalization functionality got put by the wayside for lean 4

view this post on Zulip Mario Carneiro (Apr 24 2018 at 00:40):

how about ac_focus? that sounds pretty neat

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 00:41):

more generally being able to rewrite declaratively with wildcards like _ would be sweet

view this post on Zulip Simon Hudon (Apr 24 2018 at 00:41):

I guess the algebraic normalization functionality got put by the wayside for lean 4

What are you referring to?

view this post on Zulip Simon Hudon (Apr 24 2018 at 00:42):

more generally being able to rewrite declaratively with wildcards like _ would be sweet

Can you elaborate a bit on what that would look like?

view this post on Zulip Mario Carneiro (Apr 24 2018 at 00:42):

Alternatively, the syntax could be an expression like ac_zoom _*a₄*a₅ and this is ac-unified with the goal

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 00:44):

you have (a1 * (a2 * (a3 * (a4 * (a5 * a6))))), you want a1 * a2 * (a3 * a4) * a5 * a6, hmm, maybe something like mytactic _ * _ * (a3 * a4) * _ * _

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 00:44):

perhaps you could allow less _ than variables and that would make the constraint search easier

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 00:45):

I remember hearing awhile back that there was going to be a lot of algebra machinery going in

view this post on Zulip Mario Carneiro (Apr 24 2018 at 00:45):

you could get by with only one _ on left and right with assoc only, and just one _ on left or right with ac

view this post on Zulip Mario Carneiro (Apr 24 2018 at 00:46):

if there are too many holes you can just fill them eagerly

view this post on Zulip Mario Carneiro (Apr 24 2018 at 00:46):

and fail if there aren't enough terms

view this post on Zulip Mario Carneiro (Apr 24 2018 at 00:47):

commutativity only reasoning seems trickier

view this post on Zulip Simon Hudon (Apr 24 2018 at 00:49):

You mean without associativity? Why is it trickier?

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 00:51):

:( too bad floating point math is non-associative

view this post on Zulip Reid Barton (Apr 24 2018 at 00:54):

@Simon Hudon Thanks, this bridge_gap worked in my real project too.
Only I can't seem to get the ← feature to actually work (I tried bridge_gap ←preimage_empty with all combinations of space or no space around the arrow). But it works fine if I change ← to - for some reason.

view this post on Zulip Reid Barton (Apr 24 2018 at 00:54):

With ←, I get a parse error

view this post on Zulip Reid Barton (Apr 24 2018 at 00:55):

"error: expression expected", and then it continues in a confused state

view this post on Zulip Simon Hudon (Apr 24 2018 at 00:55):

I had a hard time too with that notation. I don't understand why. It works fine with rw. Have you tried <-? That worked better for me

view this post on Zulip Reid Barton (Apr 24 2018 at 00:55):

Yes, that works... something about the arrow

view this post on Zulip Simon Hudon (Apr 24 2018 at 00:56):

I decided not to spend more time investigating that issue because <- works. It's still annoying

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:02):

You have to use tk "<-" instead of tk "←"

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:03):

by some weird setup on lean's part, the token that lean knows as <- is parsed from both <- and

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:03):

so if you write tk "←" it doesn't work at all, and tk "<-" works with both <- and

view this post on Zulip Simon Hudon (Apr 24 2018 at 01:03):

Ah! I bet that was a fun lesson for you to learn!

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

Btw, can you think of a better name than bridge_gap?

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

I expect this is in part because this is a built in notation (like the forward arrow for functions), since it shows up in do notation

view this post on Zulip Simon Hudon (Apr 24 2018 at 01:05):

That makes sense. I'm actually glad that notation is built in

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:05):

Also I think that the polarity of <- should be reversed

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:05):

eq.mpr is the forward one

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:06):

I'm not, if I had my way all notation would be declared in lean

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:06):

maybe I'll get it in lean 4

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:07):

but it does seem like a really hard one to do generically

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:07):

convert?

view this post on Zulip Simon Hudon (Apr 24 2018 at 01:08):

That's a bit too close to conv, no?

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:08):

to be fair it's actually doing a very similar thing

view this post on Zulip Simon Hudon (Apr 24 2018 at 01:09):

That's true

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 01:09):

every time i see conv i think it's talking about convolution

view this post on Zulip Simon Hudon (Apr 24 2018 at 01:09):

Is it something you'd like to have in mathlib btw?

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:09):

little tactics like this are not a big deal

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:10):

go right ahead

view this post on Zulip Simon Hudon (Apr 24 2018 at 01:10):

Cool

view this post on Zulip Mario Carneiro (Apr 24 2018 at 01:11):

I've been busy with my other obligations this past week, but I promise I'll finish updating mathlib and get on those PRs

view this post on Zulip Simon Hudon (Apr 24 2018 at 01:19):

I think the amount of work you've put on mathlib is actually amazing. I think you shouldn't feel like you have to apologize

view this post on Zulip Sean Leather (Apr 24 2018 at 06:06):

22

view this post on Zulip Sean Leather (Apr 24 2018 at 06:07):

... for anyone keeping count.

view this post on Zulip Johan Commelin (Apr 24 2018 at 06:29):

@Mario Carneiro wishing you luck. I just want to thank you for everything you're doing. Please don't feel any pressure from the game these guys are playing...

view this post on Zulip Johan Commelin (Apr 24 2018 at 06:29):

/me wouldn't want another hermit

view this post on Zulip Sean Leather (Apr 24 2018 at 06:43):

I haven't followed the entire conversation, but, to be clear, I think the PR count should not be taken as a backlog waiting to be completed but rather as a sign of interest in the growth of mathlib.

view this post on Zulip Sean Leather (Apr 24 2018 at 06:44):

Personally, I have my own backlog of things I want to contribute, but I'm waiting (patiently, mind you) for stabilization of mathlib wrt Lean.

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:03):

I absolutely agree. I put in a couple of PR's for docs recently and once I did that I felt my job was done -- people can even see the docs if they want. There was no need at all to pester anyone to accept the PR's and I had plenty of other things to worry about. The fact that Lean doesn't keep changing at the minute is also really nice

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:03):

because I am not typing leanpkg upgrade all the time

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 08:03):

so if I really wanted something in mathlib that wasn't there yet, I could just edit the mathlib in _target in my project

view this post on Zulip Patrick Massot (Apr 24 2018 at 08:06):

Yes, this is what I did in https://github.com/PatrickMassot/mathlib/tree/wlog_ext (which is upstream + 2 PR)

view this post on Zulip Scott Morrison (Apr 24 2018 at 11:48):

I like bridge_gap (or whatever it ends up called). I had a primitive version that I was calling its. That is, I'd write its X as a generalised version of exact X, and I would be left with whatever goals were required to unify X with the actual goal.

view this post on Zulip Scott Morrison (Apr 24 2018 at 11:48):

(of course, apostrophe man would probably complain)

view this post on Zulip Scott Morrison (Apr 24 2018 at 11:49):

I'm certainly planning in discarding its in favour of this one once it's in mathlib.

view this post on Zulip Kevin Buzzard (Apr 24 2018 at 13:19):

how about itis? Signed, Apostrophe man.

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

What a cool super hero name :D

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

I submitted as convert. I'm not sure why itis works.

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

I'm wondering if refine_congr would be a good name.

view this post on Zulip Kenny Lau (Apr 24 2018 at 17:57):

23

view this post on Zulip Kenny Lau (Apr 24 2018 at 17:58):

Now I need to sleep

view this post on Zulip Andrew Ashworth (Apr 24 2018 at 17:59):

it would be less than 23 if you finished all your [WIPs] :)


Last updated: May 17 2021 at 22:15 UTC