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: x and y. Those symbols represent integers: their type is int.

Introducing new symbols is done through the logic keyword.

Then, two axioms are added. The first one states that x is greater than y, and the second one state that y is greater than the constant 0.

Those two axioms are named, and introduced through the axiom keyword.

Finally, we state our goal: we want to prove that x is greater than 0.

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_0 is Valid. Indeed, no matter the values given to x and y (no matter the interpretation of x and y), if the axioms x_gt_y and y_gt_0 are verified, than x_gt_0 is 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 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 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 

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 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
        
*)

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

Boolean operators
Symbol	Name / interpretation
`not`	Negation
`and`	Conjunction
`or`	Disjonction
`xor`	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 Alt-Ergo’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 Alt-Ergo’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 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 exists in Alt-Ergo’s native language.

The universal quantifier “for all […], […]”, also written \(\forall\), represented by forall in 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.

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” (for exists) or as “it is true that” (for forall).

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: 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))

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 Alt-Ergo 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)