intersections

Stream: general

[Patrick Massot]

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

[Patrick Massot]

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

[Sean Leather]

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.

[Simon Hudon]

does cc help?

[Patrick Massot]

no

[Patrick Massot]

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

[Reid Barton]

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

[Sean Leather]

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

[Reid Barton]

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

[Sean Leather]

true:exclamation:

[Simon Hudon]

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

Excellent, that's what I wrote it for

[Simon Hudon]

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

[Reid Barton]

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

[Reid Barton]

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

[Simon Hudon]

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.

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

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?

[Simon Hudon]

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

[Simon Hudon]

I'll take a look

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

Nice!

[Simon Hudon]

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

[Kevin Buzzard]

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

[Johan Commelin]

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

[Sean Leather]

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.

[Simon Hudon]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Simon Hudon]

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

[Patrick Massot]

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

[Patrick Massot]

I'm upgrading

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

tauto solves none of my examples

[Patrick Massot]

even with updated mathlib

[Simon Hudon]

and with ext; tauto?

[Patrick Massot]

no luck

[Patrick Massot]

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

[Simon Hudon]

Ok got it

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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!

[Simon Hudon]

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

[Simon Hudon]

@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

[Patrick Massot]

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!

[Simon Hudon]

:) At your service

[Simon Hudon]

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

[Simon Hudon]

Consider:

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

[Patrick Massot]

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.

[Patrick Massot]

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

[Patrick Massot]

failed to prove recursive application is decreasing, well founded relation

[Reid Barton]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Patrick Massot]

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.

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

I don't have any recursive function

[Patrick Massot]

I have no idea what Lean is talking about

[Simon Hudon]

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"

[Patrick Massot]

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

[Simon Hudon]

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

[Patrick Massot]

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

[Patrick Massot]

Indeed, this is what I'm proving

[Patrick Massot]

and clearing this works

[Patrick Massot]

WTF?

[Patrick Massot]

Is it because I have pattern matching?

[Patrick Massot]

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

[Patrick Massot]

Indeed

[Patrick Massot]

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

[Patrick Massot]

Do you understand what happens?

[Patrick Massot]

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

[Patrick Massot]

instead of the four lines of the previous code block

[Simon Hudon]

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

[Simon Hudon]

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

[Simon Hudon]

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

[Patrick Massot]

Thanks

[Patrick Massot]

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

[Patrick Massot]

And I'll go sleeping.

[Simon Hudon]

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

[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

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

[Simon Hudon]

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

[Simon Hudon]

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?

[Mario Carneiro]

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

[Simon Hudon]

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

[Mario Carneiro]

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

[Simon Hudon]

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

[Simon Hudon]

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.

[Mario Carneiro]

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

Your wish is my command...

[Simon Hudon]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Simon Hudon]

What is this rintro thing?