Zulip Chat Archive

Stream: new members

Topic: Simplifying Prop with Known False Statements


view this post on Zulip Rocky Kamen-Rubio (Feb 10 2020 at 19:11):

I have a very long Prop that consists mostly of AND/OR statements and false equalities like 1 = 2. Is there a faster way to simplify it than going through it with cases, split, left/right? Is there a built-in function that can scan through a long Prop and replace false equalities with ff, and another than can recognize that A AND ff is equivalent to ff, or that A OR ff is equivalent to A?

view this post on Zulip Chris Hughes (Feb 10 2020 at 19:12):

norm_num would probably solve that goal.

view this post on Zulip Cerek Hillen (he) (W2'20) (Feb 10 2020 at 19:24):

And for context, if I'm not mistaken, norm_num means the tactic norm_num provided by mathlib

view this post on Zulip Rocky Kamen-Rubio (Feb 18 2020 at 04:30):

I'm implementing matricies as types fin m → fin n → nat and want to sum all the elements in each row, and then sum all those values. Is there an easy way to do this using finset.univ.sum? I've been able to do it with 1D arrays of type fin m → nat so I feel like there should be a clever lambda solution for the 2D case. I committed to this implementation before I realized mathlib has a matrix type, but it's implemented the same way, so it might not be worth the hassle of switching.

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 08:57):

def matrix_sum (m n : ) (M : fin m  fin n   ) :  :=
finset.univ.sum $ λ i, finset.univ.sum $ M i

Of course if you find yourself asking five more questions like this, and for some of them the answer is "we did it already with matrices in mathlib", then you might want to take that as an indication that you should switch. Remember -- if you define it yourself, you've got to prove all the lemmas about it yourself.

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 08:58):

PS I can't guarantee that I summed the elements in the rows rather than the columns -- this depends on your mental model.

view this post on Zulip Rocky Kamen-Rubio (Feb 18 2020 at 15:54):

Thank you! That's a good point that maybe this is a sign that I should switch to the mathlib representation. My other motivation for not switching was that eventually I want to start putting noncommutative elements (specifically entangled quantum states) into the matrix, so it would matter whether I'm ordering it by rows or columns. If we have (M : fin m → fin n → ℕ ), I guess I could also just transpose it and do matrix_sum on the transpose. This way we get both cases, and all I need is to show whether they're equal or not.

view this post on Zulip Rocky Kamen-Rubio (Feb 18 2020 at 16:26):

Ok I tried doing this and got to this point. I feel like again there's probably an easy tactic to finish this off that I'm not seeing. Maybe switching to mathlib's matrix representation would make this easier, but part of me still wants to hold out on switching because I'm not going to be multiplying or adding these matrices, just summing their elements in specific ways, and I want as much control over that as possible.

board : fin m  fin n  
 finset.sum finset.univ (λ (i : fin m), finset.sum finset.univ (board i)) =
    finset.sum finset.univ (λ (i : fin n), finset.sum finset.univ (λ (m : fin m), board m i))

view this post on Zulip Reid Barton (Feb 18 2020 at 16:27):

This is "reverse the order of summation"?

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 16:27):

Right

view this post on Zulip Reid Barton (Feb 18 2020 at 16:27):

It definitely won't be a tactic, it probably is a theorem that already exists.

view this post on Zulip Reid Barton (Feb 18 2020 at 16:28):

I think it's whatever the to_additive of prod_product is

view this post on Zulip Reid Barton (Feb 18 2020 at 16:29):

well, combined with more stuff. How can this not exist already?

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 16:29):

aah, remember the old days before automation where you could just read off the additive name in the library...

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 16:30):

Oh yeah so we're in exactly the same situation as in the other thread.

view this post on Zulip Reid Barton (Feb 18 2020 at 16:30):

oh, prod_comm

view this post on Zulip Reid Barton (Feb 18 2020 at 16:30):

this should probably have a comment with things like "fubini" and maybe "prod_prod"

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 16:31):

https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/spheres/near/188451346 also ideally needs to switch from finset.sum finset.univ (fin n) to finset.sum finset.range n

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 16:32):

theorem sum_univ_fin_eq_sum_range (n : ) (f : fin n  ) :
  finset.sum finset.univ f = (finset.range n).sum (λ i, if hi : i < n then f i, hi else 0) :=
begin
  sorry
end

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 16:32):

I don't like the look of induction on n

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 16:44):

What I'm saying is that fin n doesn't have type finset ℕ

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 17:20):

theorem sum_univ_fin_eq_sum_range (n : ) (f : fin n  ) :
  finset.sum finset.univ f = (finset.range n).sum (λ i, if hi : i < n then f i, hi else 0) :=
begin
  set F :    := λ i, if hi : i < n then f i, hi else 0 with hF,
  have H : f = λ (i : fin n), F (i.val),
  { ext i,
    rw hF,
    show f i = dite (i.val < n) (λ (hi : i.val < n), f i.val, hi) (λ (hi : ¬i.val < n), 0),
    rw dif_pos i.is_lt,
    cases i, refl,
  },
  rw H,
  rw finset.sum_image,
  { congr',
    -- ⊢ finset.image (λ (x : fin n), x.val) finset.univ = finset.range n
    ext j, -- sigh
    rw [finset.mem_range, finset.mem_image],
    split,
      rintro ⟨⟨j,hj, _, rfl,
      exact hj,
    intro hj,
    use j, hj,
    split, apply finset.mem_univ, refl
  },
  intros _ _ _ _,
  exact fin.eq_of_veq,
end

view this post on Zulip Rocky Kamen-Rubio (Feb 18 2020 at 18:33):

Amazing, thank you! I'm having trouble getting this into a form that I can use to finish my goal state though. I understand conceptually why it works, but the usual tactics like rw apply etc don't seem to be working here (even though mathematically it seems like that's what I'm doing). I've had a similar issue come up as well when I got to the following tactic and goals states. I feel like I'm missing something potentially simple and obvious.

1 goal
m n : ,
strategyA : fin m  fin n  ,
strategyB : fin n  fin m  ,
h :  (r : fin m) (c : fin n), strategyA r c = strategyB c r
 strategyB = λ (n : fin n) (m : fin m), strategyA m n

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 18:34):

ext

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 18:34):

You need to check that two functions are equal iff they agree everywhere. In term mode this is funext and in tactic mode it's ext i (or perhaps ext c r in your case)

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 18:35):

"Extensionality" is the general principle that two objects are equal if and only if they're made from equal things. I think it's one of those things which computer scientists sometimes make a fuss about, it might be an axiom or something.

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 18:36):

It results from a lack of understanding of mathematical equality ;-)

view this post on Zulip Rocky Kamen-Rubio (Feb 18 2020 at 18:48):

Fascinating. So lean doesn't automatically know that two objects made of equal parts are equal? I guess that makes sense but something feels a little absurd about that... Like I'm telling lean that instead of this equality holding for every element of a set, I'm telling it that it holds for a general element of a set, and it recognizes that as an equality but not the former?

Either way, it worked for the more recent goal state I posted but it doesn't seem to be working for the "reverse order of summation" goal state. I'm getting the following error

Screen-Shot-2020-02-18-at-1.44.34-PM.png

view this post on Zulip Bryan Gin-ge Chen (Feb 18 2020 at 18:49):

There are a lot errors like that in the docstrings; I'm not sure what the precise cause is but they shouldn't affect the validity of the actual Lean code.

view this post on Zulip Patrick Massot (Feb 18 2020 at 18:51):

Rocky: saying that two functions are equal if they take the same value when evaluated on the same input is absurd from a computer science point of view. For instance it completely disregard execution time or memory consumption for functions that can be actually run.

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 18:51):

The error in the docstring is irrelevant, that's just some parser issue.

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 18:53):

import tactic

example (m n : )
(strategyA : fin m  fin n  )
(strategyB : fin n  fin m  )
(h :  (r : fin m) (c : fin n), strategyA r c = strategyB c r)
: strategyB = λ (n : fin n) (m : fin m), strategyA m n :=
begin
  ext c r,
  rw h
end

Oh -- this is the one you can do? ext only works if the goal is of the form f = g where f and g are, say, functions or sets.

view this post on Zulip Rocky Kamen-Rubio (Feb 18 2020 at 19:00):

Yeah I got that one working fine. It's this one that's been difficult for me. Here's my attempt so far that gives me the error message I linked to in my previous post.

lemma row_sum_eq_col_sum {m n : nat} (board : fin m  fin n  nat) : row_sum board = col_sum board
:=
begin
rw row_sum,
rw col_sum,
rw matrix_sum,
rw matrix_sum,
rw sampleB,
rw sampleA,
simp,
ext c r,
end

Edit: sorry, forgot I haven't linked to how row_sum or col_sum are defined. Might be easier just to look at my final tactic state. Screen-Shot-2020-02-18-at-2.03.20-PM.png

view this post on Zulip Rocky Kamen-Rubio (Feb 18 2020 at 19:01):

Patrick Massot said:

Rocky: saying that two functions are equal if they take the same value when evaluated on the same input is absurd from a computer science point of view. For instance it completely disregard execution time or memory consumption for functions that can be actually run.

That's a good point - I hadn't though about functions different in memory use or runtime. I guess I still haven't developed a good intuition for how lean thinks about mathematical objects.

view this post on Zulip Patrick Massot (Feb 18 2020 at 19:08):

Lean supports both ways of thinking about function, without making a fuss. It simply records whether you used mathematics way or not.

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 19:11):

you need to rewrite h a lot and then use finset.sum_comm

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 19:12):

Your goal is the equality of two natural numbers so you can't use ext here.

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 19:12):

actually maybe just finset.sum_comm will work directly

view this post on Zulip Kevin Buzzard (Feb 18 2020 at 19:16):

BTW it's bad style to put simp in the middle of a proof; it should only be used to close a goal. There are ways to work around uses of simp in the middle of a proof.

view this post on Zulip Rocky Kamen-Rubio (Feb 23 2020 at 18:47):

I've been chewing on this for a few days and can't seem to figure out how to rewrite h in this case. Could I get a hint? :-)

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2020 at 19:01):

@Rocky Kamen-Rubio I scrolled up a bit in the thread but I didn't see any self-contained code that I could copy / paste to try out. Could you provide that in a post or a link to a github gist?

view this post on Zulip Rocky Kamen-Rubio (Feb 23 2020 at 19:11):

@Bryan Gin-ge Chen Here's the full proof in its current state. The part I'm struggling with is towards the end. Let me know if you have any questions since it's a bit long.

import init
import tactic
import data.nat.parity
import data.finset
import data.fintype
import algebra.big_operators
import data.real.basic
set_option class.instance_max_depth 15000000


#eval 2 --You can't put open_locale classical after an import statement for some reason so that's why this is here

open_locale classical
def board {m n : nat} (strategyA : fin m  fin n  nat) (strategyB: fin n  fin m  nat) : fin m  fin n  nat := strategyA

def consistent {m n : nat} (strategyA : fin m  fin n  nat) (strategyB: fin n  fin m  nat) : Prop
:=  (r : fin m) (c : fin n), (strategyA r c) = (strategyB c r)

def sampleA {m n : nat} (board : fin m  fin n  nat) : fin m  fin n  nat := board

def sampleB {m n : nat} (board : fin m  fin n  nat) : fin n  fin m  nat := λ (n : fin n) (m : fin m), board m n
#check sampleA
#check sampleB

lemma board_equiv_strategy {m n : nat} (strategyA : fin m  fin n  nat) (strategyB: fin n  fin m  nat) :
(consistent strategyA strategyB)  (strategyA = ((sampleA (board strategyA strategyB)))  (strategyB = (sampleB (board strategyA strategyB))))
:=
begin
intro h,
split,
rw sampleA,
rw board,
rw board,
rw sampleB,
rw consistent at h,
ext i,
rw h,
end

def each_row_sum_even {m n : nat} (board : fin m  fin n  nat) : Prop :=  (r : fin m), (finset.univ.sum (sampleA board r)).even

def each_col_sum_odd {m n : nat} (board : fin m  fin n  nat) : Prop :=  (c : fin n), ¬(finset.univ.sum (sampleB board c)).even

def even_strategy {m n : nat} (strategyA : fin m  fin n  nat) : Prop := ( r : fin m, ((finset.univ.sum (strategyA r)).even))

def odd_strategy {m n : nat} (strategyB : fin n  fin m  nat) : Prop := ( (c : fin n), ¬ (finset.univ.sum (strategyB c)).even)

lemma even_strategy_implies_even_rows {m n : nat} (strategyA : fin m  fin n  nat) (strategyB : fin n  fin m  nat)
: ((consistent strategyA strategyB)  even_strategy strategyA)  each_row_sum_even (board strategyA strategyB)
:=
begin
rw even_strategy,
rw each_row_sum_even,
rw sampleA,
rw board,
intro h,
have h := h.right,
exact h,
end

--In order to talk about a board we need to assume the two strategies are consistent. Or else we need to define the board differently to allowfor this
lemma odd_strategy_implies_odd_cols {m n : nat} (strategyA : fin m  fin n  nat) (strategyB : fin n  fin m  nat)
: ((consistent strategyA strategyB)  odd_strategy strategyB)  each_col_sum_odd (board strategyA strategyB)
:=
begin
intro h,
cases h with h1 h2,
have h3 := board_equiv_strategy strategyA strategyB h1,
cases h3 with h4 h5,
rw each_col_sum_odd,
rw  h5,
rw odd_strategy at h2,
exact h2,
end

def matrix_sum {m n : } (M : fin m  fin n   ) :  :=
finset.univ.sum $ λ i, finset.univ.sum $ M i

def row_sum {m n : nat} (board : fin m  fin n  nat) : nat := matrix_sum (sampleA board)

def col_sum {m n : nat} (board : fin m  fin n  nat) : nat := matrix_sum (sampleB board)

--sometimes I get an error here that this theorem is using sorry. Doesn't look like it is to me, so idk what's going on
theorem sum_univ_fin_eq_sum_range (n : ) (f : fin n  ) :
  finset.sum finset.univ f = (finset.range n).sum (λ i, if hi : i < n then f i, hi else 0) :=
begin
  set F :    := λ i, if hi : i < n then f i, hi else 0 with hF,
  have H : f = λ (i : fin n), F (i.val),
  { ext i,
    rw hF,
    show f i = dite (i.val < n) (λ (hi : i.val < n), f i.val, hi) (λ (hi : ¬i.val < n), 0),
    rw dif_pos i.is_lt,
    cases i, refl,
  },
  rw H,
  rw finset.sum_image,
  { congr',
    -- ⊢ finset.image (λ (x : fin n), x.val) finset.univ = finset.range n
    ext j, -- sigh
    rw [finset.mem_range, finset.mem_image],
    split,
      rintro ⟨⟨j,hj, _, rfl,
      exact hj,
    intro hj,
    use j, hj,
    split, apply finset.mem_univ, refl
  },
  intros _ _ _ _,
  exact fin.eq_of_veq,
end

lemma row_sum_eq_col_sum {m n : nat} (board : fin m  fin n  nat) : row_sum board = col_sum board
:=
begin
rw row_sum,
rw col_sum,
rw matrix_sum,
rw matrix_sum,
rw sampleB,
rw sampleA,
have h := sum_univ_fin_eq_sum_range,
sorry,
-- finset.sum_comm,
end

theorem noStrategyMN2 {m n : nat} (strategyA : fin m  fin n  nat) (strategyB: fin n  fin m  nat) :
¬ ((consistent strategyA strategyB)   (even_strategy strategyA)  (odd_strategy strategyB))
:=
begin
intro h,
cases h with c y,
cases y with even odd,
have cEven := even,
have x := even_strategy_implies_even_rows strategyA strategyB (c  even),  --why is this not ok???????
have y := odd_strategy_implies_odd_cols strategyA strategyB (c  even),
sorry,
end

view this post on Zulip Kevin Buzzard (Feb 23 2020 at 19:32):

Re: "sometimes I get an error here that this theorem is using sorry." I think this might be some kind of a bug in use. If you replace use ⟨j, hj⟩, near the end by existsi (⟨j, hj⟩ : fin n), is it any better?

view this post on Zulip Kevin Buzzard (Feb 23 2020 at 19:38):

The rw h fails (correctly), and to debug this you can try filling in some of the gaps. The more precise rw h m (λ (i : fin m), finset.sum finset.univ (board i)) fails and here the error is much clearer -- sum_univ_fin_eq_sum_range (which IIRC I wrote) is about functions from fin n to the reals, and you have a function from fin n to the naturals. The correct thing to prove is for a map to an arbitrary additive commutative monoid or something -- something which includes both the naturals and the reals. You can replace the first few lines with

theorem sum_univ_fin_eq_sum_range {A : Type*} [add_comm_monoid A] (n : ℕ) (f : fin n → A) :
  finset.sum finset.univ f = (finset.range n).sum (λ i, if hi : i < n then f ⟨i, hi⟩ else 0) :=
begin
  set F : ℕ → A := λ i, if hi : i < n then f ⟨i, hi⟩ else 0 with hF,

view this post on Zulip Kevin Buzzard (Feb 23 2020 at 19:39):

but even after the rewrites there is work to do. At least this is a step forward.

view this post on Zulip Kevin Buzzard (Feb 23 2020 at 19:44):

oh no no what am I talking about? You don't use h at all, I've misremembered the idea. You can just finish the proof with sum_comm:

rw matrix_sum,
rw sampleB,
rw sampleA,
rw finset.sum_comm,

view this post on Zulip Kevin Buzzard (Feb 23 2020 at 19:47):

So that gets row_sum_eq_col_sum compiling and now there's just an error at c ∧ even -- you ask why this is not OK, and this has an easy answer: P ∧ Q works for propositions, which means true-false statements. For example x = 2 ∧ y < 4 is fine. Now x = 2 has type Prop. Your term c has type consistent strategyA strategyB (not Prop -- it's a proof not a statement) so c ∧ ... makes no sense.

view this post on Zulip Rocky Kamen-Rubio (Feb 23 2020 at 20:17):

  1. Yes, replacing use (j,hj) with existsi ((j,hj) : fin n), resolved the issue, thank you!

  2. I had a feeling there was an easy way to do that in Lean. I'm a little confused what the purpose of defining h was then? I remember @Kevin Buzzard and @Reid Barton talking about how this proof wouldn't be possible with tactics, but maybe that was for a more general idea?

  3. I defined consistent even and oddas Props though, not as theorems. Do I still need to treat them differently?

def consistent {m n : nat} (strategyA : fin m  fin n  nat) (strategyB: fin n  fin m  nat) : Prop
:=  (r : fin m) (c : fin n), (strategyA r c) = (strategyB c r)

def even_strategy {m n : nat} (strategyA : fin m  fin n  nat) : Prop := ( r : fin m, ((finset.univ.sum (strategyA r)).even))

def odd_strategy {m n : nat} (strategyB : fin n  fin m  nat) : Prop := ( (c : fin n), ¬ (finset.univ.sum (strategyB c)).even)

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2020 at 21:10):

For your last question mark, maybe this helps:

theorem noStrategyMN2 {m n : nat} (strategyA : fin m  fin n  nat) (strategyB: fin n  fin m  nat) :
¬ ((consistent strategyA strategyB)   (even_strategy strategyA)  (odd_strategy strategyB))
:=
begin
intro h,
cases h with c y,
cases y with even odd,
have cEven := even,
have x := even_strategy_implies_even_rows strategyA strategyB c, even,
-- to give something of type A ∧ B, you need hA : A and hB : B,
-- and you put them together in angle brackets like this: ⟨hA, hB⟩,
have y := odd_strategy_implies_odd_cols strategyA strategyB c, odd,
sorry,
end

view this post on Zulip Kevin Buzzard (Feb 23 2020 at 21:49):

You defined consistent as a Prop, and and expects a Prop. So why did you give it a proof and not a Prop? You gave it a term of type P, not P itself.

view this post on Zulip Bryan Gin-ge Chen (Feb 23 2020 at 21:52):

Wanting to put an and there was the problem, since even_strategy_implies_even_rows looks like this:

lemma even_strategy_implies_even_rows {m n : nat} (strategyA : fin m  fin n  nat) (strategyB : fin n  fin m  nat)
: ((consistent strategyA strategyB)  even_strategy strategyA)  each_row_sum_even (board strategyA strategyB)

view this post on Zulip Kevin Buzzard (Feb 23 2020 at 22:02):

PS your import init is bad -- remove it. Your set_option class.instance_max_depth 15000000 is also bad -- remove it. I think the reasons were already explained above but you don't want either of these two lines.

view this post on Zulip Rocky Kamen-Rubio (Feb 24 2020 at 20:33):

Kevin Buzzard said:

You defined consistent as a Prop, and and expects a Prop. So why did you give it a proof and not a Prop? You gave it a term of type P, not P itself.

Ok, I think I'm getting this. It's working fine with the modification. Thank you!

Kevin Buzzard said:

PS your import init is bad -- remove it. Your set_option class.instance_max_depth 15000000 is also bad -- remove it. I think the reasons were already explained above but you don't want either of these two lines.

You're right. I had forgotten to take those out since they weren't actively stopping my code from compiling... Thanks for the reminder!

view this post on Zulip Rocky Kamen-Rubio (Feb 24 2020 at 20:41):

Rocky Kamen-Rubio said:

Thank you! That's a good point that maybe this is a sign that I should switch to the mathlib representation. My other motivation for not switching was that eventually I want to start putting noncommutative elements (specifically entangled quantum states) into the matrix, so it would matter whether I'm ordering it by rows or columns. If we have (M : fin m → fin n → ℕ ), I guess I could also just transpose it and do matrix_sum on the transpose. This way we get both cases, and all I need is to show whether they're equal or not.

I'm now wanting to repeat this procedure but with matrices in each column instead of integers, and taking the matrix product of all the matrices in each row. finset.univ.prod (understandably) doesn't use matrix.mul automatically when its input is a matrix. Is there a way to feed it an arbitrary function (à la MapReduce) , or should I be thinking about this differently? I could see a benefit to implementing this matrix data structure differently, maybe as a 2D linked list, to facilitate recursive matrix multiplication of its elements over a given row or column, but I feel like that shouldn't be necessary.

view this post on Zulip Kevin Buzzard (Feb 24 2020 at 21:19):

finset.univ.prod should work fine. If the function is taking values in anything which Lean knows is a monoid then it will use the monoid multiplication....oh wait. It's not commutative. Then yes you're right, you'll have to use something like list.prod

view this post on Zulip Rocky Kamen-Rubio (Feb 25 2020 at 05:33):

Kevin Buzzard said:

finset.univ.prod should work fine. If the function is taking values in anything which Lean knows is a monoid then it will use the monoid multiplication....oh wait. It's not commutative. Then yes you're right, you'll have to use something like list.prod

list.prod works, thank you! That's a shame though because now I'm going to have to choose between keeping my matrix type or using this easier product method (unless there's a snazzy way to get the rows and columns from a matrix as a list instead of as vectors, but it seems like that's not possible). I tried implementing this recursive algorithm on my matrix in the meantime too, but keep getting that the recursive call is an "unknown identifier". Is there an import statement or something I'm missing that tells Lean it's ok to use variables that haven't been fully defined yet?

import data.finset
import data.fintype
import algebra.big_operators
import data.real.basic
import data.matrix.basic
import data.matrix.pequiv

def row_product {m n : } (mat : matrix (fin m) (fin n) (matrix (fin 2) (fin 2)  )) (r : ): matrix (fin 2) (fin 2)  := row_product_helper mat r 1

def row_product_helper {m n : } (mat : matrix (fin m) (fin n) (matrix (fin 2) (fin 2)  )) (r c: ) : matrix (fin 2) (fin 2)  :=
if (c = n) then mat r c else matrix.mul (mat r c) (row_product_helper mat r (c+1))

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 09:27):

(unless there's a snazzy way to get the rows and columns from a matrix as a list instead of as vectors, but it seems like that's not possible).

I don't really know what you mean. Anything is possible. Just write the function.

I tried implementing this recursive algorithm on my matrix in the meantime too, but keep getting that the recursive call is an "unknown identifier". Is there an import statement or something I'm missing

I can't help you unless you post complete fully working code.

view this post on Zulip Mario Carneiro (Feb 25 2020 at 09:28):

You have to use the equation compiler if you want to write a recursive function like that, i.e.

def foo : type
| case1 := bla
| case2 := foo bar

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 09:31):

Is the issue simply that row_product_helper is defined after you use it in row_product? No import will help you there, you have to define things before you use them.

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 11:43):

PS I found learn you a haskell really helpful when I was trying to figure out what functional languages looked like in general.

view this post on Zulip Rocky Kamen-Rubio (Feb 25 2020 at 20:23):

Kevin Buzzard said:

(unless there's a snazzy way to get the rows and columns from a matrix as a list instead of as vectors, but it seems like that's not possible).

I don't really know what you mean. Anything is possible. Just write the function.

Looking at the documentation for row it looks like it returns a vector not a list. You're right though that I could just convert it to a list and then product. Maybe this is an indication that a more functional approach would be preferred/more in line with how Lean is built?

I tried implementing this recursive algorithm on my matrix in the meantime too, but keep getting that the recursive call is an "unknown identifier". Is there an import statement or something I'm missing

I can't help you unless you post complete fully working code.

I posted the code I have below the text. Is it not visible to you? Do you mean that I need to include all my import statements as well?

view this post on Zulip Rocky Kamen-Rubio (Feb 25 2020 at 20:25):

Kevin Buzzard said:

Is the issue simply that row_product_helper is defined after you use it in row_product? No import will help you there, you have to define things before you use them.

Even reversing the order of the two definitions, the recursive call in row_product_helper gives me an error. I'll check out learn you a haskell and see if that gives me more clarity. Thank you!

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 20:26):

I cut and pasted the code you posted and it didn't work. Yes, include everything which makes it work!

view this post on Zulip Rocky Kamen-Rubio (Feb 25 2020 at 20:26):

Mario Carneiro said:

You have to use the equation compiler if you want to write a recursive function like that, i.e.

def foo : type
| case1 := bla
| case2 := foo bar

Interesting. I'll try rewriting my function like this and see if it helps. Thank you!

view this post on Zulip Rocky Kamen-Rubio (Feb 25 2020 at 20:30):

Kevin Buzzard said:

I cut and pasted the code you posted and it didn't work. Yes, include everything which makes it work!

I added the import statements. I'll be sure to include them in future posts.

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 21:17):

Your code doesn't work because you use row_product_helper before you define it. And if you switch the order of row_product_helper and row_product it doesn't work because mat r c doesn't make sense because r has type nat and not type fin m. But even if you fix that it won't work because you can't use row_product_helper in the definition of row_product_helper, that doesn't make sense in functional programming.

view this post on Zulip Kevin Buzzard (Feb 25 2020 at 21:39):

I now understand Mario's reply (I'm much less good than some other people at "guessing what the user meant"). You can use the definition of X when defining X, as long as you only run X on strictly "smaller" things. Here's a less abstract example:

def Fib :   
| 0 := 0
| 1 := 1
| (n + 2) := Fib n + Fib (n + 1)

You might want to read about how the equation compiler works in Theorem Proving In Lean, although depending on what you know you might have to read a bunch of earlier chapters first.

view this post on Zulip Rocky Kamen-Rubio (Feb 26 2020 at 20:27):

Kevin Buzzard said:

I now understand Mario's reply (I'm much less good than some other people at "guessing what the user meant"). You can use the definition of X when defining X, as long as you only run X on strictly "smaller" things. Here's a less abstract example:

def Fib :   
| 0 := 0
| 1 := 1
| (n + 2) := Fib n + Fib (n + 1)

You might want to read about how the equation compiler works in Theorem Proving In Lean, although depending on what you know you might have to read a bunch of earlier chapters first.

That makes sense. I'll take some time to go back and try to fully understand how the equation compiler works as well as matrices, lists, and vectors. Thanks!


Last updated: May 14 2021 at 12:18 UTC