ProofCombinators

Checked equational reasoning, following Theorem Proving for All (2018). Proofs are Unit values; the theorem is expressed by their refinement.
Table of Contents

Functions

eq

Checked equational reasoning, following Theorem Proving for All (2018). Proofs are Unit values; the theorem is expressed by their refinement.
def eq (x : a) (y : a | y = x) : {v : a | v = x && v = y}

because

def because (x : a) (reason : Unit) : {v : a | v = x}

qed

def qed (x : a) : Unit

trivial

def trivial : Unit

le

def le (x : Int) (y : Int | x ≤ y) : {v : Int | v = y && x ≤ v}

lt

def lt (x : Int) (y : Int | x < y) : {v : Int | v = y && x < v}

ge

def ge (x : Int) (y : Int | x ≥ y) : {v : Int | v = y && x ≥ v}

gt

def gt (x : Int) (y : Int | x > y) : {v : Int | v = y && x > v}