## Stream: new members

### Topic: Equality of structures

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

#mwe

#### Patrick Stevens (May 23 2020 at 11:06):

Aargh, is this not a we

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

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


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


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


#### Kenny Lau (May 23 2020 at 11:12):

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

#### Patrick Stevens (May 23 2020 at 11:16):

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

#### Jalex Stark (May 23 2020 at 14:54):

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

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

#### Reid Barton (May 23 2020 at 15:02):

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

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

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

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

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

#### Jalex Stark (May 23 2020 at 16:09):

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

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

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

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

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

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

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