## 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]
(k : R)
(factors : list M)

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
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
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


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