Clausal Language (ver. 5.81.20, by P.J. Voda, J. Komara, J. Kluka)

Literature.

[1] J. Komara. Specification and Verification of Programs. Downloadable lecture notes available through the web page of the course.
[2] J. Komara and P. J. Voda. Metamathematics of Computer Programming. 2001.

Chapter. Numeric Programs.

Section. Recursion with Measure.

Measure induction. Show that the principle of measure induction (course of values induction with measure) is admissible in Peano arithmetic.

Remark. Prove the claim for the special case in the following theory.

\forall x (\forall y (μ [y] < μ [x] \to φ [y]) \to φ [x])

φ [x]

[CL] Measure induction. Syntax:

indm <measure> [; <variable(s)>]

where the induction formula is formed from the current sequent.

Example(s):

$indm μ [x]$
$\frac{φ [x] *}{\forall y (μ [y] < μ [x] \to φ [y]) \to φ [x] *}$
$indm μ [x]; a$
$\frac{φ [x] *}{\forall y (μ [y] < μ [x] \to \forall a φ [y]) \to φ [x] *}$

Greatest common divisor. Euclid algorithm based on the property

x ≦ y \land z ∣ x \to z ∣ y \leftrightarrow z ∣ y \dot{-} x

[CL] Remark. This property in the form of the following theorem

x ≦ y \land z ∣ x \to z ∣ y \dot{-} x \leftrightarrow z ∣ y

Euclid_divides_minus

is proved in the module Maux*.

\gcd (x, y) = \max (x, y) \leftarrow x = 0

\gcd (x, y) = \max (x, y) \leftarrow x \neq 0 \land y = 0

\gcd (x, y) = \gcd (x, y \dot{-} x) \leftarrow x \neq 0 \land y \neq 0 \land x < y

\gcd (x, y) = x \leftarrow x \neq 0 \land y \neq 0 \land x = y

\gcd (x, y) = \gcd (x \dot{-} y, y) \leftarrow x \neq 0 \land y \neq 0 \land x > y

Exercise. Prove the conditions of regularity for the function $\gcd (x, y)$ :

x \neq 0 \land y \neq 0 \land x < y \to \max (x, y \dot{-} x) < \max (x, y)

x \neq 0 \land y \neq 0 \land x > y \to \max (x \dot{-} y, y) < \max (x, y)

x \neq 0 \land y \neq 0 \land x < y \to \max (x, y \dot{-} x) < \max (x, y)

x \neq 0 \land y \neq 0 \land x > y \to \max (x \dot{-} y, y) < \max (x, y)

Exercise. Prove

x \neq 0 \lor y \neq 0 \to \gcd (x, y) ∣ x \land \gcd (x, y) ∣ y

(x \neq 0 \lor y \neq 0) \land z ∣ x \land z ∣ y \to z ≦ \gcd (x, y)

[CL] Hint. Prove the properties by induction with a measure . In the induction step, consider two cases according to whether the disjunction $x = 0 \lor y = 0$ holds or not. Both cases when $x = 0 \lor y = 0$ are formulated as stand-alone lemmas.

(x = 0 \lor y = 0) \land (x \neq 0 \lor y \neq 0) \to \gcd (x, y) ∣ x \land \gcd (x, y) ∣ y

x \neq 0 \lor y \neq 0 \to \gcd (x, y) ∣ x \land \gcd (x, y) ∣ y

(x = 0 \lor y = 0) \land (x \neq 0 \lor y \neq 0) \land z ∣ x \land z ∣ y \to z ≦ \gcd (x, y)

(x \neq 0 \lor y \neq 0) \land z ∣ x \land z ∣ y \to z ≦ \gcd (x, y)