How to unfold \in

Stream: new members

[Jason Orendorff]

I'm trying to prove this:

theorem mem_filter {α} {pred : α → Prop} [decidable_pred pred] {xs : list α} {x : α}
  (hmem : x ∈ xs.filter pred)
: x ∈ xs ∧ pred x := sorry

I don't know which tactic to use to break open the ∈ propositions.

[Scott Morrison]

dsimp [(∈)]

[Scott Morrison]

but almost certainly this isn't actually what you want to do

[Jason Orendorff]

Thanks for both answers

[Jalex Stark]

the theorem is called list.mem_filter and it is a simp lemma. I found it like this:

theorem mem_filter {α} {pred : α → Prop} [decidable_pred pred] {xs : list α} {x : α}
  (hmem : x ∈ xs.filter pred)
: x ∈ xs ∧ pred x := begin
  squeeze_simp at hmem,
end

[ROCKY KAMEN-RUBIO]

set.mem_set_of_eq can also be useful

[Jason Orendorff]

Thanks. The output I get from this

import tactic.squeeze
import tactic.basic

theorem mem_filter {α} {pred : α → Prop} [decidable_pred pred] {xs : list α} {x : α}
  (hmem : x ∈ xs.filter pred)
: x ∈ xs ∧ pred x := begin
  squeeze_simp at hmem,
end

is "simplify tactic failed to simplify". Do I need something else?

[Jalex Stark]

sorry for not including my imports. You'll need whatever file list.mem_filter is defined in, since it's only added to simp once it's defined

[Jalex Stark]

which should be data.list.basic

[Jalex Stark]

so this works:

import tactic

theorem mem_filter {α} {pred : α → Prop} [decidable_pred pred] {xs : list α} {x : α}
  (hmem : x ∈ xs.filter pred)
: x ∈ xs ∧ pred x := begin
  squeeze_simp at hmem,
end

[Jalex Stark]

and so does this

import tactic.basic
import data.list.basic

theorem mem_filter {α} {pred : α → Prop} [decidable_pred pred] {xs : list α} {x : α}
  (hmem : x ∈ xs.filter pred)
: x ∈ xs ∧ pred x := begin
  squeeze_simp at hmem,
end

[Jalex Stark]

I personally always work with import tactic, rather than importing only the tactics I need; I think there's no downside to this unless you're working on contributions to mathlib, where you have to be more aware of the dependency graph

[Jason Orendorff]

ok. thanks again! is there somewhere i can read about this?

[Jalex Stark]

read about what?

[Jalex Stark]

the docs page for data.list.basic? https://leanprover-community.github.io/mathlib_docs/data/list/basic.html

[Jason Orendorff]

i meant, what should I have read, to know that import tactic exists!

[Jason Orendorff]

the language reference doesn't mention import

[Jason Orendorff]

—that I could see, I didn't read the whole thing

[Kevin Buzzard]

This is one of the things you pick up on the chat :-)

[Jalex Stark]

did you do any tutorials? there should be lots of files in the tutorials that start with import tactic?

[Kevin Buzzard]

Whether or not import tactic is useful to you is very much subject-dependent. There are people here who are writing little implementations of theories who don't need any tactics at all other than those in core; there are people who actively don't want to import mathlib; there are undergraduate mathematicians who are just completely lost without ring and linarith and are encouraged by me to switch on classical logic and import all tactics on line 1.

[Jason Orendorff]

So far I've just read _Theorem Proving In Lean_, worked its examples, and done the Natural Numbers Game, dipped into the reference manual, and noodled around in lean/library/init a bit

[Kevin Buzzard]

Well the next step is to think of some formalisation project and to get going :-) I did 50 1st year maths undergraduate level questions next (which happened to be the 50 questions I was setting my own undergraduates), got stuck 40 times and asked here ;-)

[Jalex Stark]

if you want more reading, Mathematics in lean #mil probably has things interesting to you

[Jalex Stark]

reading the archives on zulip is also pretty effective, you can pick up "folklore
knowledge" that hasn't made its way into polished tutorials

[Kevin Buzzard]

Given that Patrick, Jeremy and I are all rapidly approaching the end of term/semester, hopefully MIL will have even more interesting things soon.

[Jason Orendorff]

yeah, MIL is next for me, but leanprover get tutorials also beckons

[Jalex Stark]

you probably mean leanproject get tutorials

[Jason Orendorff]

yes