no struct

Stream: new members

[Iocta]

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]

What would you do with that statement?

[Iocta]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kyle Miller]

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]

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

[Iocta]

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]

@Kevin Buzzard Why Xis capitalized there?

[Iocta]

(is there a convention this choice conforms to?)

[Mario Carneiro]

It's a set?

[Mario Carneiro]

or at least set-ish thing

[Kevin Buzzard]

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

Real computer scientists are laughing at this

[Mario Carneiro]

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

[Mario Carneiro]

so more type theory than CS

[Kenny Lau]

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