Zulip Chat Archive

Stream: new members

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


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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 00:52):

I unfortunately just get "failed"

view this post on Zulip Chris Hughes (Oct 20 2018 at 01:02):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 01:05):

I see.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 01:05):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 01:07):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 01:08):

Thanks a lot, this was easy.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 01:52):

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

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 01:52):

That seems complicated.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 01:53):

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

view this post on Zulip Chris Hughes (Oct 20 2018 at 02:32):

funext is a start

view this post on Zulip Tobias Grosser (Oct 20 2018 at 02:32):

Thanks.

view this post on Zulip Chris Hughes (Oct 20 2018 at 02:32):

But it looks really complicated.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 02:33):

That's what I feel.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 02:34):

Maybe I approach this from the wrong angle.

view this post on Zulip Chris Hughes (Oct 20 2018 at 02:34):

What is pick_encodable?

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

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 02:35):

It finds a non-zero element in the matrix.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 02:36):

And returns an optional.

view this post on Zulip Chris Hughes (Oct 20 2018 at 02:36):

What is getL?

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

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 02:37):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 02:41):

I feel I should proof something simpler.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 02:41):

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

view this post on Zulip Chris Hughes (Oct 20 2018 at 02:48):

What are xrow and fin_swap and block_mx?

view this post on Zulip Tobias Grosser (Oct 20 2018 at 02:56):

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

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:01):

Is the relevant paper.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:02):

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

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

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

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:11):

The paper justifies some of the choices they have taken.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:12):

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

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

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

view this post on Zulip Mario Carneiro (Oct 20 2018 at 03:23):

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

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

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

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

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:26):

Are you talking about Jack?

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:26):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:26):

Just use this to learn stuff.

view this post on Zulip Mario Carneiro (Oct 20 2018 at 03:26):

It might help to try to invent your own gaussian elimination

view this post on Zulip Mario Carneiro (Oct 20 2018 at 03:26):

rather than porting from coq

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:28):

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

view this post on Zulip Mario Carneiro (Oct 20 2018 at 03:28):

that's right

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:28):

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

view this post on Zulip Mario Carneiro (Oct 20 2018 at 03:28):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:28):

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

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

view this post on Zulip Mario Carneiro (Oct 20 2018 at 03:29):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:30):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:30):

Yes.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:30):

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

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:31):

@Scott Morrison , what is your goal with GE?

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

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

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:32):

mathcomp.mxalgebra?

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:32):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:33):

@Jack Crawford , no need to rush.

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:33):

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

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

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:37):

I see.

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:39):

I see,

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:39):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:39):

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

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:50):

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

view this post on Zulip Tobias Grosser (Oct 20 2018 at 03:50):

Also, feedback on the Georges paper would be interesting.


Last updated: May 14 2021 at 13:24 UTC