Zulip Chat Archive

Stream: new members

Topic: set


tica (Mar 09 2023 at 08:59):

Hello,

I am trying to work on sets, how do I do that?

constant T : Type
constant S_T : set T
instance : has_mem T S_T := λ t s_t, t  s_t -- <--

variables (t : T) (s_t : S_T)
#check t  s_t

Thanks

Alex J. Best (Mar 09 2023 at 09:00):

You likely want to use variable ins place of constant, and there should already be a has_mem instance so there shouldn't be a need to define another one in the same way

Alex J. Best (Mar 09 2023 at 09:01):

variable T : Type

variables (t : T) (s_t : set T)
#check t  s_t

should work fine

tica (Mar 09 2023 at 09:20):

What is the difference between using a constant and a variable in this case?
I don't understand why it works with a variable but not a constant

tica (Mar 09 2023 at 09:24):

It doesn't work

variable T : Type
variable S_T : set T
variables (t : T) (s_t : set T)
#check t  S_T

axiom test (t' : T) (s_t' : S_T) : t'  s_t' -- <-

Reid Barton (Mar 09 2023 at 09:25):

What are you trying to accomplish by writing variable S_T : set T, and having both S_T and s_t?

tica (Mar 09 2023 at 09:46):

constant Point : Type
constant Plane :set Point

axiom existence_of_two_points (P : Plane):  p1 p2 : Point, p1  p2  p1  P  p2  P

constant Line : set Point
axiom incidence (a b : Point): ∃! l : Line, a  l  b  l

Kevin Buzzard (Mar 09 2023 at 09:49):

There is another active thread here (search for @Quinn Culver ) where it is explained how to avoid constants and axioms (which we try to avoid) when setting this sort of thing up.

tica (Mar 09 2023 at 11:22):

I suppose you mean this topic https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/.E2.9C.94.20declare.20unique.20constants

What is the difference between a variable and a constant?

variable T : Type
constant T : Type

Reid Barton (Mar 09 2023 at 11:32):

A variable is just an additional argument to following definitions/theorems.

A constant is something that you are postulating to exist globally. 99% of the time, it doesn't make sense to do this unless you are adding exotic set theory axioms or something.

Reid Barton (Mar 09 2023 at 11:33):

Or if you had a theorem that you didn't know how to prove but wanted to assume it was true anyways, you could add it as a constant (or axiom).

tica (Mar 09 2023 at 13:03):

Ok thanks.
So I rewrote it like that.

variables (Point : Type)

structure Plane : Type :=
(points : set Point)
(existance_of_two_points :  a b : Point, a  b  a  points  b  points)

structure Line : Type :=
(points : set Point)
--(incidence (a b : Point) : ∃! l : Line, a ∈ l.points ∧ b ∈ l.points)
(incidence (a b : Point) (L L': Line) : a  L  b  L  a  L'  b  L'  L = L')

How to use the Line structure in the Line structure?
I think it's not possible because it's not defined yet, how do you do it then?

Eric Wieser (Mar 09 2023 at 15:14):

If you're adding fields to a structure containing "axioms" about equality of that structure itself, you might want a quotient type

tica (Mar 09 2023 at 15:19):

@Eric Wieser It's not that I want to but I was told above to use a structure instead of an axiom.
Would you do this differently than with a structure?

Eric Wieser (Mar 09 2023 at 15:23):

So

structure pre_line :=
(points : set Point)

instance pre_line_setoid : setoid (pre_line Point) :=
{ r := λ L L',  (a b : Point), a  L  b  L  a  L'  b  L', -- your condition here
  eqv := sorry }

def line := quotient (pre_line_setoid Point)

Eric Wieser (Mar 09 2023 at 15:27):

But I think your condition is wrong; it allows the "line" consisting of every point, and therefore says that every line is equal to every other line

Floris van Doorn (Mar 09 2023 at 15:29):

You want to define a structure that contains Line and Point types as arguments, and has some additional axioms for these two types.
We had a very similar discussion recently about the Desarguesian plane, I'd look there for some ideas on how to write this down.

Kyle Miller (Mar 09 2023 at 15:33):

I'm not sure quotient is capturing the right thing here, since incidence is supposed to be part of the conditions of what constitutes a plane.

Kyle Miller (Mar 09 2023 at 15:33):

Here's a suggestion in the context of what's been discussed here, but be sure to check out the discussion Floris linked to.

structure Plane (Point : Type) : Type :=
(lines : set (set Point))
(existence_of_two_points :  a b : Point, a  b)
(incidence (a b : Point) (L L'  lines) : a  b  a  L  b  L  a  L'  b  L'  L = L')

Kyle Miller (Mar 09 2023 at 15:34):

I made a slight change where Point is the type of points in its entirety -- there's usually no need to have a set Point since you can use subtype (for example, if s : set nat you can write Plane s and s will be coerced to a type)

Eric Wieser (Mar 09 2023 at 15:43):

That doesn't typecheck, @Kyle Miller; it tries to talk about membership of one point in another

Kyle Miller (Mar 09 2023 at 15:46):

Oops, that should be set (set Point)

tica (Mar 09 2023 at 15:49):

@Eric Wieser
I use the book: https://www.amazon.com/Foundations-Geometry-2nd-Gerard-Venema/dp/0136020585
This is how a line is described (as I understand it)
The code does not compile.
I tried to add the instance has_mem without success.

variables (Point : Type)

structure pre_line :=
(points : set Point)

instance : has_mem Point (pre_line) := λ p L, p  L

instance pre_line_setoid : setoid (pre_line Point) :=
{ r := λ L L',  (a b : Point), a  L  b  L  a  L'  b  L', -- your condition here
  iseqv := sorry }

def line := quotient (pre_line_setoid Point)

tica (Mar 09 2023 at 15:50):

@Floris van Doorn I'll take a look, thanks

tica (Mar 09 2023 at 16:03):

@Kyle Miller I am not sure I understand how to use your solution.
I did this (I still have the problem with has_mem)

structure Plane (Point : Type) : Type :=
(lines : set (set Point))
(existence_of_two_points :  a b : Point, a  b)
(incidence (a b : Point) (L L'  lines) : a  b  a  L  b  L  a  L'  b  L'  L = L')

def lies_on {T : Type}{P : Plane T} (point : T) (line  P.lines) : Prop :=
point  line

def external {T : Type}{P : Plane T} (point : T) (line  P.lines) : Prop := point  line

def parallel {T : Type}{P : Plane T} (line1 line2  P.lines) :=
¬∃ point : T, lies_on point line1  lies_on point line2

Last updated: Dec 20 2023 at 11:08 UTC