Redlog Documentation Center

This new documentation in under construction. For functions not covered yet, please use the old documentation.

documentation → tutorials → geometry

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

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