Simplifying Prop with Known False Statements

Stream: new members

[Rocky Kamen-Rubio]

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?

[Chris Hughes]

norm_num would probably solve that goal.

[Cerek Hillen (he) (W2'20)]

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

[Rocky Kamen-Rubio]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Rocky Kamen-Rubio]

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.

[Rocky Kamen-Rubio]

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))

[Reid Barton]

This is "reverse the order of summation"?

[Kevin Buzzard]

Right

[Reid Barton]

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

[Reid Barton]

I think it's whatever the to_additive of prod_product is

[Reid Barton]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Reid Barton]

oh, prod_comm

[Reid Barton]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

I don't like the look of induction on n

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Rocky Kamen-Rubio]

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

[Kevin Buzzard]

ext

[Kevin Buzzard]

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)

[Kevin Buzzard]

"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.

[Kevin Buzzard]

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

[Rocky Kamen-Rubio]

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

[Bryan Gin-ge Chen]

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.

[Patrick Massot]

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.

[Kevin Buzzard]

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

[Kevin Buzzard]

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.

[Rocky Kamen-Rubio]

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

[Rocky Kamen-Rubio]

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.

[Patrick Massot]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

actually maybe just finset.sum_comm will work directly

[Kevin Buzzard]

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.

[Rocky Kamen-Rubio]

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? :-)

[Bryan Gin-ge Chen]

@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?

[Rocky Kamen-Rubio]

@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

[Kevin Buzzard]

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?

[Kevin Buzzard]

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,

[Kevin Buzzard]

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

[Kevin Buzzard]

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,

[Kevin Buzzard]

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.

[Rocky Kamen-Rubio]

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)

[Bryan Gin-ge Chen]

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

[Kevin Buzzard]

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.

[Bryan Gin-ge Chen]

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)

[Kevin Buzzard]

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.

[Rocky Kamen-Rubio]

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!

[Rocky Kamen-Rubio]

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.

[Kevin Buzzard]

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

[Rocky Kamen-Rubio]

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))

[Kevin Buzzard]

(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.

[Mario Carneiro]

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

[Kevin Buzzard]

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.

[Kevin Buzzard]

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

[Rocky Kamen-Rubio]

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?

[Rocky Kamen-Rubio]

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!

[Kevin Buzzard]

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

[Rocky Kamen-Rubio]

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!

[Rocky Kamen-Rubio]

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.

[Kevin Buzzard]

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.

[Kevin Buzzard]

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.

[Rocky Kamen-Rubio]

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!