search

isovector / certainty-by-construction

Source material for Certainty by Construction
https://leanpub.com/certainty-by-construction/
36 stars 9 forks source link

Exponentiation doesn't work with `refl` #4

Closed blackgnezdo closed 1 year ago

blackgnezdo commented 1 year ago

As I'm going through the Naturals I ended up with a bit of a problem proving the proposition below:

    _ : two ^ one ≡ two
    _ = refl
2-numbers.agda:73,9-13
zero != suc zero of type ℕ
when checking that the expression refl has type two ^ one ≡ two

I believe I correctly re-typed the text from the chapter, but just in case, here's the module. 2-numbers.agda.txt

Random poking at ChatGPT suggests that a rewrite using an identity related to multiplication is enough to prove this, but this is yet unknown by this point in the book.

blackgnezdo commented 1 year ago

And it turns out I had a bug, my fixity was wrong and so I defined exponentiation incorrectly. Having fixed the module I have a working proof of 2^2=4 without any advanced magic.