Emulate structural recursion with Bound type

Consider the following proof:

    // ∀ n . n < n+1
    !less_than_succ*N : !{case n : Nat} -> Less(n, succ(n))
    | succ => less_succ(~n.pred, ~succ(n.pred), less_than_succ(n.pred))
    | zero => less_zero(~zero)
    * ?

As is, it can't be completed since, on the halt-case, we'll need to
prove `Less(n, succ(n))`, which we can't, since that's what we're trying
to prove. In other words, the fact Formality recursive functions need a
halt case makes that proof impossible.

We could try, for example, returning `Maybe(Less(n, succ(n)))`. That'd
be useful in the sense that "if we call the function and it doesn't
return nothing, then our theorem holds". But the fact the function can
always return `nothing` anytime invalidates it as a proof in the
mathematical sense:

    // ∀ n . n < n+1
    !less_than_succ*N : !{case n : Nat} -> Maybe(Less(n, succ(n)))
    | succ => nothing
    | zero => nothing
    * nothing

Similarly, we could, in some clever way, return a proof that either
`Less(n, succ(n))`, or that the function ran out of gas". But that still
accomplishes nothing, since we could just force the function to run out
of gas:

    // ∀ n . n < n+1
    !less_than_succ*N : !{case n : Nat} -> TrueIfHalted(N, Less(n, succ(n)))
    | succ => less_than_succ(zero)
    | zero => less_than_succ(zero)
    * did_not_halt

In order to solve it in a way that preserves the mathematical meaning of
the proof, my idea is to emulate Agda/Coq's structural recursion with a
`Bound` type. That type compares the size of the input (here, a `Nat`)
with the amount of recursion calls we have left; i.e., our "fuel";,
asserting that we always "have enough fuel" to consume the whole input.
The proof then goes like ths:

    T Bound (n : Nat, i : Ind)
    | bound_succ {~n : Nat, ~i : Ind, k : Bound(n, i)} (succ(n), step(i))
    | bound_zero {~i : Ind}                            (zero   , step(i))

    // ∀ n . n < n+1
    !less_than_succ*N : !{n : Nat, bound : Bound(n, N)} -> Less(n, succ(n))
      (case/Bound bound
      | bound_succ => {e}
        let r0 = cong_unstep(~i, ~N, ~e)
        let r1 = less_than_succ(n, k :: rewrite x in Bound(n, x) with r0)
        let r2 = less_succ(~n, ~succ(n), r1)
        r2
      | bound_zero => {e}
        less_zero(~zero)
      : {e : i == step(N)} -> Less(n, succ(n)))(refl(~step(N)))
      * absurd(absurd_bound(n, bound), ~Less(n, succ(n)))

The insight is that, instead of matching on `n` directly, we match on
`bound`, which will give us not only the predecessor of `n`, `n - 1`,
but also the predecessor of the call count, `N - 1`, together with a
proof that it is still larger the number.  We can then use this new
proof to recurse on `n`'s predecessor. That guarantees that `n` not only
always gets smaller, but that it will reach `zero` before our "call
count" reaches its limit, essentially emulating Agda's bounded
recursion. This Bound only works for Nats, but should generalize.

Note: this proof is noisy since it requires us to convince the
type-checker that the `N` inside the bound field is the same as the `N`
from the function input, which, in turn, required me to prove a bunch of
`Ind` theorems. Agda has a built-in syntax that gives you this equality
for free, I believe. Should we too?

Author: VictorTaelin

Data.Empty.fm

@@ -2,7 +2,7 @@
 T Empty
 
 // From falsehood, everything follows
-absurd : {e : Empty, P : Type} -> P
+absurd : {e : Empty, ~P : Type} -> P
   case/Empty e
   : P
 

Data.Less.fm

@@ -0,0 +1,38 @@
+import Data.Empty open
+import Data.Nat open
+import Data.Unit open
+import Induction.Nat open
+import Induction.Nat.Unstep open
+
+// a < b
+T Less (a : Nat, b : Nat)
+| less_succ {~a : Nat, ~b : Nat, l : Less(a, b)} (succ(a), succ(b))  // ∀a b. a < b -> a+1 < b+1
+| less_zero {~b : Nat}                           (zero   , succ(b))  // ∀b  . 0 < b+1
+
+// `2 < 4`
+less.example : Less(0n2, 0n4)
+  less_succ(~0n1, ~0n3,
+  less_succ(~0n0, ~0n2,
+  less_zero(~0n1)))
+
+T Bound (n : Nat, i : Ind)
+| bound_succ {~n : Nat, ~i : Ind, k : Bound(n, i)} (succ(n), step(i))
+| bound_zero {~i : Ind}                            (zero   , step(i))
+
+absurd_bound : {n : Nat, bound : Bound(n, base)} -> Empty
+  case/Bound bound
+  | bound_succ => unit
+  | bound_zero => unit
+  : <ind(i, ~{i}Type, #{~r,i}Unit, #Empty)>
+
+// ∀ n . n < n+1
+!less_than_succ*N : !{n : Nat, bound : Bound(n, N)} -> Less(n, succ(n))
+  (case/Bound bound
+  | bound_succ => {e}
+    let r0 = cong_unstep(~i, ~N, ~e)
+    let r1 = less_than_succ(n, k :: rewrite x in Bound(n, x) with r0)
+    let r2 = less_succ(~n, ~succ(n), r1)
+    r2
+  | bound_zero => {e} less_zero(~zero)
+  : {e : i == step(N)} -> Less(n, succ(n)))(refl(~step(N)))
+  * absurd(absurd_bound(n, bound), ~Less(n, succ(n)))

Data.LessThan.fm

@@ -0,0 +1,34 @@
+import Induction.Nat open
+import Data.Bool open
+import Relation.Equality open
+
+unstep : {n : Ind} -> Ind
+  new(~Ind) {~P, S}
+  dup S = S
+  let motive = {n} {b : Bool} ->
+    (%b)(~{b}Type, P(unstep(n)), P(unstep(step(n))))
+  let case_s = {~n, h, b}
+    let motive = {b} {h : P(unstep(step(n)))} -> (%b)(~{b}Type, P(unstep(step(n))), P(step(unstep(step(n)))))
+    let case_t = {x} x
+    let case_f = S(~(unstep(step(n))))
+    (%b)(~motive, case_t, case_f, h(false))
+  dup F = (%n)(~motive, #case_s)
+  # {Z}
+  let case_z = {b}
+    let motive = {b} {n : P(base)} -> (%b)(~{b}Type, P(unstep(base)), P(unstep(step(base))))
+    let case_t = {z} z
+    let case_f = {z} z
+    (%b)(~motive, case_t, case_f, Z)
+  F(case_z, true)
+
+unstep_step : {i : Ind} -> !unstep(step(i)) == i
+  let motive = {i} unstep(step(i)) == i
+  let case_s = # {~n, h} cong(~Ind, ~Ind, ~unstep(step(n)), ~n, ~step, ~h)
+  dup F = (%i)(~motive, case_s)
+  # F(refl(~base))
+
+cong_unstep : {~a : Ind, ~b : Ind, ~e : step(a) == step(b)} -> a == b
+  let r0 = cong(~Ind, ~Ind, ~step(a), ~step(b), ~unstep, ~e)
+  let r1 = r0 :: rewrite x in x == unstep(step(b)) with <unstep_step(a)>
+  let r2 = r1 :: rewrite y in a == y with <unstep_step(b)>
+  r2