# 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,axiomsandgoals.- Then, we’ll expand our logical vocabulary to state and prove more interesting things, using
boolean operators,quantifiersandpredicates.

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`

isValid. 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`

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’tuse 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)
```