Reference Guide

Syntax

Terms

The syntax for Canonical LF terms and types follows a similar style to that used by Twelf. Of note are the following structures:

Syntax	Meaning
`[x] M`	Term abstraction
`{x:A} B`	$\Pi$ -type
`A -> B`	$\Pi$ -type without dependencies

The names for variables and constants follow the same conventions as Twelf. Nominal constants are denoted by n1, n2, ...

Context Expressions

Context expressions $G$ are commonly expressed using the following syntax:

Syntax	Meaning
<empty string>	Empty context
`Gamma`	Context variable
`G, n:A`	Explicit context entry

Formulas

The syntax for formulas is the following:

Syntax	Meaning
`forall x y z ..., F`	$\forall x\ \forall y\ \forall z \ldots . F$ (Universal quantification)
`exists x y z ..., F`	$\exists x\ \exists y\ \exists z \ldots . F$ (Existential quantification)
`ctx Gamma1:C1 Gamma2:C2 ..., F`	$\Pi \Gamma_1:\mathcal{C_1}\ \Pi \Gamma_2:\mathcal{C_2}\ \ldots. F$ (Context quantification)
`F1 => F2`	$F_1 \supset F_2$ (Implication)
`F1 /\ F2`	$F_1 \land F_2$ (Conjunction)
`F1 \/ F2`	$F_1 \lor F_2$ (Disjunction)
`{ G \|- M : A }`	Atomic formula
`pred M1 M2`	Defined predicate
`true`	$\top$ (true)
`false`	$\bot$ (false)

Lemmas

To use a lemma, prove it as a theorem and then refer to it by name in another proof using the apply tactic. For example,

Theorem my_lemma : ...
...

Theorem my_theorem : ...
...
apply my_lemma to H3 H5.

Typing

Adelfa's logic is simply-typed using simple arity typing based on a single base type o and constructor ->. All terms and formulas must be well-typed.

Inductive restrictions are represented by * (smaller) and @ (equal). They are used to track the size of inductive arguments rather than using explicit numeric values. For example, suppose we apply induction on 1. when trying to prove the following subject reduction theorem,

============================
forall E V T D1 D2, {|- D1 : eval E V} -> {|- D2: of E T} ->
  exists D3, {|- D3: of V T}

We will get the following proof state.

// [!code word:*]
IH : forall E V T D1 D2, {|- D1 : eval E V}* -> {|- D2: of E T} ->
      exists D3, {|- D3: of V T}
============================
// [!code word:@]
forall E V T D1 D2, {|- D1 : eval E V}@ -> {|- D2: of E T} ->
  exists D3, {|- D3: of V T}

Here we have an inductive hypothesis where the inductive argument is flagged with *. This means that we can only apply that hypothesis to an argument which also has the *. Because * means smaller, in order to get an argument with a * we must perform case analysis on an argument that is "equal" which we denote by @. Thus, the above proof proceeds by first doing intros. and then case analysis on {|- D1 : eval E V}@. This will give us two subgoals, one which is trivial and the other which has hypotheses tagged with * and thus eligible for use with the inductive hypothesis.

Top Level Commands

Theorem

Theorem <NAME> : <FORMULA>.

Starts proof development with the given formula as the goal.

Theorem myTheorem : forall M N P, ...

Quit

Quit.

Exits from Adelfa.

Specification

Specification <QUOTED FILENAME>.

Reads in the specification indicated by the given filename.

Schema

Schema <ID> := <BLOCK SCHEMA>[; <BLOCK SCHEMA>].

Defines a context schema associated with <ID>.

A block schema has a, possibly empty, header of arity typed variables, followed by a series of, possibly empty, LF typed variables. A context schema can be comprised of any number of block schemas.

For example:

Schema C := {T:o}(x: tm, d: of x T);
            (x:tm, t:tp, d: of x t).

Set

Set <OPTION> <VALUE>.

Sets the value of options during proof development. It may be used at the top level or inside theorem construction. The options are currently:

search_depth The maximum number of times to perform type decomposition on assumption judgements during the search and assert tactics. Accepts any number as a <VALUE>. By default, this is set to 5.
schema_sub The option to enable or disable schema subsumption. Accepts true or false. By default, this is set to true.

Set search_depth 5.

Set schema_sub false.

Set search_depth 5, schema_sub false.

Tactics

In this page, we use the following LF signature to parameterize proof developments on this page. These developments will display each tactic being used, usually through a toy theorem.

tactics.lf

nat : type.
z : nat.
s : {N:nat} nat.

plus : nat -> nat -> nat -> type.
plus-z : {N:nat} plus z N N.
plus-s : {N1:nat}{N2:nat}{N3:nat}
         {D: plus N1 N2 N3}
         plus (s N1) N2 (s N3).

Search

search [<NUM>].

Search for a derivation of the current goal using matching with assumption formulas and decomposing judgments into subgoals using LF derivation rules. If a <NUM> is provided, assumption judgements are decomposed <NUM> times. If a <NUM> is not provided, the search_depth option is used. The search_depth can be changed with the Set command.

Intros

intros.

Introduces variables and assumptions from a goal formula until it no longer has top-level universal quantification, context quantification, or implications.

Specification "tactics.lf".
Schema C := ().
Theorem intro-example: ctx G:C, forall N1, { N1 : nat } => { s N1 : nat }.
intros.

Split

split.

Creates subgoals for each subformula, F1 and F2 if the current goal is a conjunction F1 /\ F2.

Theorem split_example : true /\ false.
split.

Left

left.

Changes the goal to be the left side formula, F1 if the current goal is a disjunction, F1 \/ F2.

Theorem left_example : true \/ false.
left.

Right

right.

Changes the goal to be the right side formula, F2 if the current goal is a disjunction, F1 \/ F2.

Theorem right_example : false \/ true.
right.

Assert

assert <FORMULA> [<NUM>].

Changes the proof state to one which has the given formula as a goal; once derivation of this goal is complete returns to the previous proof state with the given formula added as an assumption. Providing a <NUM> will decompose assumption judgements <NUM> times. If the asserted formula can be proven, it is added to the proof state immediately. This option defaults to search_depth when not provided and may be changed with the Set command.

Specification "tactics.lf".

Theorem plus_exist : forall N1 N2,
  {N1:nat} => {N2:nat} => exists N3 D, {D : plus N1 N2 N3}.
induction on 1. intros. case H1.
apply IH to H3 H2.
% Adelfa decomposes the {D: plus N N2 N3}* assumption
% to find this is derivable, adding it directly to the
% assumption set.
assert { N3 : nat }.
undo.
% We can tell adelfa to not perform any decomposition,
% to find this is derivable, adding it directly to the
% assumption set.
assert { N3 : nat} 0.

Apply

apply <NAME> to <HYP NAMES> [with <BINDINGS>].

Applies a hypothesis of the form ctx Gamma1:C1 ... Gammaj:Cj, forall X1 ... Xi, H1 => ... => Hk => F to argument hypotheses which match H1, ..., Hk. The result is an instantiation of F. Either or both of i and j may be zero. That is, there need not be universally quantified variables or context variables. The with clause allows specific instantiations of any of the variables X1 ... Xi and Gamma1 ... Gammaj.

Specification "tactics.lf".

Theorem plus-z-rhs : forall N,
  { N : nat } => exists D, { D : plus N z N }.
induction on 1. intros. case H1.
apply IH to H2. exists plus-s N1 z N1 D. search.
exists plus-z z. search.

Theorem plus-comm : forall N1 N2 N3 D1,
  { D1 : plus N1 N2 N3 } =>
  % what would be a lemma is listed here to display how one can apply
  % assumption formulas.
  (forall M1 M2 M3 P, { P : plus M1 M2 M3 }
    => exists P2, { P2 : plus M1 (s M2) (s M3) }) =>
  exists D2, { D2 : plus N2 N1 N3 }.
induction on 1. intros. case H1.
apply IH to H6 H2. apply H2 to H7. exists P2. search.
apply plus-z-rhs to H3. exists D. search.

Induction

induction on <NUM>.

Given a goal of the form ctx Gamma1:C1 Gamma2:C2 ..., forall X Y ..., H1 => H2 => ... => F the induction tactic allows you to induct on one of H1, H2, .... The hypothesis to be inducted on must be an atomic formula. The choice of induction is based on the number <NUM>. Applying the induction tactic results in an inductive hypothesis being added to the current set of hypotheses. Specifics on this inductive hypothesis and how it relates to the goal are given in the section Inductive Restrictions.

Adelfa supports nested induction through repeated calls to the induction tactic. See the Inductive Restrictions section for more details.

Exists

exists M.

Instantiates an existential goal with the given term, if it is of the correct arity type.

Specification "tactics.lf".

Theorem exist-example : exists N, { N : nat }.
exists z. search.

Case

case <HYP NAME>[(keep)].

Performs case analysis on the given assumption formula. By default, the assumption is removed, use (keep) to retain it.

Specification "tactics.lf".

Theorem cases-example : forall N, {N : nat} => { s N : nat }.
intros. case H1.
% keep derivation which formed { N : nat }
undo. case H1 (keep).

Weaken

weaken <HYP NAME> with A [<NUM>].

When the given assumption formula is of the form {G |- M : A}, and it can be verified that the LF type A must be well formed in the current context under G, then a new assumption is added in which the typing judgment is weakened to include the given type.

Specification "tactics.lf".

Theorem wk-example : forall N, { N : nat } => false.
intros. weaken H1 with nat.

Strengthen

strengthen <HYP NAME>.

If the given assumption formula is of the form {G, n:A1 |- M : A2} if n does not appear in M or A2 then a new assumption is added in which the typing judgment is strengthened to {G |- M : A2}.

Context Permute

ctxpermute <HYP NAME> to G.

If the given assumption is of the form {G' |- M : A}, and if the given context is a valid permutation of the context G' (i.e. does not violate dependencies), then a new assumption is added with the permuted context expression G.

Permute

permute <HYP NAME> with <PERM>.

Applies a permutation of nominal constants to the argument hypothesis. <PERM> must be a complete permutation. Mappings can be unidirectional n1 -> n2, n2 -> n or bidirectional n1 <-> n2. If the provided permutation is complete and limited to be within the relevant assumption's restricted set, a new assumption is added with the permutation applied to it.

Inst

inst <HYP NAME> with n = M.

If the given assumption formula is of the form {G1,n:B,G2 |- M:A}, and the term M can be determined to be such that {G1 |- M : B} is valid then this tactic replaces the given assumption with one in which n:B is removed from the context expression and all occurrences of n are replaced by M.

Prune

prune <HYP NAME>.

If the given assumption is of the form {G |- X n1 ... nm : A} for some eigenvariable X and distinct nominal constants n1,...,nm then this tactic will prune those nominal constants appearing as arguments to X which

Do not already appear in G and
Are not permitted in the instantiations for the context variable in G.