Documentation

Init.Data.Int.OfNat

Helper definitions and theorems for converting Nat expressions into Int one. We use them to implement the arithmetic theories in grind

@[reducible, inline]

abbrev Int.OfNat.Var :

Equations

Int.OfNat.Var = Nat

Instances For

@[reducible, inline]

abbrev Int.OfNat.Context :

Equations

Int.OfNat.Context = Lean.RArray Nat

Instances For

def Int.OfNat.Var.denote (ctx : Context) (v : Var) :

Equations

Int.OfNat.Var.denote ctx v = Lean.RArray.get ctx v

Instances For

inductive Int.OfNat.Expr :

num (v : Nat) : Expr
var (i : Var) : Expr
add (a b : Expr) : Expr
mul (a b : Expr) : Expr
div (a b : Expr) : Expr
mod (a b : Expr) : Expr

Instances For

instance Int.OfNat.instBEqExpr :

Equations

Int.OfNat.instBEqExpr = { beq := Int.OfNat.beqExpr✝ }

def Int.OfNat.Expr.denote (ctx : Context) :

Equations

Int.OfNat.Expr.denote ctx (Int.OfNat.Expr.num k) = k
Int.OfNat.Expr.denote ctx (Int.OfNat.Expr.var v) = Int.OfNat.Var.denote ctx v
Int.OfNat.Expr.denote ctx (a.add b) = (Int.OfNat.Expr.denote ctx a).add (Int.OfNat.Expr.denote ctx b)
Int.OfNat.Expr.denote ctx (a.mul b) = (Int.OfNat.Expr.denote ctx a).mul (Int.OfNat.Expr.denote ctx b)
Int.OfNat.Expr.denote ctx (a.div b) = (Int.OfNat.Expr.denote ctx a).div (Int.OfNat.Expr.denote ctx b)
Int.OfNat.Expr.denote ctx (a.mod b) = (Int.OfNat.Expr.denote ctx a).mod (Int.OfNat.Expr.denote ctx b)

Instances For

def Int.OfNat.Expr.denoteAsInt (ctx : Context) :

Equations

Int.OfNat.Expr.denoteAsInt ctx (Int.OfNat.Expr.num k) = Int.ofNat k
Int.OfNat.Expr.denoteAsInt ctx (Int.OfNat.Expr.var v) = Int.ofNat (Int.OfNat.Var.denote ctx v)
Int.OfNat.Expr.denoteAsInt ctx (a.add b) = (Int.OfNat.Expr.denoteAsInt ctx a).add (Int.OfNat.Expr.denoteAsInt ctx b)
Int.OfNat.Expr.denoteAsInt ctx (a.mul b) = (Int.OfNat.Expr.denoteAsInt ctx a).mul (Int.OfNat.Expr.denoteAsInt ctx b)
Int.OfNat.Expr.denoteAsInt ctx (a.div b) = (Int.OfNat.Expr.denoteAsInt ctx a).ediv (Int.OfNat.Expr.denoteAsInt ctx b)
Int.OfNat.Expr.denoteAsInt ctx (a.mod b) = (Int.OfNat.Expr.denoteAsInt ctx a).emod (Int.OfNat.Expr.denoteAsInt ctx b)

Instances For

theorem Int.OfNat.Expr.denoteAsInt_eq (ctx : Context) (e : Expr) :

denoteAsInt ctx e = ↑(denote ctx e)

theorem Int.OfNat.Expr.eq_denoteAsInt (ctx : Context) (e : Expr) :

↑(denote ctx e) = denoteAsInt ctx e

theorem Int.OfNat.Expr.eq (ctx : Context) (lhs rhs : Expr) :

(denote ctx lhs = denote ctx rhs) = (denoteAsInt ctx lhs = denoteAsInt ctx rhs)

theorem Int.OfNat.Expr.le (ctx : Context) (lhs rhs : Expr) :

(denote ctx lhs ≤ denote ctx rhs) = (denoteAsInt ctx lhs ≤ denoteAsInt ctx rhs)

theorem Int.OfNat.of_le (ctx : Context) (lhs rhs : Expr) :

Expr.denote ctx lhs ≤ Expr.denote ctx rhs → Expr.denoteAsInt ctx lhs ≤ Expr.denoteAsInt ctx rhs

theorem Int.OfNat.of_not_le (ctx : Context) (lhs rhs : Expr) :

¬Expr.denote ctx lhs ≤ Expr.denote ctx rhs → ¬Expr.denoteAsInt ctx lhs ≤ Expr.denoteAsInt ctx rhs

theorem Int.OfNat.of_dvd (ctx : Context) (d : Nat) (e : Expr) :

d ∣ Expr.denote ctx e → ofNat d ∣ Expr.denoteAsInt ctx e

theorem Int.OfNat.of_eq (ctx : Context) (lhs rhs : Expr) :

Expr.denote ctx lhs = Expr.denote ctx rhs → Expr.denoteAsInt ctx lhs = Expr.denoteAsInt ctx rhs

theorem Int.OfNat.of_not_eq (ctx : Context) (lhs rhs : Expr) :

¬Expr.denote ctx lhs = Expr.denote ctx rhs → ¬Expr.denoteAsInt ctx lhs = Expr.denoteAsInt ctx rhs

theorem Int.OfNat.ofNat_toNat (a : Int) :

↑a.toNat = if a ≤ 0 then 0 else a

theorem Int.OfNat.Expr.denoteAsInt_nonneg (ctx : Context) (e : Expr) :

0 ≤ denoteAsInt ctx e