refine_struct for subtypes

subtypes.lean

import algebra.ring
import group_theory.submonoid
import tactic.interactive

namespace tactic

open tactic.interactive

meta def derive_field_subtype : tactic unit :=
do b ← target >>= is_prop,
  if b then do
     field ← get_current_field,
     intros,
     `[refine subtype.eq _],
     `[repeat { apply_instance }],
     applyc field
  else do skip

run_cmd add_interactive [`derive_field_subtype]
end tactic


section
variables {α : Type*} [add_monoid α] {s : set α}

/-- `s` is an additive submonoid: a set containing 0 and closed under addition. -/
class is_add_submonoid (s : set α) : Prop :=
(zero_mem : (0:α) ∈ s)
(add_mem {a b} : a ∈ s → b ∈ s → a + b ∈ s)

instance subtype.add_monoid {s : set α} [is_add_submonoid s] : add_monoid s :=
begin
  refine_struct { 
    add   := λ a b : s, (⟨a + b, is_add_submonoid.add_mem a.2 b.2⟩ : s),
    zero  := ⟨0, is_add_submonoid.zero_mem s⟩  } ; derive_field_subtype
end

end

open group

section
variables {α : Type*} [add_group α]

/-- `s` is an additive subgroup: a set containing 0 and closed under addition and negation. -/
class is_add_subgroup (s : set α) extends is_add_submonoid s : Prop :=
(neg_mem {a} : a ∈ s → -a ∈ s)

instance subtype.add_group {s : set α} [is_add_subgroup s] : add_group s :=
by refine_struct { neg := λa, ⟨-(a.1), is_add_subgroup.neg_mem a.2⟩, .. subtype.add_monoid} ; derive_field_subtype
end

section
variables {R : Type} [ring R]

class is_subring  (S : set R) extends is_add_subgroup S, is_submonoid S : Prop.

instance subset.ring {S : set R} [is_subring S] : ring S :=
by refine_struct {..subtype.add_group, .. subtype.monoid } ; derive_field_subtype
end