Zulip Chat Archive

Stream: general

Topic: basic struggles


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

I find myself struggling with things that are extremely math-trivial. If I have a goal of the form a = b, how do I turn that into a * c = b * c? (Assume that a b c : R and [comm_ring R].)

view this post on Zulip Simon Hudon (Aug 07 2018 at 05:53):

Have you tried mul_right_cancel_iff?

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

Hmmm, I only need the easy implication, for which I don't need a cancellative instance.

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

And in fact I don't have an instance of cancellative semiblabla... :sad:

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:25):

Ok, I think I see the issue. If R was a multiplicative group, you'd have a left_cancel_semigroup for free. As it is, your statement is not true I think because rings don't have a multiplicative inverse for every non-zero element.

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:26):

If you had a field though ...

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:26):

Can you choose your c so that it has an inverse?

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

Hmmz, sorry, I've been brainfarting...

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

My c has an inverse

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:27):

How rude! :)

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

I'll copy-paste my goal.

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

(witt_polynomial n -
         map₂ witt_polynomial C
           (finset.sum finset.univ (λ (i : fin n), p ^ i.val * X_in_terms_of_W (i.val) ^ p ^ (n - i.val)))) *
      C (1 / p ^ (n + 1)) =
    X n

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

So you see that there is this term C (1 / _).

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

I would like to move it to the other side.

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

This goal has been misbehaving quite a lot, lately.

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:31):

What is the statement that C (1 / _) has an inverse like?

(it does look pretty hairy)

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

Well 1 / _ has an inverse in rat. And C is a ring hom. So it maps inverses to inverses.

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:38):

So in short, C _ is the inverse C (1 / _) I assume. It is surprisingly hard to sneak in I realize. Any chance C has an inverse? Then you could transform your goal from R to rat just long enough to play with the inverse.

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:39):

(That's probably a long shot: if you had that inverse of C, R would probably be a field)

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

No, C is the function R \to mv_polynomial Xs R that takes a ring element to the constant polynomial.

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:40):

I'm starting to think your assumptions are not strong enough for what you're trying to do

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

Ok, so rat is a field, therefore p^(n+1) has an inverse (it is nonzero). Now I apply C to p^(n+1) and I get a crazy element of some ring, and it will still have an inverse.

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

So I want to multiply both sides with C (p^(n+1)).

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

you are thinking backwards

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:42):

What if you multiply by C 1 on the right

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

you want to multiply some equation that will be your new goal by C (1 / ↑p ^ (n + 1))

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

Right

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

So I use suffices?

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:44):

... and then decompose it to C (x * 1/x) and then C x * C (1/x)

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

Here's a trick: rw (_ : _ - _ = X n * C (p ^ (n + 1)))), {simp}

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

(maybe simp won't kill that goal, you may need to do some more careful rewrites, but it should still be relatively easy)

view this post on Zulip Simon Hudon (Aug 07 2018 at 06:45):

Whaaaa?

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

there should be a simp lemma C(1/x) = 1/C x

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

then simp will kill the goal

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

Too bad:

failed to synthesize type class instance for
 has_sub (mv_polynomial  )

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

It didn't figure out the base ring...

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

You have to add a type ascription

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

or fill it in a bit more, witt_polynomial n - _ = ...

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

@Mario Carneiro I'm not sure if 1/C x makes sense? There is no division in the polynomial ring, right?

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

Or maybe there is, in the sense of Euclidean domains... but that is not what we want here.

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

Oh, I see... C x is a unit of the ring

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

maybe this is why I thought C_mul was not a good simp lemma


Last updated: May 16 2021 at 05:21 UTC