Get started with AltErgo ! Logical foundations
In this chapter, we’ll start working with AltErgo.
We’ll first learn how to state problems to AltErgo, by creating symbols, axioms and goals.
Then, we’ll expand our logical vocabulary to state and prove more interesting things, using boolean operators, quantifiers and predicates.
This chapter is an introduction to AltErgo’s native language, which will continue in the next chapters.
If you already know OCaml, Gallina (Coq’s specification language) or WhyML (from Why3), you may notice similarities with them.
Symbols, axioms and goals
To make AltErgo prove things, it is necessary to state the problems !
To do this in its native language, there are three main parts.
Stating the terms of the problem : what are the symbols that will be used ?
Stating hypotheses : what axioms should be added to builtin theories ?
Stating goals : what are we trying to prove ?
Have a look at the following problem. You can press Ask AltErgo to see AltErgo answers to this input file.
Don’t worry if you don’t understand the whole syntax yet. This will be introduced through this chapter.
logic x, y: int
axiom x_gt_y: x >= y
axiom y_gt_0: y >= 0
goal x_gt_0: x >= 0
Let’s break this down.
First, two new symbols are introduced:
x
andy
. Those symbols represent integers: their type isint
.Introducing new symbols is done through the
logic
keyword.Then, two axioms are added. The first one states that
x
is greater thany
, and the second one state thaty
is greater than the constant0
.Those two axioms are named, and introduced through the
axiom
keyword.Finally, we state our goal: we want to prove that
x
is greater than0
.If you press Ask AltErgo, you should see just below it something like
Valid (0.2250) (4 steps) (goal x_gt_0)
.This means that AltErgo has been able to prove that the goal
x_gt_0
is Valid. Indeed, no matter the values given tox
andy
(no matter the interpretation ofx
andy
), if the axiomsx_gt_y
andy_gt_0
are verified, thanx_gt_0
is verified too !(The two other numbers correspond respectively to the time – in seconds – taken by AltErgo to answer, and the number of “steps” it had to do to reach this conclusion. Let’s ignore this for the moment.)
Notice the syntax: a new symbol, axiom or goal is introduced through the keyword logic
, axiom
or goal
respectively. Just after the keyword, the name of the construction being defined is added. We then add a colon :
, followed by the definition of the construction: a type for (uninterpreted) symbols, and a logical expression for axioms and goals.
Several symbols can be defined at the same time if they have the same type: just seperate their names with a comma ,
.
Note that several goals could be defined in the same file. An invalid goal won’t stop AltErgo from looking at the other goals.
logic P, Q, R: bool
axiom P_and_Q: P and Q = true
goal P_true:
P = true
goal Q_true:
Q = true
goal P_implies_R:
P > R
goal R_implies_P_or_Q:
R > P or Q
Exercise
Before going further, have a go with it !
Can you state and prove that the product of two positive integers is positive ? Integer product is written *
in AltErgo’s native language.
You may look at the documentation if you want to look up operands, but you should already have everything you need.
Remove the comment, and write your code.
(** YOUR CODE HERE *)
Solution
There are quite a few ways to do this.
One of them would be to state all hypotheses separately.
logic x,y: int
axiom x_pos: x>=0
axiom y_pos: y>=0
goal prod_pos: x*y>=0
You may even have introduced an intermediate variable.
logic x,y,z: int
axiom x_pos: x >= 0
axiom y_pos: y >= 0
axiom z_prod: z = x*y
goal z_pos: z >= 0
You may group together the hypotheses through the and
operator.
logic x,y: int
axiom x_y_pos: x>=0 and y>=0
goal prod_pos: x*y >= 0
An even shorter solution would be to hide axioms with >
in one of the two following ways.
logic x,y: int
goal prod_pos_1:
x >= 0 and y >= 0 > x*y >= 0
goal prod_pos_2:
x >= 0 > y >= 0 > x*y >= 0
Expanding our logical vocabulary
In order to start proving more interesting things, we’ll need to learn some vocabulary, in order to express richer logical expressions.
Propositional logic with boolean operators
We’ve already used some logical operators, such as and
, or
and >
.
Those are boolean operators: they work on the type bool
.
The type bool
has two values: true
and false
Symbol 
Name / interpretation 


Negation 

Conjunction 

Disjonction 

Exclusive or 

Implication 

Equivalence 
Example
We may use them to prove tautologies, such as De Morgan’s laws.
logic P, Q: bool
goal de_morgan_1:
not(P and Q) <> not(P) or not(Q)
goal de_morgan_2:
not(P or Q) <> not(P) and not(Q)
Exercise
Prove other famous tautologies.
logic P, Q, R: bool
goal or_idempotent:
(* YOUR CODE HERE *)
goal and_commutative:
(* YOUR CODE HERE *)
goal xor_associative:
(* YOUR CODE HERE *)
goal implies_transitive:
(* YOUR CODE HERE *)
Solution
logic P, Q, R: bool
goal or_idempotent:
P or P <> P
goal and_commutative:
P and Q <> Q and P
goal xor_associative:
P xor (Q xor R) <> (P xor Q) xor R
goal implies_transitive:
(P > Q) and (Q > R) > (P > R)
The type of propositions
bool
is special among AltErgo’s native language’s types.
Indeed, it is the type of propositions: axioms and goals are defined through expressions of type bool
!
In other words, the two followings snippets are strictly equivalent.
logic P, Q: bool
axiom P_or_Q_true: P or Q = true
axiom not_Q: Q = false
goal P_true: P = true
logic P, Q: bool
axiom P_or_Q_true: P or Q
axiom not_Q: not(Q)
goal P_true: P
You may sometimes see the type prop
appear in AltErgo’s error messages, or in other people’s code.
prop
may be thought of as an alias for bool
.
(This wasn’t the case prior to AltErgo 2.3.0, because of AltErgo’s origin in Coq ecosystem, but you can ignore this historical subtlety).
Quantifiers and firstorder logic
If we worked only on those boolean operators, we would stay in the realm of propositional logic, sometimes called “zerothorder logic”.
While it is the foundation of more interesting logics, it isn’t very expressive. The main interest of SMTsolvers (over SATsolvers) is that it allows us to go into the richer world if predicate logic, also called firstorder logic, in which variables can be introduced and quantified upon.
There are two quantifiers in firstorder logic:
The existential quantifier “there exists […] such that […]”, also written \(\exists\), represented by
exists
in AltErgo’s native language.The universal quantifier “for all […], […]”, also written \(\forall\), represented by
forall
in AltErgo’s native language.
AltErgo’s version of firstorder logic is typed: all variables which are quantified must be given a type.
Example
Our example about the product of positive numbers may be expressed this way.
goal prod_pos:
forall x, y: int. x>=0 and y>=0 > x*y>=0
Notice the syntax:
We first write the quantifier (
forall
) or (exists
)We then introduce variables which are quantified upon, along with their type preceded by a colon
,
, by writing<variables> : <type>
.If several variables are used, they are separated by a comma
,
.We then add
.
, followed by the expression using quantified variables.The dot
.
can be read as “such that” (forexists
) or as “it is true that” (forforall
).
Example
Here is a more complex example.
The type bool > bool
, which we first encounter here, is the type of functions from bool
to bool
logic f: bool > bool
goal fixpoint_implies_idempotent:
(exists x:bool. f(x) = x) > (forall y:bool. f(f(y)) = f(y))
This can be translated in english the following way.
Consider \(f\) a function from booleans to booleans.If there exists a boolean \(x\) such that \(f(x)=x\), then for all booleans \(y\) it is true that \(f(f(y))=f(y)\).
This example is the occasion to emphasize the following fact: AltErgo’s native language is not a functional language ! While it shares several features with them, it doesn’t treat functions as firstclass object. It is neither possible to create higherorder functions, nor to quantify directly over them.
Indeed, the following code causes an error.
goal fixpoint_implies_idempotent:
forall f: bool > bool.
(exists x:bool. f(x) = x) > (forall y:bool. f(f(y)) = f(y))
Exercise
Try to express and prove the fact that 257 is prime.
Remember that we have learned how to combine propositions through boolean operators and quantifiers.
You may also find integer comparisons useful, using operators such as =
, <=
, <
, >=
and >
.
logic n: int
axiom n_def: n = 257
goal n_is_prime:
(** YOUR CODE
*)
Solution
Here is a possible solution, which negates the predicate “\(n\) is composite”.
logic n: int
axiom n_def: n = 257
goal n_is_prime:
not(
exists a,b:int.
1<a and a<n and 1<b and b<n and a*b = n)
The predicate “\(n\) is composite” could actually be expressed slightly more consicely, using some syntactic sugar.
logic n: int
axiom n_def: n = 257
goal n_is_prime:
not(
exists a,b:int.
1<a<n and 1<b<n and a*b = n)
Here, we use the fact that for operators such as <
whose codomain is bool
,
x0 op1 x1 op2 x2 ...
is interpreted by AltErgo as (x0 op1 x1) and (x1 op2 x2) and ...
.
This allows us to write interval conditions efficiently.
Predicates
For the moment, our code is prompt to contain a lot of repetition.
For example, the notion “is positive” was redefined several times in this example.
logic x,y: int
axiom x_pos: x>=0
axiom y_pos: y>=0
goal prod_pos: x*y>=0
This was okay here, but can get quite bad in larger code.
Predicates may be used to abstract and factor the code. Predicates are functions whose codomain is bool
.
logic x,y: int
predicate is_pos(z: int) = z>=0
axiom x_pos: is_pos(x)
axiom y_pos: is_pos(y)
goal prod_pos: is_pos(x*y)
Predicates may have several arguments (or even none).
Examples
predicate in_range(bound1:int, bound2:int, x: int) =
(bound1 <= x <= bound2) or (bound2 <= x <= bound1)
(* Valid *)
goal g1: in_range(1,5,3)
(* Valid *)
goal g2: in_range(3,1,1)
(* Invalid *)
goal g3: in_range(11,12,4)
logic f: bool > bool
predicate f_is_constant =
forall x:bool. f(x) = x
predicate f_has_fixpoint =
exists x:bool. f(x) = x
predicate f_is_idempotent =
forall x:bool. f(f(x)) = f(x)
predicate f_is_involutive =
forall x:bool. f(f(x)) = x
goal g1:
f_is_constant >
f_has_fixpoint and f_is_idempotent and f_is_involutive
goal g2:
f_is_involutive and f_has_fixpoint >
f_is_constant
goal g3:
f_has_fixpoint >
f_is_idempotent
Notice the syntax.
To create a predicate,
First, use the keyword
predicate
followed by the name of the predicate.
If this predicate has arguments, write them between parentheses. They must be named and types. Multiple arguments are separated by a comma.
If there no arguments, just write nothing (no parentheses).
Then, add the sign equal
=
. (Just like functions which we will study in the next chapter: don’t use a colon, which would lead to a syntax error.)Finally, add the definition of the predicate.
To use a predicate, simple write its name, followed by its arguments between parentheses (if it has any).
Exercise
Define a predicate is_prime
(you may have a look at the previous exercise), and use it on a few examples.
(** YOUR CODE: define the predicate is_prime here
*)
goal primality_3: is_prime(3)
goal primality_13: is_prime(13)
goal primality_257: is_prime(257)
Solution
Here is a possible solution, inspired by the previous exercise.
predicate is_prime(n:int) =
not(
exists a,b:int.
1<a<n and 1<b<n and a*b = n)
goal primality_3: is_prime(3)
goal primality_13: is_prime(13)
goal primality_257: is_prime(257)