Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Activity
  • Nov 03 2019 21:43

    leodemoura on no_type_class_dep_at_unifier

    experiment (compare)

  • Oct 31 2019 19:17

    leodemoura on master

    chore: simplify README (compare)

  • Oct 31 2019 19:15

    leodemoura on master

    chore: update README (compare)

  • 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 :=
{ add            := int.add,
  add_assoc      := by int.transfer,
  zero           := int.zero,
  zero_add       := by int.transfer,
  add_zero       := by int.transfer,
  neg            := int.neg,
  add_left_neg   := by int.transfer,
  add_comm       := by int.transfer,
  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