2 ms·
Using a Proof Assistant to Teach Programming Language Foundations (2010) [video]
- ivan_ah 8y agoWow, nice to see readable math proofs that "run themselves", e.g. they define (a unary representation of) natural numbers as follows: Inductive nat : Type := | O : nat | S : nat → nat. S = successor Then they define 'plus' as Fixpoint plus (n : nat) (m : nat) : nat := match n with | O ⇒ m | S n' ⇒ S (plus n' m) end. Adding three to two now gives five, as we'd expect: Compute (plus 3 2). The simplification that Coq performs to reach this conclusion can be visualized as follows: (* plus (S (S (S O))) (S (S O)) ==> S (plus (S (S O)) (S (S O))) by the second clause of the match ==> S (S (plus (S O) (S (S O)))) by the second clause of the match ==> S (S (S (plus O (S (S O))))) by the second clause of the match ==> S (S (S (S (S O)))) by the first clause of the match *) via https://softwarefoundations.cis.upenn.edu/lf-current/Basics.html#lab27 https://softwarefoundations.cis.upenn.edu/lf-current/Basics....