## Stream: new members

### Topic: no struct

#### Iocta (Aug 18 2020 at 20:37):

structure positive_nats :=
(s : set ℕ)
(positive : ∀ n ∈ s, n > 0)

def zero_singleton : set ℕ := {0}


How do I say "you can't instantiate positive_nats with zero_singleton"?

#### Yakov Pechersky (Aug 18 2020 at 20:44):

What would you do with that statement?

#### Iocta (Aug 18 2020 at 20:50):

It provides a counterexample to "any set nat can be a positive_nats."

#### Kevin Buzzard (Aug 18 2020 at 20:51):

example : ¬ (∃ X : positive_nats, X.s = zero_singleton) := sorry


#### Kevin Buzzard (Aug 18 2020 at 20:54):

PS you should write 0 < n not n > 0; all the lemmas use < so it makes life easier.

#### Kyle Miller (Aug 18 2020 at 20:55):

structure positive_nats :=
(s : set ℕ)
(positive : ∀ n ∈ s, 0 < n)

def zero_singleton : set ℕ := {0}

example (X : positive_nats) : X.s ≠ zero_singleton :=
begin
intro h,
have hz : 0 ∈ X.s, rw h, dunfold zero_singleton, simp,
have hpos := X.positive 0 hz,
linarith,
end


#### Kevin Buzzard (Aug 18 2020 at 21:00):

example (X : positive_nats) : X.s ≠ zero_singleton :=
λ h, lt_irrefl 0 $X.positive 0$ h.symm ▸ set.mem_singleton 0


#### Iocta (Aug 18 2020 at 21:08):

lemma no_positive_nats_zero_singleton (X : positive_nats) : X.s ≠ zero_singleton :=
λ h, lt_irrefl 0 $X.positive 0$ h.symm ▸ set.mem_singleton 0

example : ¬ (∀ nats: set ℕ,  ∃ (X: positive_nats), X.s = nats ) :=
begin
intro h,
specialize h zero_singleton,
cases h with pn hpn,
apply no_positive_nats_zero_singleton pn hpn,
end


#### Iocta (Aug 18 2020 at 21:49):

@Kevin Buzzard Why Xis capitalized there?

#### Iocta (Aug 18 2020 at 21:50):

(is there a convention this choice conforms to?)

It's a set?

#### Mario Carneiro (Aug 18 2020 at 22:08):

or at least set-ish thing

#### Kevin Buzzard (Aug 18 2020 at 22:15):

@Iocta you made the structure so you make the conventions. We call groups G, abelian groups A, monoids M, topological spaces X, etc. But you didn't name any instances of your structure so I made a convention for you, that's all. If a computer scientist had got to it first they would probably have called it \alpha, which is their version of X.

#### Mario Carneiro (Aug 18 2020 at 22:16):

Real computer scientists are laughing at this

#### Mario Carneiro (Aug 18 2020 at 22:17):

Actually I think the \alpha naming convention goes back to polymorphic type systems like system F

#### Mario Carneiro (Aug 18 2020 at 22:17):

so more type theory than CS

#### Kenny Lau (Aug 19 2020 at 06:35):

import tactic

structure positive_nats :=
(s : set ℕ)
(positive : ∀ n ∈ s, 0 < n)

def zero_singleton : set ℕ := {0}

example : ∀ X : positive_nats, X.s ≠ zero_singleton
| ⟨_, h⟩ rfl := by cases h 0 rfl


Last updated: May 11 2021 at 00:31 UTC