Cleanup a bit and reorganize

6 files changed, 577 insertions, 90 deletions

diff --git a/backends/hol4/divDefLib.sig b/backends/hol4/divDefLib.sig
new file mode 100644
index 00000000..d63d7771
--- /dev/null
+++ b/backends/hol4/divDefLib.sig
@@ -0,0 +1,93 @@
+signature divDefLib =
+sig
+  include Abbrev
+
+  (* Define a (group of mutually recursive) function(s) which uses an error
+     monad and is potentially divergent.
+
+     We encode divergence in such a way that we don't have to prove that the
+     functions we define terminate *upon defining them*, and can do those proofs
+     in an extrinsic way later. It works as follows.
+
+     Let's say you want to define the following “even” and “odd” functions
+     which operate on *integers*:
+
+     {[
+       even (i : int) : bool result = if i = 0 then Return T else odd (i - 1) /\
+
+       odd (i : int) : bool result = if i = 0 then Return F else even (i - 1)
+     ]}
+
+     It is easy to prove that the functions terminate provided the input is >= 0,
+     but it would require to be able to define those functions in the first place!
+
+     {!DefineDev} consequently does the following.
+
+     It first defines versions of “even” and “odd” which use fuel:
+     {[
+       even___fuel (n : num) (i : int) : bool result =
+         case n of 0 => Diverge
+         | SUC m => if i = 0 then Return T else odd___fuel m (i - 1) /\
+
+       odd___fuel (n : num) (i : int) : bool result =
+         case n of 0 => Diverge
+         | SUC m => if i = 0 then Return F else even___fuel m (i - 1)
+     ]}
+
+     Those functions trivially terminate.
+
+     Then, provided we have the following auxiliary definition:
+     {[
+       is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F
+     ]}
+
+     we can define the following predicates, which tell us whether “even___fuel”
+     and “odd___fuel” terminate on some given inputs:
+     {[
+       even___P i n = ~(is_diverge (even___fuel n i)) /\
+
+       odd___P i n = ~(is_diverge (odd___fuel n i))
+     ]}
+
+     We can finally define “even” and “odd” as follows. We use the excluded
+     middle to test whether there exists some fuel on which the function
+     terminates: if there exists such fuel, we call the "___fuel" versions
+     of “even” and “odd” with it (we use the least upper bound, to be more
+     precise). Otherwise, we simply return “Diverge”.
+     {[
+       even i =
+         if (?n. even___P i n) then even___fuel ($LEAST (even___P i)) i
+         else Diverge /\
+
+       odd i =
+         if (?n. odd___P i n) then odd___fuel ($LEAST (odd___P i)) i
+         else Diverge
+     ]}
+
+     The definitions above happen to satisfy the rewriting theorem we want:
+     {[
+       even (i : int) : bool result = if i = 0 then Return T else odd (i - 1) /\
+
+       odd (i : int) : bool result = if i = 0 then Return F else even (i - 1)
+     ]}
+
+     Moreover, if we prove a lemma which states that they don't evaluate to
+     “Diverge” on some given inputs (trivial recursion if we take “i >= 0”
+     and reuse the rewriting theorem just above), then we effectively proved
+     that the functions terminate on those inputs.
+
+     Remark:
+     =======
+     {!DefineDiv} introduces all the auxiliary definitions we need and
+     automatically performs the proofs. A crucial intermediate lemma
+     we need in order to establish the last theorem is that the "___fuel"
+     versions of the functions are monotonic in the fuel.
+     More precisely:
+     {[
+       !n m. n <= m ==>
+         (!ls i. even___P ls i n ==> even___fuel n ls i n = even___fuel m ls i n) /\
+         (!ls i. odd___P ls i n ==> odd___fuel n ls i n = odd___fuel m ls i n)
+     ]}
+   *)
+  val DefineDiv : term quotation -> thm list
+end
diff --git a/backends/hol4/divDefLib.sml b/backends/hol4/divDefLib.sml
index 3ecb32df..59c1edaf 100644
--- a/backends/hol4/divDefLib.sml
+++ b/backends/hol4/divDefLib.sml
@@ -1,21 +1,21 @@
 (* This file implements utilities to define potentially diverging functions *)
 
+structure divDefLib :> divDefLib =
+struct
+
 open HolKernel boolLib bossLib Parse
 open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
 
 open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
 open primitivesLib
 
-(* TODO: move *)
-Theorem case_result_same_eq:
-  !(r : 'a result).
+val case_result_same_eq = prove (
+  “!(r : 'a result).
     (case r of
        Return x => Return x
      | Fail e => Fail e
-     | Diverge => Diverge) = r
-Proof
-  rw [] >> CASE_TAC
-QED
+     | Diverge => Diverge) = r”,
+  rw [] >> CASE_TAC)
 
 (*
 val ty = id_ty
@@ -90,8 +90,6 @@ val bool_ty = “:bool”
 val alpha_tyvar : hol_type = “:'a”
 val beta_tyvar : hol_type = “:'b”
 
-val is_diverge_def = Define ‘
-  is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F’
 val is_diverge_tm = “is_diverge: 'a result -> bool”
 val diverge_tm = “Diverge : 'a result”
 
@@ -1202,84 +1200,4 @@ fun DefineDiv (def_qt : term quotation) =
     final_eqs
   end
 
-(*
-
-val def_qt = ‘
-  (even (i : int) : bool result =
-    if i = 0 then Return T else odd (i - 1)) /\
-  (odd (i : int) : bool result =
-    if i = 0 then Return F else even (i - 1))
-’
-
-val even_def = DefineDiv def_qt
-
-(* Complexigying the above definition *)
-val def_qt = ‘
-  (even (i : int) : bool result =
-    if i = 0 then
-      do
-        b <- Return T;
-        Return b
-      od
-    else do
-      b <- odd (i - 1);
-      Return b
-      od
-    ) /\
-  (odd (i : int) : bool result =
-    if i = 0 then
-      do
-        b <- Return F;
-        Return b
-      od
-    else do
-      b <- even (i - 1);
-      Return b
-      od)
-’
-
-val even_def = DefineDiv def_qt
-
-Datatype:
-  list_t =
-    ListCons 't list_t
-  | ListNil
-End
-
-val def_qt = ‘
-  nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
-  case ls of
-  | ListCons x tl =>
-    if u32_to_int i = (0:int)
-    then Return x
-    else
-      do
-      i0 <- u32_sub i (int_to_u32 1);
-      nth_mut_fwd tl i0
-      od
-  | ListNil =>
-    Fail Failure
-’
-
-val nth_mut_fwd_def = DefineDiv def_qt
-
-(* Checking what happens with non terminal calls *)
-val def_qt = ‘
-  nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
-  case ls of
-  | ListCons x tl =>
-    if u32_to_int i = (0:int)
-    then Return x
-    else
-      do
-      i0 <- u32_sub i (int_to_u32 1);
-      x <- nth_mut_fwd tl i0;
-      Return x
-      od
-  | ListNil => 
-    Fail Failure
-’
-
-val nth_mut_fwd_def = DefineDiv def_qt
-
-*)
+end
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml
index 969e9f6e..00511f00 100644
--- a/backends/hol4/primitivesScript.sml
+++ b/backends/hol4/primitivesScript.sml
@@ -36,6 +36,9 @@ Overload monad_bind = ``bind``
 Overload monad_unitbind = ``\x y. bind x (\z. y)``
 Overload monad_ignore_bind = ``\x y. bind x (\z. y)``
 
+val is_diverge_def = Define ‘
+  is_diverge (r: 'a result) : bool = case r of Diverge => T | _ => F’
+
 (* Allow the use of monadic syntax *)
 val _ = monadsyntax.enable_monadsyntax ()
 
diff --git a/backends/hol4/primitivesTheory.sig b/backends/hol4/primitivesTheory.sig
index cf550f00..fdf28172 100644
--- a/backends/hol4/primitivesTheory.sig
+++ b/backends/hol4/primitivesTheory.sig
@@ -86,6 +86,7 @@ sig
     val i8_rem_def : thm
     val i8_sub_def : thm
     val int_rem_def : thm
+    val is_diverge_def : thm
     val isize_add_def : thm
     val isize_div_def : thm
     val isize_mul_def : thm
@@ -646,6 +647,11 @@ sig
           int_rem x y =
           if x ≥ 0 ∧ y ≥ 0 ∨ x < 0 ∧ y < 0 then x % y else -(x % y)
    
+   [is_diverge_def]  Definition
+      
+      ⊢ ∀r. is_diverge r ⇔
+            case r of Return v2 => F | Fail v3 => F | Diverge => T
+   
    [isize_add_def]  Definition
       
       ⊢ ∀x y. isize_add x y = mk_isize (isize_to_int x + isize_to_int y)
diff --git a/backends/hol4/testDivDefScript.sml b/backends/hol4/testDivDefScript.sml
new file mode 100644
index 00000000..4a87895f
--- /dev/null
+++ b/backends/hol4/testDivDefScript.sml
@@ -0,0 +1,87 @@
+open HolKernel boolLib bossLib Parse
+open boolTheory arithmeticTheory integerTheory intLib listTheory stringTheory
+
+open primitivesArithTheory primitivesBaseTacLib ilistTheory primitivesTheory
+open primitivesLib divDefLib
+
+val _ = new_theory "testDivDef"
+
+val def_qt = ‘
+  (even (i : int) : bool result =
+    if i = 0 then Return T else odd (i - 1)) /\
+  (odd (i : int) : bool result =
+    if i = 0 then Return F else even (i - 1))
+’
+
+val even_def = DefineDiv def_qt
+
+(* Complexifying the above definition, and overriding on purpose *)
+val def_qt = ‘
+  (even (i : int) : bool result =
+    if i = 0 then
+      do
+        b <- Return T;
+        Return b
+      od
+    else do
+      b <- odd (i - 1);
+      Return b
+      od
+    ) /\
+  (odd (i : int) : bool result =
+    if i = 0 then
+      do
+        b <- Return F;
+        Return b
+      od
+    else do
+      b <- even (i - 1);
+      Return b
+      od)
+’
+
+val even_def = DefineDiv def_qt
+
+Datatype:
+  list_t =
+    ListCons 't list_t
+  | ListNil
+End
+
+val def_qt = ‘
+  nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
+  case ls of
+  | ListCons x tl =>
+    if u32_to_int i = (0:int)
+    then Return x
+    else
+      do
+      i0 <- u32_sub i (int_to_u32 1);
+      nth_mut_fwd tl i0
+      od
+  | ListNil =>
+    Fail Failure
+’
+
+val nth_mut_fwd_def = DefineDiv def_qt
+
+(* Complexifying the above definition, and overriding on purpose *)
+val def_qt = ‘
+  nth_mut_fwd (ls : 't list_t) (i : u32) : 't result =
+  case ls of
+  | ListCons x tl =>
+    if u32_to_int i = (0:int)
+    then Return x
+    else
+      do
+      i0 <- u32_sub i (int_to_u32 1);
+      x <- nth_mut_fwd tl i0;
+      Return x
+      od
+  | ListNil => 
+    Fail Failure
+’
+
+val nth_mut_fwd_def = DefineDiv def_qt
+
+val _ = export_theory ()
diff --git a/backends/hol4/testDivDefTheory.sig b/backends/hol4/testDivDefTheory.sig
new file mode 100644
index 00000000..a3ce2255
--- /dev/null
+++ b/backends/hol4/testDivDefTheory.sig
@@ -0,0 +1,380 @@
+signature testDivDefTheory =
+sig
+  type thm = Thm.thm
+  
+  (*  Definitions  *)
+    val even___E_def : thm
+    val even___P_def : thm
+    val even___fuel0_def_UNION_extract0 : thm
+    val even___fuel0_def_UNION_extract1 : thm
+    val even___fuel0_def_UNION_primitive : thm
+    val even___fuel_def_UNION_extract0 : thm
+    val even___fuel_def_UNION_extract1 : thm
+    val even___fuel_def_UNION_primitive : thm
+    val even_def : thm
+    val list_t_TY_DEF : thm
+    val list_t_case_def : thm
+    val list_t_size_def : thm
+    val nth_mut_fwd___E_def : thm
+    val nth_mut_fwd___P_def : thm
+    val nth_mut_fwd_def : thm
+    val odd___E_def : thm
+    val odd___P_def : thm
+    val odd_def : thm
+  
+  (*  Theorems  *)
+    val datatype_list_t : thm
+    val even___fuel0_def : thm
+    val even___fuel0_ind : thm
+    val even___fuel_def : thm
+    val even___fuel_ind : thm
+    val list_t_11 : thm
+    val list_t_Axiom : thm
+    val list_t_case_cong : thm
+    val list_t_case_eq : thm
+    val list_t_distinct : thm
+    val list_t_induction : thm
+    val list_t_nchotomy : thm
+    val nth_mut_fwd___fuel0_def : thm
+    val nth_mut_fwd___fuel0_ind : thm
+    val nth_mut_fwd___fuel_def : thm
+    val nth_mut_fwd___fuel_ind : thm
+  
+  val testDivDef_grammars : type_grammar.grammar * term_grammar.grammar
+(*
+   [primitives] Parent theory of "testDivDef"
+   
+   [even___E_def]  Definition
+      
+      ⊢ ∀even odd i.
+          even___E even odd i =
+          if i = 0 then do b <- Return T; Return b od
+          else do b <- odd (i − 1); Return b od
+   
+   [even___P_def]  Definition
+      
+      ⊢ ∀i $var$($n).
+          even___P i $var$($n) ⇔ ¬is_diverge (even___fuel0 $var$($n) i)
+   
+   [even___fuel0_def_UNION_extract0]  Definition
+      
+      ⊢ ∀x x0. even___fuel0 x x0 = even___fuel0_def_UNION (INL (x,x0))
+   
+   [even___fuel0_def_UNION_extract1]  Definition
+      
+      ⊢ ∀x x0. odd___fuel0 x x0 = even___fuel0_def_UNION (INR (x,x0))
+   
+   [even___fuel0_def_UNION_primitive]  Definition
+      
+      ⊢ even___fuel0_def_UNION =
+        WFREC
+          (@R. WF R ∧
+               (∀i $var$($n) $var$($m).
+                  $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒
+                  R (INR ($var$($m),i − 1)) (INL ($var$($n),i))) ∧
+               ∀i $var$($n) $var$($m).
+                 $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒
+                 R (INL ($var$($m),i − 1)) (INR ($var$($n),i)))
+          (λeven___fuel0_def_UNION a.
+               case a of
+                 INL ($var$($n),i) =>
+                   I
+                     (case $var$($n) of
+                        0 => Diverge
+                      | SUC $var$($m) =>
+                        if i = 0 then do b <- Return T; Return b od
+                        else
+                          do
+                            b <-
+                              even___fuel0_def_UNION
+                                (INR ($var$($m),i − 1));
+                            Return b
+                          od)
+               | INR ($var$($n'),i') =>
+                 I
+                   (case $var$($n') of
+                      0 => Diverge
+                    | SUC $var$($m) =>
+                      if i' = 0 then do b <- Return F; Return b od
+                      else
+                        do
+                          b <-
+                            even___fuel0_def_UNION (INL ($var$($m),i' − 1));
+                          Return b
+                        od))
+   
+   [even___fuel_def_UNION_extract0]  Definition
+      
+      ⊢ ∀x x0. even___fuel x x0 = even___fuel_def_UNION (INL (x,x0))
+   
+   [even___fuel_def_UNION_extract1]  Definition
+      
+      ⊢ ∀x x0. odd___fuel x x0 = even___fuel_def_UNION (INR (x,x0))
+   
+   [even___fuel_def_UNION_primitive]  Definition
+      
+      ⊢ even___fuel_def_UNION =
+        WFREC
+          (@R. WF R ∧
+               (∀i $var$($n) $var$($m).
+                  $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒
+                  R (INR ($var$($m),i − 1)) (INL ($var$($n),i))) ∧
+               ∀i $var$($n) $var$($m).
+                 $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒
+                 R (INL ($var$($m),i − 1)) (INR ($var$($n),i)))
+          (λeven___fuel_def_UNION a.
+               case a of
+                 INL ($var$($n),i) =>
+                   I
+                     (case $var$($n) of
+                        0 => Diverge
+                      | SUC $var$($m) =>
+                        if i = 0 then Return T
+                        else even___fuel_def_UNION (INR ($var$($m),i − 1)))
+               | INR ($var$($n'),i') =>
+                 I
+                   (case $var$($n') of
+                      0 => Diverge
+                    | SUC $var$($m) =>
+                      if i' = 0 then Return F
+                      else even___fuel_def_UNION (INL ($var$($m),i' − 1))))
+   
+   [even_def]  Definition
+      
+      ⊢ ∀i. even i =
+            if ∃ $var$($n). even___P i $var$($n) then
+              even___fuel0 ($LEAST (even___P i)) i
+            else Diverge
+   
+   [list_t_TY_DEF]  Definition
+      
+      ⊢ ∃rep.
+          TYPE_DEFINITION
+            (λa0'.
+                 ∀ $var$('list_t').
+                   (∀a0'.
+                      (∃a0 a1.
+                         a0' =
+                         (λa0 a1.
+                              ind_type$CONSTR 0 a0
+                                (ind_type$FCONS a1 (λn. ind_type$BOTTOM)))
+                           a0 a1 ∧ $var$('list_t') a1) ∨
+                      a0' =
+                      ind_type$CONSTR (SUC 0) ARB (λn. ind_type$BOTTOM) ⇒
+                      $var$('list_t') a0') ⇒
+                   $var$('list_t') a0') rep
+   
+   [list_t_case_def]  Definition
+      
+      ⊢ (∀a0 a1 f v. list_t_CASE (ListCons a0 a1) f v = f a0 a1) ∧
+        ∀f v. list_t_CASE ListNil f v = v
+   
+   [list_t_size_def]  Definition
+      
+      ⊢ (∀f a0 a1.
+           list_t_size f (ListCons a0 a1) = 1 + (f a0 + list_t_size f a1)) ∧
+        ∀f. list_t_size f ListNil = 0
+   
+   [nth_mut_fwd___E_def]  Definition
+      
+      ⊢ ∀nth_mut_fwd ls i.
+          nth_mut_fwd___E nth_mut_fwd ls i =
+          case ls of
+            ListCons x tl =>
+              if u32_to_int i = 0 then Return x
+              else
+                do
+                  i0 <- u32_sub i (int_to_u32 1);
+                  x <- nth_mut_fwd tl i0;
+                  Return x
+                od
+          | ListNil => Fail Failure
+   
+   [nth_mut_fwd___P_def]  Definition
+      
+      ⊢ ∀ls i $var$($n).
+          nth_mut_fwd___P ls i $var$($n) ⇔
+          ¬is_diverge (nth_mut_fwd___fuel0 $var$($n) ls i)
+   
+   [nth_mut_fwd_def]  Definition
+      
+      ⊢ ∀ls i.
+          nth_mut_fwd ls i =
+          if ∃ $var$($n). nth_mut_fwd___P ls i $var$($n) then
+            nth_mut_fwd___fuel0 ($LEAST (nth_mut_fwd___P ls i)) ls i
+          else Diverge
+   
+   [odd___E_def]  Definition
+      
+      ⊢ ∀even odd i.
+          odd___E even odd i =
+          if i = 0 then do b <- Return F; Return b od
+          else do b <- even (i − 1); Return b od
+   
+   [odd___P_def]  Definition
+      
+      ⊢ ∀i $var$($n).
+          odd___P i $var$($n) ⇔ ¬is_diverge (odd___fuel0 $var$($n) i)
+   
+   [odd_def]  Definition
+      
+      ⊢ ∀i. odd i =
+            if ∃ $var$($n). odd___P i $var$($n) then
+              odd___fuel0 ($LEAST (odd___P i)) i
+            else Diverge
+   
+   [datatype_list_t]  Theorem
+      
+      ⊢ DATATYPE (list_t ListCons ListNil)
+   
+   [even___fuel0_def]  Theorem
+      
+      ⊢ (∀i $var$($n).
+           even___fuel0 $var$($n) i =
+           case $var$($n) of
+             0 => Diverge
+           | SUC $var$($m) =>
+             if i = 0 then do b <- Return T; Return b od
+             else do b <- odd___fuel0 $var$($m) (i − 1); Return b od) ∧
+        ∀i $var$($n).
+          odd___fuel0 $var$($n) i =
+          case $var$($n) of
+            0 => Diverge
+          | SUC $var$($m) =>
+            if i = 0 then do b <- Return F; Return b od
+            else do b <- even___fuel0 $var$($m) (i − 1); Return b od
+   
+   [even___fuel0_ind]  Theorem
+      
+      ⊢ ∀P0 P1.
+          (∀ $var$($n) i.
+             (∀ $var$($m).
+                $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ P1 $var$($m) (i − 1)) ⇒
+             P0 $var$($n) i) ∧
+          (∀ $var$($n) i.
+             (∀ $var$($m).
+                $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ P0 $var$($m) (i − 1)) ⇒
+             P1 $var$($n) i) ⇒
+          (∀v0 v1. P0 v0 v1) ∧ ∀v0 v1. P1 v0 v1
+   
+   [even___fuel_def]  Theorem
+      
+      ⊢ (∀i $var$($n).
+           even___fuel $var$($n) i =
+           case $var$($n) of
+             0 => Diverge
+           | SUC $var$($m) =>
+             if i = 0 then Return T else odd___fuel $var$($m) (i − 1)) ∧
+        ∀i $var$($n).
+          odd___fuel $var$($n) i =
+          case $var$($n) of
+            0 => Diverge
+          | SUC $var$($m) =>
+            if i = 0 then Return F else even___fuel $var$($m) (i − 1)
+   
+   [even___fuel_ind]  Theorem
+      
+      ⊢ ∀P0 P1.
+          (∀ $var$($n) i.
+             (∀ $var$($m).
+                $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ P1 $var$($m) (i − 1)) ⇒
+             P0 $var$($n) i) ∧
+          (∀ $var$($n) i.
+             (∀ $var$($m).
+                $var$($n) = SUC $var$($m) ∧ i ≠ 0 ⇒ P0 $var$($m) (i − 1)) ⇒
+             P1 $var$($n) i) ⇒
+          (∀v0 v1. P0 v0 v1) ∧ ∀v0 v1. P1 v0 v1
+   
+   [list_t_11]  Theorem
+      
+      ⊢ ∀a0 a1 a0' a1'.
+          ListCons a0 a1 = ListCons a0' a1' ⇔ a0 = a0' ∧ a1 = a1'
+   
+   [list_t_Axiom]  Theorem
+      
+      ⊢ ∀f0 f1. ∃fn.
+          (∀a0 a1. fn (ListCons a0 a1) = f0 a0 a1 (fn a1)) ∧
+          fn ListNil = f1
+   
+   [list_t_case_cong]  Theorem
+      
+      ⊢ ∀M M' f v.
+          M = M' ∧ (∀a0 a1. M' = ListCons a0 a1 ⇒ f a0 a1 = f' a0 a1) ∧
+          (M' = ListNil ⇒ v = v') ⇒
+          list_t_CASE M f v = list_t_CASE M' f' v'
+   
+   [list_t_case_eq]  Theorem
+      
+      ⊢ list_t_CASE x f v = v' ⇔
+        (∃t l. x = ListCons t l ∧ f t l = v') ∨ x = ListNil ∧ v = v'
+   
+   [list_t_distinct]  Theorem
+      
+      ⊢ ∀a1 a0. ListCons a0 a1 ≠ ListNil
+   
+   [list_t_induction]  Theorem
+      
+      ⊢ ∀P. (∀l. P l ⇒ ∀t. P (ListCons t l)) ∧ P ListNil ⇒ ∀l. P l
+   
+   [list_t_nchotomy]  Theorem
+      
+      ⊢ ∀ll. (∃t l. ll = ListCons t l) ∨ ll = ListNil
+   
+   [nth_mut_fwd___fuel0_def]  Theorem
+      
+      ⊢ ∀ls i $var$($n).
+          nth_mut_fwd___fuel0 $var$($n) ls i =
+          case $var$($n) of
+            0 => Diverge
+          | SUC $var$($m) =>
+            case ls of
+              ListCons x tl =>
+                if u32_to_int i = 0 then Return x
+                else
+                  do
+                    i0 <- u32_sub i (int_to_u32 1);
+                    x <- nth_mut_fwd___fuel0 $var$($m) tl i0;
+                    Return x
+                  od
+            | ListNil => Fail Failure
+   
+   [nth_mut_fwd___fuel0_ind]  Theorem
+      
+      ⊢ ∀P. (∀ $var$($n) ls i.
+               (∀ $var$($m) x tl i0.
+                  $var$($n) = SUC $var$($m) ∧ ls = ListCons x tl ∧
+                  u32_to_int i ≠ 0 ⇒
+                  P $var$($m) tl i0) ⇒
+               P $var$($n) ls i) ⇒
+            ∀v v1 v2. P v v1 v2
+   
+   [nth_mut_fwd___fuel_def]  Theorem
+      
+      ⊢ ∀ls i $var$($n).
+          nth_mut_fwd___fuel $var$($n) ls i =
+          case $var$($n) of
+            0 => Diverge
+          | SUC $var$($m) =>
+            case ls of
+              ListCons x tl =>
+                if u32_to_int i = 0 then Return x
+                else
+                  do
+                    i0 <- u32_sub i (int_to_u32 1);
+                    nth_mut_fwd___fuel $var$($m) tl i0
+                  od
+            | ListNil => Fail Failure
+   
+   [nth_mut_fwd___fuel_ind]  Theorem
+      
+      ⊢ ∀P. (∀ $var$($n) ls i.
+               (∀ $var$($m) x tl i0.
+                  $var$($n) = SUC $var$($m) ∧ ls = ListCons x tl ∧
+                  u32_to_int i ≠ 0 ⇒
+                  P $var$($m) tl i0) ⇒
+               P $var$($n) ls i) ⇒
+            ∀v v1 v2. P v v1 v2
+   
+   
+*)
+end