Zulip Chat Archive

Stream: new members

Topic: classical.some


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

view this post on Zulip Kevin Buzzard (Jul 24 2020 at 22:18):

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

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

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

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

view this post on Zulip Scott Morrison (Jul 25 2020 at 00:31):

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

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

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

view this post on Zulip Reid Barton (Jul 25 2020 at 00:38):

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

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

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

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

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

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

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

view this post on Zulip Scott Morrison (Jul 25 2020 at 01:45):

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

view this post on Zulip Kevin Buzzard (Jul 25 2020 at 08:50):

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

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