set

Stream: new members

[tica]

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]

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]

variable T : Type

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

should work fine

[tica]

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]

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]

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

[tica]

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]

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]

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]

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]

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]

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]

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

[tica]

@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]

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]

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]

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]

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]

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]

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]

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

[Kyle Miller]

Oops, that should be set (set Point)

[tica]

@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]

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

[tica]

@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