Doxa Proof Checker - The Arda Project

A dependently typed proof checker for the Calculus of Inductive Constructions, parsed with Rumil and checked by its own kernel. Runs entirely in your browser. No server.

Examples

Sourcechecks live

// Length-indexed vectors: the length lives in the type. The theorem
// below is *about* that index, proved with Vec's dependent eliminator
// whose motive ranges over both the index and the vector.
data Nat : Type {
  zero : Nat;
  succ : Nat -> Nat;
}

data Vec[A: Type] : Nat -> Type {
  vnil  : Vec[A] zero;
  vcons : (n: Nat) -> A -> Vec[A] n -> Vec[A] (succ n);
}

fun vlength{A: Type}{n: Nat}(v: Vec[A] n): Nat = match v {
  case vnil => zero
  case vcons k x rest => succ (vlength rest)
}

// cong: equal inputs give equal images.
fun cong{A: Type}{B: Type}{x: A}{y: A}(f: A -> B, p: Eq[A] x y)
    : Eq[B] (f x) (f y) =
  match p { case refl a => refl (f a) }

// The runtime length of a vector equals the length its type carries.
val vlength_index : (A: Type) -> (n: Nat) -> (v: Vec[A] n)
                 -> Eq[Nat] (vlength v) n =
  (A: Type) =>
    Vec.ind A
      ((m: Nat) => (w: Vec[A] m) => Eq[Nat] (vlength w) m)
      (refl zero)
      ((k: Nat) => (x: A) => (rest: Vec[A] k)
        => (ih: Eq[Nat] (vlength rest) k) =>
         cong ((j: Nat) => succ j) ih)

ResultWasmGC · 76 KB gzipped · …

Loading checker…