Equality of structures

Stream: new members

[Patrick Stevens]

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.

[Kenny Lau]

#mwe

[Patrick Stevens]

Aargh, is this not a we

[Patrick Stevens]

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]

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]

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]

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]

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

[Patrick Stevens]

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

[Jalex Stark]

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

[Reid Barton]

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]

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

[Patrick Stevens]

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]

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]

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

[Patrick Stevens]

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]

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

[Patrick Stevens]

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

[Patrick Stevens]

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

[Patrick Stevens]

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]

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]

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]

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