ac.bend checks

raw source on the hub · import 0xb13667d52aa56e002b4d09883d7fce3e/ac.bend as Ac

ac.bend: sums over Nat decided by reflection. An Expr is a sum of atoms, with doubling; norm counts each atom, so two Exprs with the same counts denote the same Nat. ac turns that computation into a proof: Bend checks {norm(e1) == norm(e2)} with {==}, and the goal {eval(env, e1) == eval(env, e2)} follows for every env.

2 imports

import Base
import ./nat.bend as N

Types

type Expr source · line 10 · raw

Data

EAtom
```
@i:Nat -> Expr
```
EAdd
```
@a:Expr -> @b:Expr -> Expr
```
EDbl
```
@a:Expr -> Expr
```
EZero
```
Expr
```

Definitions

def nth source · line 17 · raw

@env:List<&2, Nat> -> @i:Nat -> Nat

the i-th atom's value; atoms past the end are 0n

def eval source · line 26 · raw

@+env:List<&2, Nat> -> @e:Expr -> Nat

def unit source · line 40 · raw

@i:Nat -> List<&2, Nat>

def vadd source · line 47 · raw

@u:List<&2, Nat> -> @v:List<&2, Nat> -> List<&2, Nat>

def norm source · line 56 · raw

@e:Expr -> List<&2, Nat>

def evalc source · line 69 · raw

@cs:List<&2, Nat> -> @+env:List<&2, Nat> -> Nat

the value of a normal form: sum of cs[i] * env[i]

def unit_ok source · line 81 · raw

@+env:List<&2, Nat> -> @+i:Nat -> {evalc(unit(i), env) == nth(env, i) : Nat}

def vadd_ok source · line 94 · raw

@+u:List<&2, Nat> -> @+v:List<&2, Nat> -> @+env:List<&2, Nat> -> {evalc(vadd(u, v), env) == Nat.add(evalc(u, env), evalc(v, env)) : Nat}

def norm_ok source · line 109 · raw

@+e:Expr -> @+env:List<&2, Nat> -> {evalc(norm(e), env) == eval(env, e) : Nat}

def ac source · line 125 · raw

@+env:List<&2, Nat> -> @+e1:Expr -> @+e2:Expr -> @h:{norm(e1) == norm(e2) : List<&2, Nat>} -> {eval(env, e1) == eval(env, e2) : Nat}

LAW-shaped entry point: two sums with equal atom counts are equal