The proof language for type conversions

Internal representation of proofs

Internally, a Proof instance is encoded by an expression tree of type GEN (which equals Generic), each subtree being either of type Literal or Compound. The private conversion routines between the types Proof and GEN are postfix .v and proof. The public routines for the syntactic manipulation of proofs are

proof$literal: Literal -> Proof

literal?: Proof -> Boolean

convert: Proof -> Literal

Creation of a leaf, testing whether a proof is a leaf and converting a leaf to a literal.

postfix (): (Proof, Tuple Proof) -> Proof

compound?: Proof -> Boolean

prefix #: Proof -> Int

postfix []: (Proof, Int) -> Proof

Creation of a compound tree, testing whether an proof is a compound tree, obtaining the arity of a compound tree and accessing a child of a compound tree.

Internal representation of problems

Syntactic utility routines

postfix .components: Proof -> Proofs

postfix .args: Proof -> Proofs

postfix .initial: Proof -> Proofs

postfix .last: Proof -> Proof

Commodity accessors for the determination of all components of a compound tree (postfix .components), of all arguments of a primitive or function call (postfix .args), of all but its last arguments (postfix .initial), and its last argument (postfix .args).

subst (pr: Proof, what: Proof, by: Proof): Proof

subst (pr: Proof, t: TABLE): Proof

Syntactic substitution of what by by in pr, or of each variable var in the table t by var[t].

General proof logic

$rule (ax: Proof, val: Proof): Proof

Construct for basic axioms: the axiom ax corresponds to a type convertability assertion, such as $converts (F, T), and the value val to the algorithm which implements the conversion. Rules are usually templated using the $forall construct

$todo (pr: Proof): Proof

Mark a part of a proof as being not yet solved.

$forall (ql: PRGS, pr: Proof): Proof

$exists (ql: PRGS, pr: Proof): Proof

Universal and existential quantification.

$implies (p1: Proof, p2: Proof): Proof

$and (p1: Proof, p2: Proof): Proof

$or (p1: Proof, p2: Proof): Proof

Basic logical connectors.

Type conversion logic

converts (t1: TYP, t2: TYP): Proof

The assertion that the type t1 can be converted into the type t2.

Permission is granted to copy, distribute and/or modify this document under the terms of the GNU General Public License. If you don't have this file, write to the Free Software Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.