https://github.com/EasyCrypt/easycrypt
Raw File
Tip revision: 30bfa950afa3806948c073d3c9ec4468d33ea940 authored by Pierre-Yves Strub on 11 December 2023, 10:58:49 UTC
New tactic: "proc change"
Tip revision: 30bfa95
StdRing.ec
(* -------------------------------------------------------------------- *)
require import Bool Int Real.
require (*--*) Ring.

(* -------------------------------------------------------------------- *)
instance ring with int
  op rzero = CoreInt.zero
  op rone  = CoreInt.one
  op add   = CoreInt.add
  op opp   = CoreInt.opp
  op mul   = CoreInt.mul
  op expr  = Ring.IntID.exp

  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(Ring.IntID.expr0)
  proof exprS     by smt(Ring.IntID.exprS).

op bid (b:bool) = b.

instance bring with bool
  op rzero = false
  op rone  = true
  op add   = Bool.( ^^ )
  op mul   = (/\)
  op opp   = bid

  proof oner_neq0 by smt()
  proof addr0     by smt()
  proof addrA     by smt()
  proof addrC     by smt()
  proof addrK     by smt()
  proof mulr1     by smt()
  proof mulrA     by smt()
  proof mulrC     by smt()
  proof mulrDl    by smt()
  proof mulrK     by smt()
  proof oppr_id   by smt().
back to top