## Stream: maths

### Topic: Working with subtypes.

#### 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".

#### Wrenna Robson (Dec 07 2020 at 22:34):

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

#### Wrenna Robson (Dec 07 2020 at 22:35):

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

#### 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.

#### 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}

#### 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


#### Wrenna Robson (Dec 07 2020 at 22:40):

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

#### 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.

#### Wrenna Robson (Dec 07 2020 at 22:42):

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

#### 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⟩


#### 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.

#### Yakov Pechersky (Dec 07 2020 at 22:44):

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

#### Wrenna Robson (Dec 07 2020 at 22:44):

For which the angle-brackets are syntactic sugar?

#### 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.

#### 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


#### 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))


#### 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


#### 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.

#### Wrenna Robson (Dec 07 2020 at 23:36):

Right! I forget about obtain.

Last updated: May 14 2021 at 20:13 UTC