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

Instances For

@[reducible, inline]

abbrev Int.OfNat.Context :

Equations

Instances For

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

Equations

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

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

Equations

Instances For

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

Equations

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