classical.some

Stream: new members

[Anya Michaelsen]

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]

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

[Scott Morrison]

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]

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

[Anya Michaelsen]

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]

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

[Scott Morrison]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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]

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

[Kevin Buzzard]

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

[Reid Barton]

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