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