Zulip Chat Archive

Stream: new members

Topic: Working with proofs on eq compiler defns


view this post on Zulip 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))
      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
--/

view this post on Zulip 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.

view this post on Zulip 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))
      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

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Jul 17 2020 at 01:50):

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

view this post on Zulip 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))
      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

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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!).

view this post on Zulip 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 }

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Scott Morrison (Jul 21 2020 at 06:31):

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

view this post on Zulip Scott Morrison (Jul 21 2020 at 06:37):

Seems unlikely.

view this post on Zulip Yakov Pechersky (Jul 21 2020 at 06:39):

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

view this post on Zulip Yakov Pechersky (Jul 21 2020 at 07:19):

Something like this?

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

view this post on Zulip 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]

view this post on Zulip 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