Re: [Axiom-developer] Proving Axiom Correct

[Kurt Pagani]

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 address@hidden:
> 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
> address@hidden
> https://lists.nongnu.org/mailman/listinfo/axiom-developer
>