Get started with Alt-Ergo ! Logical foundations¶
In this chapter, we’ll start working with Alt-Ergo.
- We’ll first learn how to state problems to Alt-Ergo, 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 Alt-Ergo’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 Alt-Ergo 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 built-in theories ?
- Stating goals : what are we trying to prove ?
Have a look at the following problem. You can press Ask Alt-Ergo to see Alt-Ergo 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:
y. Those symbols represent integers: their type is
Introducing new symbols is done through the
Then, two axioms are added. The first one states that
xis greater than
y, and the second one state that
yis greater than the constant
Those two axioms are named, and introduced through the
Finally, we state our goal: we want to prove that
xis greater than
If you press Ask Alt-Ergo, you should see just below it something like
Valid (0.2250) (4 steps) (goal x_gt_0).
This means that Alt-Ergo has been able to prove that the goal
x_gt_0is Valid. Indeed, no matter the values given to
y(no matter the interpretation of
y), if the axioms
y_gt_0are verified, than
x_gt_0is verified too !
(The two other numbers correspond respectively to the time – in seconds – taken by Alt-Ergo 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
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 Alt-Ergo 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
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 Alt-Ergo’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 *)
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
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
Those are boolean operators: they work on the type
bool has two values:
|Symbol||Name / interpretation|
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)
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 *)
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 Alt-Ergo’s native language’s types.
Indeed, it is the type of propositions: axioms and goals are defined through expressions of type
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 Alt-Ergo’s error messages, or in other people’s code.
prop may be thought of as an alias for
(This wasn’t the case prior to Alt-Ergo 2.3.0, because of Alt-Ergo’s origin in Coq ecosystem, but you can ignore this historical subtlety).
Quantifiers and first-order logic¶
If we worked only on those boolean operators, we would stay in the realm of propositional logic, sometimes called “zeroth-order logic”.
While it is the foundation of more interesting logics, it isn’t very expressive. The main interest of SMT-solvers (over SAT-solvers) is that it allows us to go into the richer world if predicate logic, also called first-order logic, in which variables can be introduced and quantified upon.
There are two quantifiers in first-order logic:
- The existential quantifier “there exists […] such that […]”, also written \(\exists\), represented by
existsin Alt-Ergo’s native language.
- The universal quantifier “for all […], […]”, also written \(\forall\), represented by
forallin Alt-Ergo’s native language.
Alt-Ergo’s version of first-order logic is typed: all variables which are quantified must be given a type.
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 (
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.
.can be read as “such that” (for
exists) or as “it is true that” (for
Here is a more complex example.
bool -> bool, which we first encounter here, is the type of functions from
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: Alt-Ergo’s native language is not a functional language ! While it shares several features with them, it doesn’t treat functions as first-class object. It is neither possible to create higher-order 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))
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
logic n: int axiom n_def: n = 257 goal n_is_prime: (** YOUR CODE *)
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
x0 op1 x1 op2 x2 ... is interpreted by Alt-Ergo as
(x0 op1 x1) and (x1 op2 x2) and ....
This allows us to write interval conditions efficiently.
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
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).
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
predicatefollowed 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).
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)
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)