The Edinburgh Logical Framework (LF) is a λ-calculus with dependent types. LF is often used for encoding deductions for formal systems. It has the advantage of capturing common properties of rules in formal systems, such as rule schemas, α-reductions, and β-reductions. This paper will describe how LF is used to represent deductions in a formal system, and give examples of its use for encoding propositional calculus and contextual semantics for the IMP programming language.
According to Hodel, a formal system consists of three things.
This definition can be simplified by considering an axiom as a rule of inference with no hypothesis. If LF is to encode deductions in formal systems, it will have to model all of these items.
Many formal languages are built from a formal grammar of some kind. Common formal grammars can be modeled by the type system of the λ-calculus. Take, for example, first-order logic of ordered fields. Terms are composed of constants (0 and 1), variables, and operators (+ and ×). Propositions are formed by applying predicates (< and =) to terms, and by applying logical connectives (¬, ⇒, ∀).
Types for terms and propositions are declared in the LF signature.
Term : type. Prop : type.
These types and functions of these types are inhabited with the constants, operators, and logical connectives (not variables) of the first-order logic.
0 : Term. 1 : Term. + : Term → Term → Term. × : Term → Term → Term. < : Term → Term → Prop. = : Term → Term → Prop. ¬ : Prop → Prop. ⇒ : Prop → Prop → Prop. ∀ : (Term → Prop) → Prop.
0 and 1 are declared to be terms. The binary operator + is represented by a function that takes two terms, and returns a new term. As is common in functional programming, one uses a curried function to represent a function of multiple parameters. So the syntax for 1 + 1 is represented by (+ 1 1), which has type Term.
Most of the other connectives work in a similar manner, except for ∀. One normally thinks of ∀ as a piece of syntax that binds a variable to a proposition using that variable. However, the only parameter for ∀ is a function. In this case one uses the binding properties of λ-expressions in the λ-calculus to capture the binding properties of the ∀ syntax.
For example, the syntax ∀x:∀y:x+y = y+x would be expressed in LF as ∀ λx:Term.∀ λy:Term.(= (+ x y) (+ y x)), which has type Prop. In LF the two terms ∀ (λx:Term.(= x x)) and ∀ (λy:Term.(= y y)) are considered equivalent because they are α-equivalent. But one considers the two statements the same from a logical perspective as well because quantified formulas have the same α-equivalence property. This is one advantage that using LF to encode deductions gives. LF can capture the α-equivalence and variable binding property found in many formal systems. As a result, normally complex rules of inference are made simpler when variable binding is already taken care of.
A formal system is a system that determines if a formal statement is derivable or not. In first order logic, one uses the single turn-style (⊦) to denote that statement is a derivable. A statement is derivable if there is some derivation of it. To encode a derivation of a formal statement in LF, one uses a derived type.
⊦ : Prop → type.
Now for each proposition A, one can construct a type ⊦ A. Terms of type ⊦ A will represent derivations of A. In formal systems there may be more than one derivation of a formal statement. Similarly in LF, there may be more than one object of this type. Also some formal statements have no derivation. In LF there will be no objects of the corresponding type. So, in order to show A is derivable, one needs to find an element of type ⊦ A.
Axioms assert the derivation of statements in a single step. So in LF, one needs to inhabit the derived type corresponding to that statement. To do this one names each axiom, and states that it is an element of the particular derived type. Here is an example of a couple of field axioms for the first-order logic of fields.
assoc : ⊦ (∀ λx:Term.(∀ λy:Term.(∀ λz:Term.(= (× (× x y) z) (× x (× y z)))). mult_ident_left : ⊦ (∀ λx:Term.(= (× x 1) x)). mult_ident_right : ⊦ (∀ λx:Term.(= (× 1 x) x)).
Many axioms occur in the form of axioms schemas. One axiom of logic is A ⇒ (B ⇒ A), where A and B could be any proposition at all. This form of axiom schemas are naturally represented as functions from a tuple of propositions to the corresponding type. So the previous axiom schema would be represented as ΠA:Prop.ΠB:Prop.⊦ (⇒ A (⇒ B A)). Here is a list of axiom schemas from propositonal logic represented in LF.
PropAx1 : ΠA:Prop.ΠB:Prop.⊦ (⇒ A (⇒ B A)). PropAx2 : ΠA:Prop.ΠB:Prop.ΠC:Prop.⊦ (⇒ (⇒ A (⇒ B C)) (⇒ (⇒ A B) (⇒ B C))). PropAx3 : ΠA:Prop.ΠB:Prop.⊦ (⇒ (⇒ (¬ A) (¬ B)) (⇒ B A)).
Axiom schema objects are λ-abstractions. To use an axioms schema in a derivation, one passes the proposition to bind to the variables A, B, and C, and then uses the instantiated axiom.
Other axioms have operations, and side rules attached. One axiom schema of first order logic is (∀x.A) ⇒ A[t/x] (t is substitutable for x in A). The encoding of this rule into LF must capture subitution of t into A, and the side condition of the axiom schema. But since LF is a type of λ-calculus, procedures for applying substitutions are built into the language. This axiom schema can be encoded in LF as ΠA:Term → Prop.Πt:Term.⊦ (⇒ (∀ A) (A t)). In order for t to be substitutable for x in A, one requires that t not have any variables that are will become bound when it is substituted for x in A. But the encoding of propositions in LF does not use variables directly. Instead, one uses λ-expressions to create variables where needed. This makes it impossible for t to refer to any variables in A since the the variables in A are locally scoped.
Not every side rule can easily be captured by the LF system; however, many rules often encountered in practice are easily encoded in LF.
The rules of inference in a formal system allow new sentences to be derived if derivations of some other sentences exist. Just like axiom schemas, this concept fits perfectly as a function in LF. This time the function will require the derivation of the hypothesis of the rule of inference before returning with the conclusion of the rule of inference. The rule of inference of modus ponens would be written in LF as follows.
MP : ΠA:Prop.ΠB:Prop.⊦ A → ⊦ (⇒ A B) → ⊦ B.
Rules of inference with side conditions are handled the same way as axioms. Also recall that axioms behave like rules of inference with no hypothesis. If one were to encode in LF a rule of inference with no hypothesis, it would have the same form as an axiom.
A theorem is a derived type that can be inhabited. That is to say there exists some object of the derived type. For example, to prove the theorem A ⇒ A by using LF, one must show that there is an object of type ΠA:Prop.⊦ (⇒ A A). The following is an example element of element of that type.
ReflexThm : ΠA:Prop.⊦ (⇒ A A) := λA:Prop.
MP (⇒ A (⇒ A A)) (⇒ A A) (PropAx1 A A)
(MP (⇒ A (⇒ (⇒ A A) A)) (⇒ (⇒ A (⇒ A A)) (⇒ A A))
(PropAx1 A (⇒ A A)) (PropAx2 A (⇒ A A) A)).
In order to verify that this is correct, one can type-check the above statement to ensure that it actually has type ΠA:Prop.⊦ (⇒ A A). This reduces the problem of proof verification to the procedure of type-checking, which is a well understood and simple procedure to implement.
This theorem applies to all propositions of the form A ⇒ A so this theorem is actually a theorem schema. This is made clear by the fact that ReflexThm is a λ-abstraction. Theorem schemas are used in the same way as axiom schemas are.
One consequence of the fact that axioms and rules of inference are on the same level is that theorems can be new rules of inference. Consider the following example.
NewRule : ΠA:Prop.ΠB:Prop.⊦ B → ⊦ (⇒ A B) := λA.Prop.λB:Prop.λC:⊦ B.MP B (⇒ A B) C (PropAx1 B A).
Here I prove a new rule of inference that says under the hypothesis of B one can infer that A ⇒ B. To prove this I show there is an inhabitant the type ΠA:Prop.ΠB:Prop.⊦ B → ⊦ (⇒ A B).
TWELF is an implementation of the LF system. It has the ability to type check theorems and verify the correctness of the encoded derivation. It also has features for type-inference, logic programming, and preliminary support for meta-theorems about a given signature in LF. Appendices A and B give examples of using TWELF to implement propositional calculus and contextual semantics for the programming language IMP. In TWELF λ-expressions, such as λx:Bool.x are written with square-brackets, as in [x:Bool] x. Π-types such as Πx:Prop are written with curly-brackets, as in {x:Prop}.
Appendix A.1 gives the input file for TWELF that describes the axioms for propositional calculus, definitions for logical connectives in terms of not and implies, and several theorems for propositional calculus. As I became more confident with deriving theorems in TWELF, I began making liberal use of the type-inference mechanisms of TWELF. Each omitted type in the input in Appendix A.1 is marked with an underscore. In the last couple of theorems, I only state the axiom and theorem schemas that I use. TWELF reconstructs the types needed.
Appendix A.2 shows the output of TWELF. The types are reconstructed and shown. Also TWELF type-checks the input file, and thereby verifying that each theorem is correctly proven. If a derivation were incorrect, TWELF would have halted with an error.
Appendix B.1 gives an input file for TWELF that describes the rules for defining a formal system for the contextual semantics of IMP. The first section defines the abstract syntax for the language. This is followed by the redex reduction rules, context definitions, and finally the global reduction rules.
The abstract syntax consists of types for expression, booleans, and commands. To facilitate the encoding into LF, there are also types for natural numbers, and memory locations.
Natural numbers are not a primitive in LF, so I needed to construct them. A natural number is either 0, or the successor of some natural number. The val function is a piece of abstract syntax that promotes a natural number into an expression. val would not likely appear in the concrete syntax of a language. It is needed in the abstract syntax tree because natural numbers cannot be expressions. If they were than the successor operator would apply to expressions, and that is not part of the IMP language.
Locations behave like references. The ! operation dereferences locations to extract the variables value as an expressions. ! is strictly a piece of abstract syntax, and not part of the concrete syntax. References are not part of the IMP language, but the reference concept is used to encode the semantics of the language.
There are no objects of type Location. Locations are created when variables are declared in a let block. The encoding of a let block in LF is a function of type Expr → (Location → Command) → Command. The first parameter is the expression for the initial value of a new variable. The second parameter is a command that may use the new variable. This second parameter is encoded as a λ-expression. This is the way objects of type Location can be introduced into the syntax. For example the command let x = 0 in x = x + 1 would be encoded as (let (val 0) (λx:Location.(assign x (plus (! x) 1)))). As I will show, this method allows frees one from worrying about variable aliasing and substitution issues by having the λ-calculus handle it.
After the syntax, Appendix B.1 gives contextual semantics for the IMP language. States are not used. Instead let expressions are kept around to hold the current values of variables. Every command should eventually evaluate to a skip statement inside a series of nested let blocks.
The informal definition of IMP does not distinguish between redexs that are expressions, booleans, or commands. Since each of those three objects have different types, there are three different types of redexs. A reduction is encoded as a predicate that matches a pair of objects. The first object is the redex, and the second object is what it reduces to. ExprRed is the reduction predicate for expressions. BoolRed and CommandRed are the reduction predicates for booleans and commands respectively.
The informal reduction rules for expressions make reference to the mathematical operations of + and ×. Since LF does not have primitives for these operations, it requires more effort to encode the semantics of plus and times. In my implementation I give the a standard recursive definition of such evaluation. A similar problem holds for booleans. The reductions rules specifically give the semantics for logical operations without short-circuit evaluation.
There are two reduction rules for the let command. These are given after the definition of contexts, since contexts are used in the definition of the reduction.
Informally a context is some program fragment with a hole in it. This is most naturally represented in LF as a λ-expression. Contexts are defined by some unary predicate. Just as with redexs, there are multiple types of contexts because of the different types of syntax. However, because the type filling the hole in the context may be different from the type of the context itself, there are more than three types of contexts.
The simplest types of contexts are holes themselves. For expressions this rule is given by the exprConHole object which has type ExprContext (λe:Expr.e). ExprContext is the predicate that determines if an object of type Expr → Expr is a valid context or not. Holes for booleans and commands are defined in a similar fashion.
Other contexts are defined recursively in terms of other contexts. For example the exprConPlus0 states that for any expression e, and any expression with a hole H, if you can provide a proof that H is a context, then (plus H e) is also a context. Since contexts are actually λ-expressions, the above is not quite correct. Instead I must state that λx:Expr.(plus (H x) e) is the context. Most other contexts are handled in a similar manner.
The context for the body of a let command is handled a bit different since the body of let is not a Command but actually a function of type Location → Command. There are no contexts of type Location → Command. To deal with this the paramter H in commandConLet1 is a function that given a location produces a possible context of type Command → Command. commandConLet1 also requires a proof that given any location l, (H l) is a context. The rest proceeds normally. This case is interesting because of the complexity of the type needed.
One example of an informal let redex is a let statement whose body is a context filled in by variable used in an expression. The side condition with this reduction is that the context does not have another let block declaring another variable by the same name. Here one sees the advantage of encoding the statement using LF. Since contexts are λ-expression, filling the context is as easy as function application. The side condition is also handled because LF handles issues with variable aliasing. The rule for this let redex is given by letRed0. The location variable l is defined in the rule itself, and no other variable occuring in H can refer it it because the definition of l is in a completely different scope. This means that the side condition is always satisfied. The other let redex is handled in a similar fashion.
There are three global reduction rules. There is one for each type of redex. Given a proof that H is a context, and a proof that r → e is a reduction rule, then H[r] → H[e] is a derivation. Derivation is a predicate of two commands, in exactly the same way that reduction were encoded with a predicate. Derivation* is a predicate which is the reflexive and transitive closure of Derivation.
The last part of Appendix B.1 gives three examples of derivations using TWELF. Sometimes the logic programming features of TWELF allow one to find a proof of a derivation. Unfortunately more often than not the backtracking search algorithm will search along an infinite path that that will not lead to an answer. But, as the three examples illustrate, derivations do exist.
One useful meta-theorem about proportional calculus is the deduction theorem. It is possible to state the deduction theorem in LF for the given implementation of propositional calculus. It would be an object of type ΠA:Prop.ΠB:Prop.(⊦ A → ⊦ B) → (⇒ A B). But with the given signature there is no object of this type. This is because of LF has the weakening property. If one adds new objects to any signature in LF, the all the derivations still remain valid. However it would be possible to add an object to the signature of propositional calculus that would make the deduction theorem false. Therefore it must be impossible to find an object that proves the deduction theorem.
This same problem applies to the implementation of IMP. One natural question to ask about the given formal semantics of IMP is is it correct? This is not a well posed question itself, but IMP was designed so that every command can be decomposed uniquely into a context and a redex. Also every command eventually derives a series of nested let blocks terminated by skip. These theorems are not possible to prove in LF because it is possible to add an object the the signature of IMP to make these theorems false.
I have shown how to implement two formal systems using LF. The examples illustrate how LF caputures the sematics of rules, rule schema, and even common side-conditions in rules. LF can encode the contextual semantics of the IMP language without much difficulty. The only drawback to using the LF system, is that the weakening properety prevents one from obtaining proofs of some meta-theorems that would be useful to use.
prop : type.
imp : prop -> prop -> prop.
not : prop -> prop.
|- : prop -> type.
mp : {A:prop} {B:prop} (|- A) -> (|- (imp A B)) -> (|- B).
ax1 : {A:prop} {B:prop} (|- (imp A (imp B A))).
ax2 : {A:prop} {B:prop} {C:prop}
(|- (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))).
ax3 : {A:prop} {B:prop} (|- (imp (imp (not A) (not B)) (imp B A))).
%%% Definitions
or : prop -> prop -> prop = [A:prop] [B:prop] (imp (not A) B).
and : prop -> prop -> prop = [A:prop] [B:prop] (not (imp A (not B))).
iff : prop -> prop -> prop = [A:prop] [B:prop] (and (imp A B) (imp B A)).
Th0 : {A:prop} {B:prop} {C:prop}
(|- (imp A B)) -> (|- (imp A (imp B C))) -> (|- (imp A C)) =
[A:prop] [B:prop] [C:prop] [d1: |- (imp A B)] [d2: |- (imp A (imp B C))]
(mp _ _ d1 (mp _ _ d2 (ax2 A B C))).
Th1 : {A:prop} {B:prop} (|- B) -> (|- (imp A B)) =
[A:prop] [B:prop] [C:|- B]
(mp _ _ C (ax1 B A)).
Th2 : {A:prop} (|- (imp A A)) =
[A:prop] (mp _ _ (ax1 A A) (mp _ _ (ax1 A (imp A A)) (ax2 A (imp A A)
A))).
Th3 : {A:prop} {B:prop} (|- (imp A (imp (imp A B) B))) =
[A:prop] [B:prop]
(Th0 _ _ _
(Th0 _ _ _ (Th2 A) (Th1 A _ (ax1 A (imp A B))))
(Th0 _ _ _ (Th1 A _ (Th2 (imp A B))) (Th1 A _ (ax2 (imp A B) A B)))
).
Th4 : {A:prop} {B:prop} {C:prop}
|- (imp (imp B C) (imp (imp A B) (imp A C))) =
[A:prop][B:prop][C:prop]
(Th0 _ _ _ (ax1 (imp B C) A) (Th1 (imp B C) _ (ax2 A B C))).
Th5 : {A:prop} |- (imp (not (not A)) A) =
[A:prop]
(Th0 _ _ _
(Th1 (not (not A)) _ (Th2 A))
(Th0 _ _ _ (Th0 _ _ _
(ax1 (not (not A)) (not (not (imp A A))))
(Th1 (not (not A)) _ (ax3 (not (imp A A)) (not A)))
)
(Th1 (not (not A)) _ (ax3 A (imp A A))))).
Th6 : {A:prop} |- (or (not A) A) = Th5.
Th7 : {A:prop} |- (imp A (not (not A))) =
[A:prop] (mp _ _ (Th5 (not A)) (ax3 (not (not A)) A)).
Th8 : {A:prop} {B:prop} |- (imp (or A B) (or B A)) =
[A:prop] [B:prop] (Th0 _ _ _
(mp _ _ (Th7 B) (Th4 (not A) B (not (not B))))
(Th1 (imp (not A) B) _ (ax3 A (not B)))).
Th9 : {A:prop} {B:prop} |- (imp A (imp B (and A B))) =
[A:prop] [B:prop] (Th0 _ _ _
(Th0 _ _ _
(Th1 A _ (Th5 (imp A (not B))))
(Th0 _ _ _
(Th3 A (not B)) (Th1 A _ (Th4 (not (not (imp A (not B)))) (imp A (not
B)) (not B)))))
(Th1 A _ (ax3 (and A B) B))).
Th10: {A:prop} {B:prop} |- (iff (or A B) (or B A)) =
[A:prop] [B:prop] (mp _ _ (Th8 B A) (mp _ _ (Th8 A B) (Th9 _ _))).
Th11: {A:prop} {B:prop} {C:prop} |- (imp (imp A (imp B C)) (imp B (imp A C))) =
[A:prop] [B:prop] [C:prop]
(Th0 _ _ _ (Th1 _ _ (ax1 _ _))
(Th0 _ _ _
(Th0 _ _ _ (ax1 (imp A (imp B C)) B)
(Th1 (imp A (imp B C)) _ (mp _ _ (ax2 A B C) (Th4 B _ _))))
(Th1 (imp A (imp B C)) _ (ax2 _ _ _)))).
Th12: {A:prop} {B:prop} {C:prop}
|- (imp (imp A B) (imp (imp B C) (imp A C))) =
[A:prop] [B:prop] [C:prop] (mp _ _ (Th4 A B C) (Th11 _ _ _)).
Th13: {A:prop} {B:prop} |- (imp (imp A B) (imp (not B) (not A))) =
[A:prop] [B:prop] (mp _ _
(ax3 (not A) (not B))
(mp _ _
(mp _ _ (mp _ _ (Th7 B) (Th4 (not (not A)) _ _))
(mp _ _ (mp _ _ (Th5 A) (Th12 (not (not A)) A B)) (Th12 _ _ _)))
(Th12 _ _ _))).
Th14: {A:prop} {B:prop} |- (imp A (imp (not A) B)) =
[A:prop] [B:prop] (Th0 _ _ _
(Th0 _ _ _ (ax1 A (not B)) (Th1 A _ (Th13 (not B) A)))
(Th1 A _ (mp _ _ (Th5 B) (Th4 (not A) _ _ )))).
Th15: {A:prop} {B:prop} |- (imp A (or A B)) = Th14.
Th16: {A:prop} {B:prop} |- (imp B (or A B)) =
[A:prop] [B:prop] (mp _ _ (Th8 _ _) (mp _ _ (Th14 B A) (Th12 _ _ _))).
Th17: {A:prop} {B:prop} |- (imp (and A B) (and B A)) =
[A:prop] [B:prop]
(mp _ _
(mp _ _ (ax3 (not B) A)
(mp _ _ (mp _ _ (Th5 B) (Th12 _ _ _)) (Th12 _ _ _)))
(Th13 _ _)).
Th18: {A:prop} {B:prop} |- (imp (and A B) A) =
[A:prop] [B:prop]
(mp _ _
(mp _ _ (Th7 _)
(mp _ _ (mp _ _ (Th14 _ _) (Th11 _ _ _)) (Th12 _ _ _)))
(ax3 _ _)).
Th19: {A:prop} {B:prop} |- (imp (and A B) B) =
[A:prop] [B:prop]
(mp _ _ (Th18 _ _) (mp _ _ (Th17 _ _) (Th12 _ _ _))).
Twelf 1.2, Aug 27 1998
%% OK %%
[Opening file prop.elf]
prop : type.
imp : prop -> prop -> prop.
not : prop -> prop.
|- : prop -> type.
mp : {A:prop} {B:prop} |- A -> |- (imp A B) -> |- B.
ax1 : {A:prop} {B:prop} |- (imp A (imp B A)).
ax2 :
{A:prop} {B:prop} {C:prop}
|- (imp (imp A (imp B C)) (imp (imp A B) (imp A C))).
ax3 : {A:prop} {B:prop} |- (imp (imp (not A) (not B)) (imp B A)).
or : prop -> prop -> prop = [A:prop] [B:prop] imp (not A) B.
and : prop -> prop -> prop = [A:prop] [B:prop] not (imp A (not B)).
iff : prop -> prop -> prop = [A:prop] [B:prop] and (imp A B) (imp B A).
Th0 :
{A:prop} {B:prop} {C:prop}
|- (imp A B) -> |- (imp A (imp B C)) -> |- (imp A C)
= [A:prop] [B:prop] [C:prop] [d1:|- (imp A B)] [d2:|- (imp A (imp B C))]
mp (imp A B) (imp A C) d1
(mp (imp A (imp B C)) (imp (imp A B) (imp A C)) d2 (ax2 A B C)).
Th1 : {A:prop} {B:prop} |- B -> |- (imp A B)
= [A:prop] [B:prop] [C:|- B] mp B (imp A B) C (ax1 B A).
Th2 : {A:prop} |- (imp A A)
= [A:prop]
mp (imp A (imp A A)) (imp A A) (ax1 A A)
(mp (imp A (imp (imp A A) A)) (imp (imp A (imp A A)) (imp A A))
(ax1 A (imp A A)) (ax2 A (imp A A) A)).
Th3 : {A:prop} {B:prop} |- (imp A (imp (imp A B) B))
= [A:prop] [B:prop]
Th0 A (imp (imp A B) A) (imp (imp A B) B)
(Th0 A A (imp (imp A B) A) (Th2 A)
(Th1 A (imp A (imp (imp A B) A)) (ax1 A (imp A B))))
(Th0 A (imp (imp A B) (imp A B))
(imp (imp (imp A B) A) (imp (imp A B) B))
(Th1 A (imp (imp A B) (imp A B)) (Th2 (imp A B)))
(Th1 A
(imp (imp (imp A B) (imp A B))
(imp (imp (imp A B) A) (imp (imp A B) B)))
(ax2 (imp A B) A B))).
Th4 : {A:prop} {B:prop} {C:prop} |- (imp (imp B C) (imp (imp A B) (imp A C)))
= [A:prop] [B:prop] [C:prop]
Th0 (imp B C) (imp A (imp B C)) (imp (imp A B) (imp A C))
(ax1 (imp B C) A)
(Th1 (imp B C) (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))
(ax2 A B C)).
Th5 : {A:prop} |- (imp (not (not A)) A)
= [A:prop]
Th0 (not (not A)) (imp A A) A (Th1 (not (not A)) (imp A A) (Th2 A))
(Th0 (not (not A)) (imp (not A) (not (imp A A))) (imp (imp A A) A)
(Th0 (not (not A)) (imp (not (not (imp A A))) (not (not A)))
(imp (not A) (not (imp A A)))
(ax1 (not (not A)) (not (not (imp A A))))
(Th1 (not (not A))
(imp (imp (not (not (imp A A))) (not (not A)))
(imp (not A) (not (imp A A))))
(ax3 (not (imp A A)) (not A))))
(Th1 (not (not A))
(imp (imp (not A) (not (imp A A))) (imp (imp A A) A))
(ax3 A (imp A A)))).
Th6 : {A:prop} |- (or (not A) A) = Th5.
Th7 : {A:prop} |- (imp A (not (not A)))
= [A:prop]
mp (imp (not (not (not A))) (not A)) (imp A (not (not A))) (Th5 (not A))
(ax3 (not (not A)) A).
Th8 : {A:prop} {B:prop} |- (imp (or A B) (or B A))
= [A:prop] [B:prop]
Th0 (imp (not A) B) (imp (not A) (not (not B))) (imp (not B) A)
(mp (imp B (not (not B)))
(imp (imp (not A) B) (imp (not A) (not (not B)))) (Th7 B)
(Th4 (not A) B (not (not B))))
(Th1 (imp (not A) B)
(imp (imp (not A) (not (not B))) (imp (not B) A)) (ax3 A (not B))).
Th9 : {A:prop} {B:prop} |- (imp A (imp B (and A B)))
= [A:prop] [B:prop]
Th0 A (imp (not (not (imp A (not B)))) (not B)) (imp B (and A B))
(Th0 A (imp (not (not (imp A (not B)))) (imp A (not B)))
(imp (not (not (imp A (not B)))) (not B))
(Th1 A (imp (not (not (imp A (not B)))) (imp A (not B)))
(Th5 (imp A (not B))))
(Th0 A (imp (imp A (not B)) (not B))
(imp (imp (not (not (imp A (not B)))) (imp A (not B)))
(imp (not (not (imp A (not B)))) (not B)))
(Th3 A (not B))
(Th1 A
(imp (imp (imp A (not B)) (not B))
(imp
(imp (not (not (imp A (not B)))) (imp A (not B)))
(imp (not (not (imp A (not B)))) (not B))))
(Th4 (not (not (imp A (not B)))) (imp A (not B)) (not B)))))
(Th1 A (imp (imp (not (and A B)) (not B)) (imp B (and A B)))
(ax3 (and A B) B)).
Th10 : {A:prop} {B:prop} |- (iff (or A B) (or B A))
= [A:prop] [B:prop]
mp (imp (or B A) (or A B))
(and (imp (or A B) (or B A)) (imp (or B A) (or A B))) (Th8 B A)
(mp (imp (or A B) (or B A))
(imp (imp (or B A) (or A B))
(and (imp (or A B) (or B A)) (imp (or B A) (or A B))))
(Th8 A B) (Th9 (imp (or A B) (or B A)) (imp (or B A) (or A B)))).
Th11 : {A:prop} {B:prop} {C:prop} |- (imp (imp A (imp B C)) (imp B (imp A C)))
= [A:prop] [B:prop] [C:prop]
Th0 (imp A (imp B C)) (imp B (imp A B)) (imp B (imp A C))
(Th1 (imp A (imp B C)) (imp B (imp A B)) (ax1 B A))
(Th0 (imp A (imp B C)) (imp B (imp (imp A B) (imp A C)))
(imp (imp B (imp A B)) (imp B (imp A C)))
(Th0 (imp A (imp B C)) (imp B (imp A (imp B C)))
(imp B (imp (imp A B) (imp A C))) (ax1 (imp A (imp B C)) B)
(Th1 (imp A (imp B C))
(imp (imp B (imp A (imp B C)))
(imp B (imp (imp A B) (imp A C))))
(mp (imp (imp A (imp B C)) (imp (imp A B) (imp A C)))
(imp (imp B (imp A (imp B C)))
(imp B (imp (imp A B) (imp A C)))) (ax2 A B C)
(Th4 B (imp A (imp B C)) (imp (imp A B) (imp A C))))))
(Th1 (imp A (imp B C))
(imp (imp B (imp (imp A B) (imp A C)))
(imp (imp B (imp A B)) (imp B (imp A C))))
(ax2 B (imp A B) (imp A C)))).
Th12 : {A:prop} {B:prop} {C:prop} |- (imp (imp A B) (imp (imp B C) (imp A C)))
= [A:prop] [B:prop] [C:prop]
mp (imp (imp B C) (imp (imp A B) (imp A C)))
(imp (imp A B) (imp (imp B C) (imp A C))) (Th4 A B C)
(Th11 (imp B C) (imp A B) (imp A C)).
Th13 : {A:prop} {B:prop} |- (imp (imp A B) (imp (not B) (not A)))
= [A:prop] [B:prop]
mp (imp (imp (not (not A)) (not (not B))) (imp (not B) (not A)))
(imp (imp A B) (imp (not B) (not A))) (ax3 (not A) (not B))
(mp (imp (imp A B) (imp (not (not A)) (not (not B))))
(imp
(imp (imp (not (not A)) (not (not B))) (imp (not B) (not A)))
(imp (imp A B) (imp (not B) (not A))))
(mp (imp (imp (not (not A)) B) (imp (not (not A)) (not (not B))))
(imp (imp A B) (imp (not (not A)) (not (not B))))
(mp (imp B (not (not B)))
(imp (imp (not (not A)) B)
(imp (not (not A)) (not (not B)))) (Th7 B)
(Th4 (not (not A)) B (not (not B))))
(mp (imp (imp A B) (imp (not (not A)) B))
(imp
(imp (imp (not (not A)) B)
(imp (not (not A)) (not (not B))))
(imp (imp A B) (imp (not (not A)) (not (not B)))))
(mp (imp (not (not A)) A)
(imp (imp A B) (imp (not (not A)) B)) (Th5 A)
(Th12 (not (not A)) A B))
(Th12 (imp A B) (imp (not (not A)) B)
(imp (not (not A)) (not (not B))))))
(Th12 (imp A B) (imp (not (not A)) (not (not B)))
(imp (not B) (not A)))).
Th14 : {A:prop} {B:prop} |- (imp A (imp (not A) B))
= [A:prop] [B:prop]
Th0 A (imp (not A) (not (not B))) (imp (not A) B)
(Th0 A (imp (not B) A) (imp (not A) (not (not B))) (ax1 A (not B))
(Th1 A (imp (imp (not B) A) (imp (not A) (not (not B))))
(Th13 (not B) A)))
(Th1 A (imp (imp (not A) (not (not B))) (imp (not A) B))
(mp (imp (not (not B)) B)
(imp (imp (not A) (not (not B))) (imp (not A) B)) (Th5 B)
(Th4 (not A) (not (not B)) B))).
Th15 : {A:prop} {B:prop} |- (imp A (or A B)) = Th14.
Th16 : {A:prop} {B:prop} |- (imp B (or A B))
= [A:prop] [B:prop]
mp (imp (or B A) (or A B)) (imp B (or A B)) (Th8 B A)
(mp (imp B (imp (not B) A))
(imp (imp (imp (not B) A) (or A B)) (imp B (or A B))) (Th14 B A)
(Th12 B (imp (not B) A) (or A B))).
Th17 : {A:prop} {B:prop} |- (imp (and A B) (and B A))
= [A:prop] [B:prop]
mp (imp (imp B (not A)) (imp A (not B)))
(imp (not (imp A (not B))) (not (imp B (not A))))
(mp (imp (imp (not (not B)) (not A)) (imp A (not B)))
(imp (imp B (not A)) (imp A (not B))) (ax3 (not B) A)
(mp (imp (imp B (not A)) (imp (not (not B)) (not A)))
(imp (imp (imp (not (not B)) (not A)) (imp A (not B)))
(imp (imp B (not A)) (imp A (not B))))
(mp (imp (not (not B)) B)
(imp (imp B (not A)) (imp (not (not B)) (not A))) (Th5 B)
(Th12 (not (not B)) B (not A)))
(Th12 (imp B (not A)) (imp (not (not B)) (not A))
(imp A (not B)))))
(Th13 (imp B (not A)) (imp A (not B))).
Th18 : {A:prop} {B:prop} |- (imp (and A B) A)
= [A:prop] [B:prop]
mp (imp (not A) (not (not (imp A (not B)))))
(imp (not (imp A (not B))) A)
(mp (imp (imp A (not B)) (not (not (imp A (not B)))))
(imp (not A) (not (not (imp A (not B))))) (Th7 (imp A (not B)))
(mp (imp (not A) (imp A (not B)))
(imp (imp (imp A (not B)) (not (not (imp A (not B)))))
(imp (not A) (not (not (imp A (not B))))))
(mp (imp A (imp (not A) (not B)))
(imp (not A) (imp A (not B))) (Th14 A (not B))
(Th11 A (not A) (not B)))
(Th12 (not A) (imp A (not B)) (not (not (imp A (not B)))))))
(ax3 A (not (imp A (not B)))).
Th19 : {A:prop} {B:prop} |- (imp (and A B) B)
= [A:prop] [B:prop]
mp (imp (and B A) B) (imp (and A B) B) (Th18 B A)
(mp (imp (and A B) (and B A))
(imp (imp (and B A) B) (imp (and A B) B)) (Th17 A B)
(Th12 (and A B) (and B A) B)).
[Closing file prop.elf]
%% OK %%
%%%% SYNTAX %%%%
Location : type.
Nat: type.
0 : Nat.
S : Nat -> Nat.
Expr : type.
val : Nat -> Expr.
! : Location -> Expr.
plus : Expr -> Expr -> Expr.
times : Expr -> Expr -> Expr.
Bool : type.
true : Bool.
false : Bool.
eq : Expr -> Expr -> Bool.
le : Expr -> Expr -> Bool.
not : Bool -> Bool.
or : Bool -> Bool -> Bool.
and : Bool -> Bool -> Bool.
Command : type.
skip : Command.
assign : Location -> Expr -> Command.
seq : Command -> Command -> Command.
if : Bool -> Command -> Command -> Command.
while : Bool -> Command -> Command.
let : Expr -> (Location -> Command) -> Command.
%%%% EXAMPLE %%%%
1 : Nat = (S 0).
program1 : Command =
(let (val 0) ([x:Location] (assign x (plus (! x) (val 1))))).
%%%% SEMANTICS %%%%
%%%% Reductions %%%%
ExprRed : Expr -> Expr -> type.
plusRed0 : {x:Nat} {y:Nat} ExprRed
(plus (val x) (val (S y))) (plus (val (S x)) (val y)).
plusRed1 : {x:Nat} ExprRed (plus (val x) (val 0)) (val x).
timesRed0 : {x:Nat} {y:Nat} ExprRed
(times (val x) (val (S y))) (plus (times (val x) (val y)) (val y)).
timesRed1 : {x:Nat} ExprRed (times (val x) (val 0)) (val 0).
BoolRed : Bool -> Bool -> type.
notRed0 : BoolRed (not true) false.
notRed1 : BoolRed (not false) true.
andRed0 : BoolRed (and true true) true.
andRed1 : BoolRed (and true false) false.
andRed2 : BoolRed (and false false) false.
andRed3 : BoolRed (and false true) false.
orRed0 : BoolRed (or true true) true.
orRed1 : BoolRed (or true false) true.
orRed2 : BoolRed (or false false) true.
orRed3 : BoolRed (or false true) false.
eqRed0 : {x:Nat} {y:Nat} BoolRed (eq (val (S x)) (val (S y))) (eq (val x) (val y)).
eqRed1 : BoolRed (eq (val 0) (val 0)) true.
eqRed2 : {x:Nat} BoolRed (eq (val 0) (val (S x))) false.
eqRed3 : {x:Nat} BoolRed (eq (val (S x)) (val 0)) false.
leRed0 : {x:Nat} {y:Nat} BoolRed (le (val (S x)) (val (S y))) (le (val x) (val y)).
leRed1 : BoolRed (le (val 0) (val 0)) true.
leRed2 : {x:Nat} BoolRed (le (val 0) (val (S x))) true.
leRed3 : {x:Nat} BoolRed (le (val (S x)) (val 0)) false.
CommandRed : Command -> Command -> type.
seqRed : {c : Command} CommandRed (seq skip c) c.
ifRed1 : {c1 : Command} {c2 : Command} CommandRed (if true c1 c2) c1.
ifRed2 : {c1 : Command} {c2 : Command} CommandRed (if false c1 c2) c2.
whileRed : {b : Bool} {c : Command}
CommandRed (while b c) (if b (seq c (while b c)) skip).
%%%% Contexts %%%%
ExprContext : (Expr -> Expr) -> type.
exprConHole : ExprContext ([e:Expr] e).
exprConPlus0 : {e:Expr} {H:Expr -> Expr} ExprContext H ->
ExprContext ([x:Expr] (plus (H x) e)).
exprConPlus1 : {n:Nat} {H:Expr -> Expr} ExprContext H ->
ExprContext ([x:Expr] (plus (val n) (H x))).
exprConTimes0 : {e:Expr} {H:Expr -> Expr} ExprContext H ->
ExprContext ([x:Expr] (times (H x) e)).
exprConTimes1 : {n:Nat} {H:Expr -> Expr} ExprContext H ->
ExprContext ([x:Expr] (times (val n) (H x))).
ExprBoolContext : (Expr -> Bool) -> type.
boolConEq0 : {e:Expr} {H:Expr -> Expr} ExprContext H ->
ExprBoolContext ([x:Expr] (eq (H x) e)).
boolConEq1 : {n:Nat} {H:Expr -> Expr} ExprContext H ->
ExprBoolContext ([x:Expr] (eq (val n) (H x))).
boolConLe0 : {e:Expr} {H:Expr -> Expr} ExprContext H ->
ExprBoolContext ([x:Expr] (le (H x) e)).
boolConLe1 : {n:Nat} {H:Expr -> Expr} ExprContext H ->
ExprBoolContext ([x:Expr] (le (val n) (H x))).
BoolContext : (Bool -> Bool) -> type.
boolConHole : BoolContext ([b:Bool] b).
boolConNot : {H:Bool -> Bool} BoolContext H ->
BoolContext ([x:Bool] (not (H x))).
boolConAnd0 : {b:Bool} {H:Bool -> Bool} BoolContext H ->
BoolContext ([x:Bool] (and (H x) b)).
boolConAnd1 : {H:Bool -> Bool} BoolContext H ->
BoolContext ([x:Bool] (and true (H x))).
boolConAnd2 : {H:Bool -> Bool} BoolContext H ->
BoolContext ([x:Bool] (and false (H x))).
boolConOr0 : {b:Bool} {H:Bool -> Bool} BoolContext H ->
BoolContext ([x:Bool] (or (H x) b)).
boolConOr1 : {H:Bool -> Bool} BoolContext H ->
BoolContext ([x:Bool] (or true (H x))).
boolConOr2 : {H:Bool -> Bool} BoolContext H ->
BoolContext ([x:Bool] (or false (H x))).
boolConExprNot : {H:Expr -> Bool} ExprBoolContext H ->
ExprBoolContext ([x:Expr] (not (H x))).
boolConExprAnd0 : {b:Bool} {H:Expr -> Bool} ExprBoolContext H ->
ExprBoolContext ([x:Expr] (and (H x) b)).
boolConExprAnd1 : {H:Expr -> Bool} ExprBoolContext H ->
ExprBoolContext ([x:Expr] (and true (H x))).
boolConExprAnd2 : {H:Expr -> Bool} ExprBoolContext H ->
ExprBoolContext ([x:Expr] (and false (H x))).
boolConExprOr0 : {b:Bool} {H:Expr -> Bool} ExprBoolContext H ->
ExprBoolContext ([x:Expr] (or (H x) b)).
boolConExprOr1 : {H:Expr -> Bool} ExprBoolContext H ->
ExprBoolContext ([x:Expr] (or true (H x))).
boolConExprOr2 : {H:Expr -> Bool} ExprBoolContext H ->
ExprBoolContext ([x:Expr] (or false (H x))).
ExprCommandContext : (Expr -> Command) -> type.
commandConAssign : {l:Location} {H:Expr -> Expr} ExprContext H ->
ExprCommandContext ([x:Expr] (assign l (H x))).
commandConLet0 : {c:Location -> Command} {H:Expr -> Expr} ExprContext H ->
ExprCommandContext ([x:Expr] (let (H x) c)).
BoolCommandContext : (Bool -> Command) -> type.
commandConIf : {c1:Command} {c2:Command} {H:Bool -> Bool}
BoolContext H -> BoolCommandContext ([x:Bool] (if (H x) c1 c2)).
commandConExprIf : {c1:Command} {c2:Command} {H:Expr -> Bool}
ExprBoolContext H -> ExprCommandContext ([x:Expr] (if (H x) c1 c2)).
CommandContext : (Command -> Command) -> type.
commandConHole : CommandContext ([c:Command] c).
commandConSeq : {c:Command} {H:Command -> Command}
CommandContext H -> CommandContext ([x:Command] (seq (H x) c)).
commandConLet1 : {n:Nat} {H:Location -> Command -> Command}
({l:Location} CommandContext (H l)) ->
CommandContext ([x:Command] (let (val n) [l:Location] ((H l) x))).
commandConBoolSeq : {c:Command} {H:Bool -> Command}
BoolCommandContext H -> BoolCommandContext ([x:Bool] (seq (H x) c)).
commandConBoolLet1 : {n:Nat} {H:Location -> Bool -> Command}
({l:Location} BoolCommandContext (H l)) ->
BoolCommandContext ([x:Bool] (let (val n) [l:Location] ((H l) x))).
commandConExprSeq : {c:Command} {H:Expr -> Command}
ExprCommandContext H -> ExprCommandContext ([x:Expr] (seq (H x) c)).
commandConExprLet1 : {n:Nat} {H:Location -> Expr -> Command}
({l:Location} ExprCommandContext (H l)) ->
ExprCommandContext ([x:Expr] (let (val n) [l:Location] ((H l) x))).
%%%% Let Reductions %%%%
letRed0 : {n:Nat} {H:Location -> Expr -> Command}
({l:Location} ExprCommandContext (H l)) ->
CommandRed (let (val n) ([l:Location] ((H l) (! l))))
(let (val n) ([l:Location] ((H l) (val n)))).
letRed1 : {n1:Nat} {n2:Nat} {H:Location -> Command -> Command}
({l:Location} CommandContext (H l)) ->
CommandRed (let (val n1) ([l:Location] ((H l) (assign l (val n2)))))
(let (val n2) ([l:Location] ((H l) skip))).
%%%% Global Reductions %%%%
Derivation : Command -> Command -> type.
global0 : {H : Expr -> Command} {r: Expr} {e: Expr} ExprCommandContext H ->
ExprRed r e -> Derivation (H r) (H e).
global1 : {H : Bool -> Command} {r: Bool} {b: Bool} BoolCommandContext H ->
BoolRed r b -> Derivation (H r) (H b).
global2 : {H : Command -> Command} {r: Command} {c: Command} CommandContext H ->
CommandRed r c -> Derivation (H r) (H c).
Derivation* : Command -> Command -> type.
derivationDer: {c:Command} {d:Command} Derivation c d -> Derivation* c d.
reflexDer : {c:Command} Derivation* c c.
transDer : {c:Command} {d:Command} {e:Command} Derivation* c d ->
Derivation* d e -> Derivation* c e.
%%%% Example Reductions %%%%
test0 = global2 ([c:Command] c) (let (val 0) ([l:Location] assign l
(plus (val 0) (! l)))) (let (val 0) ([l:Location] assign l (plus (val
0) (val 0)))) commandConHole (letRed0 0 ([m:Location] [e:Expr] (assign
m (plus (val 0) e))) ([m:Location] (commandConAssign m ([e:Expr] (plus
(val 0) e)) (exprConPlus1 0 ([f:Expr] f) exprConHole)))).
test1 = global2 ([c:Command] c) (let (val 0) ([l:Location] assign l
(val (S 0)))) (let (val (S 0)) ([l:Location] skip)) commandConHole
(letRed1 0 (S 0) ([m:Location] [d:Command] d) ([m:Location]
commandConHole)).
test2 = global2 _ _ _ commandConHole (letRed0 0 _ ([m:Location]
(commandConExprIf skip skip _ (boolConEq0 (! m) _ (exprConHole))))).