## Stream: new members

### Topic: classical.some

#### Anya Michaelsen (Jul 24 2020 at 21:56):

Hi! I've been working on writing a theorem for the Chinese Remainder Theorem ring isomorphism. I already have a theorem that gives the existence of a solution to a pair of congruences and want to use that to define one of the isomorphism maps. When proving that this map and the projection are inverses for the ring isomorphism, I ran into classical.some _' in my goal and am not sure how to work with this, i.e. access the properties that it has. I looked at the docs for classical.some and classical.some_spec but since I didn't create the classical.some (it seems to have been generated by the function.inverse goal on simplification), I'm not sure how to use these. Here is a snap shot of the code:

theorem CRTwith2 (n m : ℕ) (H: coprime n m) (npos: n > 0) (mpos: m > 0)  : zmod (n*m) ≃+* zmod n × zmod m :=
begin
--define maps
use (λ x, (x, x)),
intro xy,
have CRT := CRTwith2exist xy.1.val xy.2.val n m npos mpos H,
/-theorem CRTwith2exist (a1 a2 M1 M2 : ℕ ) (M1pos : 0 < M1) (M2pos : 0 < M2) (H : coprime M1 M2) :
∃ x : ℕ , modeq M1 x a1 ∧ modeq M2 x a2 -/
choose x Hx using CRT,
use x,

-- show inverses (needs classical.some)
{
intro y,
simp,
-- Goal here: ⊢ ↑(classical.some _) = y
},
--show other proprties...
end


Clicking on 'classical.some _' in Lean Infoview yields this picture

#### Kevin Buzzard (Jul 24 2020 at 22:18):

@Anya Michaelsen can you post complete working code (i.e. include all imports)?

#### Scott Morrison (Jul 24 2020 at 23:19):

You might like the definition

/--
A convenience method for extracting the property satisfied by a term which is merely equal to
classical.some _.
-/
lemma classical.spec_of_eq_some
{α : Type*} {p : α → Prop} {a : α} {w : ∃ x, p x} (h : a = classical.some w) : p a :=
begin
subst h,
apply classical.some_spec,
end


that Johan and I recently wanted while working on sheaves, to deal with something just like this.

#### Scott Morrison (Jul 24 2020 at 23:19):

(It will eventually be PR'd to mathlib, but you can copy and paste it and use already.)

#### Anya Michaelsen (Jul 25 2020 at 00:00):

Here the full code for this file. The other version of CRTwith2exists is in a file CRT.lean (the first import)

import CRT
import data.nat.basic
import data.nat.modeq
import data.nat.gcd
import data.zmod.basic
import tactic
import data.equiv.ring
noncomputable theory

open nat nat.modeq zmod CRT

-------------------------ISOMORPHISM VERSION--------------------------

theorem CRTwith2 (n m : ℕ) (H: coprime n m) (npos: n > 0) (mpos: m > 0)  : zmod (n*m) ≃+* zmod n × zmod m :=
begin
--define maps
use (λ x, (x, x)),
intro xy,
have CRT := CRTwith2exist xy.1.val xy.2.val n m npos mpos H,
/-theorem CRTwith2exist (a1 a2 M1 M2 : ℕ ) (M1pos : 0 < M1) (M2pos : 0 < M2) (H : coprime M1 M2) :
∃ x : ℕ , modeq M1 x a1 ∧ modeq M2 x a2 -/
choose x Hx using CRT,
use x,

-- show inverses (needs classical.some)
{
intro y,
simp,
-- Goal here: ⊢ ↑(classical.some _) = y
},
--show other proprties...
end


#### Scott Morrison (Jul 25 2020 at 00:31):

Unfortunately this doesn't help us as a #mwe.

#### Scott Morrison (Jul 25 2020 at 00:32):

The point is to give us a chunk of code to copy and paste into VSCode, so we can play with it.

#### Reid Barton (Jul 25 2020 at 00:37):

This is difficult partly because you're using tactics to create data. In fact CRTwith2 should be a def, not a theorem.

#### Reid Barton (Jul 25 2020 at 00:38):

is there a way to construct ≃+* where you only give the forward map?

#### Reid Barton (Jul 25 2020 at 00:40):

this pattern (product a ring isomorphism by giving a ring map that's bijective) ought to be in the library already

#### Reid Barton (Jul 25 2020 at 00:52):

So there's docs#equiv.of_bijective and the extra fields of ring_hom only pertain to the forward map, so this should work. I suggest defining a plain equiv using equiv.of_bijective first and then extending it to a ring_hom.

#### Scott Morrison (Jul 25 2020 at 00:55):

I recently constructed a ≃+* using the antipattern { ..f, ..e}, where f was a ring_hom and e an equiv. I'd also be happy to have a named constructor for this, or to learn where it is.

#### Mario Carneiro (Jul 25 2020 at 00:59):

why is that an antipattern? It's actually doing something you can't achieve with a named constructor, namely verifying a defeq

#### Reid Barton (Jul 25 2020 at 01:12):

does it actually verify a defeq, or does it just check that the ring_hom proofs also type check against the equiv fields (or vice versa?)

#### Reid Barton (Jul 25 2020 at 01:13):

But yeah, since ring_hom only has extra Prop fields, it would make sense to have a constructor from equiv and ring_hom plus a hypothesis of =

#### Scott Morrison (Jul 25 2020 at 01:45):

Hmm, okay, I see it's not so bad.

#### Kevin Buzzard (Jul 25 2020 at 08:50):

Maybe we should switch to is_ring_hom? Oh wait...

#### Reid Barton (Jul 25 2020 at 12:21):

Well, the issue was never really is_ring_hom` existing, it was being a class

Last updated: May 14 2021 at 04:22 UTC