https://github.com/EasyCrypt/easycrypt
Tip revision: ac9827aca3feeea075944b30d95b44c4bffb1030 authored by Charlie Jacomme on 08 March 2019, 14:00:31 UTC
rnd auto dans cramer shoup
rnd auto dans cramer shoup
Tip revision: ac9827a
IRing.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 export Int IntExtra.
require import Ring AlgTactic.
(* -------------------------------------------------------------------- *)
instance ring with int
op rzero = zero
op rone = one
op add = (+)
op opp = [-]
op mul = ( * )
op expr = IntExtra.( ^ )
proof oner_neq0 by smt
proof addr0 by smt
proof addrA by smt
proof addrC by smt
proof addrN by smt
proof mulr1 by smt
proof mulrA by smt
proof mulrC by smt
proof mulrDl by smt
proof expr0 by smt
proof exprS by smt.