Loading collection data...
Collections are a way for you to organize kata so that you can create your own training routines. Every collection you create is public and automatically sharable with other warriors. After you have added a few kata to a collection you and others can train on the kata contained within the collection.
Get started now by creating a new collection.
This comment is hidden because it contains spoiler information about the solution
If this comment is addressed to me, I am not sure I am confident enough with Coq syntax any more to know whether what you have done is OK (I haven't used Coq for about 2 years and I quickly forget things which I don't use a lot).
Either there is some issue with imports (the most likely -- even should be defined in preloaded) or there's a difference between Lean 3.5.1 (CoCalc) and Lean 3.7.2 (here) but that is vanishingly unlikely with kata at this level (cutting edge mathlib stuff changes but not basic stuff like this).
Edit: Oh, but I see you solved it :-)
@monadius :
rw X at this, exact this
can be abbreviated torwa X at this
; rwa := rw, assumption. Normally rwa is used when the goal can be rewritten to an assumption but this variant also works.The description claims that SL_2(N) is a group. Not so (no inverses). It might also be worth mentioning that the description defines SL_2(N) as being {(a,b,c,d) : ad-bc=1} but the actual definition is completely different. One could beef this kata up by asking to prove that evaluation is a bijection from the free monoid
SL₂ℕ
to the matrices with ad-bc=1, rather than just an injection to the type of all natural number matrices.This comment is hidden because it contains spoiler information about the solution
Ooh yes thanks.
PS I wouldn't bother with the mutual types -- I think the set-up here is fine.
This is type theory 101 in the CS courses, see for example https://softwarefoundations.cis.upenn.edu/lf-current/IndProp.html#lab207 . I don't think you need examples.
Suggestions:
I would call the
even_succ
constructoreven_ss
following software foundations, and similarlyodd_ss
. The standard mathlib names for your lemmas would be something like this:even_plus_one_is_odd
->odd_add_one
,odd_plus_one_is_even
->even_add_one
,every_number_is_odd_or_even
->odd_or_even
,odd_plus_odd_is_even
->odd_add_odd
,odd_plus_even_is_odd
->even_add_odd
etc,even_times_even_is_even
->even_mul_even
etc andeven_times_anything_is_even
->even_mul
. Finally, a lot of the variables should be implicit: whenever you have an assumption (n) (hn : even n) the n should be {n}; this applies toodd_add_one
etc,odd_add_odd
etc andeven_mul_even
etc.Not if (1+2+...+n) is embedded in the middle of a more complex term, for example
(3+n^2)*(5+(1+2+...+n))
. Multplying the sum by 2 is a pain.This comment is hidden because it contains spoiler information about the solution
This comment is hidden because it contains spoiler information about the solution
I can reproduce. This is hard to debug without having access to the exact contents of Preloaded.lean [do I have access to this file?]
How come one of the solutions has a sorry?
What is the point of n? Why not just ask to prove empty_place t = node t + 1?
Loading more items...