feat(tactic/subtype_instance): generating subtype instances

Author: cipher1024

data/list/basic.lean

@@ -3831,6 +3831,15 @@ theorem reverse_range' : ∀ s n : ℕ,
   map prod.fst (enum l) = range l.length :=
 by simp [enum, range_eq_range']
 
+def map_head {α} (f : α → α) : list α → list α
+| [] := []
+| (x :: xs) := f x :: xs
+
+def map_last {α} (f : α → α) : list α → list α
+| [] := []
+| [x] := [f x]
+| (x :: xs) := x :: map_last xs
+
 end list
 
 theorem option.to_list_nodup {α} (o : option α) : o.to_list.nodup :=

data/string.lean

@@ -67,4 +67,7 @@ by refine_struct {
     decidable_eq := by apply_instance, .. };
   { simp [-not_le], introv, apply_field }
 
-end string
+def map_tokens (c : char) (f : list string → list string) : string → string :=
+intercalate (singleton c) ∘ f ∘ split (= c)
+
+end string

field_theory/subfield.lean

@@ -0,0 +1,19 @@
+/-
+Copyright (c) 2018 Andreas Swerdlow. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Andreas Swerdlow
+-/
+
+import ring_theory.subring
+
+variables {F : Type*} [field F] (s : set F)
+
+class is_subfield extends is_subring s :=
+(inv_mem : ∀ {x : F}, x ∈ s → x⁻¹ ∈ s)
+
+open is_subfield
+
+instance subset.field [is_subfield s] : field s :=
+by subtype_instance
+
+instance subtype.field [is_subfield s] : field (subtype s) := subset.field s

group_theory/subgroup.lean

@@ -48,14 +48,10 @@ theorem multiplicative.is_subgroup_iff
   λ h, by resetI; apply_instance⟩
 
 instance subtype.group {s : set α} [is_subgroup s] : group s :=
-{ inv          := λa, ⟨(a.1)⁻¹, is_subgroup.inv_mem a.2⟩,
-  mul_left_inv := λa, subtype.eq $ mul_left_inv _,
-  .. subtype.monoid }
+by subtype_instance
 
 instance subtype.add_group {s : set β} [is_add_subgroup s] : add_group s :=
-{ neg          := λa, ⟨-(a.1), is_add_subgroup.neg_mem a.2⟩,
-  add_left_neg := λa, subtype.eq $ add_left_neg _,
-  .. subtype.add_monoid }
+by subtype_instance
 attribute [to_additive subtype.add_group] subtype.group
 
 theorem is_subgroup.of_div (s : set α)

group_theory/submonoid.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Johannes Hölzl, Kenny Lau, Johan Commelin, Mario Carneiro
 -/
 import algebra.group_power
+import tactic.subtype_instance
 
 variables {α : Type*} [monoid α] {s : set α}
 variables {β : Type*} [add_monoid β] {t : set β}
@@ -81,15 +82,13 @@ lemma is_submonoid.list_prod_mem [is_submonoid s] : ∀{l : list α}, (∀x∈l,
   is_submonoid.mul_mem this.1 (is_submonoid.list_prod_mem this.2)
 
 instance subtype.monoid {s : set α} [is_submonoid s] : monoid s :=
-{ mul       := λ a b : s, ⟨a * b, is_submonoid.mul_mem a.2 b.2⟩,
-  one       := ⟨1, is_submonoid.one_mem s⟩,
-  mul_assoc := λ a b c, subtype.eq $ mul_assoc _ _ _,
-  one_mul   := λ a, subtype.eq $ one_mul _,
-  mul_one   := λ a, subtype.eq $ mul_one _ }
+by subtype_instance
+
 attribute [to_additive subtype.add_monoid._proof_1] subtype.monoid._proof_1
 attribute [to_additive subtype.add_monoid._proof_2] subtype.monoid._proof_2
 attribute [to_additive subtype.add_monoid._proof_3] subtype.monoid._proof_3
 attribute [to_additive subtype.add_monoid._proof_4] subtype.monoid._proof_4
+attribute [to_additive subtype.add_monoid._proof_5] subtype.monoid._proof_5
 attribute [to_additive subtype.add_monoid] subtype.monoid
 
 namespace monoid

ring_theory/subring.lean

@@ -0,0 +1,41 @@
+/-
+Copyright (c) 2018 Johan Commelin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Johan Commelin
+-/
+
+import group_theory.subgroup
+import data.polynomial
+import algebra.ring
+
+local attribute [instance] classical.prop_decidable
+universes u v
+
+open group
+
+variables {R : Type u} [ring R]
+
+/-- `S` is a subring: a set containing 1 and closed under multiplication, addition and and additive inverse. -/
+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 subtype_instance
+
+instance subtype.ring {S : set R} [is_subring S] : ring (subtype S) := subset.ring
+
+namespace is_ring_hom
+
+instance {S : set R} [is_subring S] : is_ring_hom (@subtype.val R S) :=
+by refine {..} ; intros ; refl
+
+end is_ring_hom
+
+variables {cR : Type u} [comm_ring cR]
+
+instance subset.comm_ring {S : set cR} [is_subring S] : comm_ring S :=
+by subtype_instance
+
+instance subtype.comm_ring {S : set cR} [is_subring S] : comm_ring (subtype S) := subset.comm_ring
+
+instance subring.domain {D : Type*} [integral_domain D] (S : set D) [is_subring S] : integral_domain S :=
+by subtype_instance

tactic/algebra.lean

@@ -0,0 +1,52 @@
+/-
+Copyright (c) 2018 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Hudon
+-/
+
+import tactic.basic
+
+open lean.parser
+
+namespace tactic
+
+@[user_attribute]
+meta def ancestor_attr : user_attribute unit (list name) :=
+{ name := `ancestor,
+  descr := "ancestor of old structures",
+  parser := many ident }
+
+meta def get_ancestors (cl : name) : tactic (list name) :=
+(++) <$> (prod.fst <$> subobject_names cl <|> pure [])
+     <*> (user_attribute.get_param ancestor_attr cl <|> pure [])
+
+meta def find_ancestors : name → expr → tactic (list expr) | cl arg :=
+do cs ← get_ancestors cl,
+   r ← cs.mmap $ λ c, list.ret <$> (mk_app c [arg] >>= mk_instance) <|> find_ancestors c arg,
+   return r.join
+
+end tactic
+
+attribute [ancestor has_mul] semigroup
+attribute [ancestor semigroup has_one] monoid
+attribute [ancestor monoid has_inv] group
+attribute [ancestor group has_comm] comm_group
+attribute [ancestor has_add] add_semigroup
+attribute [ancestor add_semigroup has_zero] add_monoid
+attribute [ancestor add_monoid has_neg] add_group
+attribute [ancestor add_group has_add_comm] add_comm_group
+
+attribute [ancestor ring has_inv zero_ne_one_class] division_ring
+attribute [ancestor division_ring comm_ring] field
+attribute [ancestor field] discrete_field
+
+attribute [ancestor has_mul has_add] distrib
+attribute [ancestor has_mul has_zero] mul_zero_class
+attribute [ancestor has_zero has_one] zero_ne_one_class
+attribute [ancestor add_comm_monoid monoid distrib mul_zero_class] semiring
+attribute [ancestor semiring comm_monoid] comm_semiring
+attribute [ancestor add_comm_group monoid distrib] ring
+
+attribute [ancestor ring comm_semigroup] comm_ring
+attribute [ancestor has_mul has_zero] no_zero_divisors
+attribute [ancestor comm_ring no_zero_divisors zero_ne_one_class] integral_domain

tactic/basic.lean

@@ -509,4 +509,7 @@ do l ← local_context,
 
 run_cmd add_interactive [`injections_and_clear]
 
+meta def find_local (t : pexpr) : tactic expr :=
+do t' ← to_expr t,
+   prod.snd <$> solve_aux t' assumption
 end tactic

tactic/subtype_instance.lean

@@ -0,0 +1,81 @@
+/-
+Copyright (c) 2018 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Simon Hudon
+
+Provides a `subtype_instance` tactic which builds instances for algebraic substructures
+(sub-groups, sub-rings...).
+-/
+
+import data.string
+import tactic.interactive tactic.algebra
+import data.subtype data.set.basic
+open tactic expr name list
+
+namespace tactic
+
+open tactic.interactive (get_current_field refine_struct)
+open lean lean.parser
+open interactive
+
+/-- makes the substructure axiom name from field name, by postfacing with `_mem`-/
+def mk_mem_name (sub : name) : name → name
+| (mk_string n _) := mk_string (n ++ "_mem") sub
+| n := n
+
+meta def derive_field_subtype : tactic unit :=
+do
+  field ← get_current_field,
+  b ← target >>= is_prop,
+  if b then  do
+    `[simp [subtype.ext], dsimp],
+    intros,
+    applyc field; assumption
+  else do
+    s ← find_local ``(set _),
+    `(set %%α) ← infer_type s,
+    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,
+    subname ← local_context >>= list.mfirst (λ h, do
+      (expr.const n _, args) ← get_app_fn_args <$> infer_type h,
+      is_def_eq s args.ilast reducible,
+      return n),
+    mem_field ← resolve_constant $ mk_mem_name subname field,
+    val_mem ← mk_app mem_field hyps,
+    `(coe_sort %%s) <- target >>= instantiate_mvars,
+    tactic.refine ``(@subtype.mk _ %%s %%val %%val_mem)
+
+namespace interactive
+
+/-- builds instances for algebraic substructures
+
+Example:
+```lean
+variables {α : Type*} [monoid α] {s : 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
+````
+-/
+meta def subtype_instance :=
+do t ← target,
+   let cl := t.get_app_fn.const_name,
+   src ← find_ancestors cl t.app_arg,
+   let inst := pexpr.mk_structure_instance
+       { struct := cl,
+         field_values := [],
+         field_names := [],
+         sources := src.map to_pexpr },
+   refine_struct inst ; derive_field_subtype
+
+end interactive
+
+end tactic