Zulip Chat Archive

Stream: maths

Topic: ring hom induces ring hom between mv_polynomials


view this post on Zulip Johan Commelin (Jul 24 2018 at 10:43):

I am stuck.

import linear_algebra.multivariate_polynomial

universes u v w

-- ### FOR_MATHLIB
-- everything in this section should move to other files

section ring_hom_commutes_with_stuff

variables {R : Type u} [comm_ring R]
variables {S : Type v} [comm_ring S]
variables (i : R  S) [is_ring_hom i]
variables {X : Type w} [decidable_eq X] (s : finset X) (f : X  R)

open finset

lemma ring_hom_sum : i (sum s f) = sum s (i  f) :=
begin
  apply finset.induction_on s,
  { repeat { rw sum_empty },
    exact is_ring_hom.map_zero i },
  { intros x s' hx ih,
    repeat { rw sum_insert hx },
    rw [is_ring_hom.map_add i, ih] }
end

end ring_hom_commutes_with_stuff

namespace mv_polynomial

variables {σ : Type*} [decidable_eq σ]
variables {R : Type u} [decidable_eq R] [comm_ring R]
variables {S : Type v} [decidable_eq S] [comm_ring S]

instance : comm_ring (mv_polynomial σ R) := finsupp.to_comm_ring

instance C_is_ring_hom : is_ring_hom (C : R  mv_polynomial σ R) :=
{ map_one := C_1,
  map_add := λ x y, finsupp.single_add,
  map_mul := λ x y, eq.symm $ C_mul_monomial }

instance functorial_is_ring_hom (i : R  S) [is_ring_hom i] :
is_ring_hom (functorial i : mv_polynomial σ R  mv_polynomial σ S) :=
{ map_one :=
  begin
    simp [functorial],
    simp [finsupp.map_range],
    -- simp [function.comp],
    apply finsupp.ext,
    intro x,
    rw finsupp.on_finset_apply,
    simp [*,finsupp.single_apply],
    sorry
  end,
  map_add :=
  begin
    intros f g,
    simp [functorial,finsupp.map_range,function.comp],
    apply finsupp.ext,
    intro x,
    simp [*,finsupp.single_apply],
    rw is_ring_hom.map_add i,
  end,
  map_mul :=
  begin
    intros f g,
    simp [functorial,finsupp.map_range,function.comp,finsupp.mul_def,finsupp.sum],
    apply finsupp.ext,
    intro x,
    simp [*,finsupp.single_apply],
    rw ring_hom_sum i,
    sorry,
  end }

view this post on Zulip Johan Commelin (Jul 24 2018 at 10:43):

There are two sorrys in that bit of code. I don't know how to get rid of them.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:01):

I think you are going about this the wrong way, at least if you want a clean proof at the end

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:02):

Hmmm, so what is the right way?

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:02):

You should break the proof into smaller and more useful parts rather than just attacking the whole thing at once

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:03):

Ok, but I think I don't even really see the smaller useful parts...

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:04):

here's the first thing I would prove:

theorem map_monomial (f : α → β) [is_ring_hom f]
  (s : σ →₀ ℕ) (a : α) : map f (monomial s a) = monomial s (f a) :=
sorry

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:04):

(I renamed functorial to map)

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:05):

It is still called functorial in mathlib right?

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:05):

not in my local copy as of a minute ago

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:05):

Aaah...

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:05):

you can use functorial if it's easier

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:08):

theorem map_monomial (i : R  S) [is_ring_hom i]
  (x : σ  ) (r : R) : functorial i (monomial x r) = monomial x (i r) :=
begin
  simp [functorial,finsupp.map_range,function.comp,monomial],
  apply finsupp.ext,
  intro x,
  simp [*,finsupp.single_apply],
  split_ifs,
  { refl },
  { apply is_ring_hom.map_zero }
end

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:09):

I am suspicious still

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:09):

that proof is too complicated

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:09):

Hmmm, ok, I'll try to golf it.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:09):

it should be a one liner about the composition of map_range with single

view this post on Zulip Chris Hughes (Jul 24 2018 at 11:10):

Incidentally is @Johannes Hölzl planning on removing the use of monomial for mv_polynomials like he did for univariate polys?

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:11):

I don't know anything about this

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:11):

oh, I see he just uses single

view this post on Zulip Chris Hughes (Jul 24 2018 at 11:12):

The idea is to use C a * X^n instead of monomial

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:12):

For foundational stuff that's no good

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:13):

because the theorems about C a and X come from a theorem on single

view this post on Zulip Chris Hughes (Jul 24 2018 at 11:14):

Yeah, but once the foundations are done, users are supposed to use C a * X^n I think.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:14):

sure

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:14):

/me seems to be a user who has to do some foundational stuff...

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:14):

Johan Commelin has stumbled on a gap in mathlib

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:15):

That's the same thing right?

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:15):

not always

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:15):

fair enough

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:15):

well, I guess that depends on what qualifies as "foundational"

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:15):

in this case the API is clearly lacking, and there is even an "unfinished" comment

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:16):

Written by?

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:16):

Johan Commelin (-;

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:16):

So, I can only blame myself

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:16):

https://github.com/leanprover/mathlib/blob/master/linear_algebra/multivariate_polynomial.lean#L183

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:16):

But you can guess why I wrote that comment... because back then I would have been even worse at proving this lemma.

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:17):

Yeah, the git blame is not accurate.

view this post on Zulip Kenny Lau (Jul 24 2018 at 11:17):

I've removed 1 sorry (en hep nok 4 toegevoegt):

view this post on Zulip Kenny Lau (Jul 24 2018 at 11:17):

import linear_algebra.multivariate_polynomial

universes u v w u₁

-- ### FOR_MATHLIB
-- everything in this section should move to other files

section ring_hom_commutes_with_stuff

variables {R : Type u} [comm_ring R]
variables {S : Type v} [comm_ring S]
variables (i : R  S) [is_ring_hom i]

section finset

open finset

variables {X : Type w} [decidable_eq X] (s : finset X) (f : X  R)

lemma ring_hom_sum.finset : i (sum s f) = sum s (i  f) :=
begin
  apply finset.induction_on s,
  { repeat { rw sum_empty },
    exact is_ring_hom.map_zero i },
  { intros x s' hx ih,
    repeat { rw sum_insert hx },
    rw [is_ring_hom.map_add i, ih] }
end

end finset

section finsupp

open finsupp

variables {α : Type w} {β : Type u₁} [add_comm_monoid β]
variables [decidable_eq α] [decidable_eq β]
variables (f : α  β  R) (s : α  β)
variables (hf1 :  (a : α), f a 0 = 0)
variables (hf2 :  (a : α) (b₁ b₂ : β), f a (b₁ + b₂) = f a b₁ + f a b₂)
include hf1 hf2

lemma ring_hom_sum.finsupp : i (sum s f) = sum s (λ a b, i (f a b)) :=
begin
  apply finsupp.induction s,
  { repeat { rw sum_zero_index },
    exact is_ring_hom.map_zero i },
  { intros a b f' H1 H2 ih,
    repeat { rw sum_add_index },
    repeat { rw sum_single_index },
    rw [is_ring_hom.map_add i,  ih],
    { rw hf1; exact is_ring_hom.map_zero i },
    { apply hf1 },
    { intros, rw hf1; exact is_ring_hom.map_zero i },
    { intros, rw hf2; exact is_ring_hom.map_add i },
    { apply hf1 },
    { apply hf2 } }
end

end finsupp

end ring_hom_commutes_with_stuff

namespace mv_polynomial

variables {σ : Type*} [decidable_eq σ]
variables {R : Type u} [decidable_eq R] [comm_ring R]
variables {S : Type v} [decidable_eq S] [comm_ring S]

instance : comm_ring (mv_polynomial σ R) := finsupp.to_comm_ring

instance C_is_ring_hom : is_ring_hom (C : R  mv_polynomial σ R) :=
{ map_one := C_1,
  map_add := λ x y, finsupp.single_add,
  map_mul := λ x y, eq.symm $ C_mul_monomial }

instance functorial_is_ring_hom (i : R  S) [is_ring_hom i] :
is_ring_hom (functorial i : mv_polynomial σ R  mv_polynomial σ S) :=
{ map_one :=
  begin
    dsimp [functorial, finsupp.map_range],
    ext x,
    dsimp [finsupp.on_finset_apply],
    have H1 : (1 : mv_polynomial σ R) = (1 : (σ  )  R) := rfl,
    have H2 : (1 : mv_polynomial σ S) = (1 : (σ  )  S) := rfl,
    rw [H1, H2, finsupp.one_def, finsupp.one_def, finsupp.single_apply, finsupp.single_apply],
    split_ifs,
    { apply is_ring_hom.map_one i },
    { apply is_ring_hom.map_zero i }
  end,
  map_add :=
  begin
    intros f g,
    dsimp [functorial, finsupp.map_range],
    ext,
    simp [finsupp.single_apply, is_ring_hom.map_add i]
  end,
  map_mul :=
  begin
    intros f g,
    dsimp [functorial, finsupp.map_range],
    ext,
    dsimp [finsupp.on_finset_apply, finsupp.mul_def],
    rw [finsupp.sum_apply, finsupp.sum_apply, ring_hom_sum.finsupp i],
    sorry, sorry, sorry, sorry, sorry
  end }

end mv_polynomial

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:18):

I wrote that stuff, but didn't actually know what I was doing. So Johannes took my stuff and transformed it into something mathlib-ready.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:18):

I didn't realize you were an author of the file, you aren't credited if so

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:18):

I added you as an author

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:22):

Does that bring responsibilities with it? Does that mean I should now be able to answer foundational questions about this file?

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:22):

Not really

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:26):

By the way... I already had:

lemma functorial_ring_hom_X (i : R  S) [is_ring_hom i] (n : σ)
 : functorial i (X n) = X n :=
begin
  simp [functorial,X,finsupp.map_range,function.comp,C,monomial,*],
  apply finsupp.ext,
  intro x,
  simp [*,finsupp.single_apply],
  split_ifs,
  { apply is_ring_hom.map_one },
  { apply is_ring_hom.map_zero }
end

lemma functorial_ring_hom_C (i : R  S) [is_ring_hom i] (r : R)
: functorial i (C r) = (C (i r) : mv_polynomial σ S) :=
begin
  simp [functorial,X,finsupp.map_range,function.comp,C,monomial,*],
  apply finsupp.ext,
  intro x,
  simp [*,finsupp.single_apply],
  split_ifs,
  { refl },
  { apply is_ring_hom.map_zero }
end

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:26):

But I didn't see how to use them.

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:26):

But maybe I'm learning, because I think it was pretty close to your suggestion about monomials.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:26):

almost there:

-- `mv_polynomial σ` is a functor (incomplete)
def map : mv_polynomial σ α → mv_polynomial σ β :=
map_range f (is_ring_hom.map_zero f)

theorem map_monomial (s : σ →₀ ℕ) (a : α) : map f (monomial s a) = monomial s (f a) :=
map_range_single

theorem map_C (f : α → β) [is_ring_hom f] (a : α) : map f (C a : mv_polynomial σ α) = C (f a) :=
map_monomial _ _ _

theorem map_one (f : α → β) [is_ring_hom f] : map f (1 : mv_polynomial σ α) = 1 :=
(map_C _ _).trans $ by simp [is_ring_hom.map_one f]

theorem map_add (f : α → β) [is_ring_hom f] (p q : mv_polynomial σ α) :
  map f (p + q) = map f p + map f q :=
by simp [map]; ext a; simp [is_ring_hom.map_add f]

theorem map_mul (f : α → β) [is_ring_hom f] (p q : mv_polynomial σ α) :
  map f (p * q) = map f p * map f q :=
sorry

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:27):

Ok, please add map_X. It will turn out to be really useful.

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:28):

/me wonders when he will ever approximate the overlord-powers of Mario... :thinking_face:

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:28):

theorem map_X (f : α → β) [is_ring_hom f] (n : σ) : map f (X n : mv_polynomial σ α) = X n :=
(map_monomial _ _ _).trans $ by simp [is_ring_hom.map_one f]

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:29):

oh wait that doesn't work

theorem map_X (f : α → β) [is_ring_hom f] (n : σ) : map f (X n : mv_polynomial σ α) = X n :=
by simp [X, map_monomial, is_ring_hom.map_one f]

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:29):

You fixed it and made it shorter! Double win.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:30):

mul is probably the hard one

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:30):

Last man standing (-;

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:32):

@Mario Carneiro I wouldn't be surprised if you need the section ring_hom_commutes_with_stuff

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:33):

See Kenny's post a few lines up.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:33):

I was planning on using induction

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:33):

Right, that's what we did in that section.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:33):

no I mean to prove map_mul

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:34):

Yes, but that might mean duplicating effort... I don't know.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:35):

well, commuting with sum still leaves commuting over ^

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:39):

lemma ring_hom_powers (x : R) (n : ) : i(x^n) = (i x)^n :=
begin
  induction n with n ih,
  { simp [pow_zero,is_ring_hom.map_one i] },
  simp [pow_succ,is_ring_hom.map_mul i,ih]
end

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:39):

Was already in my file, but didn't copy it into the MWE.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:41):

I was hoping that map was defined using eval, but unfortunately it's a bit circular

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:41):

How would you define it using eval?

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:43):

I was thinking something along the lines of "evaluate the constants using C o f and the variables using X"

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:43):

but eval doesn't work like that; it maps everything into the coefficient ring rather than some other ring across a ring hom

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:44):

True. So either you need a beefed up eval, or you need map.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:44):

exactly

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:45):

Oooh, while you are editing that file. I was also thinking that the instance that eval is a ring hom should get a name. Because C is also a useful ring hom in that context.

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:45):

instance C_is_ring_hom : is_ring_hom (C : R  mv_polynomial σ R) :=
{ map_one := C_1,
  map_add := λ x y, finsupp.single_add,
  map_mul := λ x y, eq.symm $ C_mul_monomial }

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:46):

I saw that

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:46):

I agree that it is useful

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:46):

Yes, I'm currently using map C all over the place.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:47):

I think I will define beefed up eval, what should it be called?

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:50):

Hmm, I don't know a TLA...

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:50):

oh dear, I need semiring homs

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:50):

You're kidding me (-;

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:50):

You don't need them. You only want them.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:51):

if I use beefed up eval to define eval, it won't work on semiring like it does now

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:51):

Mathematicians have survived over 3000 years without needing them.

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:51):

I'm sorry, but they really do come up in lean, a lot

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:51):

nat is a semiring, ennreal is a semiring. These get lots of use

view this post on Zulip Johan Commelin (Jul 24 2018 at 11:52):

Only trolling (-;. I guess you stumbled on a gap in mathlib?

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:52):

maybe because it was written by a bunch of blithe mathematicians ;)

view this post on Zulip Mario Carneiro (Jul 24 2018 at 11:52):

who think semirings have no value

view this post on Zulip Johan Commelin (Jul 24 2018 at 12:03):

You mean the definition of is_ring_hom? Lol. We really need @Scott Morrison and you guys (Mario + @Johannes Hölzl ) to get categories into mathlib. You will be amazed at how many is_X_hom definitions will be added by a bunch of blithe mathematicians (-;

view this post on Zulip Mario Carneiro (Jul 24 2018 at 12:03):

Well, category theory doesn't save you from having to define the homs

view this post on Zulip Johan Commelin (Jul 24 2018 at 12:07):

No, I agree. But all of a sudden we will want to define a bunch of categories. And then we'll define the homs as well (-;

view this post on Zulip Johan Commelin (Jul 24 2018 at 12:08):

Although maybe we will forget about the category of semirings...

view this post on Zulip Johan Commelin (Jul 24 2018 at 12:21):

Aaaahrg, now I need to make sure that eval of polynomials is associative...

view this post on Zulip Johan Commelin (Jul 24 2018 at 13:37):

@Mario Carneiro How 's it going with eval_on_steroids?

view this post on Zulip Kevin Buzzard (Jul 24 2018 at 16:04):

nat is a semiring, ennreal is a semiring. These get lots of use

@Ali Sever (the guy formalising Euclid/Tarski geometry in Lean) was saying that he wanted to be able to say "the distance from a to b is q times the distance from c to d" where q>=0 is rational. There is no formal definition of distance, we just have a predicate eqd a b c d interpreted as "dist(a,b)=dist(c,d)", but we defined distance anyway as point x point / equiv reln (formally these are "attainable distances") and they should indeed be a semi-vector space over the semi-ring of non-negative rationals.

view this post on Zulip Mario Carneiro (Jul 25 2018 at 07:09):

I'm going to have to get back to you on eval_on_steroids, conferences tend to be a time sink so probably not until the weekend

view this post on Zulip Johan Commelin (Jul 25 2018 at 07:10):

Too bad. Have fun!

view this post on Zulip Kevin Buzzard (Jul 25 2018 at 08:53):

William Stein reported that he'd met Mario, so Mario at conferences does have advantages :-)

view this post on Zulip Johan Commelin (Jul 27 2018 at 11:23):

Mario, since you said you would take a stab at these problems, may I suggest you also consider https://gist.github.com/jcommelin/0e401d47ac3e0b7291c27d3313ea850f while you're going at it...?

view this post on Zulip Johan Commelin (Jul 27 2018 at 11:23):

Oooh, and s/functorial/map/.

view this post on Zulip Johan Commelin (Aug 02 2018 at 08:39):

Hi Mario, any news here? Do you have a definition about which I could try to prove some lemmas?

view this post on Zulip Mario Carneiro (Aug 04 2018 at 23:59):

@Johan Commelin News is here. I didn't prove the assoc lemmas but all the assoc lemmas on eval and map follow from the obvious composition lemma for map2

view this post on Zulip Mario Carneiro (Aug 06 2018 at 02:15):

@Johan Commelin I think the second associativity lemma is false:

theorem eval_assoc₂_false
  {α} [comm_semiring α] [decidable_eq α]
  {σ} [decidable_eq σ]
  {τ} [decidable_eq τ]
  (f : σ → mv_polynomial τ α) (g : τ → α)
  (H : ∀ (p : mv_polynomial σ (mv_polynomial τ α)),
    C ((p.eval f).eval g) = p.eval (C ∘ eval g ∘ f))
  (a : τ) : C (g a) = X a :=
by simpa using H (C (X a))

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:08):

@Mario Carneiro Cool! This is adding a lot of flexibility. Do you think it makes sense to add map2_neg and map2_sub?

view this post on Zulip Mario Carneiro (Aug 07 2018 at 05:09):

Sure. They should be direct applications of the is_ring_hom instance

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:10):

Ok, do you want me to do that? Or have you already done it (-;

view this post on Zulip Mario Carneiro (Aug 07 2018 at 05:11):

I haven't done it, it's up to you

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:11):

Ok, I'll add them.

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:19):

@Mario Carneiro Is rw the "morally" correct way to prove such a thing?

lemma map₂_sub : (p - q).map₂ f g = p.map₂ f g - q.map₂ f g :=
by rw is_ring_hom.map_sub (map₂ f g)

view this post on Zulip Mario Carneiro (Aug 07 2018 at 05:20):

you should be able to just apply the theorem, right? Does is_ring_hom.map_sub _ work as a proof?

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:21):

Yes, it does. Thanks! Do you want a 5 line PR?

view this post on Zulip Mario Carneiro (Aug 07 2018 at 05:21):

sure

view this post on Zulip Mario Carneiro (Aug 07 2018 at 05:21):

You should have the same theorems for eval and map too

view this post on Zulip Mario Carneiro (Aug 07 2018 at 05:22):

and C

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:24):

Ok, I'll add those too

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:28):

map_add and map_mul are simp lemmas

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:28):

But the corresponding lemmas for map2 are not.

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:28):

Is there a reason for this?

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:34):

@Mario Carneiro If you can tell me which ones should be simp lemmas, then I think I'm done.

view this post on Zulip Mario Carneiro (Aug 07 2018 at 05:34):

I think there was, but I don't think it was a good reason. Just make them all simp lemmas

view this post on Zulip Mario Carneiro (Aug 07 2018 at 05:35):

eval too

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:35):

And C as well

view this post on Zulip Mario Carneiro (Aug 07 2018 at 05:35):

There probably isn't any point in having the _sub theorems be simp lemmas, since the LHS is not in simp normal form

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:37):

Hmm, I don't think I know what that means. Nevertheless, it would be cool if simp would just do all those rewrites for me...

view this post on Zulip Johan Commelin (Aug 07 2018 at 05:40):

PR'd

view this post on Zulip Johan Commelin (Aug 07 2018 at 07:58):

@Mario Carneiro Ok, so now there are some merge conflicts... The renaming is straightforward.

view this post on Zulip Johan Commelin (Aug 07 2018 at 07:58):

Shall I make the add and mul lemmas into simp lemmas?

view this post on Zulip Mario Carneiro (Aug 07 2018 at 07:58):

yeah, same as the last version of your PR

view this post on Zulip Johan Commelin (Aug 07 2018 at 07:59):

Ok!

view this post on Zulip Johan Commelin (Aug 07 2018 at 09:47):

Updated the PR


Last updated: May 18 2021 at 08:14 UTC