basic struggles

Stream: general

[Johan Commelin]

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].)

[Simon Hudon]

Have you tried mul_right_cancel_iff?

[Johan Commelin]

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

[Johan Commelin]

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

[Simon Hudon]

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.

[Simon Hudon]

If you had a field though ...

[Simon Hudon]

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

[Johan Commelin]

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

[Johan Commelin]

My c has an inverse

[Simon Hudon]

How rude! :)

[Johan Commelin]

I'll copy-paste my goal.

[Johan Commelin]

(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

[Johan Commelin]

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

[Johan Commelin]

I would like to move it to the other side.

[Johan Commelin]

This goal has been misbehaving quite a lot, lately.

[Simon Hudon]

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

(it does look pretty hairy)

[Johan Commelin]

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

[Simon Hudon]

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.

[Simon Hudon]

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

[Johan Commelin]

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

[Simon Hudon]

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

[Johan Commelin]

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.

[Johan Commelin]

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

[Mario Carneiro]

you are thinking backwards

[Simon Hudon]

What if you multiply by C 1 on the right

[Mario Carneiro]

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

[Johan Commelin]

Right

[Johan Commelin]

So I use suffices?

[Simon Hudon]

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

[Mario Carneiro]

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

[Mario Carneiro]

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

[Simon Hudon]

Whaaaa?

[Mario Carneiro]

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

[Mario Carneiro]

then simp will kill the goal

[Johan Commelin]

Too bad:

failed to synthesize type class instance for
⊢ has_sub (mv_polynomial ℕ ℕ)

[Johan Commelin]

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

[Mario Carneiro]

You have to add a type ascription

[Mario Carneiro]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Mario Carneiro]

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

[Mario Carneiro]

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