Working with proofs on eq compiler defns

Stream: new members

[Yakov Pechersky]

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))
      ⟨k, (add_lt_add_iff_right 1).mp hk⟩
      )
  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
  admit
end
--/

[Kevin Buzzard]

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]

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))
      ⟨k, (add_lt_add_iff_right 1).mp hk⟩
      )

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

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]

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

[Yakov Pechersky]

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))
      ⟨k, (add_lt_add_iff_right 1).mp hk⟩
      )

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]

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

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]

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

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]

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]

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]

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

[Scott Morrison]

Seems unlikely.

[Yakov Pechersky]

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

[Yakov Pechersky]

Something like this?

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

[Yakov Pechersky]

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

Not sure how those help with the succ_above.