L02_Obligations.v

(** Lesson 2 -- Watch a definition become available. (About 30 minutes.)

    Read after L01_Baseline.v. This is the same Euclid algorithm and
    measure, with a fresh name and inspection commands inserted.
    Arithmetic evidence is defined in Euclid.v. This begins Phase 2.
*)

From Corelib Require Import Init.Nat Program.Wf.
From TerminationStudy Require Import Euclid.

Set Guard Checking.
Set Universe Checking.

(** Pause automatic proof search so every obligation stays visible. *)
#[local] Obligation Tactic := idtac.

Program Fixpoint euclid_trace (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_trace (S a') (S b' - S a')
      else euclid_trace (S a' - S b') (S b')
  end.euclid_trace_func has type-checked, generating 4 obligations
Solving obligations automatically...
4 obligations remaining
Obligation 1 of euclid_trace_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_trace_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_trace_func:
(forall (a b : nat)
   (euclid_trace : 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_trace (S a') (S b' - S a')
      (euclid_trace_func_obligation_1 a b euclid_trace a' b' Heq_a Heq_b)
   else
    euclid_trace (S a' - S b') (S b')
      (euclid_trace_func_obligation_2 a b euclid_trace 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_trace_func:
(well_founded
   (MR lt
      (fun recarg : {_ : nat & nat} =>
       let a := projT1 recarg in let b := projT2 recarg in a + b))).


(** Before solving anything, inspect the four pending propositions and
    the proposed term. The name with [_func] is Program's internal
    function on a packed pair of arguments. Search the Preterm output
    for [Fix_sub], [existT], [exist], and [_obligation_1].

    These commands inspect Program's pending state; they do not install
    an incomplete function in the global environment. *)
Obligations of euclid_trace_func.4 obligation(s) remaining: 
Obligation 1 of euclid_trace_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_trace_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_trace_func:
(forall (a b : nat)
   (euclid_trace : 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_trace (S a') (S b' - S a')
      (euclid_trace_func_obligation_1 a b euclid_trace a' b' Heq_a Heq_b)
   else
    euclid_trace (S a' - S b') (S b')
      (euclid_trace_func_obligation_2 a b euclid_trace 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_trace_func:
(well_founded
   (MR lt
      (fun recarg : {_ : nat & nat} =>
       let a := projT1 recarg in let b := projT2 recarg in a + b))).

Preterm of euclid_trace_func.euclid_trace_func :
(forall recarg : {_ : nat & nat},
 let a := projT1 recarg in let b := projT2 recarg in nat)
:=
(Fix_sub {_ : nat & nat}
   (MR lt
      (fun recarg : {_ : nat & nat} =>
       let a := projT1 recarg in let b := projT2 recarg in a + b))
   euclid_trace_func_obligation_4
   (fun recarg : {_ : nat & nat} =>
    let a := projT1 recarg in let b := projT2 recarg in nat)
   (fun (recarg : {_ : nat & nat})
      (euclid_trace' : forall
                         recarg' : {recarg' : {_ : nat & nat}
                                   | (let a := projT1 recarg' in
                                      let b := projT2 recarg' in a + b) <
                                     (let a := projT1 recarg in
                                      let b := projT2 recarg in a + b)},
                       let a := projT1 (proj1_sig recarg') in
                       let b := projT2 (proj1_sig recarg') in nat) =>
    let a := projT1 recarg in
    let b := projT2 recarg in
    let euclid_trace :=
      fun (a0 b0 : nat) (recproof : a0 + b0 < a + b) =>
      euclid_trace'
        (exist
           (fun recarg' : {_ : nat & nat} =>
            (let a1 := projT1 recarg' in let b1 := projT2 recarg' in a1 + b1) <
            (let a1 := projT1 recarg in let b1 := projT2 recarg in a1 + b1))
           (existT (fun _ : nat => nat) a0 b0) recproof)
      in
    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_trace (S a') (S b' - S a')
         (euclid_trace_func_obligation_1 a b euclid_trace a' b' Heq_a Heq_b)
      else
       euclid_trace (S a' - S b') (S b')
         (euclid_trace_func_obligation_2 a b euclid_trace a' b' Heq_a Heq_b)
      in
    match a as a' return a' = a -> b = b -> nat with
    | 0 => program_branch_0 b
    | S a' =>
        match b as b' return S a' = a -> b' = b -> nat with
        | 0 =>
            program_branch_1 (S a')
              (euclid_trace_func_obligation_3 a b euclid_trace a')
        | S b' => program_branch_2 a' b'
        end
    end eq_refl eq_refl))
Fail Check euclid_trace.The command has indeed failed with message:
The reference euclid_trace was not found in the current environment.
Fail Check euclid_trace_func.The command has indeed failed with message:
The reference euclid_trace_func was not found in the current environment.
Did you mean euclid_sub_func?

(** Follow the [then] call. Its local recursive function now takes an
    extra proof that the new sum is smaller than the CURRENT sum.
    Match equalities identify the current [a,b] with [S a',S b'].
    Execute [Show] before and after [subst] and read the change. *)
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
  Show.1 goal

  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
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'
  Show.1 goal

  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'
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

(** One evidence constant is now installed, but the function is not. *)
Check euclid_trace_func_obligation_1.euclid_trace_func_obligation_1
     : 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
Print euclid_trace_func_obligation_1.euclid_trace_func_obligation_1 =
fun (a b : nat) (recurse : forall a0 b0 : nat, a0 + b0 < a + b -> nat)
  (a' b' : nat) (Ha : S a' = a) (Hb : S b' = b) =>
eq_ind (S a')
  (fun a0 : nat =>
   (forall a1 b0 : nat, a1 + b0 < a0 + b -> nat) ->
   S a' + (S b' - S a') < a0 + b)
  (fun recurse0 : forall a0 b0 : nat, a0 + b0 < S a' + b -> nat =>
   eq_ind (S b')
     (fun b0 : nat =>
      (forall a0 b1 : nat, a0 + b1 < S a' + b0 -> nat) ->
      S a' + (S b' - S a') < S a' + b0)
     (fun _ : forall a0 b0 : nat, a0 + b0 < S a' + S b' -> nat =>
      TerminationFacts.subtract_right_decreases a' b')
     b Hb recurse0)
  a Ha recurse
     : 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

Arguments euclid_trace_func_obligation_1 (a b)%_nat_scope
  recurse%_function_scope (a' b')%_nat_scope Ha Hb
Fail Check euclid_trace.The command has indeed failed with message:
The reference euclid_trace was not found in the current environment.
Obligations of euclid_trace_func.3 obligation(s) remaining: 
Obligation 2 of euclid_trace_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_trace_func:
(forall (a b : nat)
   (euclid_trace : 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_trace (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_trace_func_obligation_1 a0 b0 recurse a'0 b'0 Ha Hb) a b
         euclid_trace a' b' Heq_a Heq_b)
   else
    euclid_trace (S a' - S b') (S b')
      (euclid_trace_func_obligation_2 a b euclid_trace 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_trace_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 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

(** This third goal is match bookkeeping, not another recursive call. *)
Next Obligation.forall (a b : nat)
  (euclid_trace : 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_trace (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_trace_func_obligation_1 a0 b0 recurse a'0 b'0 Ha Hb) a b
        euclid_trace a' b' Heq_a Heq_b)
  else
   euclid_trace (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_trace_func_obligation_2 a0 b0 recurse a'0 b'0 Ha Hb) a b
        euclid_trace a' b' Heq_a Heq_b)
  in
forall n : nat,
let wildcard' := S n in
forall wildcard'0 : nat, ~ (0 = wildcard' /\ wildcard'0 = 0)
  Show.1 goal

  ============================
  forall (a b : nat)
    (euclid_trace : 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_trace (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_trace_func_obligation_1 a0 b0 recurse a'0 b'0 Ha Hb) a b
          euclid_trace a' b' Heq_a Heq_b)
    else
     euclid_trace (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_trace_func_obligation_2 a0 b0 recurse a'0 b'0 Ha Hb) a b
          euclid_trace a' b' Heq_a Heq_b)
    in
  forall n : nat,
  let wildcard' := S n in
  forall wildcard'0 : nat, ~ (0 = wildcard' /\ wildcard'0 = 0)
forall (a b : nat)
  (euclid_trace : 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_trace (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_trace_func_obligation_1 a0 b0 recurse a'0 b'0 Ha Hb) a b
        euclid_trace a' b' Heq_a Heq_b)
  else
   euclid_trace (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_trace_func_obligation_2 a0 b0 recurse a'0 b'0 Ha Hb) a b
        euclid_trace a' b' Heq_a Heq_b)
  in
forall n : nat,
let wildcard' := S n in
forall wildcard'0 : nat, ~ (0 = wildcard' /\ wildcard'0 = 0)
  intros; intuition discriminate.
Defined.1 obligation remaining

(** Both decreases are proved, but the relation still needs a proof of
    well-foundedness. The public function remains unavailable. *)
Fail Check euclid_trace.The command has indeed failed with message:
The reference euclid_trace was not found in the current environment.
Fail Check euclid_trace_func.The command has indeed failed with message:
The reference euclid_trace_func was not found in the current environment.
Did you mean euclid_sub_func?
Obligations of euclid_trace_func.1 obligation(s) remaining: 
Obligation 4 of euclid_trace_func:
(well_founded
   (MR lt
      (fun recarg : {_ : nat & nat} =>
       let a := projT1 recarg in let b := projT2 recarg in a + b))).

Preterm of euclid_trace_func.euclid_trace_func :
(forall recarg : {_ : nat & nat},
 let a := projT1 recarg in let b := projT2 recarg in nat)
:=
(Fix_sub {_ : nat & nat}
   (MR lt
      (fun recarg : {_ : nat & nat} =>
       let a := projT1 recarg in let b := projT2 recarg in a + b))
   euclid_trace_func_obligation_4
   (fun recarg : {_ : nat & nat} =>
    let a := projT1 recarg in let b := projT2 recarg in nat)
   (fun (recarg : {_ : nat & nat})
      (euclid_trace' : forall
                         recarg' : {recarg' : {_ : nat & nat}
                                   | (let a := projT1 recarg' in
                                      let b := projT2 recarg' in a + b) <
                                     (let a := projT1 recarg in
                                      let b := projT2 recarg in a + b)},
                       let a := projT1 (proj1_sig recarg') in
                       let b := projT2 (proj1_sig recarg') in nat) =>
    let a := projT1 recarg in
    let b := projT2 recarg in
    let euclid_trace :=
      fun (a0 b0 : nat) (recproof : a0 + b0 < a + b) =>
      euclid_trace'
        (exist
           (fun recarg' : {_ : nat & nat} =>
            (let a1 := projT1 recarg' in let b1 := projT2 recarg' in a1 + b1) <
            (let a1 := projT1 recarg in let b1 := projT2 recarg in a1 + b1))
           (existT (fun _ : nat => nat) a0 b0) recproof)
      in
    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_trace (S a') (S b' - S a')
         (euclid_trace_func_obligation_1 a b euclid_trace a' b' Heq_a Heq_b)
      else
       euclid_trace (S a' - S b') (S b')
         (euclid_trace_func_obligation_2 a b euclid_trace a' b' Heq_a Heq_b)
      in
    match a as a' return a' = a -> b = b -> nat with
    | 0 => program_branch_0 b
    | S a' =>
        match b as b' return S a' = a -> b' = b -> nat with
        | 0 =>
            program_branch_1 (S a')
              (euclid_trace_func_obligation_3 a b euclid_trace a')
        | S b' => program_branch_2 a' b'
        end
    end eq_refl eq_refl))

Next Obligation.well_founded
  (MR lt
     (fun recarg : {_ : nat & nat} =>
      let a := projT1 recarg in let b := projT2 recarg in a + b))
  Show.1 goal

  ============================
  well_founded
    (MR lt
       (fun recarg : {_ : nat & nat} =>
        let a := projT1 recarg in let b := projT2 recarg in a + b))
well_founded
  (MR lt
     (fun recarg : {_ : nat & nat} =>
      let a := projT1 recarg in let b := projT2 recarg in a + b))
  apply measure_wf.well_founded lt exact TerminationFacts.nat_lt_wf.
Defined.No more obligations remaining

(** Crossing this last [Defined] completes the definition and its
    two-argument wrapper. No extra admission command is needed. *)
Check euclid_trace_func.euclid_trace_func
     : forall recarg : {_ : nat & nat},
       let a := projT1 recarg in let b := projT2 recarg in nat
Check euclid_trace.euclid_trace
     : nat -> nat -> nat
Print euclid_trace.euclid_trace =
fun a b : nat => euclid_trace_func (existT (fun _ : nat => nat) a b)
     : nat -> nat -> nat

Arguments euclid_trace (a b)%_nat_scope
Print euclid_trace_func.euclid_trace_func =
Fix_sub {_ : nat & nat}
  (MR lt
     (fun recarg : {_ : nat & nat} =>
      let a := projT1 recarg in let b := projT2 recarg in a + b))
  euclid_trace_func_obligation_4
  (fun recarg : {_ : nat & nat} =>
   let a := projT1 recarg in let b := projT2 recarg in nat)
  (fun (recarg : {_ : nat & nat})
     (euclid_trace' : forall
                        recarg' : {recarg' : {_ : nat & nat}
                                  | (let a := projT1 recarg' in
                                     let b := projT2 recarg' in a + b) <
                                    (let a := projT1 recarg in
                                     let b := projT2 recarg in a + b)},
                      let a := projT1 (proj1_sig recarg') in
                      let b := projT2 (proj1_sig recarg') in nat) =>
   let a := projT1 recarg in
   let b := projT2 recarg in
   let euclid_trace :=
     fun (a0 b0 : nat) (recproof : a0 + b0 < a + b) =>
     euclid_trace'
       (exist
          (fun recarg' : {_ : nat & nat} =>
           (let a1 := projT1 recarg' in let b1 := projT2 recarg' in a1 + b1) <
           (let a1 := projT1 recarg in let b1 := projT2 recarg in a1 + b1))
          (existT (fun _ : nat => nat) a0 b0) recproof)
     in
   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_trace (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_trace_func_obligation_1 a0 b0 recurse a'0 b'0 Ha Hb) a b
           euclid_trace a' b' Heq_a Heq_b)
     else
      euclid_trace (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_trace_func_obligation_2 a0 b0 recurse a'0 b'0 Ha Hb) a b
           euclid_trace a' b' Heq_a Heq_b)
     in
   match a as a' return a' = a -> b = b -> nat with
   | 0 => program_branch_0 b
   | S a' =>
       match b as b' return S a' = a -> b' = b -> nat with
       | 0 =>
           program_branch_1 (S a')
             ((fun (a0 b0 : nat)
                 (_ : forall a1 b1 : nat, a1 + b1 < a0 + b0 -> nat)
                 (n wildcard' : nat) =>
               euclid_trace_func_obligation_3 n wildcard') a b euclid_trace
                a')
       | S b' => program_branch_2 a' b'
       end
   end eq_refl eq_refl)
     : forall recarg : {_ : nat & nat},
       let a := projT1 recarg in let b := projT2 recarg in nat

Arguments euclid_trace_func recarg
Print euclid_trace_func_obligation_2.euclid_trace_func_obligation_2 =
fun (a b : nat) (recurse : forall a0 b0 : nat, a0 + b0 < a + b -> nat)
  (a' b' : nat) (Ha : S a' = a) (Hb : S b' = b) =>
eq_ind (S a')
  (fun a0 : nat =>
   (forall a1 b0 : nat, a1 + b0 < a0 + b -> nat) ->
   S a' - S b' + S b' < a0 + b)
  (fun recurse0 : forall a0 b0 : nat, a0 + b0 < S a' + b -> nat =>
   eq_ind (S b')
     (fun b0 : nat =>
      (forall a0 b1 : nat, a0 + b1 < S a' + b0 -> nat) ->
      S a' - S b' + S b' < S a' + b0)
     (fun _ : forall a0 b0 : nat, a0 + b0 < S a' + S b' -> nat =>
      TerminationFacts.subtract_left_decreases a' b')
     b Hb recurse0)
  a Ha recurse
     : 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

Arguments euclid_trace_func_obligation_2 (a b)%_nat_scope
  recurse%_function_scope (a' b')%_nat_scope Ha Hb
Print euclid_trace_func_obligation_3.euclid_trace_func_obligation_3 =
fun n : nat =>
let wildcard' := S n in
fun (wildcard'0 : nat) (H : 0 = wildcard' /\ wildcard'0 = 0) =>
and_ind
  (fun (H0 : 0 = wildcard') (_ : wildcard'0 = 0) =>
   let H1 : False :=
     eq_ind 0 (fun e : nat => match e with
                              | 0 => True
                              | S _ => False
                              end)
       I wildcard' H0
     in
   False_ind False H1)
  H
     : forall n : nat,
       let wildcard' := S n in
       forall wildcard'0 : nat, ~ (0 = wildcard' /\ wildcard'0 = 0)

Arguments euclid_trace_func_obligation_3 (n wildcard')%_nat_scope _
Print euclid_trace_func_obligation_4.euclid_trace_func_obligation_4 =
measure_wf TerminationFacts.nat_lt_wf
  (fun recarg : {_ : nat & nat} =>
   let a := projT1 recarg in let b := projT2 recarg in a + b)
     : well_founded
         (MR lt
            (fun recarg : {_ : nat & nat} =>
             let a := projT1 recarg in let b := projT2 recarg in a + b))

Arguments euclid_trace_func_obligation_4 a

Compute (euclid_trace 18 48).= 6
: nat
Example traced_result : euclid_trace 18 48 = 6.euclid_trace 18 48 = 6
Proof.euclid_trace 18 48 = 6 reflexivity. Qed.
Print Assumptions euclid_trace.Fetching opaque proofs from disk for Corelib.Init.Peano
Closed under the global context

(** Checkpoint:

    - Point to the proof argument attached to the [then] call in Preterm.
    - Classify the four obligations: two decreases, one match condition,
      one well-foundedness proof.
    - At which command does [Check euclid_trace] first succeed?

    The four propositions constrain THIS proposed term. The proofs are
    referenced or substituted into its holes, not filed beside unrelated
    source text. We inspect the final connection again in Lesson 4.

    Next: L03_Accessibility.v -- what core recursion does Fix_sub use?
*)