Zulip Chat Archive

Stream: new members

Topic: How to insert definition of a function in a proof


Tobias Grosser (Oct 20 2018 at 00:50):

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 (Oct 20 2018 at 00:52):

I unfortunately just get "failed"

Chris Hughes (Oct 20 2018 at 01:02):

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

Tobias Grosser (Oct 20 2018 at 01:05):

I see.

Tobias Grosser (Oct 20 2018 at 01:05):

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

Tobias Grosser (Oct 20 2018 at 01:07):

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

Tobias Grosser (Oct 20 2018 at 01:08):

Thanks a lot, this was easy.

Tobias Grosser (Oct 20 2018 at 01:52):

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

Tobias Grosser (Oct 20 2018 at 01:52):

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 (Oct 20 2018 at 01:52):

That seems complicated.

Tobias Grosser (Oct 20 2018 at 01:53):

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

Chris Hughes (Oct 20 2018 at 02:32):

funext is a start

Tobias Grosser (Oct 20 2018 at 02:32):

Thanks.

Chris Hughes (Oct 20 2018 at 02:32):

But it looks really complicated.

Tobias Grosser (Oct 20 2018 at 02:33):

That's what I feel.

Tobias Grosser (Oct 20 2018 at 02:34):

Maybe I approach this from the wrong angle.

Chris Hughes (Oct 20 2018 at 02:34):

What is pick_encodable?

Tobias Grosser (Oct 20 2018 at 02:34):

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

Tobias Grosser (Oct 20 2018 at 02:35):

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

Tobias Grosser (Oct 20 2018 at 02:35):

It finds a non-zero element in the matrix.

Tobias Grosser (Oct 20 2018 at 02:36):

And returns an optional.

Chris Hughes (Oct 20 2018 at 02:36):

What is getL?

Tobias Grosser (Oct 20 2018 at 02:36):

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 (Oct 20 2018 at 02:37):

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 (Oct 20 2018 at 02:37):

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

Tobias Grosser (Oct 20 2018 at 02:41):

I feel I should proof something simpler.

Tobias Grosser (Oct 20 2018 at 02:41):

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

Chris Hughes (Oct 20 2018 at 02:48):

What are xrow and fin_swap and block_mx?

Tobias Grosser (Oct 20 2018 at 02:56):

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

Tobias Grosser (Oct 20 2018 at 03:01):

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

Tobias Grosser (Oct 20 2018 at 03:01):

Is the relevant paper.

Tobias Grosser (Oct 20 2018 at 03:02):

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

Chris Hughes (Oct 20 2018 at 03:08):

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 (Oct 20 2018 at 03:10):

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 (Oct 20 2018 at 03:10):

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

Tobias Grosser (Oct 20 2018 at 03:11):

The paper justifies some of the choices they have taken.

Tobias Grosser (Oct 20 2018 at 03:12):

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

Tobias Grosser (Oct 20 2018 at 03:12):

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

Tobias Grosser (Oct 20 2018 at 03:14):

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 (Oct 20 2018 at 03:23):

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

Mario Carneiro (Oct 20 2018 at 03:24):

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 (Oct 20 2018 at 03:24):

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

Scott Morrison (Oct 20 2018 at 03:25):

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 (Oct 20 2018 at 03:25):

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

Tobias Grosser (Oct 20 2018 at 03:26):

Are you talking about Jack?

Tobias Grosser (Oct 20 2018 at 03:26):

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

Tobias Grosser (Oct 20 2018 at 03:26):

Just use this to learn stuff.

Mario Carneiro (Oct 20 2018 at 03:26):

It might help to try to invent your own gaussian elimination

Mario Carneiro (Oct 20 2018 at 03:26):

rather than porting from coq

Mario Carneiro (Oct 20 2018 at 03:27):

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

Tobias Grosser (Oct 20 2018 at 03:28):

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

Mario Carneiro (Oct 20 2018 at 03:28):

that's right

Tobias Grosser (Oct 20 2018 at 03:28):

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

Mario Carneiro (Oct 20 2018 at 03:28):

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

Tobias Grosser (Oct 20 2018 at 03:28):

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

Tobias Grosser (Oct 20 2018 at 03:29):

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

Mario Carneiro (Oct 20 2018 at 03:29):

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

Tobias Grosser (Oct 20 2018 at 03:30):

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

Tobias Grosser (Oct 20 2018 at 03:30):

Yes.

Tobias Grosser (Oct 20 2018 at 03:30):

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

Tobias Grosser (Oct 20 2018 at 03:31):

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

Tobias Grosser (Oct 20 2018 at 03:31):

@Scott Morrison , what is your goal with GE?

Jack Crawford (Oct 20 2018 at 03:31):

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 (Oct 20 2018 at 03:31):

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

Tobias Grosser (Oct 20 2018 at 03:32):

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 (Oct 20 2018 at 03:32):

mathcomp.mxalgebra?

Tobias Grosser (Oct 20 2018 at 03:32):

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

Tobias Grosser (Oct 20 2018 at 03:33):

@Jack Crawford , no need to rush.

Tobias Grosser (Oct 20 2018 at 03:33):

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

Jack Crawford (Oct 20 2018 at 03:34):

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 (Oct 20 2018 at 03:37):

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 (Oct 20 2018 at 03:37):

I see.

Jack Crawford (Oct 20 2018 at 03:38):

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 (Oct 20 2018 at 03:39):

I see,

Tobias Grosser (Oct 20 2018 at 03:39):

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

Tobias Grosser (Oct 20 2018 at 03:39):

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

Jack Crawford (Oct 20 2018 at 03:46):

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 (Oct 20 2018 at 03:50):

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

Tobias Grosser (Oct 20 2018 at 03:50):

Also, feedback on the Georges paper would be interesting.


Last updated: Dec 20 2023 at 11:08 UTC