# IRC log for #isabelle, 2015-10-30

All times shown according to UTC.

Time Nick Message
00:29 ilbot3 joined #isabelle
00:29 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
02:47 ilbot3 joined #isabelle
02:47 Topic for #isabelle is now Official channel for the Isabelle/HOL theorem prover: http://www.cl.cam.ac.uk/research/hvg/Isabelle/index.html || Now with logging: http://irclog.perlgeek.de/isabelle/
03:25 tautologico I want to prove an equality f x = g y where both f and g are defined functions. trying to use "by simp" unfolds the left side but not the right side. and the result is a big term that I don't want to write explicitly. how can I prove this?
08:41 ThreeOfEight tautologico: that is impossible to answer without more context
09:43 tautologico I (re)defined natural numbers with S and Z constructors, a multiplication function (mult) and factorial. I want to prove factorial 5 = mult 12 10 (where 5 = (S (S (S (S (S Z))))) and so on)
10:08 ThreeOfEight tautologico: well show me your code
10:08 ThreeOfEight put it in a paste bin or something
10:09 ThreeOfEight (if it's a university assignment or something like that, use a private paste bin, /msg the link to me and delete it afterwards)
10:10 ThreeOfEight but from what you have told me so far, I wonder how you defined "5", "12", and "10"
10:10 ThreeOfEight and my guess would be that you would have to unfold those definitions
13:09 tautologico it's not an assignment :)
13:10 tautologico I'm translating parts of the "Software Foundations" book (uses Coq) to Isabelle/HOL, as an exercise
13:14 tautologico the relevant parts are in this gist: https://gist.github.com/tautologico/59fe0d68c4616e9ecb55
13:26 ThreeOfEight tautologico: oh that's easy
13:26 ThreeOfEight you just have to unfold the definitions of ten/twelve
13:26 ThreeOfEight e.g. "unfolding ten_def twelve_def by simp"
13:26 ThreeOfEight or "by (simp add: ten_def twelve_def)"
13:27 ThreeOfEight note that this proof will fail, because both your ten and your twelve are actually nines
13:28 tautologico that's right
13:28 tautologico it works, thank you :)
13:29 tautologico the original book uses a submodule when defining the naturals, and later closes the submodule so the rest of the code uses the standard nat type in Coq, so it can use number literals in this part
13:42 ThreeOfEight well if you really want to do this sort of thing, you should prove that your natural numbers form a semiring
13:42 ThreeOfEight http://downthetypehole.de/paste/GNbfdVQL
13:42 ThreeOfEight then you can use numeral syntax for them out of the box
13:43 ThreeOfEight I left out all the instance proofs (i.e. the semiring axioms for nat), but those are pretty straightforward
13:44 ThreeOfEight adding the eval_nat_numeral I proved in there to the simp set automatically converts numerals to the corresponding "S (S (S Z)))" notation
13:44 ThreeOfEight as shown in the example
13:45 ThreeOfEight (numerals are stored in LSBF binary internally)
14:20 tautologico that's good to know
14:20 tautologico I think if I define my nats inside a local context or "experiment" (I saw something like this in the manual) I can mirror the structure of the original text