How to insert definition of a function in a proof

Stream: new members

[Tobias Grosser]

Hi, I again have a simple beginners questions. The definition of

def Gaussian_elimination [decidable_eq α] [has_inv α]:
   Π (m n), matrix (fin m) (fin n) α →
   (matrix (fin m) (fin m) α × matrix (fin n) (fin n) α × nat)
| (x+1) (y+1) A :=
  let optional_ij := pick_encodable (α) (λ el, el ≠ 0) (x+1) (y+1) A in
  match optional_ij with
  | some ij :=
    let i := ij.1 in
    let j := ij.2 in
    let a := A i j in
    let A1 := xrow i 0 (xcol j 0 A) in
    let A1' := fin_swap A1 in
    let B := A1' in
    let u := ursubmx A1' in
    let v := a⁻¹ • dlsubmx A1' in
    let (L, U, r) := Gaussian_elimination (x) (y) (drsubmx A1' - (v *ₘ u)) in
    (
      xrow i 0 (fin_swap (block_mx 1 0 v L)),
      xcol j 0 (fin_swap (block_mx (λ i1 j1, a) u 0 U)),
      r + 1
    )
  | none :=
     (
      (1 : (matrix (fin (x+1)) (fin (x+1)) α)),
      (1 : (matrix (fin (y+1)) (fin (y+1)) α)),
      0
     )
  end
| x y A :=
     (
      (1 : (matrix (fin (x)) (fin (x)) α)),
      (1 : (matrix (fin (y)) (fin (y)) α)),
      0

appears in a proof state:

α : Type,
_inst_5 : ordered_ring α,
_inst_8 : decidable_eq α,
_inst_9 : has_inv α,
_inst_10 : has_one α,
m n : ℕ,
M : matrix (fin m) (fin m) α
⊢ (Gaussian_elimination m m M).fst *ₘ ((Gaussian_elimination m m M).snd).fst = M

I expected a simple rw Gaussian_elimination to inline the definition of Gaussian_eliminatin into the proof. But unfortunately this did not work out. Any ideas what I did wrong?

[Tobias Grosser]

I unfortunately just get "failed"

[Chris Hughes]

It will only reduce if it's applied to m+1 or 0, not m

[Tobias Grosser]

I see.

[Tobias Grosser]

Any quick pointer how I introduce m+1 or 0?

[Tobias Grosser]

Found it. Just need to do 'induction m'.

[Tobias Grosser]

Thanks a lot, this was easy.

[Tobias Grosser]

OK, the basecase is now also proofen. Learned the 'ext' tactic and fin_zero_elim.

[Tobias Grosser]

I am now in

case nat.succ
α : Type,
_inst_5 : ordered_ring α,
_inst_8 : decidable_eq α,
_inst_9 : has_inv α,
_inst_10 : has_one α,
n m_n : ℕ,
m_ih :
  ∀ (M : matrix (fin m_n) (fin m_n) α),
    (Gaussian_elimination m_n m_n M).fst *ₘ ((Gaussian_elimination m_n m_n M).snd).fst = M,
M : matrix (fin (nat.succ m_n)) (fin (nat.succ m_n)) α
⊢ (Gaussian_elimination._match_1 m_n m_n M
         (λ (ij : fin (m_n + 1) × fin (m_n + 1)),
            Gaussian_elimination m_n m_n
              (drsubmx (fin_swap (xrow (ij.fst) 0 (xcol (ij.snd) 0 M))) +
                 -((M (ij.fst) (ij.snd))⁻¹ • dlsubmx (fin_swap (xrow (ij.fst) 0 (xcol (ij.snd) 0 M))) *ₘ
                      ursubmx (fin_swap (xrow (ij.fst) 0 (xcol (ij.snd) 0 M))))))
         (pick_encodable α (λ (el : α), ¬el = 0) (m_n + 1) (m_n + 1) M)).fst *ₘ
      ((Gaussian_elimination._match_1 m_n m_n M
          (λ (ij : fin (m_n + 1) × fin (m_n + 1)),
             Gaussian_elimination m_n m_n
               (drsubmx (fin_swap (xrow (ij.fst) 0 (xcol (ij.snd) 0 M))) +
                  -((M (ij.fst) (ij.snd))⁻¹ • dlsubmx (fin_swap (xrow (ij.fst) 0 (xcol (ij.snd) 0 M))) *ₘ
                       ursubmx (fin_swap (xrow (ij.fst) 0 (xcol (ij.snd) 0 M))))))
          (pick_encodable α (λ (el : α), ¬el = 0) (m_n + 1) (m_n + 1) M)).snd).fst =
    M

[Tobias Grosser]

That seems complicated.

[Tobias Grosser]

In case anybody wants to drop me a bone, this would be appreciated.

[Chris Hughes]

funext is a start

[Tobias Grosser]

Thanks.

[Chris Hughes]

But it looks really complicated.

[Tobias Grosser]

That's what I feel.

[Tobias Grosser]

Maybe I approach this from the wrong angle.

[Chris Hughes]

What is pick_encodable?

[Tobias Grosser]

I basically want to show that " (M : matrix (fin m) (fin m) α) : (getL M) *ₘ (getU M) = M :="

[Tobias Grosser]

That comes from: let optional_ij := pick_encodable (α) (λ el, el ≠ 0) (x+1) (y+1) A in

[Tobias Grosser]

It finds a non-zero element in the matrix.

[Tobias Grosser]

And returns an optional.

[Chris Hughes]

What is getL?

[Tobias Grosser]

def getL [decidable_eq α] [has_inv α] {m n : nat}  (M : matrix (fin n) (fin m) α) :=
  let res := Gaussian_elimination n m M in
  res.1

def getU [decidable_eq α] [has_inv α] {m n : nat}  (M : matrix (fin n) (fin m) α) :=
  let res := Gaussian_elimination n m M in
  res.2.1

[Tobias Grosser]

That's the full algorithm:

def Gaussian_elimination [decidable_eq α] [has_inv α]:
   Π (m n), matrix (fin m) (fin n) α →
   (matrix (fin m) (fin m) α × matrix (fin n) (fin n) α × nat)
| (x+1) (y+1) A :=
  let optional_ij := pick_encodable (α) (λ el, el ≠ 0) (x+1) (y+1) A in
  match optional_ij with
  | some ij :=
    let i := ij.1 in
    let j := ij.2 in
    let a := A i j in
    let A1 := xrow i 0 (xcol j 0 A) in
    let A1' := fin_swap A1 in
    let B := A1' in
    let u := ursubmx A1' in
    let v := a⁻¹ • dlsubmx A1' in
    let (L, U, r) := Gaussian_elimination (x) (y) (drsubmx A1' - (v *ₘ u)) in
    (
      xrow i 0 (fin_swap (block_mx 1 0 v L)),
      xcol j 0 (fin_swap (block_mx (λ i1 j1, a) u 0 U)),
      r + 1
    )
  | none :=
     (
      (1 : (matrix (fin (x+1)) (fin (x+1)) α)),
      (1 : (matrix (fin (y+1)) (fin (y+1)) α)),
      0
     )
  end
| x y A :=
     (
      (1 : (matrix (fin (x)) (fin (x)) α)),
      (1 : (matrix (fin (y)) (fin (y)) α)),
      0
     )

[Tobias Grosser]

It computes a matrix L, a matrix U and the rank of the matrix M.

[Tobias Grosser]

I feel I should proof something simpler.

[Tobias Grosser]

E.g. that the result matrix is in upper triangular form.

[Chris Hughes]

What are xrow and fin_swap and block_mx?

[Tobias Grosser]

https://github.com/tobig/lean-polyhedra/blob/master/src/polyhedra.lean

[Tobias Grosser]

http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.652.3183&rep=rep1&type=pdf

[Tobias Grosser]

Is the relevant paper.

[Tobias Grosser]

I just started playing around with it. See sec 3.1 for the relevant algorithm.

[Chris Hughes]

That is surprising. I was going to say that my instinct would be to do it totally differently, and express each Gaussian elimination operation, as multiplication by a well chosen matrix, and prove the properties of the matrices that correspond to the Gaussian elimination operations. Georges Gonthier probably knows what he's doing though.

[Tobias Grosser]

I am new to lean. Probably this problem is too difficult for now, but I feel I understand matrices so I want to follow a proof that already exists, is interesting and at the same time useful.

[Tobias Grosser]

If you have advices what would be reasonable steps and which parts would be useful for mathlib, that would certainly be helpful.

[Tobias Grosser]

The paper justifies some of the choices they have taken.

[Tobias Grosser]

Now the proof structure itself can likely be changed without affecting everything that uses Gaussian elimination.

[Tobias Grosser]

Would be interesting to see if your proof idea might even be nicer than their original proof idea.

[Tobias Grosser]

I doubt that the proof structure depends a lot on coq vs. lean, but if your proof is more accessible to people less advanced than Georges, this would be interesting to me.

[Mario Carneiro]

My guess is that translating so strictly from Coq is not going to come out well

[Mario Carneiro]

The thing about translations is that even though the axioms are similar, the language, in the informal sense, is different. We use different modes of speech for the same kinds of things

[Mario Carneiro]

and the library is "written in that language", meaning that you will encounter friction if you don't use it

[Scott Morrison]

My student @Jack Crawford has also been looking at gaussian elimination. He's been using an inductive type describing individual steps of row operations.

[Scott Morrison]

It acts like a "relation" between two matrices, but carries the data of the elementary matrix to multiply by.

[Tobias Grosser]

Are you talking about Jack?

[Tobias Grosser]

I mean, I obviously have no idea what the right approach is.

[Tobias Grosser]

Just use this to learn stuff.

[Mario Carneiro]

It might help to try to invent your own gaussian elimination

[Mario Carneiro]

rather than porting from coq

[Mario Carneiro]

Use the coq development and wikipedia to help you with the maths, and just focus on the lean encoding part

[Tobias Grosser]

So you feel my translation from coq is not very ideomatic in lean?

[Mario Carneiro]

that's right

[Tobias Grosser]

It seems to do what I want, so I am reasonably happy with it.

[Mario Carneiro]

in particular, I would work more with fintypes and less with fin n

[Tobias Grosser]

As I don't really know lean, I have zero feeling what would be more ideomatic

[Tobias Grosser]

OK, I can change this. Not sure though if this would change the overall algorithm a lot.

[Mario Carneiro]

I would be curious to hear how Jack is doing things differently

[Tobias Grosser]

It might be interesting to look into the code from @Jack Crawford

[Tobias Grosser]

Yes.

[Tobias Grosser]

He promised to share the code, but his now on exam leave.

[Tobias Grosser]

It seems Scott gave already quite some input on @Jack Crawford 's code, so I assume it is more ideomatic.

[Tobias Grosser]

@Scott Morrison , what is your goal with GE?

[Jack Crawford]

I really need to clean a few things up first and am currently on mobile so don’t have my code with me, but as Scott said, I’m just using inductive types to break row equivalence down into steps

[Jack Crawford]

I’ll share the code as soon as I have it neater and a little more complete

[Tobias Grosser]

Would it make sense to build up a matrix theory similar to http://citeseerx.ist.psu.edu/viewdoc/download?doi=10.1.1.652.3183&rep=rep1&type=pdf

[Tobias Grosser]

mathcomp.mxalgebra?

[Tobias Grosser]

Or is this not even useful in the context of lean?

[Tobias Grosser]

@Jack Crawford , no need to rush.

[Tobias Grosser]

I would be glad to look over your code to learn from it.

[Jack Crawford]

I have an inductive type that represents a single “step” of a row equivalence, with a constructor for scaling, swapping, and linear addition of matrices, and then I have another inductive type that gives me the transitive closure of this.

[Jack Crawford]

Then I have a few functions that perform individual steps of the GE algorithm (putting the pivot in the right place, scaling the pivot, eliminating down the column). Then I show that the result of each of these steps are row-equivalent (by my previous inductive definition of row-equivalence) with the original matrix, and then I make a new function that just combines these steps of the Gaussian elimination in the obvious way, and show that it is also row-equivalent by carrying through my proofs that each of the individual steps that it is composed of is row-equivalent

[Tobias Grosser]

I see.

[Jack Crawford]

and from my row-equivalence I can get the proof that the invertible matrix which represents all of the steps of the row reduction, times the original matrix, is in fact the row-reduced version of the matrix

[Tobias Grosser]

I see,

[Tobias Grosser]

Do you also compute an extended gaussian elimination similar to what 'Georges Gonthier' does?

[Tobias Grosser]

Meaning, do you e.g. have proofs about the rank of the matrix?

[Jack Crawford]

Not yet, I haven’t actually gotten to proving much at all yet because I’ve had to re-write substantial parts of my code a few times over now. Hopefully this will be the final iteration! Haven’t really given much of a thought to matrix rank yet

[Tobias Grosser]

OK. Please ping me when it's time to look at your code.

[Tobias Grosser]

Also, feedback on the Georges paper would be interesting.