How to handle dependent type on Nat?

Stream: Is there code for X?

[Kenny Lau]

import Mathlib

abbrev g : ℕ → Type := fun _ ↦ ℤ
def gMul (i j : ℕ) : g i → g j → g (i + j) := sorry

abbrev g' : ℕ → Type := fun _ ↦ ℚ
def gMul' (i j : ℕ) : g' i → g' j → g' (i + j) := sorry

def map (i : ℕ) : g i → g' i := fun x ↦ x / i

@[simp] lemma map_gMul (i j : ℕ) (x : g i) (y : g j) :
    map (i + j) (gMul i j x y) = gMul' i j (map i x) (map i y) := sorry

def component : g 1 := 3
def big : g 2 := gMul 1 1 component component

@[simp] lemma map_component : map 1 component = 0 := sorry
@[simp] lemma gMul'_eq_zero (i j x y) : gMul' i j x y = 0 := sorry

lemma map_big : map 2 big = 0 := by
  simp [big] -- fails to close the goal
  -- ⊢ map 2 (gMul 1 1 component component) = 0
  simp [map_gMul 1 1] -- works

I have this graded ring structure on my personal repo, which I've minimised to the code above.

My problem here is that the simp lemma map_gMul doesn't match the goal normally (because 1 + 1 is not 2 :shock: ), and I'll have to provide it the custom indices 1 1 to make it work. What's the best way to solve this?

[Eric Wieser]

I assume you're aware of docs#GradedMonoid.GMonoid ?

[Kenny Lau]

ah, i kept it at the back of my head and then forgot it; but how does this get rid of the problem that 2 is not 1+1?

[Jz Pan]

Kenny Lau said:

how does this get rid of the problem that 2 is not 1+1?

I don't think this problem has things to do with dependent type. Even the type is not dependent, your simp [big] is not working:

import Mathlib

abbrev g := ℤ
def gMul (i j : ℕ) : g → g → g := sorry

abbrev g' := ℚ
def gMul' (i j : ℕ) : g' → g' → g' := sorry

def map (i : ℕ) : g → g' := fun x ↦ x / i

@[simp] lemma map_gMul (i j : ℕ) (x y : g) :
    map (i + j) (gMul i j x y) = gMul' i j (map i x) (map i y) := sorry

def component : g := 3
def big : g := gMul 1 1 component component

@[simp] lemma map_component : map 1 component = 0 := sorry
@[simp] lemma gMul'_eq_zero (i j x y) : gMul' i j x y = 0 := sorry

lemma map_big : map 2 big = 0 := by
  simp [big] -- fails to close the goal
  -- ⊢ map 2 (gMul 1 1 component component) = 0
  simp [map_gMul 1 1] -- works

[Eric Wieser]

I think your example is a little too contrived; ideally the types would actually be dependent

[Jz Pan]

Note that rw [map_gMul] following simp [big] is also not working. You need rw [map_gMul 1 1] or erw [map_gMul] to make it work.

[Jz Pan]

erw also works in the original example

[Kenny Lau]

Eric Wieser said:

I think your example is a little too contrived; ideally the types would actually be dependent

well... that's the spirit behind #mwe :upside_down:

[Kenny Lau]

so is there a known solution?

[Jz Pan]

I don't think so; seems that this is because the distinction between rw and erw...

My solution would be simp [big, show 2 = 1 + 1 from rfl] (untested)

[Aaron Liu]

that sounds like it will loop

[Jz Pan]

Oh, 1 + 1 = 2 is a simp lemma

[Ruben Van de Velde]

simp [← one_add_one_eq_two], maybe

[Kenny Lau]

well i have 2+1 in my example too

[Kenny Lau]

is there a way to write a simp procedure to look at the three natural number expressions %k %i %j and try to prove %k = %i + %j by rfl?

[Aaron Liu]

there's already a simproc that does the other way around so you'll be fighting it

[Kenny Lau]

i meant, in the context of this lemma

[Kenny Lau]

so it only activates when it sees map %k (x : g %i) (y : g %j)

[Aaron Liu]

that could work

[Ruben Van de Velde]

You could do this:

import Mathlib

abbrev g := ℤ
def gMul (i j : ℕ) : g → g → g := sorry

abbrev g' := ℚ
def gMul' (i j : ℕ) : g' → g' → g' := sorry

def map (i : ℕ) : g → g' := fun x ↦ x / i

@[simp] lemma map_gMul (i j : ℕ) (x y : g) :
    map (i + j) (gMul i j x y) = gMul' i j (map i x) (map i y) := sorry

lemma map_gMul_of_eq (i j k : ℕ) (x y : g) (hk : k = i + j) :
    map k (gMul i j x y) = gMul' i j (map i x) (map i y) := by
  subst k
  apply map_gMul

def component : g := 3
def big : g := gMul 1 1 component component

@[simp] lemma map_component : map 1 component = 0 := sorry
@[simp] lemma gMul'_eq_zero (i j x y) : gMul' i j x y = 0 := sorry

lemma map_big : map 2 big = 0 := by
  simp [big, map_gMul_of_eq] -- works

(I didn't expect it to just work like that, but maybe that's the simproc mentioned above)

[Kenny Lau]

@Ruben Van de Velde except that that example has been minimised (by others) to get rid of the dependent type; if you tried to do this in my original example you'll end up with a type error

[Ruben Van de Velde]

Well, then you need to unminimize it :)

[Kenny Lau]

@Ruben Van de Velde

import Mathlib

abbrev g : ℕ → Type := fun n ↦ Vector ℤ n
def gMul (i j : ℕ) : g i → g j → g (i + j) := sorry

abbrev g' : ℕ → Type := fun n ↦ Vector ℚ n
def gMul' (i j : ℕ) : g' i → g' j → g' (i + j) := sorry

instance : Zero (g' n) where
  zero := Vector.mk (Array.mk (List.iterate id 0 n)) (by simp)

def map (i : ℕ) : g i → g' i := fun v ↦ v.map (fun x : ℤ ↦ x / i)

@[simp] lemma map_gMul (i j : ℕ) (x : g i) (y : g j) :
    map (i + j) (gMul i j x y) = gMul' i j (map i x) (map j y) := sorry

lemma map_gMul_of_eq (i j k : ℕ) (x : g i) (y : g j) (hk : k = i + j) :
    map k (gMul i j x y) = gMul' i j (map i x) (map j y) := by
  subst k
  apply map_gMul

def component : g 1 := Vector.mk (Array.mk [3]) rfl
def big : g 2 := gMul 1 1 component component

@[simp] lemma map_component : map 1 component = 0 := sorry
@[simp] lemma gMul'_eq_zero (i j x y) : gMul' i j x y = 0 := sorry

lemma map_big : map 2 big = 0 := by
  simp [big] -- fails to close the goal
  -- ⊢ map 2 (gMul 1 1 component component) = 0
  simp [map_gMul 1 1] -- works

[Kenny Lau]

Eric Wieser said:

I assume you're aware of docs#GradedMonoid.GMonoid ?

now I have an idea in my head of how to make this all work using the sigma type, lemme try it...

[Kenny Lau]

in particular, I have a proposal to (the underlying thing would be a graded algebra, but I want to always keep it homogeneous):

1. Only ever multiply things together in the sigma type
2. Only ever add things together in the individual modules

[Kenny Lau]

Update: it almost worked, if not for the fact that GradedMonoid.snd_mul is tagged with @[simp], and I don't know if attribute [-simp] is a good idea...