RingCloning.ec
``````(* This theory should make use of theories for groups.
It is currently mostly being developed towards getting
fixed-length bitstrings formalized as boolean rings,
automatically yielding many useful lemmas from a
small number of simple core axioms. *)
theory Ring.
type ring.

const zero: ring.
op ( + ) : ring -> ring -> ring.
op [ - ] : ring -> ring.

axiom addrA (r1 r2 r3 : ring):
(r1 + r2) + r3 = r1 + (r2 + r3).

axiom addrC (r1 r2 : ring):
r1 + r2 = r2 + r1.

zero + r = r.

r + -r = zero.

(** Ring multiplication *)
const one: ring.
op ( * ): ring -> ring -> ring.

axiom mulrA (r1 r2 r3 : ring):
(r1 * r2) * r3 = r1 * (r2 * r3).

axiom mul1r (r : ring):
one * r = r.

(** Distributivity of addition over multiplication *)
axiom mulrDadd (r1 r2 r3 : ring):
r1 * (r2 + r3)= (r1 * r2) + (r1 * r3).

axiom mulDradd (r1 r2 r3 : ring):
(r1 + r2) * r3 = (r1 * r3) + (r2 * r3).
end Ring.

theory RingT.
clone import Ring.
abbrev ( - ) (r1 r2 : ring) = r1 + -r2.

(** Lemmas *)
r + zero = r.
proof strict.
qed.

-r + r = zero.
proof strict.
qed.

lemma addIr (r r1 r2 : ring):
(r1 + r = r2 + r) =>
r1 = r2.
proof strict.
by move=> r1_r2;
qed.

lemma addrI (r r1 r2 : ring):
(r + r1 = r + r2) =>
r1 = r2.
proof strict.
qed.
end RingT.

theory CRing.
clone import Ring.

axiom mulrC (r1 r2 : ring):
r1 * r2 = r2 * r1.
end CRing.

theory CRingT.
clone        Ring.
clone        CRing with
theory Ring <- Ring.
clone        RingT with
theory Ring <- Ring.

import Ring.
import CRing.
import RingT.

lemma mulrC (r1 r2 : ring):
r1 * r2 = r2 * r1.
proof strict.
by rewrite mulrC.
qed.

lemma mulrCA (r1 r2 r3 : ring):
r1 * (r2 * r3) = r2 * (r1 * r3).
proof strict.
by rewrite -2!mulrA (mulrC r1).
qed.

lemma mulrAC (r1 r2 r3 : ring):
(r1 * r2) * r3 = (r1 * r3) * r2.
proof strict.
by rewrite 2!mulrA (mulrC r2).
qed.

lemma mulrACA (r1 r2 r3 r4 : ring):
(r1 * r2) * (r3 * r4) = (r1 * r3) * (r2 * r4).
proof strict.
by rewrite mulrA (mulrCA r2) -mulrA.
qed.
end CRingT.

theory BRing.
clone import Ring.

axiom mulrK (r : ring):
r * r = r.
end BRing.

theory BRingT.
clone        Ring.
clone        RingT with
theory Ring <- Ring.
clone        BRing with
theory Ring <- Ring.

import Ring.
import RingT.
import BRing.

lemma neg_is_id (r : ring):
r + r = zero.
proof strict.
by rewrite -(addIr (r + r) (r + r) zero) //
qed.

lemma mulrC (r1 r2 : ring):
r1 * r2 = r2 * r1.
proof strict.
by rewrite -(addIr (r2 * r1) (r1 * r2) (r2 * r1)) // (neg_is_id (r2 * r1))
-{4}(addrI r1 (r1 * r2 + (r2 * r1 + r2)) r2) // -addrA
qed.
end BRingT.

(*
(* Example: Ring structures on bool *)
theory BoolRing.
require import Bool.
op id (b:bool) = b.
clone Ring as RBool with
type ring = bool,
op zero = false,
op ( + ) = (^^),
op [ - ] = id,
op one = true,
op ( * ) = (/\)
proof * by (delta; smt).

clone BRing as BRBool with
theory Ring = RBool
proof * by (move=> r; delta; smt).

clone BRingT as BRBoolT with
theory Ring = RBool.

print theory BRBoolT.
*)
``````