(** Lesson 4 -- What was actually installed? (About 20 minutes.)

    Read after L03_Accessibility.v. This closes the Phase 2 walkthrough.
    Source paths below are relative to the Rocq checkout; README.md has
    the source map with line references and the recorded commit.
*)

From Corelib Require Import Init.Nat Program.Wf.
From TerminationStudy Require Import L02_Obligations L03_Accessibility.

Set Guard Checking.
Set Universe Checking.

(** The public wrapper only packs arguments for the generated function.
    This is a checked equality for arbitrary inputs, by conversion. *)
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
Example wrapper_is_generated_function (a b : nat) :
  euclid_trace a b = euclid_trace_func (pack a b).
a, b: nat
euclid_trace a b = euclid_trace_func (pack a b)
Proof.
a, b: nat
euclid_trace a b = euclid_trace_func (pack a b) reflexivity. Qed.

(** Inspect the artifact and its evidence. In [euclid_trace_func], find
    the application of [Fix_sub], the reference to obligation 4, and
    the two calls carrying obligations 1 and 2. Obligation 3 belongs
    to the elaborated match. The full output stays in this lesson's log. *)
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))
  L02_Obligations.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) =>
          L02_Obligations.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) =>
          L02_Obligations.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) =>
               L02_Obligations.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
(* Generated obligations require qualification after importing a module. *)
Check L02_Obligations.euclid_trace_func_obligation_1.
L02_Obligations.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
Check L02_Obligations.euclid_trace_func_obligation_2.
L02_Obligations.euclid_trace_func_obligation_2
     : 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
Check L02_Obligations.euclid_trace_func_obligation_3.
L02_Obligations.euclid_trace_func_obligation_3
     : forall n : nat,
       let wildcard' := S n in
       forall wildcard'0 : nat, ~ (0 = wildcard' /\ wildcard'0 = 0)
Check L02_Obligations.euclid_trace_func_obligation_4.
L02_Obligations.euclid_trace_func_obligation_4
     : well_founded
         (MR lt
            (fun recarg : {_ : nat & nat} =>
             let a := projT1 recarg in let b := projT2 recarg in a + b))

Example installed_examples :
  euclid_trace 48 18 = 6 /\ euclid_trace 18 48 = 6 /\
  euclid_trace 0 5 = 5 /\ euclid_trace 5 0 = 5.
euclid_trace 48 18 = 6 /\
euclid_trace 18 48 = 6 /\ euclid_trace 0 5 = 5 /\ euclid_trace 5 0 = 5
Proof.
euclid_trace 48 18 = 6 /\
euclid_trace 18 48 = 6 /\ euclid_trace 0 5 = 5 /\ euclid_trace 5 0 = 5 repeat split; reflexivity. Qed.

Print Assumptions euclid_trace.
Fetching opaque proofs from disk for Corelib.Init.Peano
Closed under the global context
Print Assumptions euclid_trace_func.
Closed under the global context
Print Assumptions L02_Obligations.euclid_trace_func_obligation_1.
Closed under the global context
Print Assumptions L02_Obligations.euclid_trace_func_obligation_4.
Closed under the global context
Print Assumptions wrapper_is_generated_function.
Closed under the global context
Print Assumptions installed_examples.
Closed under the global context

(** Follow one call, end to end:

    source: euclid_trace (S a') (S b' - S a')
      -> a recursive-function argument with an extra decrease proof
      -> [exist] carrying [existT ...] and obligation 1's proof
      -> [Fix_sub] invokes [Fix_F_sub] with obligation 4's [Acc] proof
      -> [Acc_inv] uses that call's proof to select a child [Acc] proof
      -> [Fix_F_sub] recurses structurally on this child proof.

    The generated Euclid body is an ordinary term applying an existing
    recursor. [Fix_F_sub]'s recursive body was checked when Corelib was
    built; declaring Euclid does not reinstall that library definition.

    Implementation trail at commit
    67ab16a375d31812dc1dd788f92d446d7d6dcd45:

    - vernac/comFixpoint.ml: [encapsulate_Fix_sub], [build_wellfounded]
      build the relation, proof holes, recursor application, and wrapper.
    - vernac/declare.ml: [prepare_obligations], [declare_obligation],
      [obligation_substitution], [update_obls], [declare_definition]
      connect solved evidence to the proposed term and complete it.
    - vernac/declare.ml: [declare_constant] calls [Global.add_constant].
    - kernel/safe_typing.ml: [add_constant] checks a definition before
      adding its constant body to the environment.
    - kernel/typeops.ml: the [Fix] case calls [Inductive.check_fix];
      kernel/inductive.ml implements the guard check.

    Thus the proof-producing elaborator and tactics may change while
    their output remains subject to the existing kernel's checks.
    This observation does not justify changing the kernel or its rules.

    In the study's vocabulary:
    substrate = the existing core theory and environment;
    proposer = source author plus elaboration/proof-producing tools;
    evidence = the typed decrease and well-foundedness proof terms;
    gate = kernel checking of the resulting declarations, with guards
           and universe checking enabled;
    admission policy = add definitions accepted under those core rules;
    reflective depth = construct terms in the existing theory.

    We have not added native reduction rules. We have not proved a
    general guarantee about all future admission histories. Changing
    conversion or the gate itself requires a different argument.
*)

(** Stop for discussion here, as requested in study_plan.md.

    Explain the trace using [right_call] and [Fix_F_sub], then ask:
    what evidence must remain transparent for this function to compute?
    That is an open experimental question for Phase 3.

    Later checkpoints are planned in README.md: controlled changes,
    the scope of the admission discipline, then native rewrite rules.
    This import shows how we use the saved lesson; it is not a claim
    that normal [Require Import] independently rechecks every proof.
*)