Zulip Chat Archive
Stream: new members
Topic: Simplifying Prop with Known False Statements
Rocky KamenRubio (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 builtin 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 (Feb 10 2020 at 19:12):
norm_num
would probably solve that goal.
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
Rocky KamenRubio (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.
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.
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.
Rocky KamenRubio (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.
Rocky KamenRubio (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))
Reid Barton (Feb 18 2020 at 16:27):
This is "reverse the order of summation"?
Kevin Buzzard (Feb 18 2020 at 16:27):
Right
Reid Barton (Feb 18 2020 at 16:27):
It definitely won't be a tactic, it probably is a theorem that already exists.
Reid Barton (Feb 18 2020 at 16:28):
I think it's whatever the to_additive of prod_product
is
Reid Barton (Feb 18 2020 at 16:29):
well, combined with more stuff. How can this not exist already?
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...
Kevin Buzzard (Feb 18 2020 at 16:30):
Oh yeah so we're in exactly the same situation as in the other thread.
Reid Barton (Feb 18 2020 at 16:30):
oh, prod_comm
Reid Barton (Feb 18 2020 at 16:30):
this should probably have a comment with things like "fubini" and maybe "prod_prod"
Kevin Buzzard (Feb 18 2020 at 16:31):
https://leanprover.zulipchat.com/#narrow/stream/113489newmembers/topic/spheres/near/188451346 also ideally needs to switch from finset.sum finset.univ (fin n)
to finset.sum finset.range n
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
Kevin Buzzard (Feb 18 2020 at 16:32):
I don't like the look of induction on n
Kevin Buzzard (Feb 18 2020 at 16:44):
What I'm saying is that fin n
doesn't have type finset ℕ
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
Rocky KamenRubio (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
Kevin Buzzard (Feb 18 2020 at 18:34):
ext
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)
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.
Kevin Buzzard (Feb 18 2020 at 18:36):
It results from a lack of understanding of mathematical equality ;)
Rocky KamenRubio (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
ScreenShot20200218at1.44.34PM.png
Bryan Ginge 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.
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.
Kevin Buzzard (Feb 18 2020 at 18:51):
The error in the docstring is irrelevant, that's just some parser issue.
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.
Rocky KamenRubio (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. ScreenShot20200218at2.03.20PM.png
Rocky KamenRubio (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.
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.
Kevin Buzzard (Feb 18 2020 at 19:11):
you need to rewrite h
a lot and then use finset.sum_comm
Kevin Buzzard (Feb 18 2020 at 19:12):
Your goal is the equality of two natural numbers so you can't use ext
here.
Kevin Buzzard (Feb 18 2020 at 19:12):
actually maybe just finset.sum_comm
will work directly
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.
Rocky KamenRubio (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? :)
Bryan Ginge Chen (Feb 23 2020 at 19:01):
@Rocky KamenRubio I scrolled up a bit in the thread but I didn't see any selfcontained code that I could copy / paste to try out. Could you provide that in a post or a link to a github gist?
Rocky KamenRubio (Feb 23 2020 at 19:11):
@Bryan Ginge 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 (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?
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,
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.
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,
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 truefalse 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 KamenRubio (Feb 23 2020 at 20:17):

Yes, replacing
use (j,hj)
withexistsi ((j,hj) : fin n),
resolved the issue, thank you! 
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?

I defined
consistent
even
andodd
asProp
s 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 Ginge 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
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.
Bryan Ginge 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)
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.
Rocky KamenRubio (Feb 24 2020 at 20:33):
Kevin Buzzard said:
You defined
consistent
as a Prop, andand
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. Yourset_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 KamenRubio (Feb 24 2020 at 20:41):
Rocky KamenRubio 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 domatrix_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 (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
Rocky KamenRubio (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 likelist.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 (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.
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
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.
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.
Rocky KamenRubio (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?
Rocky KamenRubio (Feb 25 2020 at 20:25):
Kevin Buzzard said:
Is the issue simply that
row_product_helper
is defined after you use it inrow_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 (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!
Rocky KamenRubio (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!
Rocky KamenRubio (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.
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.
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.
Rocky KamenRubio (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