Zulip Chat Archive

Stream: new members

Topic: no struct


view this post on Zulip 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"?

view this post on Zulip Yakov Pechersky (Aug 18 2020 at 20:44):

What would you do with that statement?

view this post on Zulip Iocta (Aug 18 2020 at 20:50):

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

view this post on Zulip Kevin Buzzard (Aug 18 2020 at 20:51):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip Iocta (Aug 18 2020 at 21:49):

@Kevin Buzzard Why Xis capitalized there?

view this post on Zulip Iocta (Aug 18 2020 at 21:50):

(is there a convention this choice conforms to?)

view this post on Zulip Mario Carneiro (Aug 18 2020 at 22:07):

It's a set?

view this post on Zulip Mario Carneiro (Aug 18 2020 at 22:08):

or at least set-ish thing

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Aug 18 2020 at 22:16):

Real computer scientists are laughing at this

view this post on Zulip Mario Carneiro (Aug 18 2020 at 22:17):

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

view this post on Zulip Mario Carneiro (Aug 18 2020 at 22:17):

so more type theory than CS

view this post on Zulip 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