Zulip Chat Archive

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

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

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

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

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