Zulip Chat Archive

Stream: general

Topic: intersections


view this post on Zulip Patrick Massot (Jul 03 2018 at 15:56):

Do we have a better way to do

example {α : Type*} (a b c : set α) : a  b  (a  c) = a  b  c :=
by ext x ; split ; finish

view this post on Zulip Patrick Massot (Jul 03 2018 at 15:56):

Of course I'm not asking for the magic sequence of rewrite, I want Lean to figure it out.

view this post on Zulip Sean Leather (Jul 04 2018 at 06:43):

It would be nice if there was. I run into something similar with conjunction (e.g. a ∧ b ∧ (a ∧ c) = a ∧ b ∧ c) all the time.

view this post on Zulip Simon Hudon (Jul 04 2018 at 07:00):

does cc help?

view this post on Zulip Patrick Massot (Jul 04 2018 at 08:50):

no

view this post on Zulip Patrick Massot (Jul 04 2018 at 13:05):

A related question is: can anyone bring https://leanprover.github.io/programming_in_lean/#09_Writing_Automation.html up to date with current Lean?

view this post on Zulip Reid Barton (Jul 04 2018 at 14:01):

@Sean Leather for a ∧ b ∧ (a ∧ c) ↔ a ∧ b ∧ c, tauto works.

view this post on Zulip Sean Leather (Jul 04 2018 at 14:03):

Yeah, that may be true for that example. But I've run into others where tauto didn't work.

view this post on Zulip Reid Barton (Jul 04 2018 at 14:04):

Yes, tauto is good at failing frustratingly close to the goal

view this post on Zulip Sean Leather (Jul 04 2018 at 14:04):

true:exclamation:

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:04):

Yes, tauto is good at failing frustratingly close to the goal

Excellent, that's what I wrote it for

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:05):

But seriously, any examples of what it can't handle?

view this post on Zulip Reid Barton (Jul 04 2018 at 15:17):

as alluded to above, example (p : Prop) : p ∧ true ↔ p := by tauto

view this post on Zulip Reid Barton (Jul 04 2018 at 15:17):

Somewhat less trivially, I often find it gets stuck needing to prove a = b when b = a is available as a hypothesis

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:23):

The latter should be getting better. @Scott Morrison recently submitted a patch to consider the symmetry of relations in solve_by_elim which tauto uses.

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:24):

As for the first, true is probably the culprit. That's an easy fix, I can submit a PR right away

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:25):

While I'm at it, I'll also take care of false in the assumptions.

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:39):

Done: https://github.com/leanprover/mathlib/pull/175

view this post on Zulip Patrick Massot (Jul 04 2018 at 15:41):

Simon, what is the relation between this tauto and https://leanprover.github.io/programming_in_lean/#09_Writing_Automation.html Would you be able to update the later?

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:49):

I haven't looked closely but that should be doable.

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:50):

I'll take a look

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:54):

By the way, don't despair, I haven't forgotten your request for tutorials

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:55):

I'm preparing a talk about Lean tactics that I'll give at the DeepSpec summer school. That should be the seed for a useful tutorial

view this post on Zulip Patrick Massot (Jul 04 2018 at 15:56):

Nice!

view this post on Zulip Simon Hudon (Jul 04 2018 at 15:56):

I think I'll present the transportable problem that @Kevin Buzzard brought in a few months ago

view this post on Zulip Kevin Buzzard (Jul 04 2018 at 16:22):

+1 from me -- as I've probably said 100 times, this is something which mathematicians do subconsciously.

view this post on Zulip Johan Commelin (Jul 04 2018 at 16:54):

(And that is subconsciously, with big fat capital letters :wink:)

view this post on Zulip Sean Leather (Jul 05 2018 at 06:09):

Reid:

Somewhat less trivially, I often find it gets stuck needing to prove a = b when b = a is available as a hypothesis

Same here! That's the main reason I gave up on using tauto.

Simon:

The latter should be getting better. Scott Morrison recently submitted a patch to consider the symmetry of relations in solve_by_elim which tauto uses.

Cool. I'll have to try it out again.

view this post on Zulip Simon Hudon (Jul 05 2018 at 06:30):

Also, Mario merged my PR today. The one thing tauto doesn't do well still is proving disjunction. I didn't want to do back tracking out of fear that it would get slow but maybe I should do it anyway

view this post on Zulip Patrick Massot (Jul 05 2018 at 15:37):

Here is what I can currently do on this topic:

variables {α : Type*} (a b c : set α) (x : α)

example : a  b  c = c  b  a :=
by simp_inter


example : a  b  a = a  b :=
by simp_inter

example : a  b  (a  c) = a  b  c :=
by simp_inter

example (x  a  b  c) : x  b :=
by simp_inter

example (x  a  b  c) : x  b  a :=
by simp_inter

example (h : x  a) (h' : x  b) (h'' : x  c) : x  b  a :=
by simp_inter

example : x  a   x  b   x  c  x  b  a :=
by simp_inter

view this post on Zulip Patrick Massot (Jul 05 2018 at 15:38):

This is based on the destruct_conjunctions tactic from PIL and then poor's man tactic writing

view this post on Zulip Patrick Massot (Jul 05 2018 at 15:38):

open tactic monad expr
/-- Recursively destructs all hypotheses that are conjunctions. From programming in Lean. -/
meta def destruct_conjunctions : tactic unit :=
repeat (do
  l  local_context,
  first $ l.map (λ h, do
    ht  infer_type h >>= whnf,
    match ht with
    | `(and %%a %%b) := do
      n  get_unused_name `h none,
      mk_mapp ``and.left [none, none, some h] >>= assertv n a,
      n  get_unused_name `h none,
      mk_mapp ``and.right [none, none, some h] >>= assertv n b,
      clear h
    | _ := failed
    end))

/-- Simplify proving intersection and conjunctions goals -/
meta def simp_inter : tactic unit :=
`[  destruct_conjunctions,
    try { ext } ; try { split } ; try { intros }; destruct_conjunctions,
    all_goals { repeat { split } ; assumption }]

view this post on Zulip Patrick Massot (Jul 05 2018 at 15:38):

Any cleaner and more general way to do this is welcome :wink:

view this post on Zulip Patrick Massot (Jul 05 2018 at 15:39):

Note that all examples below should really be solved by the general purpose come_on tactic.

view this post on Zulip Simon Hudon (Jul 05 2018 at 15:40):

Haha! Have you tried tauto since Mario merged my PR yesterday?

view this post on Zulip Patrick Massot (Jul 05 2018 at 15:49):

No. I thought you only changed stuff is true or false appears explicitly.

view this post on Zulip Patrick Massot (Jul 05 2018 at 15:49):

I'm upgrading

view this post on Zulip Simon Hudon (Jul 05 2018 at 15:51):

In your case, it should already work, you're right

view this post on Zulip Simon Hudon (Jul 05 2018 at 15:51):

but recently, there's been added support for symmetric relations and true and false appearing in formulas

view this post on Zulip Patrick Massot (Jul 05 2018 at 15:57):

tauto solves none of my examples

view this post on Zulip Patrick Massot (Jul 05 2018 at 15:57):

even with updated mathlib

view this post on Zulip Simon Hudon (Jul 05 2018 at 15:59):

and with ext; tauto?

view this post on Zulip Patrick Massot (Jul 05 2018 at 16:01):

no luck

view this post on Zulip Patrick Massot (Jul 05 2018 at 16:01):

you can try my examples, they depend on nothing else but mathlib

view this post on Zulip Simon Hudon (Jul 05 2018 at 16:06):

Ok got it

view this post on Zulip Simon Hudon (Jul 05 2018 at 16:06):

first import data.set.basic. That's where set extensionality is declared

view this post on Zulip Simon Hudon (Jul 05 2018 at 16:07):

Next:

example : a  b  c = c  b  a :=
by ext; dsimp; tauto


example : a  b  a = a  b :=
by ext; dsimp; tauto

example : a  b  (a  c) = a  b  c :=
by ext; dsimp; tauto

example (x  a  b  c) : x  b :=
by dsimp at *; tauto

example (x  a  b  c) : x  b  a :=
by dsimp at *; tauto

example (h : x  a) (h' : x  b) (h'' : x  c) : x  b  a :=
by dsimp at *; tauto

example : x  a   x  b   x  c  x  b  a :=
by dsimp at *; tauto

view this post on Zulip Simon Hudon (Jul 05 2018 at 16:07):

Unfortunately, you need to unfold set notation for tauto to work

view this post on Zulip Simon Hudon (Jul 05 2018 at 16:09):

And I'm not sure that adding dsimp to tauto would be a good idea.

view this post on Zulip Simon Hudon (Jul 05 2018 at 16:11):

What I could do is match on hypotheses and goal using definitional equality instead of pattern matching

view this post on Zulip Simon Hudon (Jul 05 2018 at 16:12):

Then the first proof would become:

by ext; tauto

I'm wondering if that would make auto slower. Maybe we could enable this feature with tauto!

view this post on Zulip Simon Hudon (Jul 05 2018 at 16:13):

(In French, that would sound like you're insulting someone, with the exclamation mark)

view this post on Zulip Simon Hudon (Jul 05 2018 at 16:27):

@Mario Carneiro I managed to add support for disjunction but it requires tactic.interactive to import logic.basic. I think the creation of tactic.cache would fix that situation. Should I submit that change in a separate PR? (separate from the traversable PR) If you need more time to review the traversable PR, I think that would be a good way to move forward

view this post on Zulip Patrick Massot (Jul 05 2018 at 17:04):

It does look like one could define

meta def come_one : tactic unit := `[try { ext ; dsimp at *; tauto}, try { dsimp at *; tauto}]

or something like this. It looks much better, thanks!

view this post on Zulip Simon Hudon (Jul 05 2018 at 17:07):

:) At your service

view this post on Zulip Simon Hudon (Jul 05 2018 at 17:08):

I would advise you to call it COME_ON. And you may want to add three exclamation marks, to communicate impatience ;-)

view this post on Zulip Simon Hudon (Jul 05 2018 at 17:09):

Consider:

meta def COME_ON (x y z : parse (tk "!")) : tactic unit := ...

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:13):

The version is used currently is at https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/tactic/easy.lean It passes both the tests I had for simp_inter and the tauto tests from mathlib.

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:18):

Oh, it doesn't work in my real use case :(

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:18):

failed to prove recursive application is decreasing, well founded relation

view this post on Zulip Reid Barton (Jul 05 2018 at 20:23):

Do you have a _let_match or similar in the tactic state?

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:24):

I don't know what is similar to _let_match since I have no idea what it means

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:26):

The full error is:

failed to prove recursive application is decreasing, well founded relation
  @has_well_founded.r
    (Σ' (a : @smooth_compatible X _inst_1 φ ψ) (a : @smooth_compatible X _inst_1 ψ φ),
       @smooth_compatible X _inst_1 ψ χ)
    (@has_well_founded_of_has_sizeof
       (Σ' (a : @smooth_compatible X _inst_1 φ ψ) (a : @smooth_compatible X _inst_1 ψ φ),
          @smooth_compatible X _inst_1 ψ χ)
       (default_has_sizeof
          (Σ' (a : @smooth_compatible X _inst_1 φ ψ) (a : @smooth_compatible X _inst_1 ψ φ),
             @smooth_compatible X _inst_1 ψ χ)))
Possible solutions:
  - Use 'using_well_founded' keyword in the end of your definition to specify tactics for synthesizing well founded relations and decreasing proofs.
  - The default decreasing tactic uses the 'assumption' tactic, thus hints (aka local proofs) can be provided using 'have'-expressions.
The nested exception contains the failure state for the decreasing tactic.
nested exception message:
invalid apply tactic, failed to unify
  0 < 0
with
  ?m_1 < ?m_1 + ?m_2
state:
X : Type,
_inst_1 : inhabited X,
φ ψ χ : chart X,
open_triple_intersection :
  (Σ' (a : smooth_compatible φ ψ) (a : smooth_compatible ψ φ), smooth_compatible ψ χ) 
  is_open (φ '' (φ.domain  ψ.domain  χ.domain)),
op_φ_ψ : is_open_intersection φ ψ,
smooth_φ_ψ : is_smooth_transition φ ψ,
op_ψ_φ : is_open_intersection ψ φ,
smooth_ψ_φ : is_smooth_transition ψ φ,
op_ψ_χ : is_open_intersection ψ χ,
smooth_ψ_χ : is_smooth_transition ψ χ,
x : X,
a : smooth_compatible φ ψ,
a : smooth_compatible ψ φ,
a : smooth_compatible ψ χ
 0 < 0

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:28):

Replacing meta def easy : tactic unit := `[try { ext } , try { dsimp at * }, all_goals { tauto }] by meta def easy : tactic unit := `[try { ext } , try { dsimp }, all_goals { tauto }] make it work in this case but fail in others. Somehow the try is not enough to prevent the error.

view this post on Zulip Simon Hudon (Jul 05 2018 at 20:36):

Well-foundedness is only checked at the end of the proof I believe which means that it won't make individual tactics fail.

view this post on Zulip Simon Hudon (Jul 05 2018 at 20:37):

You may just need to add a have : _ < _, from _ expression to state and prove that some quantity decreases in your recursive function

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:37):

I don't have any recursive function

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:38):

I have no idea what Lean is talking about

view this post on Zulip Simon Hudon (Jul 05 2018 at 20:38):

Can you show the goal prior to calling the tactic? There might be a way of saying "I'm not trying to bring in the curse of recursion"

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:39):

X : Type,
_inst_1 : inhabited X,
φ ψ χ : chart X,
open_triple_intersection :
  smooth_compatible φ ψ 
  smooth_compatible ψ φ  smooth_compatible ψ χ  is_open (φ '' (φ.domain  ψ.domain  χ.domain)),
op_φ_ψ : is_open_intersection φ ψ,
smooth_φ_ψ : is_smooth_transition φ ψ,
op_ψ_φ : is_open_intersection ψ φ,
smooth_ψ_φ : is_smooth_transition ψ φ,
op_ψ_χ : is_open_intersection ψ χ,
smooth_ψ_χ : is_smooth_transition ψ χ,
op : is_open (ψ '' (ψ.domain  φ.domain  χ.domain)),
this : ψ '' (ψ.domain  φ.domain  χ.domain)  ψ '' (ψ.domain  φ.domain),
op : is_open (transition ψ φ '' (ψ '' (ψ.domain  φ.domain  χ.domain))),
h :
  transition ψ φ '' (ψ '' (ψ.domain  φ.domain  χ.domain)) =
    φ '' (ψ.domain  φ.domain  χ.domain)
 ψ.domain  φ.domain  χ.domain = φ.domain  ψ.domain  χ.domain

view this post on Zulip Simon Hudon (Jul 05 2018 at 20:40):

Is the lemma that you're trying to prove open_triple_intersection? If so, try clear open_triple_intersection before calling the tactic.

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:40):

Note that ext, dsimp, tauto works here, but I want a tactic which also works when you need to dsimp something from context

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:41):

Indeed, this is what I'm proving

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:41):

and clearing this works

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:41):

WTF?

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:42):

Is it because I have pattern matching?

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:42):

https://github.com/PatrickMassot/lean-differential-topology/blob/master/src/manifold.lean#L185

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:43):

Indeed

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:43):

If I remove the matching and start with

  intros h h' h'',
  rcases h with op_φ_ψ, smooth_φ_ψ,
  rcases h' with op_ψ_φ, smooth_ψ_φ,
  rcases h'' with op_ψ_χ, smooth_ψ_χ,

Then easy works

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:44):

Do you understand what happens?

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:45):

@Mario Carneiro We really need a hybrid of intros and rcases that would allow writing intros ⟨op_φ_ψ, smooth_φ_ψ⟩ ⟨op_ψ_φ, smooth_ψ_φ⟩ ⟨op_ψ_χ, smooth_ψ_χ⟩

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:45):

instead of the four lines of the previous code block

view this post on Zulip Simon Hudon (Jul 05 2018 at 20:46):

The situation is that pattern matching and recursion are rooted in the same machinery

view this post on Zulip Simon Hudon (Jul 05 2018 at 20:47):

When you pattern match, Lean gives you the opportunity to make a recursive call. It gives you more than you need and once you're done with the proof, it checks whether you introduced recursion / induction and makes sure that it's well-founded

view this post on Zulip Simon Hudon (Jul 05 2018 at 20:47):

Tactics don't see the difference between assumptions that are in fact a recursive call and the rest

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:56):

Thanks

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:56):

I'll forget about matching and patiently wait for rintros to land in mathlib.

view this post on Zulip Patrick Massot (Jul 05 2018 at 20:57):

And I'll go sleeping.

view this post on Zulip Simon Hudon (Jul 05 2018 at 21:06):

You could do something like clear_rec that you call after pattern matching

view this post on Zulip Mario Carneiro (Jul 06 2018 at 05:36):

I managed to add support for disjunction but it requires tactic.interactive to import logic.basic. I think the creation of tactic.cache would fix that situation. Should I submit that change in a separate PR? (separate from the traversable PR) If you need more time to review the traversable PR, I think that would be a good way to move forward

@Simon Hudon I think this is a good idea. Splitting up the different unrelated parts will make it easier to merge things

view this post on Zulip Simon Hudon (Jul 06 2018 at 05:39):

Nice, I hadn't thought of it that way but we'll kill two birds with one stone. I can pull a few more PRs from traversable

view this post on Zulip Simon Hudon (Jul 06 2018 at 05:48):

What's your opinion about using lemmas in tactics that require predicates to be decidable? Would you just let it fail if some predicate is not decidable or would you silently use prop_decidable?

view this post on Zulip Mario Carneiro (Jul 06 2018 at 05:52):

Depends on the use case. I think by_cases will fail, but adding prop_decidable as a local instance fixes this, so this seems sufficiently flexible

view this post on Zulip Simon Hudon (Jul 06 2018 at 05:59):

That's straightforward. With tauto, decidable constraints can come from a lot of different sources and become relevant without obvious reasons

view this post on Zulip Mario Carneiro (Jul 06 2018 at 06:10):

It would be nice if the tactic reports the decidability problem in the error, that way the user can decide what to do about it

view this post on Zulip Simon Hudon (Jul 06 2018 at 06:14):

That's true. Unfortunately, tauto can keep going for a while once it has failed to find a decidable instance

view this post on Zulip Simon Hudon (Jul 06 2018 at 06:21):

I'm thinking that tauto! could add prop_decidable as a local instance right from the start. Then when you're not sure why tauto failed, you can try that and move on.

view this post on Zulip Mario Carneiro (Jul 06 2018 at 07:38):

I'll forget about matching and patiently wait for rintros to land in mathlib.

Your wish is my command...

view this post on Zulip Simon Hudon (Jul 06 2018 at 07:40):

@Mario Carneiro Tag, you're it! https://github.com/leanprover/mathlib/pull/178

view this post on Zulip Patrick Massot (Jul 06 2018 at 07:42):

I love that! My next wish is you answer my Wednesday email :wink:

view this post on Zulip Patrick Massot (Jul 06 2018 at 07:42):

And I'm sure this rintro tactic will soon be all over the place.

view this post on Zulip Simon Hudon (Jul 06 2018 at 07:43):

What is this rintro thing?


Last updated: May 14 2021 at 07:19 UTC