## Tutorial 2: Geometry in the Real Domain

### Domain Selection

```
Reduce (Free CSL version), 19-Aug-15 ...
1: rlset reals;
{}{}
```

We select the real domain, which is also known as Tarski Algebra. We could
also have used its short name `R`

instead of `reals`

.

### Deriving Heron's Formula

Heron's
formula, also known as Qin's Formula, relates the area \(F\) of a
triangle to its side lengths \(a\), \(b\), \(c\):
$$
F^2=s(s-a)(s-b)(s-c),\quad\text{where}\quad s=\frac{a+b+c}{2}.
$$
For later comparison, we explicitly compute this as a Redlog equation. With
the definition of `s`

notice how "`$`

" in contrast
to "`;`

" as a terminator suppresses the output:

```
2: s := (a+b+c)/2$
3: heron := rlsimpl(f^2=s*(s-a)*(s-b)*(s-c));
heron := a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ + 16⋅f² = 0
```

In order to automatically derive this theorem we choose coordinates for an
arbitrary triangle as
`A=(-z,0)`

, `B=(z,0)`

, and `C=(x₀,y₀)`

. Then
the area `f`

and the side lengths `a`

,
`b`

, and `c`

satisfy the corresponding equations in the
formula `φ`

in the following Redlog commands.

```
4: phi := ex({x0,y0,z},f=z*y0 and a**2=(z-x0)**2+y0**2 and
4: b**2 = (z+x0)**2+y0**2 and c=2*z);
φ := ∃x₀ ∃y₀ ∃z (f - y₀⋅z = 0 ∧ a² - x₀² + 2⋅x₀⋅z - y₀² - z² = 0
∧ b² - x₀² - 2⋅x₀⋅z - y₀² - z² = 0 ∧ c - 2⋅z = 0)
5: rlvarl phi;
{{a,b,c,f},{x₀,y₀,z}}
```

The prenex formula `φ`

contains two sorts of variables, free ones
and bound ones, which we also call *parameters* and *quantified
variables*, respectively. The function rlvarl splits them into two lists for us, which can be convenient for
larger formulas.

We have not specified that any of the parameters `a`

,
`b`

, `c`

, or `f`

be positive, so that our
formalization might be too general. In geometric deduction there is a
general expectation to have support from the prover for such non-degeneracy
conditions. Real quantifier elimination rlqe will, similarly to Heron's formula, yield a condition equivalent
to `φ`

but containing only the parameters.

```
6: rlqe phi;
(c ≠ 0 ∧ a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ ≤ 0 ∧ (
(c⋅f ≥ 0 ∧ a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ + 16⋅f² = 0)
∨ (c⋅f ≤ 0 ∧ a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ + 16⋅f² = 0)))
∨ (c ≠ 0 ∧ b²⋅c² - 4⋅f² ≥ 0 ∧ ((c⋅f ≥ 0 ∧ a²⋅c - b²⋅c - c³ ≥ 0
∧ a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ + 16⋅f² = 0) ∨ (c⋅f ≤ 0
∧ a²⋅c - b²⋅c - c³ ≥ 0
∧ a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ + 16⋅f² = 0) ∨ (c⋅f ≥ 0
∧ a²⋅c - b²⋅c - c³ ≤ 0
∧ a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ + 16⋅f² = 0) ∨ (c⋅f ≤ 0
∧ a²⋅c - b²⋅c - c³ ≤ 0
∧ a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ + 16⋅f² = 0)))
∨ (f = 0 ∧ (a - b + c = 0 ∨ a + b - c = 0))
∨ (f = 0 ∧ (a - b - c = 0 ∨ a + b + c = 0))
```

We are not entirely happy with this result. It is quite big, and we spot
several conditions, like
`c≠0`

or `f=0`

, related to degenerate cases, which
probably complicates the formula. This points at using *generic*
quantifier elimination rlgqe,
which—besides a quantifier-free equivalent—generates a list of
negated equations called *theory*.

```
7: sol := rlgqe phi;
sol := {{c ≠ 0},
b²⋅c² - 4⋅f² ≥ 0 ∧ ((a²⋅c - b²⋅c - c³ ≤ 0
∧ a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ + 16⋅f² = 0) ∨ (
a²⋅c - b²⋅c - c³ ≥ 0
∧ a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ + 16⋅f² = 0))}
```

The—much smaller—elimination result is equivalent
to `φ`

provided that side `c`

does not have length
zero, in which case we would not have a triangle anymore. The elimination
result in `sol`

is still a bit complicated. We apply an advanced
simplifier rlgqe based on Gröbner basis
techniques.

```
8: gsol := rlgsn second sol;
gsol := b²⋅c² - 4⋅f² ≥ 0
∧ a⁴ - 2⋅a²⋅b² - 2⋅a²⋅c² + b⁴ - 2⋅b²⋅c² + c⁴ + 16⋅f² = 0
```

This brings us close to Heron's formula in size. We suspect that
in `gsol`

the inequality is implied by the equation and thus
redundant. Let us try:

```
9: rlqe rlall(part(gsol, 2) impl part(gsol, 1));
true
```

Finally, we can automatically verify that the equation in `gsol`

is equivalent to Heron's formula.

```
10: rlqe rlall(gsol equiv heron);
true
```

In fact, it is even equal.

```
11: part(gsol, 2, 1) - part(heron, 1);
0
```

Note that our derived result happens to be correct also for the excluded
degenerate case `c=0`

. We could, more carefully, test for
equivalence taking into account the assumption `c≠0`

:

```
12: rlqe rlall(first first sol impl (gsol equiv heron));
true
```

In general, the theory `first sol`

would contain several atomic
formulas, which at this point has to be converted into a conjunction using a
`for each`

loop with Redlog's mkand action.

### References

- A. Dolzmann and T. Sturm. Simplification of quantifier-free formulae over ordered fields. J. Symb. Comput., 24(2), 1997.
- A. Dolzmann, T. Sturm, and V. Weispfenning. A new approach for automatic theorem proving in real geometry. J. Autom. Reasoning, 21(3), 1998.