2 ms·
Wow, nice to see readable math proofs that "run themselves", e.g. they define (a unary representation of) natural numbers as follows: Inductive nat : Typ
by ivan_ah 8y ago
Wow, 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....