convert_struct?

Stream: general

[Yury G. Kudryashov]

How hard would it be to generalize something like the following to a tactic acting similar to refine_struct but generating equality goals if two .. substructure arguments provide non-defeq values for a field? This equality can be used to combine proofs coming from those .. substructure arguments even if they can't be unified.

structure subsemiring (R : Type u) [semiring R] extends submonoid R, add_submonoid R
instance : has_coe (subsemiring R) (set R) := ⟨subsemiring.carrier⟩
instance : has_mem R (subsemiring R) := ⟨λ m S, m ∈ (S:set R)⟩

/-- Construct a `subsemiring R` from a set `s`, a submonoid `sm`, and an additive
submonoid `sa` such that `x ∈ s ↔ x ∈ sm ↔ x ∈ sa`. -/
def mk' (s : set R) (sm : submonoid R) (hm : ∀ {x}, x ∈ s ↔ x ∈ sm)
  (sa : add_submonoid R) (ha : ∀ {x}, x ∈ s ↔ x ∈ sa) :
  subsemiring R :=
{ carrier := s,
  zero_mem' := ha.2 sa.zero_mem,
  one_mem' := hm.2 sm.one_mem,
  add_mem' := λ x y, by simpa only [ha] using sa.add_mem,
  mul_mem' := λ x y, by simpa only [hm] using sm.mul_mem }

[Yury G. Kudryashov]

Probably I want a def anyway because this way I can easily prove something like mk'_to_submonoid.

[Yury G. Kudryashov]

I think what I actually want is an attribute that automatically generates a function like lattice.copy and a theorem x.copy _ = x.

[Yury G. Kudryashov]

Then my mk' would become something like { .. sm.copy _, .. sa.copy _ }.