3 ms·

I could not write this stuff. It looks simple but it isn't. I played with Sebastian Ulrich's Lean 4 Port of Conor Mc Bride's Agda Code. ( bottom of https://le

• Twisol 4y ago
  > My intuition is: evaluating in Lean and embedding the result in the toy language is identical to big step evaluation in the toy language. Yes, I think that's right. > But I can't parse the theorem. I think there's a bit of a divide between languages with tactic-based proofs and languages without tactics, and it looks like both Lean and Isabelle use tactics. I've gotten very comfortable with Agda over the past year. Agda doesn't have a real tactics metalanguage; but I honestly prefer working with proof terms, since it's easier (I feel) to write comprehensible proofs. While tactics make for very compact proofs, I think giving a proof some space to breathe is a good thing -- I'm interested in why it's true, not only that it's true. I think the analogous theorem in Conor McBride's Agda version of this development is here [1]: ev=>* : {t : Ty} (x : Exp t) -> x =>* ve (ev x) where "eval _" in Lean becomes "ev x", and "_.embed" becomes "ve _". The theorem body is heavily commented (nice!), and each case is handled explicitly and in full. While the development is probably a little bit longer than in Lean or Isabelle, I find it easier to approach. [1] https://github.com/pigworker/Samizdat/blob/main/ExampleSemantics.agda#L285 https://github.com/pigworker/Samizdat/blob/main/ExampleSeman... > I could not write this stuff. It looks simple but it isn't. True that. I bounced a number of times off of proof assistants before it stuck. Like I said, I feel very comfortable with Agda now; but I won't claim this is easy.
  • hackandthink 4y ago
    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" )
    • Twisol 4y ago
      > 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...