Zulip Chat Archive

Stream: new members

Topic: partial order for matrix


view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:02):

Dear all, as you know I just get up-to-speed on lean (and theorem proving) and don't do it fulltime for now. However, I picked as first toy-project to get started the extension of matrix as an instance of partial_order. (See https://github.com/tobig/lean-polyhedra/blob/master/src/polyhedra.lean)

view this post on Zulip Andrew Ashworth (Sep 18 2018 at 19:03):

Hi Tobias, you may want to post this in the #maths channel so people who are interested in this sort of stuff see it!

view this post on Zulip Andrew Ashworth (Sep 18 2018 at 19:04):

or you may post in #general if this is a concrete matrix implementation meant for use in computation

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:11):

Honestly, I don't even know how to post to the #maths channel. I see a "general" and a "new members" stream, but no "#maths" channel. I know streams and topics from https://zulipchat.com/help/about-streams-and-topics, but have no ideas of channels. I can obviously move this topic to the general stream if this helps. Would also post it to a math channel, if you can explain what a math channel is? Are you refering to "stream:general topic:#maths"?

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:11):

I posted it in new members, as my questions are for now still very simple.

view this post on Zulip Reid Barton (Sep 18 2018 at 19:12):

"Channel" means stream in this context I think.

view this post on Zulip Andrew Ashworth (Sep 18 2018 at 19:13):

whew, yes, I forgot Zulip isn't IRC

view this post on Zulip Reid Barton (Sep 18 2018 at 19:13):

#maths

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:13):

OK, got it. Had to subscribe to #maths explicitly

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:14):

My questions still remain simple. I mostly would like to know how to destruct an equality: https://github.com/tobig/lean-polyhedra/blob/master/src/polyhedra.lean#L51

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:16):

I spend some time looking and will probably figure it out eventually, but maybe somebody has a pointer.

view this post on Zulip Reid Barton (Sep 18 2018 at 19:17):

Don't you need to construct an equality?

view this post on Zulip Reid Barton (Sep 18 2018 at 19:17):

I guess you mean: "destruct" the goal

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:17):

Exactly.

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:18):

I had the same problem with the <=, but there I could just "assume i" and lean would auto-destruct it.

view this post on Zulip Reid Barton (Sep 18 2018 at 19:18):

I'm assuming your matrices are functions (of two variables), so the low-level way is to apply funext (twice)

view this post on Zulip Andrew Ashworth (Sep 18 2018 at 19:19):

you will probably want ext_iff in ring_theory.matrix

view this post on Zulip Andrew Ashworth (Sep 18 2018 at 19:20):

this will allow you to turn M = N into (∀ i j, M i j = N i j)

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:24):

Right. ext_iff looks good. Now I need to figure out how to apply it.

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:25):

Reid's proposal also worked.

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:25):

But from there I would not know how to proceed.

view this post on Zulip Johan Commelin (Sep 18 2018 at 19:25):

Either ext or rw ext_iff probably works

view this post on Zulip Andrew Ashworth (Sep 18 2018 at 19:25):

indeed, ext_iff is defined using multiple funext applications

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:26):

Perfect. All works.

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:26):

So easy. I tried rw, but had missed a comma before. Thought I needed more magic.

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:26):

Thanks guys. This got me over a slow phase. Will finish my proofs and get back. Very nice community here.

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:39):

Just to report back, my proof went through and I know have the partial_order I wanted to define on matrix.

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 19:39):

protected def matrix.le_antisymm [partial_order α] (a b: matrix n m α) :
a  b  b  a  a = b :=
begin
  assume h1: a  b,
  assume h2: b  a,
  apply funext, intro i, apply funext, intro j,
-- or   funext i,funext j,
-- or  ext i j,
  exact le_antisymm (h1 i j) (h2 i j),
end

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:39):

Ah, even better.

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:39):

Thanks @Kevin Buzzard

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:40):

@Kevin Buzzard, I used this for a proof on polyhedra. Would it make sense to add such defintions to your recent mathlib changes?

view this post on Zulip Mario Carneiro (Sep 18 2018 at 19:41):

golfed:

protected lemma matrix.le_antisymm [partial_order α] (a b: matrix n m α)
  (h1 : a ≤ b) (h2 : b ≤ a) : a = b :=
by ext i j; exact le_antisymm (h1 i j) (h2 i j)

view this post on Zulip Mario Carneiro (Sep 18 2018 at 19:41):

(also I don't have your definitions, so I had to guess if that's right)

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 19:43):

It would not surprise me if the Pi_instance tactic did this automatically, but it might not do.

view this post on Zulip Kenny Lau (Sep 18 2018 at 19:43):

golfeded:

protected lemma matrix.le_antisymm [partial_order α] (a b: matrix n m α)
  (h1 : a  b) (h2 : b  a) : a = b :=
by ext i j; from le_antisymm (h1 i j) (h2 i j)

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:47):

Nice, this lean golf.

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:47):

The two solutions from Mario and Kenny don't work in my editor.

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:47):

Need to replace "by" with "begin .. end"

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:48):

Not yet sure why, but this proofs starts to look really nice. And you are all fast in golfing. ;-)

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:51):

Got it, need a semicolon for 'by'.

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 19:52):

yes, by takes only one tactic, so you can either do {tactic 1, tactic 2} or tactic 1;tactic 2

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 19:53):

Did you notice that they both moved the hypotheses to the left of the colon? That's standard Lean style, so it seems; put as many hypotheses as possible on the left of the colon unless you can't do this for some reason (e.g. you're using the equation compiler).

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 19:54):

It makes your tactic proof two lines shorter at no extra cost

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:55):

I noticed and changed my code, but lacked the explanation. Thanks for providing it.

view this post on Zulip Mario Carneiro (Sep 18 2018 at 19:55):

basically, if the very first thing in your proof is a lambda/intro, you should probably shift your colon

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 19:55):

my partner does that for a living

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 19:55):

she's a colorectal surgeon

view this post on Zulip Mario Carneiro (Sep 18 2018 at 19:56):

I need an emoji for this

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:58):

Meanwhile, things look a lot better: https://github.com/tobig/lean-polyhedra/blob/master/src/polyhedra.lean

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:58):

In case you have more suggestions:

protected def matrix.le_trans [partial_order α] (a b c: matrix n m α)
  (h1 : a ≤ b) (h2 : b ≤ c) : a ≤ c :=
begin
  assume i: n,
  assume j: m,
  have h1l: a i j ≤ b i j, from h1 i j,
  have h2l: b i j ≤ c i j, from h2 i j,
  transitivity,
  apply h1l,
  apply h2l,
end

and

protected def matrix.le_refl [partial_order α] (A: matrix n m α) :
A ≤ A :=
begin
  assume i: n,
  assume j: m,
  refl
end

are also open for golfing. ;-)

view this post on Zulip Tobias Grosser (Sep 18 2018 at 19:59):

I will golf myself a little browsing mathlib code.

view this post on Zulip Kenny Lau (Sep 18 2018 at 19:59):

protected def matrix.le_trans [partial_order α] (a b c: matrix n m α)
  (h1 : a  b) (h2 : b  c) : a  c :=
by intros i j; from le_trans (h1 i j) (h2 i j)

protected def matrix.le_refl [partial_order α] (A: matrix n m α) :
  A  A :=
by intros i j; refl

view this post on Zulip Kenny Lau (Sep 18 2018 at 20:00):

protected def matrix.le_trans [partial_order α] (a b c: matrix n m α)
  (h1 : a  b) (h2 : b  c) : a  c :=
by intros i j; transitivity; solve_by_elim

view this post on Zulip Kenny Lau (Sep 18 2018 at 20:01):

hmm the last one may not work

view this post on Zulip Tobias Grosser (Sep 18 2018 at 20:03):

They all work.

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 20:03):

protected def matrix.le_refl [partial_order α] (A: matrix n m α) :
A  A := λ i j, le_refl _

view this post on Zulip Tobias Grosser (Sep 18 2018 at 20:03):

I learned a lot. So much fun.

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 20:04):

protected def matrix.le_refl [partial_order α] (A: matrix n m α) :
A  A := λ_ _, le_refl _

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 20:05):

bad style (should be a space after the lambda)

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 20:05):

but I'm just trying to beat Kenny

view this post on Zulip Tobias Grosser (Sep 18 2018 at 20:05):

Now I am unsure which ones to commit.

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 20:06):

set_option profiler true and see which one is quickest :-)

view this post on Zulip Tobias Grosser (Sep 18 2018 at 20:06):

I feel the last ones are a little too tight. What's the stylistic preferred solution?

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 20:06):

protected def matrix.le_refl [partial_order α] (A: matrix n m α) :
A  A := λ _ _, le_refl _

would probably be fine for mathlib I suspect

view this post on Zulip Chris Hughes (Sep 18 2018 at 20:09):

Shouldn't all of this be by pi_instance?

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 20:09):

right

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 20:10):

but I don't know if they did partial orders and I didn't look.

view this post on Zulip Kenny Lau (Sep 18 2018 at 20:10):

I believe they did

view this post on Zulip Kenny Lau (Sep 18 2018 at 20:10):

though I too did not look

view this post on Zulip Kevin Buzzard (Sep 18 2018 at 20:11):

@Tobias Grosser The original matrix add_comm_group code was written by Ellen Arlt and I was rewriting it in a live Lean coding session with an audience of undergrads, and Chris pointed out that pi_instances just did everything immediately.

view this post on Zulip Tobias Grosser (Sep 18 2018 at 20:15):

Interesting. I don't know how to use pi_instance(s)

view this post on Zulip Tobias Grosser (Sep 18 2018 at 20:17):

If I just write pi_instance, I get "too many constructors" for the first two lemmas, and "failed" for the last.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 05:41):

I made some good progress, but got stuck in type class resolution. I try to do dependent pattern matching in the following code:

#check matrix
universe v
def Gaussian_elimination {α : Type v} [ordered_ring α] :
   Π {x y : Type u}  [fintype x] [fintype y], matrix x y α →  α
| _ _ _ := 1

Unfortunately, I get the following error at location 'matrix':

polyhedra.lean:104:46: error

failed to synthesize type class instance for
α : Type v,
_inst_4 : ordered_ring α,
x y : Type u,
_inst_5 : fintype x,
_inst_6 : fintype y
⊢ fintype x
polyhedra.lean:104:46: error

view this post on Zulip Tobias Grosser (Sep 19 2018 at 05:43):

I modeled this according to https://leanprover.github.io/theorem_proving_in_lean/induction_and_recursion.html#dependent-pattern-matching, and therae the example on vector works without problems. In case anybody has some flyby ideas.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 06:03):

by exactI 1

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:23):

Is this in reply to the type class issue?

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:24):

def Gaussian_elimination {α : Type v} [ordered_ring α] :
   Π {x y : Type u}  [fintype x] [fintype y], matrix x y α   α
| _ _ _ := by exactI 1

does not work for me.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:24):

I still get an error at 'matrix x y \a'

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:27):

I also don't see why I would add a tactics proof at a definition of a value. This seems to not make a lot of sense to me.

view this post on Zulip Kenny Lau (Sep 19 2018 at 06:28):

def Gaussian_elimination {α : Type v} [ordered_ring α] :
   Π {x y : Type u}  [fintype x] [fintype y], matrix x y α   α
| _ _ _ _ _ := by exactI 1

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:31):

Thanks, now I know how to use syntax highlighting.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:31):

But your code does not work either.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:31):

I still get:

polyhedra.lean:108:46: error

failed to synthesize type class instance for
α : Type v,
_inst_4 : ordered_ring α,
x y : Type u,
_inst_5 : fintype x,
_inst_6 : fintype y
⊢ fintype x

view this post on Zulip Kenny Lau (Sep 19 2018 at 06:32):

is that the whole error?

view this post on Zulip Kenny Lau (Sep 19 2018 at 06:32):

oh, the error is in the type

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:32):

I get it 4 times in a row at the same location.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:32):

Yes, something is broken. I just don't know how to interpret the error message.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:33):

It seems to derive fintype x, but I feel I provided all information.

view this post on Zulip Kenny Lau (Sep 19 2018 at 06:33):

def Gaussian_elimination {α : Type v} [ordered_ring α] :
   Π {x y : Type u}  [hx : fintype x] [hy : fintype y], @matrix x y α hx hy _   α
| _ _ _ _ _ := by exactI 1

view this post on Zulip Kenny Lau (Sep 19 2018 at 06:33):

something like that

view this post on Zulip Kenny Lau (Sep 19 2018 at 06:33):

the order of the arguments may be wrong

view this post on Zulip Kenny Lau (Sep 19 2018 at 06:34):

I don't see why you would need pattern matching

view this post on Zulip Kenny Lau (Sep 19 2018 at 06:35):

def Gaussian_elimination {α : Type v} [ordered_ring α] {x y : Type u} [fintype x] [fintype y] :
  matrix x y α   α
| _ := 1

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:36):

The one without pattern matching works (I managed to write sth similar myself).

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:36):

The @matrix one breaks with:

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:37):

polyhedra.lean:192:57: error

type mismatch at application
  matrix x y
term
  α
has type
  Type v : Type (v+1)
but is expected to have type
  fintype x : Type u

view this post on Zulip Kenny Lau (Sep 19 2018 at 06:37):

def Gaussian_elimination {α : Type v} [ordered_ring α] :
   Π {x y : Type u}  [hx : fintype x] [hy : fintype y], @matrix x y hx hy α _  α
| _ _ _ _ _ := by exactI 1

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:37):

I want to implement something similar to

Fixpoint Gaussian_elimination {m n} : 'M_(m, n) → 'M_m × 'M_n × nat :=
  match m, n with
  | _.+1, _.+1 ⇒ fun A : 'M_(1 + _, 1 + _) ⇒
    if [pick ij | A ij.1 ij.2 != 0] is Some (i, j) then
      let a := A i j in let A1 := xrow i 0 (xcol j 0 A) in
      let u := ursubmx A1 in let v := a^-1 *: dlsubmx A1 in
      let: (L, U, r) := Gaussian_elimination (drsubmx A1 - v ×m u) in
      (xrow i 0 (block_mx 1 0 v L), xcol j 0 (block_mx a%:M u 0 U), r.+1)
    else (1%:M, 1%:M, 0%N)
  | _, _ ⇒ fun _ ⇒ (1%:M, 1%:M, 0%N)
  end.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:38):

As implemented in mathcomp.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:38):

Need it to compute the matrix rank.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:40):

polyhedra.lean:196:57: error

function expected at
  matrix x y α
term has type
  Type (max u v)

for the last one.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:41):

Matrix is defined as matrix : Π (m n : Type u_1) [_inst_1 : fintype m] [_inst_2 : fintype n], Type u_2 → Type (max u_1 u_2)

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:42):

This one works:

def Gaussian_elimination5 {α : Type v} [ordered_ring α] :
   Π {x y : Type u}  [hx : fintype x] [hy : fintype y], @matrix x y hx hy α  α
| _ _ _ _ _ := by exactI 1

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:43):

Thanks.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:43):

Need to read up what all this stuff does.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:43):

I am especially surprised that I need to pass the hx, hy as parameters.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 06:54):

I never answered your question about how to use pi_instances. It was used at some point in the code defining matrices, but this was in a branch of mathlib-community in code that got rewritten and then I think the branch was deleted? I couldn't find it anyway. In short, it's a tactic whereby if f x has a certain structure (e.g. that of an additive group) thenPi x, f x gets it too. For matrices over a ring it would immediately give them the structure of an additive commutative group by just guessing addition and zero and then figuring out the proofs itself. Of course it can't guess multiplication (if you asked it to, I guess it would guess pointwise multiplication of matrices).

view this post on Zulip Tobias Grosser (Sep 19 2018 at 06:58):

Thanks.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:01):

Ok, the last one for this morning:

def Gaussian_elimination5 {α : Type v} [ordered_ring α] {x y} [has_one x] [has_one y]:
   Π {x y}  [hx : fintype x] [hy : fintype y], @matrix x y hx hy α  → α
| (x+1) _ _ _ _ := by exactI 1

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:02):

Gives me "equation compiler failed (use 'set_option trace.eqn_compiler.elim_match true' for additional details)".
Setting this option does not give me more details.

view this post on Zulip Kenny Lau (Sep 19 2018 at 07:03):

1. you have two x and two y, which would cause much confusion, although it is not the source of the error

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:03):

I wanted x to be both a fintype and a type with has_one.

view this post on Zulip Kenny Lau (Sep 19 2018 at 07:03):

the source of the error is that the type of (x+1), whatever it is, is not an inductive type with _+1 as one of the constructors

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:04):

Right. It's a fintype.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:04):

I also want to make it to satisfy has_one.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:04):

That's why I added additional constraints.

view this post on Zulip Kenny Lau (Sep 19 2018 at 07:05):

you have two x and two y. Lean treats those as separate objects.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:05):

Right, I lack the notation how to add more constraints on x.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:05):

I tried this one before:

def Gaussian_elimination5 {α : Type v} [ordered_ring α]  :
   Π {x y} [has_one x] [has_one y]  [hx : fintype x] [hy : fintype y], @matrix x y hx hy α  → α
| (x+1) _ _ _ _ := by exactI 1

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:06):

x is not a number, it's a type

view this post on Zulip Kenny Lau (Sep 19 2018 at 07:06):

I don't know what x+1 is supposed to mean

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:06):

This differs from the Coq development because matrices are not defined with indices in 1..n, they are drawn from an arbitrary finite type

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:07):

Right.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:08):

I assumed I can fix this by defining my algorithm to only work if x and y are both finite _and_ satisfy has_one.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:08):

You could define your function on matrix (fin m) (fin n) α if you want to do induction on m and n

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:08):

there is no problem with assuming your type has a one, but that doesn't license you to write x+1

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:09):

That's what I tried ( I forgot that fin m exists, Johannes mentioned it at some point)

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:09):

if x is a type containing a 1, then 1 : x is okay

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:09):

def Gaussian_elimination5 {α : Type v} [ordered_ring α]  :
   Π {x y} [hx : fin x] [hy : fin y], @matrix x y hx hy α   α
| (_+1) _ _ _ _ := by exactI 1

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:10):

Now I am here. This works so far, but gives the error:

polyhedra.lean:201:46: error

maximum class-instance resolution depth has been reached (the limit can be increased by setting option 'class.instance_max_depth') (the class-instance resolution trace can be visualized by setting option 'trace.class_instances')

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:10):

fin is not a typeclass, it is an actual type

def Gaussian_elimination5 {α : Type v} [ordered_ring α]  :
   Π (m n : ℕ), matrix (fin m) (fin n) α  → α
| (m+1) (n+1) := 1

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:13):

Amazing:

def Gaussian_elimination6 {α : Type v} [ordered_ring α]  :
   Π (m n), matrix (fin m) (fin n) α   α
| (m+1) (n+1) A := A 0 0
| _ _ A := (0 : α)

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:14):

That type checks and does what I want. Thanks guys for getting me started.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:31):

has_one only means there's some term in your type called 1. You need has_add too to make sense of x + 1.

view this post on Zulip Johan Commelin (Sep 19 2018 at 07:33):

Right, so you want has_one Type and has_add Type (-;

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:53):

That's what I understand.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:53):

Now I don't understand how torequest such a type in a pattern match.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:53):

def Gaussian_elimination5 {α : Type v} [ordered_ring α] :
   Π {x y : Type u} [has_one x] [has_add x] [has_one y] [has_add y] [hx : fintype x] [hy : fintype y], @matrix x y hx hy α  α
| a b c d e f g h i :=

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:53):

This is what I came up with.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:54):

you can't pattern match on types

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:54):

As a general rule you shouldn't need to name variables which are showing up in [boxes like this]

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:54):

The system is supposed to do that for you

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:54):

I don't want to match on types.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:54):

It seems I need to match on all the boxes for this to type check.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:55):

What I would like is something like

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:55):

You could move stuff to the left of the colon

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:55):

this line is almost certainly not what you want

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:55):

the equation compiler only matches on stuff to the right of the colon

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:56):

and similarly in general you should be able to avoid using @

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:56):

because Lean is supposed to guess correctly

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:57):

Also, in case it wasn't clear Johan's suggestion above was not serious

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:57):

you don't actually want has_add Type

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:57):

Perhaps you could explain what you are trying to do informally?

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:58):

You're more likely to want has_add X with X : Type

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:58):

I'm not sure you want that either though, in this case

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:58):

On the other hand, I am pretty sure we want Gaussian Elimination

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:59):

I want a function that takes a (matrix n m \a) and returns an alpha (for now)

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:59):

It's kind of a disgrace that we only just got matrices and that we still don't have differentiation of functions from R to R

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:59):

I also want to do induction over n and m

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:59):

So I looked at dependent type pattern matching

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:59):

@Tobias Grosser your two goals sound very achievable

view this post on Zulip Mario Carneiro (Sep 19 2018 at 07:59):

In that case you should go with the version I stated with fin m and fin n

view this post on Zulip Tobias Grosser (Sep 19 2018 at 07:59):

And my understanding is that I need to constrain n and m to satisfy has_add and has_one.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 07:59):

if fin n makes sense

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:00):

then n : nat

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:00):

Right. That one works perfectly.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:00):

fin m is a type, which already has a one and an add

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:00):

and nat already has a 1 and an +

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:00):

as does fin n

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:00):

I have a variant that works

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:01):

feel free to post code

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:01):

Which is:

def Gaussian_elimination6 {α : Type v} [ordered_ring α]  :
   Π (m n), matrix (fin m) (fin n) α   α
| (m+1) (n+1) A := A 0 0
| _ _ A := (0 : α)

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:02):

(I mean the pattern match, not the gaussian elimination yet)

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:02):

gotcha

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:02):

You use m and n to mean two different things

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:02):

you were doing this with x and y earlier

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:02):

I find it quite confusing

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:02):

I think it was a bad idea to call the types m and n in the definition of matrix

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:03):

I was asking for has_one has_add out of curiosity (and also it seemed it would be preferable)

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:03):

we never use lowercase latin for types

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:03):

def Gaussian_elimination6 {α : Type v} [ordered_ring α]  :
   Π (m n), matrix (fin m) (fin n) α   α
| (x+1) (y+1) A := A 0 0
| _ _ A := (0 : α)

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:03):

The matching only matches stuff to the right of the colon, so you're writing "let m = m + 1".

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:04):

I used to do this in mathematics when I was younger -- "I have a quadratic equation x^2+bx+c=0 -- now let's complete the square by setting x=x+b/2"

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:04):

I am aware that 'n' and 'm' in my original example mean different things.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:04):

where would you want to perform an addition, where you can't already?

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:04):

All is good in this example.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:04):

I never write that now because it's so easy to lose track of whether you're using the old x or the new x. Now I write "let y = x+b/2"

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:04):

Things work fo rme.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:05):

The only time I let "x=x+1" nowadays is in procedural programming when I actually want the old value to be forgotten forever

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:06):

Here is a working version that doesn't use fin:

def Gaussian_elimination6 {α : Type v} [ordered_ring α]
  (M N) [fintype M] [fintype N] : matrix M N α  → α
| A := A 0 0

But you can't do induction on m : nat in this case, since there is no m

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:06):

Right.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:06):

def Gaussian_elimination6 {α : Type v} [ordered_ring α]  :
   Π (m n), matrix (fin m) (fin n) α   α
| (x+1) (y+1) A := A 0 0
| _ _ A := (0 : α)

Do you see that you're also using the fact that fin (x+1) has a zero here.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:07):

Type class inference figured that out for you and let you use it

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:07):

Yes.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:07):

That's why I had to write (0:\a) in the second match.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:07):

I think.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:07):

0 by itself means "the zero of something"

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:07):

Because in that case it is not known that a zero exists.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:07):

Kevin means the 0 in A 0 0

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:07):

Lean was expecting something of type "fin (x+1)" and you wrote "0"

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:08):

Right.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:08):

and Lean figured "aah, this must be one of those types that has a zero, let me find an instance of has_zero (fin (x+1)) behind the scenes

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:08):

I wrote

def Gaussian_elimination6 {α : Type v} [ordered_ring α]  :
   Π (m n), matrix (fin m) (fin n) α   α
| (x+1) (y+1) A := A 0 0
| _ _ A := A 0 0

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:08):

Initially

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:09):

Lean's typeclass magic: example (x : ℕ) : has_zero (fin (x+1)) := by apply_instance

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:09):

your initial approach doesn't work becasue fin 0 is the empty type and in particular has no zero

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:09):

Right.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:09):

I understood this.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:09):

That's very interesting.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:10):

example : has_zero (fin 0) := by apply_instance -- "failed to generate instance" error

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:10):

This black magic is related to the square bracket stuff and it took me a very long time before I got comfortable with it.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:10):

I see.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:11):

In retrospect I wish that people had stressed earlier how basic notation like 0 and + worked in Lean

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:11):

The only thing I do not understand is if it is possible to take Mario's stuff, but expose n and m without introducing 'fin n', but instead just use has_one and has_add.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:11):

because it seems to me that this is a very good introduction to the type class system

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:11):

I feel this should work, but seems to be far beyond my type_class capabilities.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:11):

I'm afraid I'm not a computer scientist and I don't know what "expose" means

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:12):

As I have a solution, that's not needed. But would be nice to understand this eventually.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:12):

matrix eats something of type fin n

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:12):

so you have to give it something of type fin n

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:12):

actually it eats a fintype

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:12):

"expose" means pattern match on n and m to be able to do induction on n and m

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:12):

Right. I can pass it a fin n and all is good.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:13):

wait, that's not even true any more

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:13):

I was wondering if I could pass it a fintype x, where I know that x has_add and has_one.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:13):

any fintype has a cardinality, fintype.card X, and you can do induction on that

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:13):

sorry, I seem to be behind the times

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:13):

#check @matrix -- matrix : Π (m n : Type u_1) [_inst_1 : fintype m] [_inst_2 : fintype n], Type u_2 → Type (max u_1 u_2)

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:13):

You don't usually need a one and an add on the index type

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:13):

what is this needed for?

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:14):

So how can I do induction over card? That's what I am trying to figure out.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:14):

It's a bit messy

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:14):

Do you want to prove things for matrices indexed by random finite types?

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:14):

I just want to do induction on my dimensionality to do gaussion elimination.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:14):

No. If you tell me 'fin x' is enough, we are done.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:15):

I guess this is a design decision

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:15):

Just got curious about the type classes. Seems matlib likes to generalize things.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:15):

I am fine being in 'fin x'. That seems a lot less messy.

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:15):

Yes, if mathlib did Gaussian Elimination it would almost certainly do it for random types which are fintypes

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:15):

Let's leave it at this for now.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:15):

def Gaussian_elimination6 {α : Type v} [ordered_ring α]
  : ∀ (m n M N) [fintype M] [fintype N], fintype.card M = m → fintype.card N = n → matrix M N α  → α
| m n M N _ _ h1 h2 A := A 0 0

You will need some @'s in there, my typechecker isn't running

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:16):

If you do it like that then you can induct on m and n

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:16):

More likely, I would just do it on fin m by induction and then use equivalence lemmas to transfer to the original fintype

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:17):

failed to synthesize type class instance for
α : Type v,
_inst_1 : ordered_ring α,
m : ?m_1,
n : ?m_2,
M : Type ?,
N : Type ?,
_inst_2 : fintype M,
_inst_3 : fintype N
 fintype M

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:17):

boo

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:17):

Or find a way to work with subsets of a fixed type of size m

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:17):

you have to put a by exactI in there

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:17):

in the statement??

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:17):

yeah

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:18):

because there are typeclass args right of the colon

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:18):

either that or use @ a lot

view this post on Zulip Kenny Lau (Sep 19 2018 at 08:18):

deja vu

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:19):

def Gaussian_elimination6 {α : Type v} [ordered_ring α]
  :  (m n M N) [fintype M] [fintype N],
      by exactI fintype.card M = m  fintype.card N = n  matrix M N α   α
| m n M N _ _ h1 h2 A := sorry

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:19):

eew

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:19):

soon to be not fixed in Lean 4

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:20):

that looks fine, not at all confusing for beginners

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:20):

like I said, messy

view this post on Zulip Kevin Buzzard (Sep 19 2018 at 08:20):

Isn't there some pre-rolled fintype.induction_on?

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:21):

not to mention that this is not going to be a nice inductive proof since you have to build a recursive subtype

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:21):

It's probably better to do induction over the finsets on a fixed type

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:21):

Cool. At least it works.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:22):

I feel I can do induction by using x+1 and y+1

def Gaussian_elimination6 {α : Type v} [ordered_ring α]
  :  (m n M N) [fintype M] [fintype N],
      by exactI fintype.card M = m  fintype.card N = n  matrix M N α   α
| (x+1) (y+1) M N _ _ h1 h2 A := (0 : α)
| _ _ M N _ _ h1 h2 A := (0 : α)

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:22):

Not sure what recursive subtypes mean.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:22):

I will start with the (fin n) stuff, which is sth I certainly understand.

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:23):

If all works, I can see if I can generalize things.

view this post on Zulip Mario Carneiro (Sep 19 2018 at 08:23):

when applying the induction hypothesis, you will need to build a type that contains one fewer element than the type you started with

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:23):

I see. That's annoying. I will certainly stay with (fin n)

view this post on Zulip Tobias Grosser (Sep 19 2018 at 08:24):

Thanks again. Now I learned quite a bit. Will need to read up on exactI in type definitions.

view this post on Zulip Sean Leather (Sep 19 2018 at 08:26):

Will need to read up on exactI in type definitions.

Note that tactics are simply ways of generating code. They can appear in definitions or proofs. It's just that they are most useful in proofs.


Last updated: May 13 2021 at 00:41 UTC