https://github.com/EasyCrypt/easycrypt
Tip revision: 846710a2a656834065e745d19416ebdc83158f55 authored by Benjamin Gregoire on 14 July 2019, 06:50:07 UTC
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Start restructuration of the code to be able to avant mutual dependency between type and mpath
Tip revision: 846710a
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.
(** Ring addition *)
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.
axiom add0r (r : ring):
zero + r = r.
axiom addNr (r : ring):
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 *)
lemma addr0 (r : ring):
r + zero = r.
proof strict.
by rewrite addrC add0r.
qed.
lemma addrN (r : ring):
-r + r = zero.
proof strict.
by rewrite addrC addNr.
qed.
lemma addIr (r r1 r2 : ring):
(r1 + r = r2 + r) =>
r1 = r2.
proof strict.
by move=> r1_r2;
rewrite -addr0 -(addr0 r2) -(addNr r) -2!addrA -r1_r2.
qed.
lemma addrI (r r1 r2 : ring):
(r + r1 = r + r2) =>
r1 = r2.
proof strict.
by rewrite 2!(addrC r)=> r1_r2; rewrite (addIr r r1 r2).
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) //
(add0r (r + r)) -(mulrK r) -{1 2}mulrDadd -mulDradd 2!mulrK.
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))
-(addIr r2 (r1 * r2 + r2 * r1) zero) // (add0r r2) addrA
-{4}(addrI r1 (r1 * r2 + (r2 * r1 + r2)) r2) // -addrA
-{1}(mulrK r1) -{3}(mulrK r2) -2!mulrDadd -mulDradd mulrK.
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.
*)