|
I am nothing more than an enthusiastic dabbler, but these have helped me. There are two very different directions
1. the sort of full on proof automation with tactics https://direct.mit.edu/books/oa-monograph/4021/Certified-Pro... Dr. Chlipala builds up understanding of the "crush" tactic, which more or less lets you specify an inductive hypothesis, and that tactic fiddles around with identifying the base case, and expanding enough to generate the n+1 step. Along the way, you get exposure to using Gallina to write your own tactics. it's neat, from a programmer point of view, because you can automate away the boring parts. There is pretty good discussion of debugging tactics, which might provide a path to transforming machine proofs into something a bit more comprehensible. at the very least, you can recover the application of axioms and such that did the transformation. The other direction, that has been much more enlightening for me (the amateur hobbyist) was agda and Jesper Cockx's tutorial- https://github.com/jespercockx/agda-lecture-notes/blob/maste...
he builds up all of the notation from, well, nothing.
for example, you get refl, and then build up -- symmetry of equality
sym : {A : Set} {x y : A} → x ≡ y → y ≡ x sym refl = refl
-- transitivity of equality
trans : {A : Set} {x y z : A} → x ≡ y → y ≡ z → x ≡ z (54) trans refl refl = refl
-- congruence of equality
cong : {A B : Set} {x y : A} → (f : A → B) → x ≡ y → f x ≡ f y cong f refl = refl
along with the syntax that comes with the agda std lib.
agda is different, but you can still extract to Haskell (and allegedly javascript for node, but that was a little flakey for me and might go away in a future release). less useful for your goals, much more programming oriented - https://plfa.github.io is pretty good, and worth mentioning as a reference. |