https://github.com/EasyCrypt/easycrypt
Tip revision: 0ea747e8820cd9b084d76ca576c4406acbc841ab authored by Pierre-Yves Strub on 13 October 2023, 13:06:18 UTC
lambda bindings now take simple variables only
lambda bindings now take simple variables only
Tip revision: 0ea747e
StdOrder.ec
(* -------------------------------------------------------------------- *)
require import AllCore Ring StdRing.
require (*--*) Number.
(*---*) import IntID.
(* -------------------------------------------------------------------- *)
theory IntOrder.
clone include Number.RealDomain
with type t <- int,
pred Domain.unit (z : int) <- (z = 1 \/ z = -1),
op Domain.zeror <- 0,
op Domain.oner <- 1,
op Domain.( + ) <- Int.( + ),
op Domain.([-]) <- Int.([-]),
op Domain.( * ) <- Int.( * ),
op Domain.invr <- (fun (z : int) => z),
op Domain.intmul <- IntID.intmul,
op Domain.ofint <- IntID.ofint_id,
op Domain.exp <- IntID.exp,
op Domain.lreg <- IntID.lreg,
op minr <- min,
op maxr <- max,
op "`|_|" <- Int."`|_|",
op ( <= ) <- Int.(<=),
op ( < ) <- Int.(< )
proof Domain.* by smt(invr0), Axioms.* by smt()
remove abbrev Domain.(-)
remove abbrev Domain.(/).
(* -------------------------------------------------------------------- *)
op signz (z : int) = (exp (-1) (b2i (z < 0))) * (b2i (z <> 0)).
lemma signzE z : z = (signz z) * `|z|.
proof.
rewrite /signz; case: (z = 0) => [->|]; 1: by rewrite normr0.
move=> nz_z; rewrite mulr1; case: (z < 0); rewrite (expr0, expr1).
by move=> /ltr0_norm => ->; rewrite mulN1r opprK.
by rewrite ltrNge => /= /ger0_norm => ->.
qed.
lemma signzN (z : int) : signz (-z) = - (signz z).
proof.
rewrite /signz oppr_eq0; case: (z = 0) => //= nz_z.
rewrite b2i1 /= oppr_lt0 ltrNge ler_eqVlt nz_z /=.
by case: (z < 0) => //=; rewrite !(expr0, expr1).
qed.
lemma signz0 : signz 0 = 0.
proof. by rewrite /signz ltrr. qed.
lemma signz_gt0 (z : int) : 0 < z => signz z = 1.
proof.
move=> gt0_z; rewrite /signz (gtr_eqF z) // b2i1 /=.
by rewrite ltrNge ltrW // b2i0 expr0.
qed.
lemma signz_lt0 (z : int) : z < 0 => signz z = -1.
proof.
by move=> lt0_z; rewrite -(opprK z) signzN signz_gt0 ?oppr_gt0.
qed.
lemma signVzE (z : int) : `|z| = (signz z) * z.
proof.
rewrite {3}(signzE) mulrA /signz; case: (z = 0).
by move=> ->; rewrite normr0.
move=> nz_0; rewrite b2i1 /= -{1}(mul1r `|z|); congr.
rewrite -exprD_nneg ?b2i_ge0 -signr_odd ?addr_ge0 ?b2i_ge0.
by rewrite -mul1r2z oddM /ofint_id intmulz odd2 expr0.
qed.
end IntOrder.
(* -------------------------------------------------------------------- *)
theory RealOrder.
clone include Number.RealField
with type Field.t <- real,
op Field.zeror <- 0%r,
op Field.oner <- 1%r,
op Field.( + ) <- Real.( + ),
op Field.([-]) <- Real.([-]),
op Field.( * ) <- Real.( * ),
op Field.invr <- Real.inv,
op Field.intmul <- RField.intmul,
op Field.ofint <- RField.ofint,
op Field.exp <- RField.exp,
op Field.lreg <- RField.lreg,
op minr = fun x y : real => if x <= y then x else y,
op maxr = fun x y : real => if y <= x then x else y,
op "`|_|" <- Real."`|_|",
op ( <= ) <- Real.(<=),
op ( < ) <- Real.(< )
proof Field.* by smt(RField.invr0), Axioms.* by smt()
remove abbrev Field.(-)
remove abbrev Field.(/).
(* This is used by the upto tactic *)
lemma upto_maxr (E1 E1b E1nb E2 E2b E2nb E1b' E2b' : real) :
E1 = E1b + E1nb =>
E2 = E2b + E2nb =>
E1nb = E2nb =>
0.0 <= E1b =>
E1b <= E1b' =>
0.0 <= E2b =>
E2b <= E2b' =>
`| E1 - E2 | <= maxr E1b' E2b'.
proof.
move=> h1 h2 h3 h4 h5 h6 h7.
apply (ler_trans `|E1b - E2b|); 1: by apply (upto_abs _ _ _ _ _ _ h1 h2 h3).
apply (ler_trans (maxr E1b E2b)); 1: by apply (ler_norm_maxr _ _ h4 h6).
by apply ler_maxr_trans.
qed.
end RealOrder.