From time to time I'm starting a Theorem prover tutorial, sometimes I even finish. The learning curve is long.
Thanks, I looked at the Agda version. It is more explicit and well documented.
And I agree: tactics are another thing to learn and can be very arcane.
But in this discussion everybody admires Isabelle/Hol's automation: "I'm envious of the degree of automation that Isabelle affords".
---
My problem with "theorem eval_eval : x ~>* (eval x).embed" was very basic.
I got confused by the infix definition of "~>*".
Viewing the type in the playground as "∀ {a : Ty} {x : Exp a}, RTC Eval x (Val.embed a (eval x))" helped.
---
I am just dabbling around but I will try Lean 4. It seems to work well though it is not officially released.
And Lean 4 seems to be a very fast funcional programming language.
(I actually finished an Agda Tutorial a few years ago, it's focus is on programming. Lean somehow succeeded to "fix" or "hack around" this annoying intensional equality:
"Lean's standard library defines an additional axiom, propositional extensionality, and a quotient construction which in turn implies the principle of function extensionality"
> I got confused by the infix definition of "~>*".
Aaah, I'm sorry -- I thought you meant the theorem body -- the proof itself -- was hard to parse. (Which it also is!)
Yes, custom infix operators are just one of many novelties you can find in these languages. I think Haskell is the only "mainstream" (hah) language I'm familiar with that has anywhere close to the same degree of syntax customization.
All these things together really do make for a steep learning curve...
Thanks, I looked at the Agda version. It is more explicit and well documented.
And I agree: tactics are another thing to learn and can be very arcane.
But in this discussion everybody admires Isabelle/Hol's automation: "I'm envious of the degree of automation that Isabelle affords".
---
My problem with "theorem eval_eval : x ~>* (eval x).embed" was very basic.
I got confused by the infix definition of "~>*".
Viewing the type in the playground as "∀ {a : Ty} {x : Exp a}, RTC Eval x (Val.embed a (eval x))" helped.
---
I am just dabbling around but I will try Lean 4. It seems to work well though it is not officially released.
And Lean 4 seems to be a very fast funcional programming language.
(I actually finished an Agda Tutorial a few years ago, it's focus is on programming. Lean somehow succeeded to "fix" or "hack around" this annoying intensional equality:
"Lean's standard library defines an additional axiom, propositional extensionality, and a quotient construction which in turn implies the principle of function extensionality"
)