-title: GearsAgda

-- files

    whileTestGears.agda          Gears form of proof

-- Continuation form makes Hoare logic simple

Write a program in Gears form, which is a lightweight continuation style.

   code : {t : Set} -> (next : t -> t ) -> t

-- Gears version of a program

    record Env  : Set where
      field
        varn : ℕ
        vari : ℕ
    open Env

    {-# TERMINATING #-}
    whileLoop : {l : Level} {t : Set l} → Env → (Code : Env → t) → t
    whileLoop env next with lt 0 (varn env)
    whileLoop env next | false = next env
    whileLoop env next | true =
        whileLoop (record {varn = (varn env) - 1 ; vari = (vari env) + 1}) next

We need TERMINATING, because Agda does not understand the termination.

-- A Segmented code gear with a condition

    whileLoopSeg : {l : Level} {t : Set l} → {c10 :  ℕ } → (env : Env) → ((varn env) + (vari env) ≡ c10)
       → (next : (e1 : Env )→ varn e1 + vari e1 ≡ c10 → varn e1 < varn env → t)     -- next with PostCondition
       → (exit : (e1 : Env )→ vari e1 ≡ c10 → t) → t

It includes a reduction sequence "varn e1 < varn env → t)".

The invariant is directly described in the program, we don't need sytax tree of a code nor a code with conditions.

-- Specification

    whileTestSpec1 : (c10 : ℕ) →  (e1 : Env ) → vari e1 ≡ c10 → ⊤
    whileTestSpec1 _ _ x = tt

This is the condition to be proved.

-- while loop in GearsAgda

    TerminatingLoopS : {l : Level} {t : Set l} (Index : Set ) → {Invraiant : Index → Set } → ( reduce : Index → ℕ)
       → (loop : (r : Index)  → Invraiant r → (next : (r1 : Index)  → Invraiant r1 → reduce r1 < reduce r  → t ) → t)
       → (r : Index) → (p : Invraiant r)  → t 

TerminatingLoopS defines a loop connective, which define the loop and it also gives a correctness of exit condition.

    whileTest' : {l : Level} {t : Set l}  → {c10 :  ℕ } → (Code : (env : Env)  → ((vari env) ≡ 0) /\ ((varn env) ≡ c10) → t) → t

    conversion1 : {l : Level} {t : Set l } → (env : Env) → {c10 :  ℕ } → ((vari env) ≡ 0) /\ ((varn env) ≡ c10)
                   → (Code : (env1 : Env) → (varn env1 + vari env1 ≡ c10) → t) → t

    proofGearsTermS : {c10 :  ℕ } → ⊤
    proofGearsTermS {c10} = whileTest' {_} {_}  {c10} (λ n p →  conversion1 n p (λ n1 p1 →
        TerminatingLoopS Env (λ env → varn env)
            (λ n2 p2 loop → whileLoopSeg {_} {_} {c10} n2 p2 loop (λ ne pe → whileTestSpec1 c10 ne pe)) n1 p1 )) 

This a proof, because it is a value not a type. whileTestSpec get a proof of specification.