Zulip Chat Archive

Stream: maths

Topic: Working with subtypes.


view this post on Zulip Wrenna Robson (Dec 07 2020 at 22:34):

Suppose I have terms I : ideal R, hI : I.is_prime, (with R a comm_ring), and the type prime_spectrum R = {I : ideal R // I.is_prime}.

How does one go "well I clearly have a term of type prime_spectrum R, it's "I", suitably reinterpreted".

view this post on Zulip Wrenna Robson (Dec 07 2020 at 22:34):

I thought there would just be a function but I can't see it.

view this post on Zulip Wrenna Robson (Dec 07 2020 at 22:35):

Maybe this should have been in "Is there code for X?"

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:39):

For any subtype, a subtype's value is subtype.val or in your case (ps : prime_spectrum R).val.

view this post on Zulip Alex J. Best (Dec 07 2020 at 22:40):

And to go the other way ⟨I, hI⟩ is notation for a term of type {I : ideal R // I.is_prime}

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:40):

And with the concomitant proof

lemma is_prime_ps (ps : prime_spectrum R) : ps.val.is_prime := ps.property

view this post on Zulip Wrenna Robson (Dec 07 2020 at 22:40):

Alex, that's perfect I think. Thank you.

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:41):

That notation works, but only if it can be inferred that that is the exact type you need. Otherwise, you might have complaints. Sorry, I misread your initial message in the opposite direction.

view this post on Zulip Wrenna Robson (Dec 07 2020 at 22:42):

That's alright! It works for me in context.

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:42):

You might have something like

def prime_spectrum.of_is_prime {I : ideal R} (hI : I.is_prime) : prime_spectrum R := I, hI

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:43):

that way you don't even have to think about supplying the I as long as you have the associated I.is_prime hypothesis in hand.

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:44):

The "function" you asked about is docs#subtype.mk

view this post on Zulip Wrenna Robson (Dec 07 2020 at 22:44):

For which the angle-brackets are syntactic sugar?

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:50):

As far as I understand, the brackets construct or destruct, based on the context. They construct or destruct inductive types. In this case, subtype p for some p : \a \to Prop is a structure with two required records, so you provide those in the ⟨I, hI⟩ construction.

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:50):

And in the case of a destruction, you could "unwrap" a subtype p like so:

def ideal_from_prime_spectrum : prime_spectrum R -> ideal R
| I, hI := I

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:53):

Of course, you can use these brackets to make something like

(⟨rfl, rfl : and (1 = 1) (2 = 2))

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 22:59):

I find these brackets useful in places where I need to prove something about a complex statement, lets say

import tactic.default

example : ∃! (x : ),  y, x  y  x + x = x :=
begin
  refine 0, _, _⟩,
  { intro y,
    exact nat.zero_le y, rfl },
  { intros z hz,
    obtain zle, zeq := hz 0,
    exact le_antisymm zle (nat.zero_le z) },
end

view this post on Zulip Yakov Pechersky (Dec 07 2020 at 23:02):

The first refine is an example of a similar tactic step like use 0 would be, where we are piece-meal constructing the full exists_unique term. The first exact shows how one can construct an and term using the brackets. The obtain line shows how we can destruct a similar and term.

view this post on Zulip Wrenna Robson (Dec 07 2020 at 23:36):

Right! I forget about obtain.


Last updated: May 14 2021 at 20:13 UTC