How to use mem_set_of_eq with ¬A

Stream: new members

[Michael Palm]

I am trying to prove {x | A x} = compl {x | ¬A x} without matlib (core library only). However I am not capable of using mem_set_of_eq correctly in conjunction with ¬A and the rewrite tactic. I appreciate any help.

Since the definitions of compl et al have been removed from the core library in the last commit (I don't know, if by accident or intent), I have to implement my own. Also, I like to implement the extensionality axiom by myself:

open set

constant Ω : Type

notation `Pred` := Ω → Prop
notation `Set` := set Ω

variables A B C : Pred
variables X Y Z : Set
variables x y z : Ω

axiom not.not_iff {A : Prop} : ¬¬A ↔ A
axiom set_eq.intro {X Y : Set} : (∀z, z ∈ X ↔ z ∈ Y) → X = Y
axiom set_eq.elim {X Y : Set} : X = Y → (∀z, z ∈ X ↔ z ∈ Y)

def compl (X : Set) : Set := {z | z ∉ X}


theorem t₁ {A : Pred} : {y | A y} = compl {y | ¬A y} :=
begin
  suffices : ∀x, x∈{y | A y} ↔ x ∈ compl {y | ¬A y},
  show {y | A y} = compl {y | ¬A y}, from set_eq.intro this,

  show ∀x, x∈{y | A y} ↔ x ∈ compl {y | ¬A y}, from
  begin
    assume x : Ω,
    show x∈{y | A y} ↔ x ∈ compl {y | ¬A y}, from calc
      x∈{y | A y} ↔   A x                       : by refl
              ... ↔ ¬¬A x                       : by rw not.not_iff
              ... ↔ x ∈ {z | ¬¬A z}             : by rw mem_set_of_eq
              ... ↔ x ∈ {z | ¬(z ∈ {y | ¬A y})} : by rw ←@mem_set_of_eq Ω _ (not ∘ A) -- this does not work!
              ... ↔ x ∈ {z | z ∉ {y | ¬A y}}    : by assumption
              ... ↔ x ∈ compl {y | ¬A y}        : by assumption
  end,
end

I have no idea, how to correctly call mem_set_of_eq. I tried
rw ←@mem_set_of_eq Ω _ (¬A)
rw ←@mem_set_of_eq Ω _ (λ x : Ω, ¬A x)
rw ←@mem_set_of_eq Ω _ (not ∘ A)
and all different kinds of other approaches.
(not ∘ A) at least has the correct type. But it says that it cannot find an instance of the pattern (not ∘ A) ?m_1.

Any help is appreciated.

[Kevin Buzzard]

by refl works fine.

[Kevin Buzzard]

rw works up to syntactic equality not definitional equality, so it can't see through things like ∘.

[Kevin Buzzard]

Many other tactics work up to definitional equality (for example example : Pred = Set := rfl works fine) but for rewrite you need a syntactic match.

[Kevin Buzzard]

    show x∈{y | A y} ↔ x ∈ compl {y | ¬A y}, from calc
      x∈{y | A y} ↔   A x                       : by refl
              ... ↔ ¬¬A x                       : by rw not.not_iff
              ... ↔ x ∈ compl {y | ¬A y}        : by refl

[Michael Palm]

@Kevin Buzzard Thank you for your answer and the great content you provide. I have read your explanations on the different kinds of equality here. However I would like to explicitly state all the syntactic transformations which are necessary in the proof. How can I do that?
Using refl hides the necessary syntactic transformations.

[Riccardo Brasca]

You can add a lemma (whose proof is rfl) saying x∈{y | A y} ↔ A x, and then rewrite that.

[Alex J. Best]

In mathlib there is docs#set.mem_set_of

[Michael Palm]

@Riccardo Brasca @Alex J. Best I am trying to use mem_set_of_eq from the core lib (Line 24), which seems to be exactly what you propose? But I keep failing using it.

[Riccardo Brasca]

Just a tip: you can write docs#set.mem_set_of_eq (docs # set.mem_set_of_eq without spaces) and you get a link to the lemma you want.

[Riccardo Brasca]

In docs#set.mem_set_of_eq there is = instead of ↔, maybe that's the problem.

[Riccardo Brasca]

You can try to use docs#eq.to_iff, that is also in core.

[Alex J. Best]

Here's one way to do it with conv:

open set


constant Ω : Type

notation `Pred` := Ω → Prop
notation `Set` := set Ω

variables A B C : Pred
variables X Y Z : Set
variables x y z : Ω

axiom not.not_iff {A : Prop} : ¬¬A ↔ A
axiom set_eq.intro {X Y : Set} : (∀z, z ∈ X ↔ z ∈ Y) → X = Y
axiom set_eq.elim {X Y : Set} : X = Y → (∀z, z ∈ X ↔ z ∈ Y)

def compl (X : Set) : Set := {z | z ∉ X}


theorem t₁ {A : Pred} : {y | A y} = compl {y | ¬A y} :=
begin
  suffices : ∀x, x∈{y | A y} ↔ x ∈ compl {y | ¬A y},
  show {y | A y} = compl {y | ¬A y}, from set_eq.intro this,

  show ∀x, x∈{y | A y} ↔ x ∈ compl {y | ¬A y}, from
  begin
    assume x : Ω,
    show x∈{y | A y} ↔ x ∈ compl {y | ¬A y}, from calc
      x∈{y | A y} ↔   A x                       : by refl
              ... ↔ ¬¬A x                       : by rw not.not_iff
              ... ↔ x ∈ {z | ¬¬A z}             : by rw mem_set_of_eq
              ... ↔ x ∈ {z | ¬(z ∈ {y | ¬A y})} : by conv in (¬ _ ∈ _) { rw mem_set_of_eq } -- this does not work!
              ... ↔ x ∈ compl {y | ¬A y}        : by refl
  end,
end

[Michael Palm]

@Alex J. Best This is nice. Thank you. This is very helpful. I have not known conv before. But why is that necessary? What is the p : Ω → Prop that mem_set_of_eq has inferred here? ¬A and ¬A _ obviously do not work.

[Alex J. Best]

The issue isn't that rw isn't inferring the right argument (as you saw you could force the arguments with the @ symbol), it is because rewrite doesn't work "under binders", for example:

import tactic
example : (λ x : ℕ, x + 1) = λ x : ℕ, 1 + x :=
begin
  rw add_comm, --fails
end

here there are a few ways around the issue

import tactic

lemma a : (λ x : ℕ, x + 1) = λ x : ℕ, 1 + x :=
begin
  ext,
  rw add_comm,
end


lemma b : (λ x : ℕ, x + 1) = λ x : ℕ, 1 + x :=
begin
  conv in (_ + _) { rw add_comm, }
end
#print b

lemma c : (λ x : ℕ, x + 1) = λ x : ℕ, 1 + x :=
begin
  simp [add_comm],
end

[Alex J. Best]

Using simp with the right arguments would probably also work in your case too

[Alex J. Best]

We also have a nice doc page on conv mode if you havent seen it already: https://leanprover-community.github.io/extras/conv.html

[Michael Palm]

Thanks! That's exactly the piece of information I needed!

[Matt Diamond]

@Michael Palm not sure if someone mentioned this already but you can also use simp_rw, which acts like rw except it can work under binders

[Alberto Navarro Garmendia]

Hello! I have an Apple M1 laptop and I am trying to install LEAN following the instructions of https://leanprover-community.github.io/install/macos.html

Unfortunately, I made the mistake of first trying the Intel instructions :face_palm:
When I tryed to follow the M1 instructions it gets stucked at point 3. Can someone help?

More info, following the instructions just mean copy-paste in the terminal window all commands from the instructions. I do not know what they actually mean. More concretely:

1.1) I copy-paste at the terminal "xcode-select --install" at terminal. It says "error: tools are already installed"
1.2) I copy-paste at the terminal "softwareupdate --install-rosetta", agree, and then the console says "install of Rosetta 2 finished succesfully"
2.1) I copy-paste at the terminal "arch -x86_64 zsh", it doesn't say anything at all
3.1) I copy-paste at the terminal " /bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/Homebrew/install/HEAD/install.sh)" "
3.1.1) I introduce at the terminal my administrator password. The terminal says "this script will install blablabla... please RETURN/ENTER to continuo or any other key to abort"
3.1.2) I press RETURN
3.1.3) The terminal does its thing for a while (says "Downloading and installing Homebrew... blablabla..." and then gets stucked while showing
"error: Not a valid ref: refs/remotes/origin/master
fatal: ambiguous argument 'refs/remotes/origin/master': unknown revision or path not in the working tree.
Use '--' to separate paths from revisions, like this:
'git <command> [<revision>...] -- [<file>...]'
"

Any help?

[Alberto Navarro Garmendia]

Wait, the problem was myself for not waiting enough. It now says "Installation successful"

4.1) I copy paste at the terminal
" /usr/local/bin/brew install elan-init mathlibtools
elan toolchain install stable
elan default stable "
the terminal answers
"Running brew update --auto-update...
fatal: Could not resolve HEAD to a revision
Warning: No available formula with the name "elan-init".
==> Searching for similarly named formulae...
Error: No similarly named formulae found.
==> Searching for a previously deleted formula (in the last month)...
Error: No previously deleted formula found.
==> Searching taps on GitHub...
Error: No formulae found in taps.
zsh: command not found: elan
zsh: command not found: elan
"
4.2) I copy paste only the first line. It returns
"Warning: No available formula with the name "elan-init".
==> Searching for similarly named formulae...
Error: No similarly named formulae found.
==> Searching for a previously deleted formula (in the last month)...
Error: No previously deleted formula found.
==> Searching taps on GitHub...
Error: No formulae found in taps."

4.2) I copy paste the second line "elan toolchain install stable". The terminal does nothing

4.3) I copy paste the third line "elan default stable " it returns, "zsh: command not found: elan"

I think this is broken now. In any case I continue

5) I copy paste "brew install --cask visual-studio-code && code --install-extension jroesch.lean". It returns

"==> Downloading https://update.code.visualstudio.com/1.71.0/darwin/stable
==> Downloading from https://az764295.vo.msecnd.net/stable/784b0177c56c607789f96
######################################################################## 100.0%
==> Installing Cask visual-studio-code
==> Moving App 'Visual Studio Code.app' to '/Applications/Visual Studio Code.app
==> Linking Binary 'code' to '/usr/local/bin/code'
:beer: visual-studio-code was successfully installed!
Installing extensions...
Installing extension 'jroesch.lean'...
(node:18998) [DEP0005] DeprecationWarning: Buffer() is deprecated due to security and usability issues. Please use the Buffer.alloc(), Buffer.allocUnsafe(), or Buffer.from() methods instead.
(Use Electron --trace-deprecation ... to show where the warning was created)
Extension 'jroesch.lean' v0.16.54 was successfully installed."

Am I finished? Is it correctly installed?
I don't think so. I dont find LEAN anywhere in my laptop

[Wrenna Robson]

Matt Diamond said:

Michael Palm not sure if someone mentioned this already but you can also use simp_rw, which acts like rw except it can work under binders

Though simp_rw has the occasionally undesirable (though mostly desirable) behaviour that it will repeat things until they stabilize, which rw won't do. Which occasionally leaves one in an odd position.

[Eric Wieser]

simp only [lemma] {single_pass := tt} avoids that

[Wrenna Robson]

Oh that's cool, didn't know that was a thing.

[Wrenna Robson]

What is the difference between simp_rw and simp only?

[Kevin Buzzard]

nobody knows :-) I think sometimes one works and the other doesn't? They both in theory do the same thing. Chris Hughes once told me that he didn't understand why simp_rw was even added to mathlib, given that simp only was already there.

[Eric Wieser]

The former is implemented in terms of the latter

[Matt Diamond]

Weird... the docs say:

For example, neither simp nor rw can solve the following, but simp_rw can:

example {α β : Type} {f : α → β} {t : set β} :
  (∀ s, f '' s ⊆ t) = ∀ s : set α, ∀ x ∈ s, x ∈ f ⁻¹' t :=
by simp_rw [set.image_subset_iff, set.subset_def]

But if you replace simp_rw with simp, it still works fine. Maybe simp used to be weaker?

[Matt Diamond]

well, this is the PR where it was added (and it has a Zulip link for context), so if anyone's actually curious, the answer is here: https://github.com/leanprover-community/mathlib/pull/1900

[Matt Diamond]

@Kevin Buzzard you were there when @Anne Baanen came up with it! "nobody knows :-)" lol

[Matt Diamond]

in your defense it was 2.5 years ago

[Wrenna Robson]

simp_rw actually has the advantage that it does its re-writes in order and you can click midway through to see how far it gets (like rw). That is something I do find useful sometimes, to work out how a simplification is happening.