Euclid.v

(** Subtraction-based Euclid: complete baseline and supporting proofs.

    Start the guided walkthrough in L01_Baseline.v. This reference module
    contains the algorithm and every arithmetic lemma used by the lessons.
    Build everything with [python3 check.py] from this folder.
*)

From Corelib Require Import Init.Nat Program.Wf.

Set Guard Checking.
Set Universe Checking.

(* The ordinary structural termination checker rejects this program.
   Fail asserts rejection; it does not admit the definition. *)
Fail Fixpoint euclid_sub_plain (a b : nat) : nat :=
  match a, b with
  | 0, _ => b
  | _, 0 => a
  | S a', S b' =>
      if Nat.leb (S a') (S b')
      then euclid_sub_plain (S a') (S b' - S a')
      else euclid_sub_plain (S a' - S b') (S b')
  end.The command has indeed failed with message:
Cannot guess decreasing argument of fix.

(* Elementary arithmetic support, requiring only Corelib. *)
Module TerminationFacts.

Lemma le_transitive n m p : n <= m -> m <= p -> n <= p.n, m, p: nat
n <= m -> m <= p -> n <= p
Proof.n, m, p: nat
n <= m -> m <= p -> n <= p
  intros Hnm Hmp.n, m, p: nat
Hnm: n <= m
Hmp: m <= p
n <= p induction Hmp.n, m: nat
Hnm: n <= m
n <= m
n, m: nat
Hnm: n <= m
m0: nat
Hmp: m <= m0
IHHmp: n <= m0
n <= S m0
  -n, m: nat
Hnm: n <= m
n <= m exact Hnm.
  -n, m: nat
Hnm: n <= m
m0: nat
Hmp: m <= m0
IHHmp: n <= m0
n <= S m0 apply le_S.n, m: nat
Hnm: n <= m
m0: nat
Hmp: m <= m0
IHHmp: n <= m0
n <= m0 exact IHHmp.
Defined.

Lemma sub_le n m : n - m <= n.n, m: nat
n - m <= n
Proof.n, m: nat
n - m <= n
  revert m.n: nat
forall m : nat, n - m <= n induction n as [|n IH]; intros [|m]; simpl.0 <= 0
m: nat
0 <= 0
n: nat
IH: forall m : nat, n - m <= n
S n <= S n
n: nat
IH: forall m : nat, n - m <= n
m: nat
n - m <= S n
  -0 <= 0 apply le_n.
  -m: nat
0 <= 0 apply le_n.
  -n: nat
IH: forall m : nat, n - m <= n
S n <= S n apply le_n.
  -n: nat
IH: forall m : nat, n - m <= n
m: nat
n - m <= S n apply le_S.n: nat
IH: forall m : nat, n - m <= n
m: nat
n - m <= n apply IH.
Defined.

Lemma add_le_left n m k : n <= m -> k + n <= k + m.n, m, k: nat
n <= m -> k + n <= k + m
Proof.n, m, k: nat
n <= m -> k + n <= k + m
  intro H.n, m, k: nat
H: n <= m
k + n <= k + m induction k as [|k IH]; simpl.n, m: nat
H: n <= m
n <= m
n, m, k: nat
H: n <= m
IH: k + n <= k + m
S (k + n) <= S (k + m)
  -n, m: nat
H: n <= m
n <= m exact H.
  -n, m, k: nat
H: n <= m
IH: k + n <= k + m
S (k + n) <= S (k + m) apply le_n_S.n, m, k: nat
H: n <= m
IH: k + n <= k + m
k + n <= k + m exact IH.
Defined.

Lemma add_le_right n m k : n <= m -> n + k <= m + k.n, m, k: nat
n <= m -> n + k <= m + k
Proof.n, m, k: nat
n <= m -> n + k <= m + k
  intro H.n, m, k: nat
H: n <= m
n + k <= m + k induction H; simpl.n, k: nat
n + k <= n + k
n, k, m: nat
H: n <= m
IHle: n + k <= m + k
n + k <= S (m + k)
  -n, k: nat
n + k <= n + k apply le_n.
  -n, k, m: nat
H: n <= m
IHle: n + k <= m + k
n + k <= S (m + k) apply le_S.n, k, m: nat
H: n <= m
IHle: n + k <= m + k
n + k <= m + k exact IHle.
Defined.

Lemma subtract_right_decreases a b :
  S a + (S b - S a) < S a + S b.a, b: nat
S a + (S b - S a) < S a + S b
Proof.a, b: nat
S a + (S b - S a) < S a + S b
  unfold lt.a, b: nat
S (S a + (S b - S a)) <= S a + S b simpl.a, b: nat
S (S (a + (b - a))) <= S (a + S b) rewrite <- plus_n_Sm.a, b: nat
S (S (a + (b - a))) <= S (S (a + b))
  apply le_n_S, le_n_S, add_le_left, sub_le.
Defined.

Lemma subtract_left_decreases a b :
  (S a - S b) + S b < S a + S b.a, b: nat
S a - S b + S b < S a + S b
Proof.a, b: nat
S a - S b + S b < S a + S b
  unfold lt.a, b: nat
S (S a - S b + S b) <= S a + S b simpl.a, b: nat
S (a - b + S b) <= S (a + S b)
  apply le_n_S, add_le_right, sub_le.
Defined.

Lemma nat_lt_wf : well_founded lt.well_founded lt
Proof.well_founded lt
  assert (bounded : forall n m, m < n -> Acc lt m).forall n m : nat, m < n -> Acc lt m
bounded: forall n m : nat, m < n -> Acc lt m
well_founded lt
  {forall n m : nat, m < n -> Acc lt m intro n.n: nat
forall m : nat, m < n -> Acc lt m induction n as [|n IH]; intros m Hm.m: nat
Hm: m < 0
Acc lt m
n: nat
IH: forall m : nat, m < n -> Acc lt m
m: nat
Hm: m < S n
Acc lt m
    -m: nat
Hm: m < 0
Acc lt m inversion Hm.
    -n: nat
IH: forall m : nat, m < n -> Acc lt m
m: nat
Hm: m < S n
Acc lt m constructor.n: nat
IH: forall m : nat, m < n -> Acc lt m
m: nat
Hm: m < S n
forall y : nat, y < m -> Acc lt y intros k Hk.n: nat
IH: forall m : nat, m < n -> Acc lt m
m: nat
Hm: m < S n
k: nat
Hk: k < m
Acc lt k apply IH.n: nat
IH: forall m : nat, m < n -> Acc lt m
m: nat
Hm: m < S n
k: nat
Hk: k < m
k < n
      unfold lt in *.n: nat
IH: forall m : nat, S m <= n -> Acc (fun n m0 : nat => S n <= m0) m
m: nat
Hm: S m <= S n
k: nat
Hk: S k <= m
S k <= n
      eapply le_transitive; [exact Hk |].n: nat
IH: forall m : nat, S m <= n -> Acc (fun n m0 : nat => S n <= m0) m
m: nat
Hm: S m <= S n
k: nat
Hk: S k <= m
m <= n
      apply le_S_n.n: nat
IH: forall m : nat, S m <= n -> Acc (fun n m0 : nat => S n <= m0) m
m: nat
Hm: S m <= S n
k: nat
Hk: S k <= m
S m <= S n exact Hm.
  }bounded: forall n m : nat, m < n -> Acc lt m
well_founded lt
  intro n.bounded: forall n m : nat, m < n -> Acc lt m
n: nat
Acc lt n apply (bounded (S n) n).bounded: forall n m : nat, m < n -> Acc lt m
n: nat
n < S n apply le_n.
Defined.

End TerminationFacts.

(* The same algorithm, with measure a + b and checked proofs.
   In each positive-input branch, one argument stays unchanged while
   the other decreases. Neither decreases in every branch, but their
   sum does. The recursive calls are unchanged.
*)
#[local] Obligation Tactic := idtac.

Program Fixpoint euclid_sub (a b : nat) {measure (a + b)} : nat :=
  match a, b with
  | 0, _ => b
  | _, 0 => a
  | S a', S b' =>
      if Nat.leb (S a') (S b')
      then euclid_sub (S a') (S b' - S a')
      else euclid_sub (S a' - S b') (S b')
  end.euclid_sub_func has type-checked, generating 4 obligations
Solving obligations automatically...
4 obligations remaining
Obligation 1 of euclid_sub_func:
(forall a b : nat,
 (forall a0 b0 : nat, a0 + b0 < a + b -> nat) ->
 forall a' b' : nat, S a' = a -> S b' = b -> S a' + (S b' - S a') < a + b).
Obligation 2 of euclid_sub_func:
(forall a b : nat,
 (forall a0 b0 : nat, a0 + b0 < a + b -> nat) ->
 forall a' b' : nat, S a' = a -> S b' = b -> S a' - S b' + S b' < a + b).
Obligation 3 of euclid_sub_func:
(forall (a b : nat) (euclid_sub : forall a0 b0 : nat, a0 + b0 < a + b -> nat),
 let program_branch_0 :=
   fun (wildcard' : nat) (_ : 0 = a) (_ : wildcard' = b) => b in
 let program_branch_1 :=
   fun (wildcard' : nat)
     (_ : forall wildcard'0 : nat, ~ (0 = wildcard' /\ wildcard'0 = 0))
     (_ : wildcard' = a) (_ : 0 = b) =>
   a in
 let program_branch_2 :=
   fun (a' b' : nat) (Heq_a : S a' = a) (Heq_b : S b' = b) =>
   if S a' <=? S b'
   then
    euclid_sub (S a') (S b' - S a')
      (euclid_sub_func_obligation_1 a b euclid_sub a' b' Heq_a Heq_b)
   else
    euclid_sub (S a' - S b') (S b')
      (euclid_sub_func_obligation_2 a b euclid_sub a' b' Heq_a Heq_b)
   in
 forall n : nat,
 let wildcard' := S n in
 forall wildcard'0 : nat, ~ (0 = wildcard' /\ wildcard'0 = 0)).
Obligation 4 of euclid_sub_func:
(well_founded
   (MR lt
      (fun recarg : {_ : nat & nat} =>
       let a := projT1 recarg in let b := projT2 recarg in a + b))).


Next Obligation.forall a b : nat,
(forall a0 b0 : nat, a0 + b0 < a + b -> nat) ->
forall a' b' : nat, S a' = a -> S b' = b -> S a' + (S b' - S a') < a + b
  intros a b recurse a' b' Ha Hb.a, b: nat
recurse: forall a0 b0 : nat, a0 + b0 < a + b -> nat
a', b': nat
Ha: S a' = a
Hb: S b' = b
S a' + (S b' - S a') < a + b subst a b.a', b': nat
recurse: forall a b : nat, a + b < S a' + S b' -> nat
S a' + (S b' - S a') < S a' + S b'
  apply TerminationFacts.subtract_right_decreases.
Defined.3 obligations remaining
Solving obligations automatically...
3 obligations remaining

Next Obligation.forall a b : nat,
(forall a0 b0 : nat, a0 + b0 < a + b -> nat) ->
forall a' b' : nat, S a' = a -> S b' = b -> S a' - S b' + S b' < a + b
  intros a b recurse a' b' Ha Hb.a, b: nat
recurse: forall a0 b0 : nat, a0 + b0 < a + b -> nat
a', b': nat
Ha: S a' = a
Hb: S b' = b
S a' - S b' + S b' < a + b subst a b.a', b': nat
recurse: forall a b : nat, a + b < S a' + S b' -> nat
S a' - S b' + S b' < S a' + S b'
  apply TerminationFacts.subtract_left_decreases.
Defined.2 obligations remaining
Solving obligations automatically...
2 obligations remaining

Next Obligation.forall (a b : nat) (euclid_sub : forall a0 b0 : nat, a0 + b0 < a + b -> nat),
let program_branch_0 :=
  fun (wildcard' : nat) (_ : 0 = a) (_ : wildcard' = b) => b in
let program_branch_1 :=
  fun (wildcard' : nat)
    (_ : forall wildcard'0 : nat, ~ (0 = wildcard' /\ wildcard'0 = 0))
    (_ : wildcard' = a) (_ : 0 = b) =>
  a in
let program_branch_2 :=
  fun (a' b' : nat) (Heq_a : S a' = a) (Heq_b : S b' = b) =>
  if S a' <=? S b'
  then
   euclid_sub (S a') (S b' - S a')
     ((fun (a0 b0 : nat)
         (recurse : forall a1 b1 : nat, a1 + b1 < a0 + b0 -> nat)
         (a'0 b'0 : nat) (Ha : S a'0 = a0) (Hb : S b'0 = b0) =>
       euclid_sub_func_obligation_1 a0 b0 recurse a'0 b'0 Ha Hb) a b
        euclid_sub a' b' Heq_a Heq_b)
  else
   euclid_sub (S a' - S b') (S b')
     ((fun (a0 b0 : nat)
         (recurse : forall a1 b1 : nat, a1 + b1 < a0 + b0 -> nat)
         (a'0 b'0 : nat) (Ha : S a'0 = a0) (Hb : S b'0 = b0) =>
       euclid_sub_func_obligation_2 a0 b0 recurse a'0 b'0 Ha Hb) a b
        euclid_sub a' b' Heq_a Heq_b)
  in
forall n : nat,
let wildcard' := S n in
forall wildcard'0 : nat, ~ (0 = wildcard' /\ wildcard'0 = 0)
  (* Pattern matching bookkeeping: zero is not a successor. *)
  intros; intuition discriminate.
Defined.1 obligation remaining

Next Obligation.well_founded
  (MR lt
     (fun recarg : {_ : nat & nat} =>
      let a := projT1 recarg in let b := projT2 recarg in a + b))
  (* There is no infinite descending chain of natural-number measures. *)
  apply measure_wf.well_founded lt exact TerminationFacts.nat_lt_wf.
Defined.No more obligations remaining

(* The accepted definition computes and has no axioms. *)
Compute (euclid_sub 48 18).= 6
: nat
Compute (euclid_sub 18 48).= 6
: nat
Compute (euclid_sub 0 5).= 5
: nat
Compute (euclid_sub 5 0).= 5
: nat

Print Assumptions euclid_sub.Fetching opaque proofs from disk for Corelib.Init.Peano
Closed under the global context