(* --------------------------------------------------------------------
* Copyright (c) - 2012--2015 - IMDEA Software Institute
* Copyright (c) - 2012--2015 - Inria
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require import Fun Int IntDiv.
require (*--*) Subtype Ring.
(* -------------------------------------------------------------------- *)
(* This abstract theory provides the construction of the ring Z/pZ. *)
(* The structure is also equipped with a (finite) field structure when *)
(* the modulus is an actual prime. *)
(* -------------------------------------------------------------------- *)
const p : { int | 2 <= p } as le2_p.
(* -------------------------------------------------------------------- *)
type zmod.
clone Subtype as Sub with
type T <- int, type sT <- zmod,
pred P (x : int) <- 0 <= x < p.
(* -------------------------------------------------------------------- *)
op inzmod (z : int) = Sub.insubd (z %% p).
op asint (z : zmod) = Sub.val z.
lemma inzmodK (z : int): asint (inzmod z) = z %% p.
proof. smt. qed.
lemma asint_inj: injective asint by apply/Sub.val_inj.
(* -------------------------------------------------------------------- *)
op zero = inzmod 0.
op one = inzmod 1.
op [ - ] x = inzmod (- asint x).
op ( + ) x y = inzmod (asint x + asint y).
op ( * ) x y = inzmod (asint x * asint y).
(* -------------------------------------------------------------------- *)
lemma zeroE: asint Self.zero = 0.
proof. by rewrite /zero inzmodK mod0z. qed.
lemma oneE: asint Self.one = 1.
proof. by rewrite /one inzmodK modz_small; smt. qed.
lemma oppE (x : zmod): asint (-x) = (- (asint x)) %% p.
proof. by rewrite /[-] /inzmod /asint /= Sub.insubdK; smt. qed.
lemma addE (x y : zmod): asint (x + y) = (asint x + asint y) %% p.
proof. by rewrite /(+) /inzmod /asint /= Sub.insubdK; smt. qed.
lemma mulE (x y : zmod): asint (x * y) = (asint x * asint y) %% p.
proof. rewrite /( * ) /inzmod /asint /= Sub.insubdK; smt. qed.
(* -------------------------------------------------------------------- *)
theory ZModule.
lemma addrA (x y z : zmod): x + (y + z) = (x + y) + z.
proof. by apply/asint_inj; rewrite !addE modzDml modzDmr addzA. qed.
lemma addrC (x y : zmod): x + y = y + x.
proof. by apply/asint_inj; rewrite !addE addzC. qed.
lemma add0r (x : zmod): Self.zero + x = x.
proof. by apply/asint_inj; rewrite !(addE, zeroE) add0z smt. qed.
lemma addNr (x : zmod): (-x) + x = Self.zero.
proof.
apply/asint_inj; rewrite !(zeroE, addE, oppE).
by rewrite modzDml addNz mod0z.
qed.
end ZModule.
(* -------------------------------------------------------------------- *)
clone Ring.ZModule as ZModpZMod with
type t <- zmod,
op zeror <- Self.zero,
op (+) <- Self.( + ),
op [-] <- Self.([-])
proof *.
realize addrA. proof. by apply/ZModule.addrA. qed.
realize addrC. proof. by apply/ZModule.addrC. qed.
realize add0r. proof. by apply/ZModule.add0r. qed.
realize addNr. proof. by apply/ZModule.addNr. qed.
(* -------------------------------------------------------------------- *)
theory ComRing.
lemma oner_neq0 : Self.one <> Self.zero by smt.
lemma mulrA (x y z : zmod): x * (y * z) = (x * y) * z.
proof. by apply/asint_inj; rewrite !mulE modzMml modzMmr mulzA. qed.
lemma mulrC (x y : zmod): x * y = y * x.
proof. by apply/asint_inj; rewrite !mulE mulzC. qed.
lemma mul1r (x : zmod): Self.one * x = x.
proof. by apply/asint_inj; rewrite !(mulE, oneE) mul1z smt. qed.
lemma mulrDl (x y z : zmod): (x + y) * z = (x * z) + (y * z).
proof.
apply/asint_inj; rewrite !(addE, mulE).
by rewrite !(modzMml, modzMmr, modzDml, modzDmr) mulzDl.
qed.
end ComRing.
(* -------------------------------------------------------------------- *)
lemma inzmodD (a b : int):
inzmod (a + b) = inzmod a + inzmod b.
proof. by apply/asint_inj; rewrite addE !inzmodK modzDmr modzDml. qed.
lemma inzmodM (a b : int):
inzmod (a * b) = inzmod a * inzmod b.
proof. by apply/asint_inj; rewrite mulE !inzmodK modzMmr modzMml. qed.
lemma inzmodN (n : int):
inzmod (- n) = -(inzmod n).
proof. by apply/asint_inj; rewrite oppE !inzmodK modzNm. qed.
lemma inzmodB (a b : int):
inzmod (a - b) = (inzmod a) + (- (inzmod b)).
proof. by rewrite inzmodD inzmodN. qed.