Rewriting `fin n` in summations

Stream: new members

[Eric Wieser]

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]

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]

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]

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

[Eric Wieser]

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]

Maybe have a lemma that distributes eval over a *?

[Eric Wieser]

I don't think it distributes in any helpful way

[Eric Wieser]

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

[Yakov Pechersky]

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

[Eric Wieser]

Yeah, that probably is where the pain is

[Eric Wieser]

So perhaps summing over some mix of list.range and list.permutations would work better

[Yakov Pechersky]

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]

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]

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

The files in group_theory/perm might fit the bill.

[Yury G. Kudryashov]

I'm sorry for the typo.