Cartesian products agains

Stream: new members

[Andrew Lubrino]

Hi everyone. I posted a similar question about one week ago, but I took a break from Lean for a few days and missed all the responses. I'm going to post my question again with some details addressing questions on my first post. I'm using Lean mainly to learn formal logic and abstract math for the first time, so I don't want to use tactics because tactics make it hard to see what's actually happening under the hood. Below is MWE example of the problem I'm having. I think there is some issue with the types of my variables, but I can't get anything with Cartesian products to work:

import data.set
open set

-- Proof Designer Suggested Problems - 46

variables {U : Type}
variables A B C : set U

example : A × (B ∩ C) ⊆ (A × B) ∩ (A × C) :=
assume x,
assume y,
assume h₁ : (x, y) ∈ A × (B ∩ C),
have h₂ : (x, y) ∈ A ×ˢ (B ∩ C) = (x ∈ A ∧ y ∈ B ∩ C), from prod_mk_mem_set_prod_eq,
have h₃ : x ∈ A ∧ y ∈ B ∩ C, from eq.subst h₂ h₁,
have h₄ : (x, y) ∈ A ×ˢ B, from
  (have h₅ : y ∈ B, from (h₃.right).left,
  show (x, y) ∈ A ×ˢ B, from mk_mem_prod (h₃.left) h₅),
have h₅ : (x, y) ∈ A ×ˢ C, from
  (have h₆ : y ∈ C, from (h₃.right).right,
  show (x, y) ∈ A ×ˢ C, from mk_mem_prod (h₃.left) h₆),
show (x, y) ∈ (A ×ˢ B) ∩ (A ×ˢ C), from and.intro h₄ h₅

I'm getting failed to synthesize type class instance errors on my first assume. Any idea what's causing this and how I might fix it? Thanks!

[Reid Barton]

I think you want to use ×ˢ consistently--your theorem statement is about whatever × is, and it's probably causing your error

[Andrew Lubrino]

Okay, that helped. But now I'm getting an error on my assume x line type mismatch and it's basically displaying the proven goal in formal logic format rather than set theory format. What do you think is causing the issue?

import data.set
open set

-- Proof Designer Suggested Problems - 46

variables {U : Type}
variables A B C : set U

example : A ×ˢ (B ∩ C) ⊆ (A ×ˢ B) ∩ (A ×ˢ C) :=
assume x,
assume y,
assume h₁ : (x, y) ∈ A ×ˢ (B ∩ C),
have h₂ : (x, y) ∈ A ×ˢ (B ∩ C) = (x ∈ A ∧ y ∈ B ∩ C), from prod_mk_mem_set_prod_eq,
have h₃ : x ∈ A ∧ y ∈ B ∩ C, from eq.subst h₂ h₁,
have h₄ : (x, y) ∈ A ×ˢ B, from
  (have h₅ : y ∈ B, from (h₃.right).left,
  show (x, y) ∈ A ×ˢ B, from mk_mem_prod (h₃.left) h₅),
have h₅ : (x, y) ∈ A ×ˢ C, from
  (have h₆ : y ∈ C, from (h₃.right).right,
  show (x, y) ∈ A ×ˢ C, from mk_mem_prod (h₃.left) h₆),
show (x, y) ∈ (A ×ˢ B) ∩ (A ×ˢ C), from and.intro h₄ h₅

[Andrew Lubrino]

I actually just set up Lean with VSCode and put my code in there and I'm getting a different error now. unexpected token pops up on my product symbol with the small s on top.

[Reid Barton]

Yes, I assume a missing import or wrong version of mathlib

[Reid Barton]

So this:

example : A ×ˢ (B ∩ C) ⊆ (A ×ˢ B) ∩ (A ×ˢ C) :=
assume x,
assume y,
assume h₁ : (x, y) ∈ A ×ˢ (B ∩ C),
_

is already wrong. You can delete the third assume to see what the types of x and y are, they are not what you think.

[Reid Barton]

If you want to write proofs this long in term mode, you basically have to preserve the invariant that your proof type checks aside from places where you used _ to fill in for a part of the proof you haven't gotten to yet.

[Andrew Lubrino]

yep, just realized I didn't have data.set imported. Lean's telling me I don't have that in my path. I'll figure out how to download that and get it set up.

When I delete the third assume, I get that x and y are Type U. They should both be set U right?

[Reid Barton]

Also this will get a bit easier if you replace example by lemma moo, for boring technical reasons--Lean is trying to use your proof to understand the statement for some reason, and it's going to have a hard time if your proof is not correct/finished yet.

[Kevin Buzzard]

I think you'd better get your imports sorted out before we worry about any other questions. If Lean doesn't know the notation you're using then the errors you see may well be consequences of this.

but I took a break from Lean for a few days and missed all the responses.

You understand that all the responses are still there though, right? Just click on your own name and search for "view messages sent" and then click on a message to see the reponses.

[Reid Barton]

Andrew Lubrino said:

When I delete the third assume, I get that x and y are Type U. They should both be set U right?

I don't agree that that's what you get. Probably Kevin is right that something more fundamental is not working yet.

[Kevin Buzzard]

Furthermore you didn't need to start a new thread to discuss this -- it's just as easy to resurrect an old thread, and more convenient too.

[Reid Barton]

What happened to set.prod btw?

[Andrew Lubrino]

Okay, let me sort out my imports. And wow, thanks for that Kevin. Didn't realize I could look at history in this chat. I'll know for next time and make sure not to start new threads like that! sorry

[Kevin Buzzard]

Zulip is an extremely powerful chat instance. You can browse threads from years ago (and find interesting threads by searching)

[Andrew Lubrino]

got it. I'll make sure to make use of that.

[Andrew Lubrino]

okay so leanpkg is definitely installed on my machine

[Andrew Lubrino]

how should I use that to install data.set? I think that's my problem

[Kevin Buzzard]

have you opened not just a file but a Lean project folder in VS Code using the "open folder" functionality? Have you read the information at the URL contained in the error message?

[Andrew Lubrino]

yes, I created an empty folder that I created specifically for Lean files and then opened that folder in VSCode and created a new lean file from there. I also just visited the link in the error message. I'm working through those instructions now. Thanks!

[Kevin Buzzard]

yes, I created an empty folder that I created specifically for Lean files and then opened that folder in VSCode and created a new lean file from there.

Yeah, that won't work, because that's an empty folder, not a Lean project. You have to create what is called a Lean project on your computer. Instructions for doing that are here https://leanprover-community.github.io/install/project.html and instructions on how to install Lean and the community tools are here https://leanprover-community.github.io/get_started.html .

[Andrew Lubrino]

Okay, I had leanproject create a folder and I put my test.lean file in src. I tried import data.set, but still I'm getting errors. I took a look in _target/mathlib/deps/src and was able to find data/set, and I checked where Lean is looking for the files and I'm in the right spot.

[Kevin Buzzard]

Why don't you send a screenshot of your VS Code with the file explorer tab open. Here's what mine looks like:
working_project.png

[Kevin Buzzard]

And can you clarify what the errors are, and where they are (e.g. are they on imports or are we on to some new errors now?)

[Andrew Lubrino]

Here's what my screen looks like. I just have import data.set in a file and nothing else, so the only error I'm getting now is invalid import: data.set could not resolve import: data.set
image.png

[Arthur Paulino]

Did you do leanproject add-mathlib?

[Andrew Lubrino]

just tried that and got This project already depends on mathlib

[Andrew Lubrino]

also just tried leanproject get-mathlib-cache and leanpkg configure to no avail

[Arthur Paulino]

Maybe import mathlib.data.set (I'm guessing at this point)

[Alex J. Best]

In vscode you should open the directory with leanpkg.path in test it looks like you opened one directory higher in the screenshot

[Kevin Buzzard]

I think Alex is right -- you still have not opened a Lean project folder; right now you have opened a directory which contains a Lean project folder.

[Kevin Buzzard]

And the less you fiddle with typing random leanproject commands, the better! The problem is and has always been that you have not opened a Lean project folder with VS Code's open folder functionality.

[Andrew Lubrino]

that did the trick. Thanks!

[Andrew Lubrino]

also, to answer Reid's initial question the type of x is U × U and the type of y is x ∈ A ×ˢ (B ∩ C) in my below example (pasted again for reference):

import data.set

open set

-- Proof Designer Suggested Problems - 46

variables {U : Type}
variables A B C : set U

lemma moo : A ×ˢ (B ∩ C) ⊆ (A ×ˢ B) ∩ (A ×ˢ C) :=
assume x,
assume y,
--assume h₁ : (x, y) ∈ A ×ˢ (B ∩ C),
have h₂ : (x, y) ∈ A ×ˢ (B ∩ C) = (x ∈ A ∧ y ∈ B ∩ C), from prod_mk_mem_set_prod_eq,
have h₃ : x ∈ A ∧ y ∈ B ∩ C, from eq.subst h₂ h₁,
have h₄ : (x, y) ∈ A ×ˢ B, from
  (have h₅ : y ∈ B, from (h₃.right).left,
  show (x, y) ∈ A ×ˢ B, from mk_mem_prod (h₃.left) h₅),
have h₅ : (x, y) ∈ A ×ˢ C, from
  (have h₆ : y ∈ C, from (h₃.right).right,
  show (x, y) ∈ A ×ˢ C, from mk_mem_prod (h₃.left) h₆),
show (x, y) ∈ (A ×ˢ B) ∩ (A ×ˢ C), from and.intro h₄ h₅

[Andrew Lubrino]

I've tried changing the types to U and set U. I still get errors either way. Any ideas on how I can fix this?

[Andrew Lubrino]

that is, I've changed both types to U and then I changed both types to set U, they always have the same type

[Reid Barton]

The types of x and y are determined by the statement you are proving, you can't just change them.

[Andrew Lubrino]

hmmm, well the x I declared is U × U, maybe I could use that and access its members using x.fst and x.snd. I was looking at the Lean docs for prod and found some examples that use that structure.

[Kevin Buzzard]

U : Type,
A B C : set U,
x : U × U,
y : x ∈ A ×ˢ (B ∩ C)

is your context. I think that you think x and y are different to what Lean thinks they are.

Also, this proof would be much easier in tactic mode. That way you'd be able to see what you were doing instead of coding blind.

lemma moo : A ×ˢ (B ∩ C) ⊆ (A ×ˢ B) ∩ (A ×ˢ C) :=
begin
  intro x,
  intro y,
  -- realisation that x and y are not what you think they are
  have h₂ : x ∈ A ×ˢ (B ∩ C) = (x.1 ∈ A ∧ x.2 ∈ B ∩ C), from prod_mk_mem_set_prod_eq,
  -- etc etc
  sorry
end

[Reid Barton]

Andrew Lubrino said:

hmmm, well the x I declared is U × U, maybe I could use that and access its members using x.fst and x.snd.

Yes, you can. Or you can use assume ⟨x, y⟩, to introduce the argument and break it into components at the same time.

[Andrew Lubrino]

oh wow. Thanks so much for the help here. I just tried my first suggestion and that seemed to work. I'll probably use your suggestion in the future since it's more clear.

[Kevin Buzzard]

lemma moo : A ×ˢ (B ∩ C) ⊆ (A ×ˢ B) ∩ (A ×ˢ C) :=
begin
  rintro ⟨x, y⟩,
  -- x and y are now what you think they are
  have h₂ : (x, y) ∈ A ×ˢ (B ∩ C) = (x ∈ A ∧ y ∈ B ∩ C), from prod_mk_mem_set_prod_eq,
  -- etc etc
  sorry
end

[Andrew Lubrino]

yes, tactic mode is on my list next of things to do with Lean. I should really figure out the tactic mode. Thanks again for all the help with this.

[Kevin Buzzard]

#tpil does a lot of stuff in term mode before introducing it, but by the end of chapter 4 some of the proofs are getting really unwieldy, and one false move (e.g. a bracket in the wrong place) brings the house down (e.g. random sync errors at unpredictable places, leading to code which is hard to debug). I introduce my students (mathematicians, not computer scientists) to tactic mode on day 1 before I've even talked about what a term and a type are.

[Andrew Lubrino]

got it. And your students have no previous experience with formal logic? If that's the case, I'll dig into tactic mode right now. I was a little hesitant because up until now, I thought tactics = automation, which is not what I want, but if that's not the case then I'm okay with it.

[Alex J. Best]

Some tactics are heavy automation, others are really just essential ways of building terms that would be unweildy to cosntruct by hand, any long chain of rewrites (i.e. eq.subst) is really so much easier to do in tactic mode

[Andrew Lubrino]

Okay, that makes sense. I'll take a look at tpil and use the examples in there to get started. Thanks for the suggestions