Begin work on subtype instance tactic

tactic/subtype_instance.lean

@@ -0,0 +1,108 @@
+import algebra.group_power
+
+import tactic.interactive
+import data.subtype data.set.basic
+open tactic expr name list
+open tactic.interactive (get_current_field)
+
+def mk_mem_name : name -> name
+| (mk_string n (mk_string n' p)) := mk_string (n ++ "_mem") (mk_string ("is_sub" ++ n') p)
+| n := n
+
+meta def find_local (t : pexpr) : tactic expr :=
+do t' ← to_expr t,
+   prod.snd <$> solve_aux t' assumption
+
+meta def derive_field_subtype : tactic unit :=
+do 
+  field ← get_current_field,
+  b ← target >>= is_prop,
+  if b then  do
+    `[simp [subtype.ext]],
+    intros,
+    applyc field,
+    try assumption
+  else do 
+    `(set %%α) ← find_local ``(set _) >>= infer_type, 
+    e ← mk_const field,
+    expl_arity ← get_expl_arity $ e α,
+    xs ← (iota expl_arity).mmap $ λ _, intro1,
+    args ← xs.mmap $ λ x, mk_app `subtype.val [x],
+    hyps ← xs.mmap $ λ x, mk_app `subtype.property [x],
+    val ← mk_app field args,
+    val_mem ← mk_app (mk_mem_name field) hyps,
+    `(coe_sort %%s) <- target >>= instantiate_mvars,
+    tactic.refine ``(@subtype.mk _ %%s %%val %%val_mem)
+
+meta def subtype_instance := `[refine_struct {..} ; derive_field_subtype]
+
+section
+variables {α : Type*} [monoid α] {s : set α}
+variables {β : Type*} [add_monoid β] {t : set β}
+
+class is_submonoid (s : set α) : Prop :=
+(one_mem : (1:α) ∈ s)
+(mul_mem {a b} : a ∈ s → b ∈ s → a * b ∈ s)
+
+instance subtype.monoid {s : set α} [is_submonoid s] : monoid s :=
+by subtype_instance
+
+class is_subadd_monoid (s : set β) : Prop :=
+(zero_mem : (0:β) ∈ s)
+(add_mem {a b} : a ∈ s → b ∈ s → a + b ∈ s)
+
+instance subtype.add_monoid {t : set β} [is_subadd_monoid t] : add_monoid t :=
+by subtype_instance
+end
+
+section
+variables {α : Type*} [group α] {s : set α}
+{β : Type*} [add_group β]
+
+class is_subgroup (s : set α) extends is_submonoid s : Prop :=
+(inv_mem {a} : a ∈ s → a⁻¹ ∈ s)
+
+instance subtype.group {s : set α} [is_subgroup s] : group s :=
+by refine_struct {..subtype.monoid} ; derive_field_subtype
+
+class is_subadd_group (s : set β) extends is_subadd_monoid s : Prop :=
+(neg_mem {a} : a ∈ s → -a ∈ s)
+set_option trace.app_builder true
+
+instance subtype.add_group {s : set β} [is_subadd_group s] : add_group s :=
+by refine_struct {..subtype.add_monoid} ; derive_field_subtype
+end
+
+section
+variables {R : Type*} [ring R]
+
+
+class is_subring  (S : set R) extends is_subadd_group S, is_submonoid S : Prop.
+
+instance subtype.ring {S : set R} [is_subring S] : ring S :=
+by refine_struct { .. subtype.add_group, .. subtype.monoid } ; derive_field_subtype
+
+variables {cR : Type*} [comm_ring cR]
+
+
+instance subset.comm_ring {S : set cR} [is_subring S] : comm_ring S :=
+by refine_struct { ..subtype.ring } ; derive_field_subtype
+end
+
+section
+variables {F : Type*} [field F] (s : set F)
+
+class is_subfield extends is_subring s :=
+(inv_mem : ∀ {x : F}, x ∈ s → x⁻¹ ∈ s)
+
+
+instance subtype.field [is_subfield s] : field s :=
+begin
+ refine_struct {.. subset.comm_ring}, 
+ { derive_field_subtype },
+ { 
+   sorry },
+ { derive_field_subtype },
+ { derive_field_subtype }
+end
+end