Symbolic (non-finite) square matrices

Stream: new members

[Robert Maxton]

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]

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]

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

[Robert Maxton]

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

[Robert Maxton]

uh, hm

[Robert Maxton]

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]

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]

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

[Robert Maxton]

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]

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]

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

[Robert Maxton]

but ideally I'd reduce the expression instead

[Eric Wieser]

You shouldn't need the has_pow there

[Eric Wieser]

And algebra_pow should be docs#smul_pow

[Robert Maxton]

ah, I was wondering

[Robert Maxton]

but couldn't find it

[Robert Maxton]

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

[Eric Wieser]

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

[Eric Wieser]

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

[Eric Wieser]

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]

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

[Robert Maxton]

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]

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]

but sure

[Robert Maxton]

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]

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

[Robert Maxton]

... so I can. Thanks!

[Eric Wieser]

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]

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

[Jireh Loreaux]

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]

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

[Jireh Loreaux]

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.