TypePow

Stream: mathlib4

[Kenny Lau]

abbrev TypePow (α : Type u) : Nat → Type u
| 0 => PUnit
| 1 => α
| (n+1) => α × TypePow α n

example {α : Type u} : TypePow α 3 = (α × α × α) := rfl

#check ((3, 4, 5) : TypePow Nat 3)

[Kenny Lau]

In #maths > Projective Space I briefly touched on the possibility of having type power. What do yall think? Would this be a good idea to replace the current idiom Fin n -> R?

[Kevin Buzzard]

IIRC we had this in LTE but it was filed under "hacks".

[Kenny Lau]

The advantage of this is that this would enable us to reason about R^n while not sacrificing usability for low-dimension cases. For example, we can prove that each R^n is a module, but we can still construct explicit elements of R^3.

[Kenny Lau]

what is LTE?

[Aaron Liu]

Kenny Lau said:

The advantage of this is that this would enable us to reason about R^n while not sacrificing usability for low-dimension cases. For example, we can prove that each R^n is a module, but we can still construct explicit elements of R^3.

We can also construct elements of Fin n → ℝ with the vector notation

[Kenny Lau]

@Aaron Liu This is after @David Ang discovered that R × R × R is better behaved than Fin 3 -> R and it makes more things defeq, and he has an open PR doing that refactor on elliptic curves. He is probably in a better position than me to explain why R × R × R is better.

[Aaron Liu]

Well I guess there's the eta unfolding but I don't see anything else right now

[David Ang]

My justification is in #maths > thoughts on elliptic curves @ 💬.

[Aaron Liu]

that link is broken nvm you fixed it

[David Ang]

Yeah I just realised all my old links to Zulip posts are broken (sorry Kenny! I'm fixing them now)

[Kevin Buzzard]

LTE is this https://github.com/leanprover-community/lean-liquid/blob/master/src/hacks_and_tricks/type_pow.lean but I am wrong -- it seems that we just used Fin n -> X.

[Kenny Lau]

David Ang said:

My justification is in #maths > thoughts on elliptic curves @ 💬.

I like how nobody in that thread has even thought about my proposed solution

[David Ang]

Would be nice if we have the abbrev .thd for your solution :)

[Kenny Lau]

@David Ang I tried to read the thread, I saw you said that this causes a lot of theorems to need erw; would you have an example of that? I think it would be easier for me to contextualise the whole situation if I'm presented with a concrete example of what actually breaks without the defeq

[Kenny Lau]

David Ang said:

Would be nice if we have the abbrev .thd for your solution :)

for that, Johan's suggestion with 11 thumbs up is to define .x .y .z specialised for elliptic curves. is that a good idea?

[David Ang]

Yeah, that's what I have in #24593

[David Ang]

An example of erw that I removed is here but I don't remember if that was one of the annoying ones.

[David Ang]

In any case I argue that ![x, y, z] 2 and z should be equal in some strong sense (e.g. definitionally) and shouldn't need a bunch of Matrix.head/tail_cons rewrites

[Eric Wieser]

Wish granted?

import Mathlib

example {x y z : α} : ![x, y, z] 2 = z := rfl

[Eric Wieser]

There is even a dsimproc that performs the simplification

[David Ang]

Yeah I guess I don't just mean definitionally, but something that can be rewritten over (I don't remember what this is called)

[Eric Wieser]

docs#Matrix.cons_val is that "rewrite":

example {x y z ret : α} (h : ret = z) : ![x, y, z] 2 = ret := by
  simp_rw [Matrix.cons_val]
  exact h.symm

[Aaron Liu]

What kind of rewriting? I know for rw if the head symbols don't match it doesn't even try.

[David Ang]

Yes, that's precisely the thing I'm trying to avoid - it shouldn't need a rewrite at all

[Eric Wieser]

I think you're going to have to make a mwe to make your point

[David Ang]

I don't have time to make an MWE right now but it's embedded in the permalink to my PR above. But in general:

lemma fin3_def {R : Type} [CommRing R] (P : Fin 3 → R) : ![P 0, P 1, P 2] = P := by ext n; fin_cases n <;> rfl
lemma smul_fin3 {R : Type} [CommRing R] (P : Fin 3 → R) (u : R) : u • P = ![u * P 0, u * P 1, u * P 2] := by simp [← List.ofFn_inj]

These should be rfl in my opinion

[Eric Wieser]

Best I can do is

import Mathlib

lemma fin3_def {R : Type} [CommRing R] (P : Fin 3 → R) : ![P 0, P 1, P 2] = P :=
  FinVec.etaExpand_eq _
lemma smul_fin3 {R : Type} [CommRing R] (P : Fin 3 → R) (u : R) : u • P = ![u * P 0, u * P 1, u * P 2] :=
  FinVec.etaExpand_eq _ |>.symm

[David Ang]

My point is that with the product construction (at least for R x R x R), these are true by rfl

[David Ang]

So the issue is really with eta expansion not being a rfl, but I guess there's not much we can do there

[Eric Wieser]

It's not clear to me how this translates to needing erw

[Eric Wieser]

erw only helps when things are rfl but not with_reducible rfl

[David Ang]

Yeah definitely! I'm saying I don't have time to make an MWE because I have deadlines coming and referred you to my link, so I just gave the simplest thing I wanted to hold

[Kenny Lau]

import Mathlib

universe u

abbrev TypePow (α : Type u) : ℕ → Type u
  | 0 => PUnit
  | 1 => α
  | (n+2) => α × TypePow α (n+1)

lemma typePow_succ {α n} : TypePow α (n+2) = (α × (TypePow α (n+1))) := rfl

#check fun α : Type u ↦ α ^ 3 -- check that it has not been defined

instance : Pow (Type u) ℕ :=
  ⟨TypePow⟩

example {α : Type u} : α ^ 3 = (α × α × α) := rfl

#check ((3, 4, 5) : ℕ ^ 3)

def TypePow.get {α : Type u} : {n : ℕ} → α ^ n → Fin n → α
  | 0, _, i => i.elim0
  | 1, x, _ => x
  | (_+2), x, i => Fin.cases x.1 (get x.2) i

def test : ℕ ^ 3 := (3, 4, 5)

#eval test.get -- ![3, 4, 5]
#eval test.get 0 -- 3
#eval test.get 1 -- 4
#eval test.get 2 -- 5

def TypePow.smul {α : Type u} {β : Type v} [SMul α β] (r : α) : {n : ℕ} → β ^ n → β ^ n
  | 0, _ => PUnit.unit
  | 1, x => r • x
  | (_+2), x => (r • x.1, smul r x.2)

instance (α : Type u) (β : Type v) [SMul α β] (n : ℕ) : SMul α (β ^ n) :=
  ⟨fun r x ↦ TypePow.smul r x⟩

example {α β : Type*} [SMul α β] (r : α) (x : β ^ 3) :
    r • x = (r • TypePow.get x 0, r • x.get 1, r • x.get 2) :=
  rfl

[Kenny Lau]

not sure if this is 100% desirable, maybe there's some implementation details

[Kenny Lau]

it definitely needs polishing, so let's steer the topic back to whether we want this in mathlib

[Aaron Liu]

well we already have docs#List.TProd

[Kenny Lau]

Aaron Liu said:

well we already have docs#List.TProd

that is not good, I specifically used three cases to make sure that α ^ 1 is defeq to α!

[Eric Wieser]

I think we could easily change TProd to do the same thing, but it's not clear to me that there's any motivation for this defeq

[Kenny Lau]

Eric Wieser said:

I think we could easily change TProd to do the same thing, but it's not clear to me that there's any motivation for this defeq

so that you can write ((3, 4, 5) : ℕ ^ 3)