## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• Nov 03 2019 21:43

leodemoura on no_type_class_dep_at_unifier

experiment (compare)

• Oct 31 2019 19:17

leodemoura on master

• Oct 31 2019 19:15

leodemoura on master

• Oct 31 2019 18:45
cipher1024 commented #2006
• Oct 31 2019 18:21
jwaldmann opened #2006
• Oct 30 2019 02:49
cipher1024 commented #2004
• Oct 30 2019 02:39
fpvandoorn commented #2004
• Oct 30 2019 02:37
fpvandoorn commented #2004
• Oct 30 2019 00:36
JasonGross commented #2005
• Oct 30 2019 00:33
JasonGross opened #2005
• Oct 30 2019 00:28
JasonGross opened #2004
• Oct 24 2019 01:52
enricozb closed #2003
• Oct 24 2019 01:52
enricozb commented #2003
• Oct 24 2019 01:50
enricozb opened #2003
• Oct 18 2019 15:13
mrakgr closed #2002
• Oct 18 2019 15:02
cipher1024 commented #2002
• Oct 18 2019 13:42
mrakgr edited #2002
• Oct 18 2019 13:41
mrakgr opened #2002
• Oct 14 2019 07:53
mrakgr closed #2001
• Oct 13 2019 22:17
semorrison commented #2001
Mario Carneiro
@digama0
You will have to do cases on the two Homs first (or use pattern matching to do cases)
Kenny Lau
@kckennylau
⊢ {T' := T', map_add' := map_add', map_mul' := map_mul'} =
{T' := T'_1, map_add' := map_add'_1, map_mul' := map_mul'_1}
good lord
I can handle this, thanks
theorem ext (A B : Hom K V W) (HAB : ∀ v, A.T v = B.T v) : A = B :=
begin
cases A,
cases B,
congr,
apply funext,
simp [T] at HAB,
exact HAB
end
general grievous, you're shorter than I expected
Kenny Lau
@kckennylau
@digama0 is there a reason as to why there is no linear algebra?
Mario Carneiro
@digama0
No one has had the time?
The whole library didn't exist only a few months ago
Kenny Lau
@kckennylau
will you considering using my codes lol
The whole library didn't exist only a few months ago
wow!
you're free to modify any part of it of course, if you want to use my codes
and no credits
Mario Carneiro
@digama0
A better question is what exactly would you want to see in a linear algebra development
Kenny Lau
@kckennylau
I'm proving that the dual space is a space now
reasonable instances would be vector spaces like polynomials or Q(sqrt(2)) or finite field extensions
reals are incomputable :P
Mario Carneiro
@digama0
You realize that each of those is at least a week to maybe a few months' work, right?
We're a bit short on manpower
Kenny Lau
@kckennylau
I understand
I mean, I can do those myself
and then you just need to import them to the library
Mario Carneiro
@digama0
Well, try it, polish it, make sure it covers everything one would expect of such a development, and PR it
Kenny Lau
@kckennylau
ok
is there any reason as to why add_comm_group requires what I call zero_add and add_zero when one of them is enough?
actually, it's zero_add that is enough
Mario Carneiro
@digama0
It is a side effect of the way structures work. add_comm_group inherits from add_group which provides both components to the structure
Kenny Lau
@kckennylau
why does that require that?
Mario Carneiro
@digama0
Oh, right
Well, it inherits from add_monoid and there it definitely can't be derived
Kenny Lau
@kckennylau
oh...
unary negation symbol?
(-) doesn't work
has_neg.neg is too long
Mario Carneiro
@digama0
One solution is to have a custom constructor that proves the theorems using some minimal set, but you don't get the structure notation
sorry, no suggestions re: has_neg.neg
Kenny Lau
@kckennylau
ok
well I do have suggestion
to define neg first and then instance : has_neg := \<neg\>
but that's too much work
Mario Carneiro
@digama0
Here's a suggestion: look at how it's done in the libraries, and try to emulate that style
Kenny Lau
@kckennylau
doing
protected meta def transfer_core : tactic unit := do
transfer.transfer [relator.rel_forall_of_total, relator.rel_not,
int.rel_eq, int.rel_zero, int.rel_one,
int.rel_add, int.rel_neg, int.rel_mul]

protected meta def transfer (distrib := tt) : tactic unit :=
if distrib then [int.transfer_core, simp [add_mul, mul_add]]
else [int.transfer_core, simp]

instance : comm_ring int :=
zero           := int.zero,
neg            := int.neg,
mul            := int.mul,
mul_assoc      := by int.transfer tt,
one            := int.one,
one_mul        := by int.transfer,
mul_one        := by int.transfer,
left_distrib   := by int.transfer tt,
right_distrib  := by int.transfer tt,
mul_comm       := by int.transfer}
protected meta def
nope
Mario Carneiro
@digama0
nope?
Kenny Lau
@kckennylau
"nope" is a comical thing that means kind of "nope I'm out of here"
Mario Carneiro
@digama0
int is a bit of a special case, the proof proceeds by constructing a custom tactic that proves the theorems
Kenny Lau
@kckennylau
right