Totality of Euclid's GCD algorithm

Executable Specification

[View gcd.sig] [View gcd.mod]
sig gcd.

kind    nat, bool        type.

type    z                nat.
type    s                nat -> nat.
type    tt, ff           bool.

type    nat              nat -> o.
type    bool             bool -> o.
type    sub, gcd         nat -> nat -> nat -> o.
type    less             nat -> nat -> bool -> o.
type    lt               nat -> nat -> o.

%% Euclid's GCD algorithm
%%
%% Adapted from the %reduces example in the Twelf User's Guide:
%% http://www.cs.cmu.edu/~twelf/guide-1-4/twelf_8.html#SEC47

module gcd.

nat z.
nat (s N) :- nat N.

bool tt.
bool ff.

sub X z X.
sub (s X) (s Y) Z :- sub X Y Z.

less z (s X) tt.
less X z ff.
less (s X) (s Y) B :- less X Y B.

lt z (s Y).
lt (s X) (s Y) :- lt X Y.

gcd z Y Y.
gcd X z X.
gcd (s X) (s Y) Z :- less X Y tt, sub Y X Y', gcd (s X) Y' Z.  % (1)
gcd (s X) (s Y) Z :- less X Y ff, sub X Y X', gcd X' (s Y) Z.  % (2)

Reasoning

[View gcd.thm]

Click on a command or tactic to see a detailed view of its use.

%% This requires strong induction which we can encode using regular
%% inducution together with an ordering on natural numbers.
%%
%% Adapted from the %reduces example in the Twelf User's Guide:
%% http://www.cs.cmu.edu/~twelf/guide-1-4/twelf_8.html#SEC47

Specification "gcd".

Theorem sub_total_tt : forall X Y,
  {less X Y tt} -> exists Z, {sub Y X Z}.

Theorem sub_total_ff : forall X Y,
  {less X Y ff} -> exists Z, {sub X Y Z}.

Theorem less_total : forall X Y,
  {nat X} -> {nat Y} -> exists B, {bool B} /\ {less X Y B}.

Theorem lt_trans : forall X Y Z,
  {lt X (s Y)} -> {lt Y Z} -> {lt X Z}.

Theorem lt_nat : forall X Y,
  {lt X Y} -> {nat X}.

Theorem lt_x_sx : forall X,
  {nat X} -> {lt X (s X)}.

Theorem lt_s : forall X Y,
  {lt X Y} -> {lt X (s Y)}.

Theorem sub_lt : forall X Y Z,
  {nat X} -> {sub X Y Z} -> {lt Z (s X)}.

Theorem gcd_total_strong : forall A B,
  {nat A} -> {nat B} ->
    (forall X Y, {lt X A} -> {lt Y B} -> exists Z, {nat Z} /\ {gcd X Y Z}).


Theorem gcd_total : forall X Y,
   {nat X} -> {nat Y} -> exists Z, {nat Z} /\ {gcd X Y Z}.