proving transitivity with simp

Stream: general

[Bernd Losert]

So I'm trying to prove this goal:

∀ {x : a} {l l' : filter a}, l ≤ l' → l' ≤ pure x → l ≤ pure x

When I use by simp to prove it, it get's confused and produces this goal:

∀ {x : a} {l l' : filter a}, l ≤ l' → {x} ∈ l' → {x} ∈ l

Is this unavoidable?

[Adam Topaz]

#mwe ?

[Adam Topaz]

Also, what do you expect simp to do? l' ≤ pure x simplifies to {x} ∈ l'.

[Yaël Dillies]

Apply transitivity maybe?

[Bernd Losert]

Well, when I write out the proof, it look like this:

  le_conv := begin
    assume x : a,
    assume l l' : filter a,
    assume h : l <= l',
    assume h' : l' <= pure x,
    exact le_trans h h',
  end,

[Adam Topaz]

import order.filter.basic

open filter

example {α} (F G : filter α) (x : α) (h : F ≤ G) (hh : G ≤ (pure x : filter α)) :
  F ≤ pure x :=
le_trans h hh

[Bernd Losert]

Is simp not smart enough to apply le_trans for me?

[Patrick Massot]

example {a : Type*} {x : a} {l l' : filter a} : l ≤ l' → l' ≤ pure x → l ≤ pure x :=
λ hl hl', hl.trans hl'

[Patrick Massot]

Adam was faster

[Adam Topaz]

simp is not a tactic that solves simple things. Rather it's a tactic that simplifies expressions using lemmas tagged with simp.

[Patrick Massot]

This is not at all simp's job

[Bernd Losert]

Well, I guess I'm confused about the purpose of simp.

[Adam Topaz]

In this case, it applies docs#filter.le_pure_iff

[Bernd Losert]

In some cases, it automagically works. In others, I have to write the proofs.

[Patrick Massot]

https://leanprover-community.github.io/extras/simp.html

[Adam Topaz]

Notice the @[simp] tag above the statement of the lemma.

[Patrick Massot]

Bernd, everybody goes through this stage.

[Bernd Losert]

Is there a tactic that applies le_trans for me?

[Adam Topaz]

import order.filter.basic

open filter

example {α} (F G : filter α) (x : α) (h : F ≤ G) (hh : G ≤ (pure x : filter α)) :
  F ≤ pure x :=
begin
  transitivity',
  assumption'
end

[Bernd Losert]

I would like to write a one-liner, like by le_trans or something similar.

[Adam Topaz]

Although if you look at the goals after transitivity', you will see some metavariables, so this is not an ideal solution.

[Bernd Losert]

Alright. Thanks guys. I'll stick with the long proof.

[Patrick Massot]

Note that the proof is done by tauto, but this is a coincidence depending on the precise implementation of those definitions.

[Bernd Losert]

Where is tauto? I keep getting unknown identifier 'tauto'.

[Patrick Massot]

You should import tactic to make sure you have (almost) every toy at hand.

[Bernd Losert]

For some reason, that's not working for me. Do I need to say by tauto or just tauto?

[Bernd Losert]

OK, it's by tauto.

[Patrick Massot]

Sure, you asked for a tactic, not a proof term.

[Bernd Losert]

I never know when to use by and when not to use it.

[Patrick Massot]

by enters tactic mode, it's a shorter version of begin end

[Bernd Losert]

Ah. I'll have to remember. Thanks.

[Patrick Massot]

glossary#tactic-mode

[Bernd Losert]

So there's by, {} and begin end.

[Bernd Losert]

Any more?

[Patrick Massot]

{} is grouping stuff, but it doesn't enter tactic mode.

[Bernd Losert]

Oh...

[Patrick Massot]

Writing { tauto } instead of by tauto wouldn't work

[Bernd Losert]

I guess I got confused because begin end is also used for grouping.

[Bernd Losert]

Or at least, I think it is.

[Johan Commelin]

You can use it for grouping, but it's a pretty verbose variant.