## Stream: new members

### Topic: Working with proofs on eq compiler defns

#### Yakov Pechersky (Jul 16 2020 at 18:40):

What's the way to simplify the _match statement in the proof below? The #reduce gives basically the right answer modulo some cancellations, so I wonder what the hang-up is.

import data.matrix.notation
import data.real.basic

universe u
variables {R : Type*} [field R]
variables {n : ℕ}

variables (a b c d : R)
variables (A B : matrix (fin n) (fin n) R)

open_locale matrix big_operators
open matrix

def det' {R : Type*} [field R] :
Π {n : ℕ}, matrix (fin n) (fin n) R -> fin n -> R
| 0 _ _ := 1
| 1 M i := M i i
| (n + 2) M i :=
match i with
| ⟨0, h⟩  := ∑ j, (M i j * (-1 : R) ^ (i.val + j.val) * det' (minor M (fin.succ_above i) (fin.succ_above j)) 0)
| ⟨k + 1, hk⟩ := ∑ j, (M i j * (-1 : R) ^ (i.val + j.val) * det' (minor M (fin.succ_above i) (fin.succ_above j))
)
end

-- this seems to work
#reduce det' ![![a, b], ![c, d]] 0
-- field.add (field.mul (field.mul a field.one) d)
-- (field.add (field.mul (field.mul b (field.mul (field.neg field.one) field.one)) c) field.zero)

example {R : Type*} [field R] {a b c d : R} {n' : ℕ} : det' ![![a, b], ![c, d]] 0 = a * d - b * c :=
begin
simp [det', minor, vec_cons],
sorry,
end

/-
example {R : Type ?} {n' : ℕ}
[field R]
{a b c d : R} :
det'._match_1 0
(fin.cons (fin.cons a (fin.cons b vec_empty))
(fin.cons (fin.cons c (fin.cons d vec_empty)) vec_empty))
0
(λ (h : 0 < 0 + 2) (j : fin (0 + 2)),
fin.cons (fin.cons a (fin.cons b vec_empty))
(fin.cons (fin.cons c (fin.cons d vec_empty)) vec_empty)
(0.succ_above 0)
(j.succ_above 0))
(λ (k : ℕ) (hk : k + 1 < 0 + 2) (j : fin (0 + 2)),
fin.cons (fin.cons a (fin.cons b vec_empty))
(fin.cons (fin.cons c (fin.cons d vec_empty)) vec_empty)
(0.succ_above ⟨k, _⟩)
(j.succ_above ⟨k, _⟩))
0 =
a * d - b * c :=
begin
end
--/


#### Kevin Buzzard (Jul 16 2020 at 21:03):

Can you not just put | (n + 2) M ⟨0, h⟩ := ... | (n + 2) M ⟨k + 1, hk⟩ := ... in the definition, and avoid match? Just a guess.

#### Yakov Pechersky (Jul 16 2020 at 22:21):

Okay, this works. But how is#reduce able to reduce through the sum, but I have to go through the calc, rw step?

import data.matrix.notation
import data.real.basic

universe u
variables {R : Type*} [field R]
variables {n : ℕ}

variables (a b c d : R)
variables (A B : matrix (fin n) (fin n) R)

open_locale matrix big_operators
open matrix

def det' {R : Type*} [field R] :
Π {n : ℕ}, matrix (fin n) (fin n) R -> fin n -> R
| 0 _ _ := 1
| 1 M i := M i i
| (n + 2) M ⟨0, h⟩ := ∑ j, (M 0 j * (-1 : R) ^ (j.val) * det' (minor M (fin.succ_above ⟨0, h⟩) (fin.succ_above j)) 0)
| (n + 2) M ⟨k + 1, hk⟩ := ∑ j, (M ⟨k + 1, hk⟩ j * (-1 : R) ^ (k + 1 + j.val) * det' (minor M (fin.succ_above ⟨k + 1, hk⟩) (fin.succ_above j))
)

-- this seems to work
#reduce det' ![![a, b], ![c, d]] 0
-- field.add (field.mul (field.mul a field.one) d)
-- (field.add (field.mul (field.mul b (field.mul (field.neg field.one) field.one)) c) field.zero)

example {R : Type*} [field R] {a b c d : R} {n' : ℕ} : det' ![![a, b], ![c, d]] 0 = a * d - b * c :=
begin
dunfold det',
have : ∀ f : fin 2 → R, ∑ x : fin 2, f x = f 0 + f 1, by
{ intro f,
calc ∑ x : fin 2, f x = _ + _ : rfl
...                   = f 0 + f 1 : by { simp, ring } },
rw this,
simpa,
end


#### Kevin Buzzard (Jul 16 2020 at 22:33):

Maybe you can show what #reduce is printing out (there seem to be some negs and ones in there) and go on from there?

#### Scott Morrison (Jul 17 2020 at 01:50):

There's a unfold_aux tactic which is sometimes helpful in these situations.

#### Yakov Pechersky (Jul 17 2020 at 02:26):

I'm not sure where you would place the unfold_aux tactic. (Also, it's not listed in the docs at https://leanprover-community.github.io/mathlib_docs/tactics.html). I thought I would be able to also show the equivalent result for 3 dimensional matrices, but something is up with the arrangement of terms. The #reduce line for 3 dimensions seems like it works still.

import data.matrix.notation
import data.real.basic

universe u
variables {R : Type*} [field R]
variables {n : ℕ}

variables (a b c d : R)
variables (A B : matrix (fin n) (fin n) R)

open_locale matrix big_operators
open matrix

def det' {R : Type*} [field R] :
Π {n : ℕ}, matrix (fin n) (fin n) R -> fin n -> R
| 0 _ _ := 1
| 1 M i := M i i
| (n + 2) M ⟨0, h⟩ := ∑ j, (M 0 j * (-1 : R) ^ (j.val) * det' (minor M (fin.succ_above ⟨0, h⟩) (fin.succ_above j)) 0)
| (n + 2) M ⟨k + 1, hk⟩ := ∑ j, (M ⟨k + 1, hk⟩ j * (-1 : R) ^ (k + 1 + j.val) * det' (minor M (fin.succ_above ⟨k + 1, hk⟩) (fin.succ_above j))
)

example {R : Type*} [field R] {a b c d : R} {n' : ℕ} : det' ![![a, b], ![c, d]] 0 = a * d - b * c :=
begin
dunfold det',
have : ∀ f : fin 2 → R, ∑ x : fin 2, f x = f 0 + f 1, by
{ intro f,
calc ∑ x : fin 2, f x = _ + _ : rfl
...                   = f 0 + f 1 : by { simp, ring } },
rw this,
simpa,
end

variables {e f g h i: R}

#reduce det' ![![a, b, c], ![d, e, f], ![g, h, i]] 0

example {R : Type*} [field R] {a b c d e f g h i: R} {n' : ℕ} :
det' ![![a, b, c], ![d, e, f], ![g, h, i]] 0 =
a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g :=
begin
dunfold det',
have f3 : ∀ f : fin 3 → R, ∑ x : fin 3, f x = f 0 + f 1 + f 2, by
{ intro f,
calc ∑ x : fin 3, f x = _ + _: rfl
...                   = f 0 + f 1 + f 2: by { simp, ring } },
rw f3,
have f2 : ∀ f : fin 2 → R, ∑ x : fin 2, f x = f 0 + f 1, by
{ intro f,
calc ∑ x : fin 2, f x = _ + _ : rfl
...                   = f 0 + f 1 : by { simp, ring } },
rw f2,
abel,
simp,
sorry,
end


#### Scott Morrison (Jul 17 2020 at 02:32):

@Bryan Gin-ge Chen I don't actually know this --- what do we need to do to make core tactics appear in the mathlib documentation?

#### Scott Morrison (Jul 17 2020 at 02:50):

What if you add lots of lemmas like

lemma foo : (1 : fin 2).succ_above (0 : fin 1) = (2 : fin 2) := rfl


Then dsimp [minor], dsimp [foo] makes some further progress.

#### Bryan Gin-ge Chen (Jul 17 2020 at 03:07):

@Scott Morrison We've been putting tactic doc entries for core tactics in tactic.lean_core_docs (Thanks to @Kevin Buzzard for adding these!).

#### Yakov Pechersky (Jul 21 2020 at 05:14):

I couldn't get the rewriting of the 0.succ_above 0 deep in the statement to work, so I just used local notation on the #reduce statement to help generate this:

example {R : Type*} [field R] {a b c d e f g h i: R} {n' : ℕ} :
det' ![![a, b, c], ![d, e, f], ![g, h, i]] 0 =
a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g :=
calc det' ![![a, b, c], ![d, e, f], ![g, h, i]] 0 = _ : rfl
... = a * 1 * (e * 1 * i + (f * (- 1 * 1) * h + 0)) +
(b * (- 1 * 1) * (d * 1 * i + (f * (- 1 * 1) * g + 0)) +
(c * (- 1 * (- 1 * 1)) * (d * 1 * h + (e * (- 1 * 1) * g + 0)) + 0)) : rfl
... = a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g : by { simp, ring }


#### Yakov Pechersky (Jul 21 2020 at 05:53):

Ah, just needed a lot more of these intermediate rfl lemmas:

example {R : Type*} [field R] {a b c d e f g h i : R} {n' : ℕ} :
det' ![![a, b, c], ![d, e, f], ![g, h, i]] 0 =
a * e * i - a * f * h - b * d * i + b * f * g + c * d * h - c * e * g :=
begin
dunfold det',
have f3 : ∀ f : fin 3 → R, ∑ x : fin 3, f x = f 0 + f 1 + f 2, by
{ intro f,
calc ∑ x : fin 3, f x = _ + _: rfl
...                   = f 0 + f 1 + f 2: by { simp, ring } },
rw f3,
have f2 : ∀ f : fin 2 → R, ∑ x : fin 2, f x = f 0 + f 1, by
{ intro f,
calc ∑ x : fin 2, f x = _ + _ : rfl
...                   = f 0 + f 1 : by { simp, ring } },
simp only [f2],
have l00 : (0 : fin 2).succ_above (0 : fin 1) = 1 := rfl,
have l00' : (0 : fin 3).succ_above (0 : fin 2) = 1 := rfl,
have l10' : (1 : fin 2).succ_above (0 : fin 1) = 0 := rfl,
have l10 : (1 : fin 3).succ_above (0 : fin 2) = 0 := rfl,
have l11 : (1 : fin 3).succ_above (1 : fin 2) = 2 := rfl,
have l20 : (2 : fin 3).succ_above (0 : fin 2) = 0 := rfl,
have l21 : (2 : fin 3).succ_above (1 : fin 2) = 1 := rfl,
have l01' : (0 : fin 3).succ_above (1 : fin 2) = 2 := rfl,
have l0 : ((⟨0, by norm_num⟩) : fin 2).succ_above (0 : fin 1) = 1 := rfl,
have l0' : ((⟨0, by norm_num⟩) : fin 3).succ_above (0 : fin 2) = 1 := rfl,
have l1' : ((⟨0, by norm_num⟩) : fin 3).succ_above (1 : fin 2) = 2 := rfl,
have hv : ∀ k l m : R, ![k, l, m] 2 = m := by { intros, simpa },
have hc : ∀ k : R, (λ (i : fin 1), k) = ![k] := by { intros, ext, simp },
dsimp [minor],
simp [l00, l00', l01', l0, l0', l1', l10, l11, l20, l21, l10', hv, hc],
ring
end


#### Yakov Pechersky (Jul 21 2020 at 05:54):

Not sure why simp isn't firing on a lot of those rfl lemmas. I couldn't find a place to use unfold_aux.

#### Scott Morrison (Jul 21 2020 at 06:31):

Can you write some simp lemmas in terms of bit0 and bit1?

Seems unlikely.

#### Yakov Pechersky (Jul 21 2020 at 06:39):

There'd have to be some ite going on in those lemmas. Maybe.

#### Yakov Pechersky (Jul 21 2020 at 07:19):

Something like this?

example {n : ℕ} : ∀ k : fin n, (bit0 k).val = bit0 (k.val) % n
| ⟨_, _⟩ := rfl


#### Yakov Pechersky (Jul 21 2020 at 07:36):

@[simp] lemma bit0_val {n : ℕ} : ∀ k : fin n, (bit0 k).val = bit0 (k.val) % n
| ⟨_, _⟩ := rfl

@[simp] lemma bit1_val {n : ℕ} : ∀ k : fin (n + 1), (bit1 k).val = (bit1 (k.val)) % (n + 1)
| ⟨_, _⟩ := by simp [bit1, bit0, fin.add_def, fin.one_val]


#### Yakov Pechersky (Jul 21 2020 at 07:38):

Not sure how those help with the succ_above.

Last updated: May 14 2021 at 03:27 UTC