swh:1:snp:a009335c9ad61a15b4ffe398f445dd601942b68c
Tip revision: 9e114126d5961fa73a21372b8a44f64723d79242 authored by François Dupressoir on 16 January 2020, 20:48:25 UTC
Generalize arguments about sampling in dexcepted
Generalize arguments about sampling in dexcepted
Tip revision: 9e11412
Real.ec
(* --------------------------------------------------------------------
* Copyright (c) - 2012--2016 - IMDEA Software Institute
* Copyright (c) - 2012--2018 - Inria
* Copyright (c) - 2012--2018 - Ecole Polytechnique
*
* Distributed under the terms of the CeCILL-B-V1 license
* -------------------------------------------------------------------- *)
(* -------------------------------------------------------------------- *)
require import Int Ring AlgTactic.
op zero : real.
op one : real.
op ( + ) : real -> real -> real.
op [ - ] : real -> real.
op ( * ) : real -> real -> real.
op inv : real -> real.
op ( < ) : real -> real -> bool.
op ( <= ) = fun x y => x < y \/ x = y.
abbrev ( - ) (x y : real) = x + -y.
abbrev ( / ) (x y : real) = x * (inv y).
abbrev [-printing] ( > ) (x y : real) = y < x.
abbrev [-printing] ( >= ) (x y : real) = y <= x.
(* -------------------------------------------------------------------- *)
op from_int: int -> real.
(* -------------------------------------------------------------------- *)
abbrev b2r (b:bool) = if b then from_int 1 else from_int 0.
(* -------------------------------------------------------------------- *)
op "`|_|" x = if from_int 0 <= x then x else -x.
op ( ^ ) : real -> int -> real.
axiom powrN (x : real) (n : int) :
x^(-n) = inv (x^n).
axiom powr0 (x : real) :
x^0 = one.
axiom powrS (x : real) (n : int) :
0 <= n => x^(n+1) = x^n * x.