-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Subtype instance #267
Subtype instance #267
Changes from all commits
cad3f3c
4b2aca4
b2dbc9c
411cefd
224e980
14b28ae
c474eba
File filter
Filter by extension
Conversations
Jump to
Diff view
Diff view
There are no files selected for viewing
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -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 |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,77 @@ | ||
/- | ||
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 | ||
|
||
section tactic | ||
|
||
open tactic.interactive (get_current_field refine_struct) | ||
open lean lean.parser | ||
open interactive | ||
|
||
/-- make names as in `is_add_subgroup` from `add_group` by global prefacing with `is_` | ||
and prefacing the last underscore delimeted item with `sub` -/ | ||
def mk_substructure_name (x : string) : string := | ||
"is_" ++ string.map_tokens '_' (list.map_last $ (++) "sub") x | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. A better way is analyse what the substructure is by looking into the local context in We have the following shape: instance subset.ring {S : set R} [is_subring S] : ring S := by subtype_instance It should be easy to figure out that There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. I'm not sure what you're getting at. |
||
|
||
/-- makes the substructure axiom name from field name, by postfacing with `_mem`-/ | ||
def mk_mem_name : name -> name | ||
| (mk_string n (mk_string n' p)) := mk_string (n ++ "_mem") (mk_string (mk_substructure_name n') p) | ||
| 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 | ||
`(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, | ||
mem_field ← resolve_constant $ mk_mem_name field, | ||
val_mem ← mk_app mem_field hyps, | ||
`(coe_sort %%s) <- target >>= instantiate_mvars, | ||
tactic.refine ``(@subtype.mk _ %%s %%val %%val_mem) | ||
|
||
/-- 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 := | ||
There was a problem hiding this comment. Choose a reason for hiding this commentThe reason will be displayed to describe this comment to others. Learn more. This should be in the |
||
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 tactic |
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,77 @@ | ||
/- | ||
Copyright (c) 2018 Simon Hudon. All rights reserved. | ||
Released under Apache 2.0 license as described in the file LICENSE. | ||
Authors: Simon Hudon | ||
-/ | ||
|
||
import algebra.group_power | ||
import tactic.subtype_instance | ||
|
||
namespace test_tactics | ||
|
||
section | ||
variables {α : Type*} [monoid α] {s : set α} | ||
variables {β : Type*} [add_monoid β] {t : set β} | ||
|
||
-- TODO(Simon) these could be generated from `monoid` | ||
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_add_submonoid (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_add_submonoid 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 subtype_instance | ||
|
||
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 subtype_instance | ||
|
||
end | ||
|
||
section | ||
variables {R : Type*} [ring R] | ||
|
||
|
||
class is_subring (S : set R) extends is_add_subgroup S, is_submonoid S : Prop. | ||
|
||
instance subtype.ring {S : set R} [is_subring S] : ring S := | ||
by subtype_instance | ||
|
||
variables {cR : Type*} [comm_ring cR] | ||
|
||
|
||
instance subset.comm_ring {S : set cR} [is_subring S] : comm_ring S := | ||
by subtype_instance | ||
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 := | ||
by subtype_instance | ||
end | ||
|
||
end test_tactics | ||
|
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
This should be a
namespace tactic
.