set_like idiom

Stream: general

[Patrick Massot]

In the following snippet

import group_theory.subgroup.basic

def G : add_subgroup ℤ :=
{ carrier := {n | ∃ k, n = 2*k},
  zero_mem' := sorry,
  add_mem' := sorry,
  neg_mem' := sorry }

def H : add_subgroup ℤ :=
{ carrier := {n | ∃ k, n = 4*k},
  zero_mem' := sorry,
  add_mem' := sorry,
  neg_mem' := sorry }

example : H ≤ G :=
begin
  intros x x_in,
  change ∃ k, x = 4*k at x_in,
  change ∃ k, x = 2*k,
  sorry
end

what is the idiomatic way to get to this proof state without manually writing the two change lines? Using dsimp [G, H] at * brings the awful goal

x ∈
  {carrier := {n : ℤ | ∃ (k : ℤ), n = 2 * k},
   zero_mem' := G._proof_1,
   add_mem' := G._proof_2,
   neg_mem' := G._proof_3}

[Johan Commelin]

There is a add_subgroup.mem_mk lemma missing.

[Johan Commelin]

@Patrick Massot

import group_theory.subgroup.basic

@[simp] lemma add_subgroup.mem_mk {G : Type*} [add_group G] (s : set G) (h1) (h2) (h3) (g : G) :
  g ∈ add_subgroup.mk s h1 h2 h3 ↔ g ∈ s := iff.rfl

def G : add_subgroup ℤ :=
{ carrier := {n | ∃ k, n = 2*k},
  zero_mem' := sorry,
  add_mem' := sorry,
  neg_mem' := sorry }

def H : add_subgroup ℤ :=
{ carrier := {n | ∃ k, n = 4*k},
  zero_mem' := sorry,
  add_mem' := sorry,
  neg_mem' := sorry }

example : H ≤ G :=
begin
  intros x x_in,
  squeeze_simp [H, G] at x_in ⊢,
  -- Try this: simp only [H, G, add_subgroup.mem_mk, set.mem_set_of_eq] at x_in ⊢
  sorry
end

[Patrick Massot]

@[simp, to_additive]
lemma subgroup.mem_mk {G : Type*} [group G] {s : set G} {x : G}
  (h_one : (1 : G) ∈ s) (h_mul : ∀ x y, x ∈ s → y ∈ s → x*y ∈ s) (h_inv : ∀ x ∈ s, x⁻¹ ∈ s) :
x ∈ subgroup.mk s h_one h_mul h_inv  ↔ x ∈ s :=
iff.rfl

[Patrick Massot]

I didn't dare not writing the assumptions :flushed:

[Patrick Massot]

Next question is whether this should be a more general lemma involving set_like

[Johan Commelin]

Hmm, that would be nice. But I don't know how to do that

[Patrick Massot]

@Eric Wieser

[Patrick Massot]

Unless Eric has a better idea, I'll soon PR

import group_theory.subgroup.basic

@[simp, to_additive]
lemma subgroup.mem_mk {G : Type*} [group G] {s : set G} {x : G} (h_one) (h_mul) (h_inv) :
  x ∈ subgroup.mk s h_one h_mul h_inv  ↔ x ∈ s := iff.rfl

@[simp, to_additive]
lemma subgroup.mk_le_mk {G : Type*} [group G] {s t : set G} (h_one) (h_mul) (h_inv)
  (h_one') (h_mul') (h_inv') :
subgroup.mk s h_one h_mul h_inv ≤ subgroup.mk t h_one' h_mul' h_inv'  ↔ s ⊆ t :=
by simpa [set_like.le_def]

but I'm not sure I'll have courage to PR all variations for bundled subobjects

[Eric Wieser]

There's no way to generalize I can think of

[Eric Wieser]

Does iff.rfl prove that second one?

[Patrick Massot]

Actually it does. I didn't in the beginning but I think I slightly changed the statement after trying

[Eric Wieser]

Another option would be to have separate mk_le and le_mk lemmas, which might close more goals

[Eric Wieser]

But they might also make things more awkward for other cases