# Zulip Chat Archive

## Stream: new members

### Topic: Rewriting `fin n` in summations

#### Eric Wieser (Nov 20 2020 at 18:18):

Apologies for the long-winded non-m we:

```
import linear_algebra.clifford_algebra
import group_theory.perm.sign
variables {R : Type*} [comm_ring R]
variables {M : Type*} [add_comm_group M] [module R M]
variables {Q : quadratic_form R M}
open_locale big_operators
open clifford_algebra
variables (Q)
include Q
@[ext]
structure blade.pre :=
(k : R)
(factors : list M)
namespace blade
namespace pre
instance : monoid (pre Q) :=
{ mul := λ a b, ⟨a.k * b.k, a.factors ++ b.factors⟩,
one := ⟨1, []⟩,
mul_assoc := λ a b c, pre.ext _ _ (mul_assoc _ _ _) (list.append_assoc _ _ _),
one_mul := λ a, pre.ext _ _ (one_mul _) (list.nil_append _),
mul_one := λ a, pre.ext _ _ (mul_one _) (list.append_nil _) }
instance : mul_action R (pre Q) :=
{ smul := λ k a, ⟨k * a.k, a.factors⟩,
mul_smul := λ x y k, pre.ext _ _ (mul_assoc _ _ _) rfl,
one_smul := λ x, pre.ext _ _ (one_mul _) rfl }
@[simp]
lemma mul_factors (a b : pre Q) : (a * b).factors = a.factors ++ b.factors := rfl
@[simp]
lemma mul_k (a b : pre Q) : (a * b).k = a.k * b.k := rfl
variables {Q}
def eval (b : blade.pre Q) : clifford_algebra Q :=
b.k • ∑ σ : equiv.perm (fin b.factors.length),
(equiv.perm.sign σ : ℤ) • (b.factors.map (ι Q)).prod
variables (Q)
def of (m : M) : blade.pre Q := ⟨1, [m]⟩
variables {Q}
@[simp]
def of_k (m : M) : (of Q m).k = 1 := rfl
@[simp]
def of_factors (m : M) : (of Q m).factors = [m] := rfl
lemma eval_mul_of (a b : blade.pre Q) (h : a.eval = b.eval) (m : M) : (a * of Q m).eval = (b * of Q m).eval :=
begin
dunfold blade.pre.eval at ⊢ h,
dsimp at ⊢ h,
simp, -- HERE
have : (a.factors ++ (of Q m).factors).length = a.factors.length.succ := by simp,
-- subst this, --fails
sorry,
end
lemma eval_mul_eq (a b c : blade.pre Q) (h : a.eval = b.eval) : (a * c).eval = (b * c).eval :=
begin
dunfold blade.pre.eval at ⊢ h,
dsimp at ⊢ h,
simp, -- HERE
induction c.factors,
{ rw [mul_comm _ c.k, mul_comm _ c.k, mul_smul, mul_smul],
have h := congr_arg ((•) c.k) h,
convert h, -- creates 18 goals!!
repeat {sorry} -- new tactic, `very_sorry`?
},
sorry
end
end pre
end blade
```

On the lines marked `HERE`

, the goal contains some obviously simplifiable subexpressions of the form `(a ++ b).length`

. However, I can't work out any way to rewrite them with `list.length_append`

, and attempting to hammer the problem with `convert`

yields a ridiculous number of very similar goals.

#### Yakov Pechersky (Nov 20 2020 at 18:21):

Taking a look now. But it might work if you replace the `fin long-value-here`

with a `fin k`

, then induct on `k`

#### Yakov Pechersky (Nov 20 2020 at 18:22):

You need to have some way of breaking down a sum over equiv.perm, a la `fin.sum_univ_succ`

. Been thinking of making one, but haven't gotten there yet.

#### Eric Wieser (Nov 20 2020 at 18:23):

Right, obviously I'm missing a lot of lemmas to do the full proof here

#### Eric Wieser (Nov 20 2020 at 18:23):

But I'm annoyed that I can't apply the lemmas that I do have (`list.length_append`

, `of_factors`

, etc) to simplify the problem a little

#### Yakov Pechersky (Nov 20 2020 at 18:23):

Maybe have a lemma that distributes `eval`

over a `*`

?

#### Eric Wieser (Nov 20 2020 at 18:24):

I don't think it distributes in any helpful way

#### Eric Wieser (Nov 20 2020 at 18:26):

Also my definition is wrong anyway - this question is about the rewrites, rather than whether my definitions make sense

#### Yakov Pechersky (Nov 20 2020 at 18:31):

One of the issues is that the summands are on different types.

#### Eric Wieser (Nov 20 2020 at 18:34):

Yeah, that probably is where the pain is

#### Eric Wieser (Nov 20 2020 at 18:34):

So perhaps summing over some mix of `list.range`

and `list.permutations`

would work better

#### Yakov Pechersky (Nov 20 2020 at 18:55):

The docs in `data/equiv/basic`

say `group structure on equiv.perm α. More lemmas about equiv.perm can be found in data/equiv/perm.`

but I can't find that `data/equiv/perm`

file

#### Bryan Gin-ge Chen (Nov 20 2020 at 19:06):

Hmm, it seems that `data/equiv/perm`

didn't even exist when that module doc was added: https://github.com/leanprover-community/mathlib/tree/3f7bf3ca2284d614ee2119edebd5d3db7f923803/src/data/equiv

#### Bryan Gin-ge Chen (Nov 20 2020 at 19:09):

@Yury G. Kudryashov do you know which file you meant to refer to in that module doc?

(As the reviewer of that PR, I should have asked this much earlier :sweat_smile: )

#### Bryan Gin-ge Chen (Nov 20 2020 at 19:16):

The files in `group_theory/perm`

might fit the bill.

#### Yury G. Kudryashov (Nov 22 2020 at 07:48):

I'm sorry for the typo.

Last updated: May 18 2021 at 16:25 UTC