## Stream: new members

### Topic: Symbolic (non-finite) square matrices

#### Robert Maxton (Apr 14 2022 at 07:44):

Bleh. Okay, I now have an expression
↑6 * kp ^ 2 * km ^ 2
Unfortunately, what this actually says is

@has_mul.mul ℂ (mul_one_class.to_has_mul ℂ) (@has_mul.mul  ℂ (distrib.to_has_mul ℂ) ↑(6: ℕ) (kp ^ 2)) (km ^ 2)


#### Robert Maxton (Apr 14 2022 at 07:45):

and as such is not recognized when I do set kp2m2_6 := 6 * kp ^ 2 * km ^ 2 which is a much saner set of has_mul.mul ℂ ℂs

#### Kevin Buzzard (Apr 14 2022 at 07:45):

Can you post a #mwe ? It's very difficult to help otherwise.

#### Robert Maxton (Apr 14 2022 at 07:46):

I'd like to have something... less perverse if at all possible

uh, hm

#### Robert Maxton (Apr 14 2022 at 07:48):

I mean, I can just type out the exact expression above with a minimal amount of context, but that's a really artifical example?

#### Robert Maxton (Apr 14 2022 at 07:49):

the reason I have to deal with that expression is that it's in the middle of a simplification, so I can't easily just choose a different representation, I don't think...

#### Kevin Buzzard (Apr 14 2022 at 07:53):

Click on the #mwe link if you're not clear about what I mean

#### Robert Maxton (Apr 14 2022 at 07:54):

import tactic algebra.ring.basic data.real.basic
data.complex.basic algebra.star.basic algebra.algebra.basic
analysis.normed_space.star.basic analysis.normed.normed_field
analysis.complex.basic

namespace scratch

section
universe u
parameter (R: Type u)

variables [normed_ring R] [star_ring R] [has_involutive_star R]
[cstar_ring R]
parameters (kp km : ℂ)
variables (ap am xp xm b: R)

variables [normed_algebra ℂ R] [star_module ℂ R]
notation a†:1024 := has_star.star a

instance : has_pow R ℕ := { pow := λ (r: R) (n: ℕ), ring.npow n r }

variables (k : ℂ) (r s t : R)

lemma algebra_pow (n: ℕ): (k • r) ^ n = k ^ n • r ^ n :=
begin
induction n, simp only [pow_zero, one_smul],
repeat {rw pow_succ},
rw n_ih, exact smul_mul_smul k _ r _,
end

example : xp = kp • (ap + ap†) → xm = km • (am + am†)
→ 6 • xp ^ 2 * xm ^ 2 = b :=
begin
introv xp_def xm_def, substs xp_def xm_def,
repeat {rw algebra_pow},
rw ←smul_assoc 6 _ _,
rw smul_mul_smul _ (km ^ 2) _ _,
rw nsmul_eq_mul 6, all_goals {sorry}
end

end
end scratch


#### Robert Maxton (Apr 14 2022 at 07:54):

I mean I'm familiar with the concept of an #mwe, but it's not always clear exactly what "minimal" in fact means in practice

#### Robert Maxton (Apr 14 2022 at 08:32):

for now, I'm just going to suck it up and use set with the overcomplicated definition

#### Robert Maxton (Apr 14 2022 at 08:32):

but ideally I'd reduce the expression instead

#### Eric Wieser (Apr 14 2022 at 08:55):

You shouldn't need the has_pow there

#### Eric Wieser (Apr 14 2022 at 08:56):

And algebra_pow should be docs#smul_pow

#### Robert Maxton (Apr 14 2022 at 09:18):

ah, I was wondering

#### Robert Maxton (Apr 14 2022 at 09:18):

but couldn't find it

#### Robert Maxton (Apr 14 2022 at 09:18):

okay, fixed that, but still looking for a way to simplify that product

#### Eric Wieser (Apr 14 2022 at 10:01):

Can you give an mwe that better indicates exactly what you consider the problem to be?

#### Eric Wieser (Apr 14 2022 at 10:02):

(note your original mwe is false, as b is unconstrained)

#### Eric Wieser (Apr 14 2022 at 10:04):

In particular, it sounds like you're complaining that the set tactic isn't working, but your mwe doesn't demonstrate this because it doesn't mention set!

#### Robert Maxton (Apr 14 2022 at 10:53):

the original mwe is intentionally false, because I'm essentially trying to (ab)use Lean as a simplifier/calculation aid

#### Robert Maxton (Apr 14 2022 at 10:53):

and AFAIK there's no way to just tell Lean "here is what I have, let's just calculate this and see where it goes"

#### Robert Maxton (Apr 14 2022 at 10:55):

Eric Wieser said:

In particular, it sounds like you're complaining that the set tactic isn't working, but your mwe doesn't demonstrate this because it doesn't mention set!

well, the thing I was mentioning involved just looking at the expansion in the infoview

but sure

#### Robert Maxton (Apr 14 2022 at 10:56):

I've tacked on the relevant set line; after that line, the definition is added to the context but no replacements are made

#### Eric Wieser (Apr 14 2022 at 11:09):

If you use set ... with hk, can you rw ←hk to make the replacements?

#### Robert Maxton (Apr 14 2022 at 11:11):

... so I can. Thanks!

#### Eric Wieser (Apr 14 2022 at 11:11):

Looking at the infoview feels like it was going down an #xy problem; the problem seems to be in set not being as clever as rw

#### Eric Wieser (Apr 14 2022 at 11:15):

(in that rw can see through the difference you found in the infoview, but set can't)

#### Jireh Loreaux (Apr 14 2022 at 11:35):

That has_involutive_star variable is also extraneous, which is going to cause you problems because you'll have two star operations on R

#### Robert Maxton (Apr 14 2022 at 13:09):

ah, nice catch, I've been burned a bunch of times by that already -_-

#### Jireh Loreaux (Apr 14 2022 at 16:24):

If you're unsure whether or not you need a low-level class to get a higher-level class (e.g., cstar_ring needs star_ring) one quick trick is to try deleting the low-level class from the variable list. If Lean doesn't complain, it was redundant. This isn't necessarily the best or most fool-proof way of determining this information, but it can help in a pinch.

Last updated: Dec 20 2023 at 11:08 UTC