Hi Tim that's great, indeed. Coq also seems to me best suited for this challenging task, however, I would suggest to use "the mathematical proof language (MPL)" as described in chapeter 11 of the reference manual. It's a matter of taste, of courese, but imho MPL is much more readable (at least to mathematicians) I guess.
The following primitive example (standard vs. mpl) might be convincing. Standard proof language: ------------------------ Section Group. Parameter S : Set. Parameter e : S. Parameter inv : S -> S. Parameter op: S -> S -> S. Infix "*" := op. Axiom left_id : forall x:S, e * x = x. Axiom left_inv : forall x:S, inv x * x = e. Axiom assoc : forall x y z:S, x * (y * z) = (x * y) * z. Proposition left_cancel : forall x y z:S, x * y = x * z -> y = z. Proof. intros. assert (inv x * (x * y) = inv x * (x * z)) as H1. rewrite H. reflexivity. rewrite assoc in H1. rewrite assoc in H1. rewrite left_inv in H1. rewrite left_id in H1. rewrite left_id in H1. assumption. Qed. Proposition right_id : forall x:S, x * e = x. Proof. intros. apply left_cancel with (x:=inv x). rewrite assoc. rewrite left_inv. apply left_id. Qed. the same in MPL: ---------------- Section Group. Parameter S : Set. Parameter e : S. Parameter inv : S -> S. Parameter op: S -> S -> S. Infix "*" := op. Axiom left_id : forall x:S, e * x = x. Axiom left_inv : forall x:S, inv x * x = e. Axiom assoc : forall x y z:S, x * (y * z) = (x * y) * z. Proposition left_cancel : forall x y z:S, x * y = x * z -> y = z. proof. let x:S, y:S, z:S. assume (x*y=x*z). then (inv x *(x*y) = inv x * (x*z)). then ((inv x * x)*y=(inv x* x)*z) by assoc. then (e*y=e*z) by left_inv. then (y=z) by left_id. take _fact0. end proof. Qed. Proposition right_id : forall x:S, x * e = x. proof. let x:S. then (e*e=e) by left_id. then ((inv x * x)*e=inv x * x) by left_inv. then (inv x*(x*e)= inv x * x) by assoc. hence (x*e=x) by left_cancel. end proof. Qed. Well, it's a quick hack, however, it contains almost every principle to prove the 'algebra' correct. Kurt Am 16.07.2015 um 08:03 schrieb d...@axiom-developer.org: > COQ is being used as the proof engine for Spad-level code. > > The latest change will automatically extract literate chunks > labelled 'coq' into a separate location for the COQ proof engine. > This can be controlled from the make command line by adding COQ=coq. > > ACL2, with its lisp-based syntax and semantics, is the appropriate > engine for proving the interpreter and compiler. COQ, with its > ability to form dependent types, is the appropriate engine for > proving the algebra. Thus we're able to use the best tool for > each level of abstraction. > > Tim > > _______________________________________________ > Axiom-developer mailing list > Axiom-developer@nongnu.org > https://lists.nongnu.org/mailman/listinfo/axiom-developer > _______________________________________________ Axiom-developer mailing list Axiom-developer@nongnu.org https://lists.nongnu.org/mailman/listinfo/axiom-developer
