ONijn - Coq Proof Script Generation

Quickstart

Public API

The public API consists of three modules: Syntax, Coq, and Parser.

• Syntax Provides submodules for syntactic constructions. It contains representations for Types, Terms, Polynomials, and rewriting rules.

• Coq Provides interfacing to generate strings that are valid coq constructions. For more details, check the Coq.Grammar and Coq.Proof_script modules.

• Parser Provides abstract interfacing for creating parsers of file formats accepted by ONijn.

Input File Format

In order to certify terminaion of a rewriting system, one must first represent the certificate (stating the termination property) in a way that onijn understands it.

The rewriting formalism of accepted by onijn is AFS (Algebraic Functional Systems).

Grammar for Signature and Rules

answer := YES | NO | MAYBE
sort, fn, var := ['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9']*

type := sort | type -> type

term := var | fn | term term | /\var.term

rewrite_rule := term => term

Where answer represents the termination status given by a termination tool. In the construct for sort, fn, and var, the regex expression ['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9']* stating the string format accepted as names for sorts, function symbols, and variables, respectively.

In algebraic functional systems, type declarations and types are not the same. The type construct defines the usual simple types. Expressions in type are parsed assuming that => is right-associative, as usual.

We can already represent signature and rewriting systems. Let us take the map TRS as exemple.

map F nil => nil
map F (hd :: tl) => F(hd) :: (map F tl)

In onijn format this system is represented as:

Signature: [
  cons : a -> list -> list ;
  map : list -> (a -> a) -> list ;
  nil : list
]

Rules: [
  map nil F => nil ;
  map (cons X Y) G => cons (G X) (map Y G)
]

Grammar for Polynomial Interpretations

We represent polynomials with the grammar below:

var := ['a'-'z' 'A'-'Z'] ['a'-'z' 'A'-'Z' '0'-'9']*
poly := n | var | var(poly) | poly + poly | poly * poly
poly_fun := Lam[var_1; ...; var_n] . poly
poly_int := J(fn) = poly_fun

Continuing with the map example, we represet an interpretation for it in onijn as follows:

Interpretation: [
  J(cons) = Lam[y0;y1].3 + 2*y1;
  J(map) = Lam[y0;G1].3*y0 + 3*y0*G1(y0);
  J(nil) = 3
]

Removed Rules

An onijn file must end with a list of rules that can be oriented with the given interpretation.

Removed: [
  map nil F => nil ;
  map (cons X Y) G => cons (G X) (map Y G)
]

A Complete File Example

Putting everything together we get a file map_trs.onijn as follows:

(** This is a comment. It will be ignored by onijn. **)
YES
Signature: [
  cons : a -> list -> list ;
  map : list -> (a -> a) -> list ;
  nil : list
]

Rules: [
  map nil F => nil ;
  map (cons X Y) G => cons (G X) (map Y G)
]

Interpretation: [
  J(cons) = Lam[y0;y1].3 + 2*y1 ;
  J(map) = Lam[y0;G1].3*y0 + 3*y0*G1(y0) ;
  J(nil) = 3
]

Removed: [
  map nil F => nil ;
  map (cons X Y) G => cons (G X) (map Y G)
]