Zulip Chat Archive

Stream: new members

Topic: Equality of structures


view this post on Zulip Patrick Stevens (May 23 2020 at 11:02):

I have the following:

structure small_things {A B : Type*} [partial_order B] (m : B) (f : A  B) :=
  mk :: (x : A) (pr : f x  m)

instance {A B : Type*} [partial_order B] {m : B} {f : A  B} [dec : decidable_eq A] : decidable_eq (small_things m f) :=
begin
  intros r s,
  rcases r with  r , pr_r ,
  rcases s with  s , pr_s ,
  cases dec r s,
  { left,
    intros eq,
    apply h,
    sorry
  },
  { right,
    subst h, },
end

At the sorry, I have eq saying that my two inputs r and s of type small_things are equal. From this, I need to derive that r.x and s.x are equal. How can I do that? Aesthetically I would prefer not to assume anything classical, if that's an option.

view this post on Zulip Kenny Lau (May 23 2020 at 11:05):

#mwe

view this post on Zulip Patrick Stevens (May 23 2020 at 11:06):

Aargh, is this not a we

view this post on Zulip Patrick Stevens (May 23 2020 at 11:08):

I assert that it is at least working; it fails to be minimal in that I could have truncated the f x <= m to e.g. True, I suppose

view this post on Zulip Patrick Stevens (May 23 2020 at 11:09):

structure small_things {A : Type*} :=
  mk :: (x : A) (pr : tt)

instance {A : Type*} [dec : decidable_eq A] : decidable_eq small_things :=
begin
  intros r s,
  rcases r with  r , pr_r ,
  rcases s with  s , pr_s ,
  cases dec r s,
  { left,
    intros eq,
    apply h,
    sorry
  },
  { right,
    subst h, },
end

view this post on Zulip Kenny Lau (May 23 2020 at 11:11):

here's one way to approach things:

import tactic

universes u v

variables {A : Type u} {B : Type v} [partial_order B] (m : B) (f : A  B)

structure small_things :=
(x : A)
(pr : f x  m)

variables {m f}

namespace small_things

@[ext] lemma ext {r s : small_things m f} (H : r.x = s.x) : r = s :=
by { cases r, cases s, congr' 1, exact H }

lemma ext_iff {r s : small_things m f} : r = s  r.x = s.x :=
congr_arg x, ext

instance {A B : Type*} [partial_order B] {m : B} {f : A  B} [decidable_eq A] : decidable_eq (small_things m f) :=
λ r s, decidable_of_decidable_of_iff (by apply_instance) ext_iff.symm

end small_things

view this post on Zulip Kenny Lau (May 23 2020 at 11:11):

but here's a more efficient way:

universes u v

variables {A : Type u} {B : Type v} [partial_order B] (m : B) (f : A  B)

def small_things :=
{ x // f x  m }

variables {m f}

namespace small_things

instance {A B : Type*} [partial_order B] {m : B} {f : A  B} [decidable_eq A] : decidable_eq (small_things m f) :=
subtype.decidable_eq

end small_things

view this post on Zulip Kenny Lau (May 23 2020 at 11:12):

the point of the first way is to show you how to extract lemmas

view this post on Zulip Patrick Stevens (May 23 2020 at 11:16):

Thanks - the refinement version solves my actual XY much better too

view this post on Zulip Jalex Stark (May 23 2020 at 14:54):

@Patrick Stevens do you understand why your example was not a (m)we?

view this post on Zulip Reid Barton (May 23 2020 at 15:02):

I think people could relax a bit about this whole #mwe thing. It's literally less effort to notice the error on rcases and add import tactic than it is to have this conversation.

view this post on Zulip Reid Barton (May 23 2020 at 15:02):

Some of the recent conversations with genuinely new users have not seemed very welcoming to me.

view this post on Zulip Patrick Stevens (May 23 2020 at 15:25):

Sigh - I copy-pasted my example to the top of the file I was working on to check, but it didn't occur to me that tactics were imported

view this post on Zulip Jalex Stark (May 23 2020 at 16:04):

Yeah, probably the most efficient path forward in an example like this is exactly what Kenny did, post a working version and then answer the question

view this post on Zulip Jalex Stark (May 23 2020 at 16:05):

I agree I've been pretty aggressive towards some newcomers, and I should practice more patience / empathy

view this post on Zulip Patrick Stevens (May 23 2020 at 16:08):

In fairness, now I know that I literally have to use a completely new file to verify that an example works, I can do that

view this post on Zulip Jalex Stark (May 23 2020 at 16:09):

Any ideas on how to make the #mwe page convey that idea more effectively?

view this post on Zulip Patrick Stevens (May 23 2020 at 16:10):

The problem wasn't a lack of knowledge, in that sense - it was a broken model of Lean

view this post on Zulip Patrick Stevens (May 23 2020 at 16:10):

I'm entirely aware of the value of a mwe, I just thought my shortcut was a valid one for producing them

view this post on Zulip Patrick Stevens (May 23 2020 at 16:12):

The MWE page does already say "you should test this", I was simply lazy because I couldn't imagine the imports making a difference - which is obvious nonsense when stated

view this post on Zulip Jalex Stark (May 23 2020 at 16:13):

Mm sense. I guess we're at the point where we've laid out a useful reference material, and it serves as only part of the teaching strategy

view this post on Zulip Jalex Stark (May 23 2020 at 16:13):

After all, we do much more in an algebra 1 course than tell people to read the first third of dummit and Foote

view this post on Zulip Mario Carneiro (May 23 2020 at 19:44):

Reid Barton said:

I think people could relax a bit about this whole #mwe thing. It's literally less effort to notice the error on rcases and add import tactic than it is to have this conversation.

I usually try to have both conversations in parallel


Last updated: May 09 2021 at 19:11 UTC