Zulip Chat Archive

Stream: new members

Topic: How to unfold \in


view this post on Zulip Jason Orendorff (Jun 15 2020 at 13:39):

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.

view this post on Zulip Scott Morrison (Jun 15 2020 at 13:41):

dsimp [(∈)]

view this post on Zulip Scott Morrison (Jun 15 2020 at 13:41):

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

view this post on Zulip Jason Orendorff (Jun 15 2020 at 13:43):

Thanks for both answers

view this post on Zulip Jalex Stark (Jun 15 2020 at 14:08):

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

view this post on Zulip ROCKY KAMEN-RUBIO (Jun 15 2020 at 19:02):

set.mem_set_of_eq can also be useful

view this post on Zulip Jason Orendorff (Jun 15 2020 at 19:12):

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?

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:14):

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

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:14):

which should be data.list.basic

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:15):

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

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:16):

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

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:17):

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

view this post on Zulip Jason Orendorff (Jun 15 2020 at 19:17):

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

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:19):

read about what?

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:19):

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

view this post on Zulip Jason Orendorff (Jun 15 2020 at 19:21):

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

view this post on Zulip Jason Orendorff (Jun 15 2020 at 19:22):

the language reference doesn't mention import

view this post on Zulip Jason Orendorff (Jun 15 2020 at 19:22):

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

view this post on Zulip Kevin Buzzard (Jun 15 2020 at 19:27):

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

view this post on Zulip Jalex Stark (Jun 15 2020 at 19:34):

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

view this post on Zulip Kevin Buzzard (Jun 15 2020 at 19:37):

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.

view this post on Zulip Jason Orendorff (Jun 15 2020 at 21:58):

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

view this post on Zulip Kevin Buzzard (Jun 15 2020 at 21:59):

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 ;-)

view this post on Zulip Jalex Stark (Jun 15 2020 at 22:00):

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

view this post on Zulip Jalex Stark (Jun 15 2020 at 22:00):

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

view this post on Zulip Kevin Buzzard (Jun 15 2020 at 22:01):

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

view this post on Zulip Jason Orendorff (Jun 15 2020 at 22:07):

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

view this post on Zulip Jalex Stark (Jun 15 2020 at 22:11):

you probably mean leanproject get tutorials

view this post on Zulip Jason Orendorff (Jun 16 2020 at 14:50):

yes


Last updated: May 15 2021 at 23:13 UTC