Start making tests in HOL4

1 files changed, 825 insertions, 0 deletions

diff --git a/backends/hol4/Test.sml b/backends/hol4/Test.sml
new file mode 100644
index 00000000..b29589d5
--- /dev/null
+++ b/backends/hol4/Test.sml
@@ -0,0 +1,825 @@
+open HolKernel boolLib bossLib Parse
+
+val _ = new_theory"test"
+
+(* SML declarations  *)
+(* for example: *)
+(*val th = save_thm("SKOLEM_AGAIN",SKOLEM_THM) *)
+
+local open boolTheory integerTheory wordsTheory stringTheory in end
+
+Datatype:
+  error = Failure
+End
+
+Datatype:
+  result = Return 'a | Fail error | Loop
+End
+
+Type M = ``: 'a result``
+
+(* TODO: rename *)
+val st_ex_bind_def = Define `
+  (st_ex_bind : 'a M -> ('a -> 'b M) -> 'b M) x f =
+    case x of
+      Return y => f y
+    | Fail e => Fail e
+    | Loop => Loop`;
+
+val st_ex_return_def = Define `
+  (st_ex_return : 'a -> 'a M) x =
+    Return x`;
+
+Overload monad_bind[local] = ``st_ex_bind``
+Overload monad_unitbind[local] = ``\x y. st_ex_bind x (\z. y)``
+Overload monad_ignore_bind[local] = ``\x y. st_ex_bind x (\z. y)``
+(*Overload ex_bind[local] = ``st_ex_bind`` *)
+(* Overload ex_return[local] = ``st_ex_return`` *)
+(*Overload failwith = ``raise_Fail``*)
+
+(* Temporarily allow the monadic syntax *)
+val _ = monadsyntax.temp_add_monadsyntax ();
+
+val test1_def = Define `
+  test1 (x : bool) = Return x`
+
+val is_true_def = Define ‘
+  is_true (x : bool) = if x then Return () else Fail Failure’
+
+val test1_def = Define ‘
+  test1 (x : bool) = Return x’
+
+val test_monad_def = Define `
+  test_monad v =
+    do
+      x <- Return v;
+      Return x
+    od`;
+
+
+val test_monad2_def = Define `
+  test_monad2 =
+    do
+      x <- Return T;
+      Return x
+    od`;
+
+val test_monad3_def = Define `
+  test_monad3 x =
+    do
+      is_true x;
+      Return x
+    od`;
+
+(**
+ *  Arithmetic
+ *)
+
+open intLib
+
+val test_int1 = Define ‘int1 = 32’
+val test_int2 = Define ‘int2 = -32’
+
+Theorem INT_THM1:
+  !(x y : int). x > 0 ==> y > 0 ==> x + y > 0
+Proof
+  ARITH_TAC
+QED
+
+Theorem INT_THM2:
+  !(x : int). T
+Proof
+  rw[]
+QED
+
+val _ = prefer_int ()
+
+val x = “-36217863217862718”
+
+(* Deactivate notations for int *)
+val _ = deprecate_int ()
+open arithmeticTheory
+
+
+val m = Hol_pp.print_apropos;
+val f = Hol_pp.print_find;
+
+(*
+m “SUC (x : num) + y = _”
+m “(ZERO : num) < SUC y”
+m “(_ : num) < SUC y”
+m “x < (y : num) <=> _”
+f "ADD"
+ADD
+
+val x  = “1:num”
+dest_term x
+val (x1, x2) = dest_comb x
+dest_term “0n:num”
+dest_term “ZERO:num”
+m “ZERO + (_ : num) = _”
+
+m “BIT1 _ = _”
+NUMERAL_DEF
+
+val x = “ZERO = (0:num)”
+dest_term x
+
+m “0 < SUC 0”
+*)
+
+(* Display types on/off: M-h C-t *)
+(* Move back: M-h b *)
+
+val _ = numLib.deprecate_num ()
+val _ = numLib.prefer_num ()
+
+(*
+m “!x. x = x”
+*)
+
+Theorem NAT_THM1:
+  !(n : num). n < n + 1
+Proof
+  Induct_on ‘n’ >> DECIDE_TAC
+QED
+
+Theorem NAT_THM2:
+  !(n : num). n < n + (1 : num)
+Proof
+  gen_tac >>
+  Induct_on ‘n’ >- (
+    PURE_REWRITE_TAC [ADD, NUMERAL_DEF, BIT1, ALT_ZERO] >>
+    PURE_REWRITE_TAC [prim_recTheory.LESS_0_0]) >>
+  PURE_REWRITE_TAC [ADD] >>
+  irule prim_recTheory.LESS_MONO >>
+  asm_rewrite_tac []
+QED
+
+
+val x = “1278361286371286:num”
+
+
+(********************** PRIMITIVES *)
+val _ = prefer_int ()
+
+val _ = new_type ("u32", 0)
+val _ = new_type ("i32", 0)
+
+val u32_min_def = Define ‘u32_min = (0:int)’
+val u32_max_def = Define ‘u32_max = (4294967295:int)’
+
+(* TODO: change that *)
+val usize_max_def = Define ‘usize_max = (4294967295:int)’
+
+val i32_min_def = Define ‘i32_min = (-2147483648:int)’
+val i32_max_def = Define ‘i32_max = (2147483647:int)’
+
+val _ = new_constant ("u32_to_int", “:u32 -> int”)
+val _ = new_constant ("i32_to_int", “:i32 -> int”)
+
+val _ = new_constant ("int_to_u32", “:int -> u32”)
+val _ = new_constant ("int_to_i32", “:int -> i32”)
+
+
+(* TODO: change to "...of..." *)
+val u32_to_int_bounds =
+  new_axiom (
+    "u32_to_int_bounds",
+    “!n. u32_min <= u32_to_int n /\ u32_to_int n <= u32_max”)
+
+val i32_to_int_bounds =
+  new_axiom (
+    "i32_to_int_bounds",
+    “!n. i32_min <= i32_to_int n /\ i32_to_int n <= i32_max”)
+
+val int_to_u32_id =
+  new_axiom (
+    "int_to_u32_id",
+    “!n. u32_min <= n /\ n <= u32_max ==>
+     u32_to_int (int_to_u32 n) = n”)
+
+val int_to_i32_id =
+  new_axiom (
+    "int_to_i32_id",
+    “!n. i32_min <= n /\ n <= i32_max ==>
+     i32_to_int (int_to_i32 n) = n”)
+
+val mk_u32_def = Define
+  ‘mk_u32 n =
+    if u32_min <= n /\ n <= u32_max then Return (int_to_u32 n)
+    else Fail Failure’
+
+val u32_add_def = Define ‘u32_add x y = mk_u32 ((u32_to_int x) + (u32_to_int y))’
+
+Theorem MK_U32_SUCCESS:
+  !n. u32_min <= n /\ n <= u32_max ==>
+  mk_u32 n = Return (int_to_u32 n)
+Proof
+  rw[mk_u32_def]
+QED
+
+Theorem U32_ADD_EQ:
+  !x y.
+    u32_to_int x + u32_to_int y <= u32_max ==>
+    ?z. u32_add x y = Return z /\ u32_to_int z = u32_to_int x + u32_to_int y
+Proof
+  rpt gen_tac >>
+  rpt DISCH_TAC >>
+  exists_tac “int_to_u32 (u32_to_int x + u32_to_int y)” >>
+  imp_res_tac MK_U32_SUCCESS >>
+  (* There is probably a better way of doing this *)
+  sg ‘u32_min <= u32_to_int x’ >- (rw[u32_to_int_bounds]) >>
+  sg ‘u32_min <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >>
+  fs [u32_min_def, u32_add_def] >>
+  irule int_to_u32_id >>
+  fs[u32_min_def]
+QED
+
+val u32_sub_def = Define ‘u32_sub x y = mk_u32 ((u32_to_int x) - (u32_to_int y))’
+
+Theorem U32_SUB_EQ:
+  !x y.
+    u32_min <= u32_to_int x - u32_to_int y ==>
+    ?z. u32_sub x y = Return z /\ u32_to_int z = u32_to_int x - u32_to_int y
+Proof
+  rpt gen_tac >>
+  rpt DISCH_TAC >>
+  exists_tac “int_to_u32 (u32_to_int x - u32_to_int y)” >>
+  imp_res_tac MK_U32_SUCCESS >>
+  (* There is probably a better way of doing this *)
+  sg ‘u32_to_int x − u32_to_int y ≤ u32_max’ >-(
+    sg ‘u32_to_int x <= u32_max’ >- (rw[u32_to_int_bounds]) >>
+    sg ‘u32_min <= u32_to_int y’ >- (rw[u32_to_int_bounds]) >>
+    fs [u32_min_def] >>
+    COOPER_TAC
+  ) >>
+  fs [u32_min_def, u32_sub_def] >>
+  irule int_to_u32_id >>
+  fs[u32_min_def]
+QED
+
+val mk_i32_def = Define
+  ‘mk_i32 n =
+    if i32_min <= n /\ n <= i32_max then Return (int_to_i32 n)
+    else Fail Failure’
+
+val i32_add_def = Define ‘i32_add x y = mk_i32 ((i32_to_int x) + (i32_to_int y))’
+
+Theorem MK_I32_SUCCESS:
+  !n. i32_min <= n /\ n <= i32_max ==>
+  mk_i32 n = Return (int_to_i32 n)
+Proof
+  rw[mk_i32_def]
+QED
+
+Theorem I32_ADD_EQ:
+  !x y.
+    i32_min <= i32_to_int x + i32_to_int y ==>
+    i32_to_int x + i32_to_int y <= i32_max ==>
+    ?z. i32_add x y = Return z /\ i32_to_int z = i32_to_int x + i32_to_int y
+Proof
+  rpt gen_tac >>
+  rpt DISCH_TAC >>
+  exists_tac “int_to_i32 (i32_to_int x + i32_to_int y)” >>
+  imp_res_tac MK_I32_SUCCESS >>
+  fs [i32_min_def, i32_add_def] >>
+  irule int_to_i32_id >>
+  fs[i32_min_def]
+QED
+
+open listTheory
+
+val _ = new_type ("vec", 1)
+val _ = new_constant ("vec_to_list", “:'a vec -> 'a list”)
+
+val VEC_TO_LIST_NUM_BOUNDS =
+  new_axiom (
+    "VEC_TO_LIST_BOUNDS",
+    “!v. let l = LENGTH (vec_to_list v) in
+     (0:num) <= l /\ l <= (4294967295:num)”)
+
+Theorem VEC_TO_LIST_INT_BOUNDS:
+  !v. let l = int_of_num (LENGTH (vec_to_list v)) in
+     u32_min <= l /\ l <= u32_max
+Proof
+  gen_tac >>
+  rw [u32_min_def, u32_max_def] >>
+  assume_tac VEC_TO_LIST_NUM_BOUNDS >>
+  fs[]
+QED
+
+val VEC_LEN_DEF = Define ‘vec_len v = int_to_u32 (int_of_num (LENGTH (vec_to_list v)))’
+
+(*
+(* Useless *)
+Theorem VEC_LEN_BOUNDS:
+  !v. u32_min <= u32_to_int (vec_len v) /\ u32_to_int (vec_len v) <= u32_max
+Proof
+  gen_tac >>
+  qspec_then ‘v’ assume_tac VEC_TO_LIST_INT_BOUNDS >>
+  fs[VEC_LEN_DEF] >>
+  IMP_RES_TAC int_to_u32_id >>
+  fs[]
+QED
+*)
+
+(* The type parameters are ordered in alphabetical order *)
+Datatype:
+  test = Variant1 'b | Variant2 'a
+End
+
+Datatype:
+  test2 = Variant1_1 'T2 | Variant2_1 'T1
+End
+
+Datatype:
+  test2 = Variant1_2 'T1 | Variant2_2 'T2
+End
+
+(*
+“Variant1_1 3”
+“Variant1_2 3”
+
+type_of “CONS 3”
+*)
+
+(* TODO: argument order, we must also omit arguments in new type *)
+Datatype:
+  list_t =
+    ListCons 't list_t
+  | ListNil
+End
+
+val list_nth_mut_loop_loop_fwd_def = Define ‘
+  list_nth_mut_loop_loop_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);
+      list_nth_mut_loop_loop_fwd tl i0
+      od
+  | ListNil => 
+    Fail Failure
+’
+
+(*
+CoInductive coind:
+ !x y. coind x /\ coind y ==> coind (x + y)
+End
+*)
+
+(*
+(* This generates inconsistent theorems *)
+CoInductive loop:
+ !x. loop x = if x then loop x else 0
+End
+
+CoInductive loop:
+ !(x : int). loop x = if x > 0 then loop (x - 1) else 0
+End
+*)
+
+(* This terminates *)
+val list_nth_mut_loop_loop_fwd_def = Define ‘
+  list_nth_mut_loop_loop_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);
+      list_nth_mut_loop_loop_fwd tl i0
+      od
+  | ListNil => 
+    Fail Failure
+’
+
+(* This is sort of a coinductive definition.
+
+   This can be justified:
+   - we first define a version [nth_fuel] which uses fuel (and is thus terminating)
+   - we define the predicate P:
+     P ls i n = case nth_fuel n ls i of Return _ => T |  _ => F
+   - we then use [LEAST] (least upper bound for natural numbers) to define nth as:
+     “nth ls i = if (?n. P n) then nth_fuel (LEAST (P ls i)) ls i else Fail Loop ”
+   - we finally prove that nth satisfies the proper equation.
+
+     We would need the following intermediate lemma:
+     !n.
+       n < LEAST (P ls i) ==> nth_fuel n ls i = Fail _ /\
+       n >= LEAST (P ls i) ==> nth_fuel n ls i = nth_fuel (LEAST P ls i) ls i
+     
+ *)
+val _ = new_constant ("nth", “:'t list_t -> u32 -> 't result”)
+val nth_def = new_axiom ("nth_def", “
+ nth (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 tl i0
+      od
+  | ListNil => 
+    Fail Failure
+ ”)
+
+
+(*** Examples of proofs on [nth] *)
+val list_t_v_def = Define ‘
+  list_t_v ls =
+    case ls of
+    | ListCons x tl => x :: list_t_v tl
+    | ListNil => []
+’
+
+(* TODO: move *)
+open dep_rewrite
+open integerTheory
+
+Theorem INT_OF_NUM_INJ:
+  !n m. &n = &m ==> n = m
+Proof
+  rpt strip_tac >>
+  fs [Num]
+QED
+
+Theorem NUM_SUB_1_EQ:
+  !i. 0 <= i - 1 ==> Num i = SUC (Num (i-1))
+Proof
+  rpt strip_tac >>
+  (* 0 <= i *)
+  sg ‘0 <= i’ >- COOPER_TAC >>
+  (* Get rid of the SUC *)
+  sg ‘SUC (Num (i - 1)) = 1 + Num (i - 1)’ >-(rw [ADD]) >>
+  rw [] >>
+  (* Convert to integers*)
+  irule INT_OF_NUM_INJ >>
+  imp_res_tac (GSYM INT_OF_NUM) >>
+  (* Associativity of & *)
+  PURE_REWRITE_TAC [GSYM INT_ADD] >>
+  fs []
+QED
+
+(* TODO:
+   - list all the integer variables, and insert bounds in the assumptions
+   - replace u32_min by 0?
+   - i - 1
+   - auto lookup of spec lemmas
+*)
+
+Theorem nth_lem:
+  !(ls : 't list_t) (i : u32).
+    u32_to_int i < int_of_num (LENGTH (list_t_v ls)) ==>
+    case nth ls i of
+    | Return x => x = EL (Num (u32_to_int i)) (list_t_v ls)
+    | Fail _ => F
+    | Loop => F
+Proof
+  Induct_on ‘ls’ >~ [‘ListNil’] >> rpt strip_tac >>
+  PURE_ONCE_REWRITE_TAC [nth_def] >> rw [] >-(
+    (* TODO: automate this *)
+    fs [list_t_v_def, LENGTH] >>
+    qspec_then ‘i’ assume_tac u32_to_int_bounds >>
+    rw [] >> fs [u32_min_def] >>
+    intLib.COOPER_TAC
+  ) >- (
+    PURE_ONCE_REWRITE_TAC [list_t_v_def] >>
+    rw [HD]
+  ) >>
+  (* TODO: we need specialized tactics here - first: subgoal *)
+  sg ‘u32_min <= u32_to_int i - u32_to_int (int_to_u32 1)’ >-(
+    fs [u32_min_def] >>
+    (* We need to detect that we're in the bounds, etc. *)
+    DEP_ONCE_REWRITE_TAC [int_to_u32_id] >>
+    strip_tac >- (fs [u32_min_def, u32_max_def] >> COOPER_TAC) >>
+    sg ‘u32_min <= u32_to_int i’ >- (rw[u32_to_int_bounds]) >>
+    fs [u32_min_def] >>
+    COOPER_TAC
+  ) >>
+  imp_res_tac U32_SUB_EQ >> fs [st_ex_bind_def] >>
+  (* Automate this *)
+  PURE_ONCE_REWRITE_TAC [list_t_v_def] >> rw [] >>
+  (* Automate this *)
+  sg ‘u32_to_int (int_to_u32 1) = 1’ >-(
+    DEP_ONCE_REWRITE_TAC [int_to_u32_id] >>
+    fs [u32_min_def, u32_max_def] >> COOPER_TAC
+  ) >>
+  fs [] >>
+  (* TODO: automate this *)
+  sg ‘u32_min <= u32_to_int z’ >-(rw[u32_to_int_bounds]) >> fs [u32_min_def] >>
+  qspec_then ‘u32_to_int z’ imp_res_tac NUM_SUB_1_EQ >> rw [] >>
+  (* Finish the proof by recursion *)
+  pop_last_assum (qspec_then ‘z’ assume_tac) >>
+  pop_last_assum mp_tac >>
+  qspec_then ‘ListCons t ls’ assume_tac list_t_v_def >>
+  rw [] >>
+  fs [INT] >>
+  sg ‘u32_to_int z < &LENGTH (list_t_v ls)’ >- COOPER_TAC >>
+  fs [] >>
+  (* Rem.: rfs! *)
+  rfs []
+QED
+
+(***
+ * Example of how to get rid of the fuel in practice
+ *)
+val nth_fuel_def = Define ‘
+ nth_fuel (n : num) (ls : 't list_t) (i : u32) : 't result =
+  case n of
+  | 0 => Loop
+  | SUC n => 
+    do 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_fuel n tl i0
+        od
+    | ListNil => 
+      Fail Failure
+    od
+ ’
+
+(*
+whileTheory.LEAST_DEF
+type_of “$LEAST”
+val x = “LEAST_DEF”
+*)
+
+val is_loop_def = Define ‘is_loop r = case r of Loop => T | _ => F’
+ 
+val nth_fuel_P_def = Define ‘
+  nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i)
+’
+
+Theorem nth_fuel_mono:
+  !n m ls i.
+    n <= m ==>
+    if is_loop (nth_fuel n ls i) then T
+    else nth_fuel n ls i = nth_fuel m ls i
+Proof
+  Induct_on ‘n’ >- (
+    rpt gen_tac >>
+    DISCH_TAC >>
+    PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
+    rw[is_loop_def]
+  ) >>
+  (* Interesting case *)
+  rpt gen_tac >>
+  DISCH_TAC >>
+  CASE_TAC >>
+  Cases_on ‘m’ >- (
+    (* Contradiction: SUC n < 0 *)
+    sg ‘SUC n = 0’ >- decide_tac >>
+    fs [is_loop_def]
+  ) >>
+  fs [is_loop_def] >>
+  pop_assum mp_tac >>
+  PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
+  fs [] >>
+  DISCH_TAC >>
+  (* We just have to explore all the paths: we can have dedicated tactics for that
+     (we need to do case analysis) *)
+  Cases_on ‘ls’ >> fs [] >>
+  Cases_on ‘u32_to_int (i :u32) = (0 :int)’ >> fs [] >>
+  fs [st_ex_bind_def] >>
+  Cases_on ‘u32_sub (i :u32) (int_to_u32 (1 :int))’ >> fs [] >>
+  (* Apply the induction hypothesis *)
+  first_x_assum (qspecl_then [‘n'’, ‘l’, ‘a’] assume_tac) >>
+  first_x_assum imp_res_tac >>
+  pop_assum mp_tac >>
+  CASE_TAC
+QED
+
+Theorem nth_fuel_P_mono:
+  !n m ls i.
+    n <= m ==>
+    nth_fuel_P ls i n ==>
+    nth_fuel n ls i = nth_fuel m ls i
+Proof
+  rpt gen_tac >> rpt DISCH_TAC >>
+  fs [nth_fuel_P_def] >>
+  imp_res_tac nth_fuel_mono >>
+  pop_assum (qspecl_then [‘ls’, ‘i’] assume_tac) >>
+  pop_assum mp_tac >> CASE_TAC >> fs []
+QED
+
+Theorem nth_fuel_least_fail_mono:
+  !n ls i.
+    n < $LEAST (nth_fuel_P ls i) ==>
+    nth_fuel n ls i = Loop
+Proof
+  rpt gen_tac >>
+  disch_tac >>
+  imp_res_tac whileTheory.LESS_LEAST >>
+  fs [nth_fuel_P_def, is_loop_def] >>
+  pop_assum mp_tac >>
+  CASE_TAC
+QED
+
+Theorem nth_fuel_least_success_mono:
+  !n ls i.
+    $LEAST (nth_fuel_P ls i) <= n ==>
+    nth_fuel n ls i = nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
+Proof
+  rpt gen_tac >>
+  disch_tac >>
+  (* Case disjunction on whether there exists a fuel such that it terminates *)
+  Cases_on ‘?m. nth_fuel_P ls i m’ >- (
+    (* Terminates *)
+    irule EQ_SYM >>
+    irule nth_fuel_P_mono >> fs [] >>
+    (* Prove that calling with the least upper bound of fuel succeeds *)    
+    qspec_then ‘nth_fuel_P (ls :α list_t) (i :u32)’ imp_res_tac whileTheory.LEAST_EXISTS_IMP
+  ) >>
+  (* Doesn't terminate *)
+  fs [] >>
+  sg ‘~(nth_fuel_P ls i n)’ >- fs [] >>
+  sg ‘~(nth_fuel_P ls i ($LEAST (nth_fuel_P ls i)))’ >- fs [] >>
+  fs [nth_fuel_P_def, is_loop_def] >>
+  pop_assum mp_tac >> CASE_TAC >>
+  pop_assum mp_tac >>
+  pop_assum mp_tac >> CASE_TAC
+QED
+
+val nth_def_raw = Define ‘
+  nth ls i =
+    if (?n. nth_fuel_P ls i n) then nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
+    else Loop
+’
+
+(* This makes the proofs easier, in that it helps us control the context *)
+val nth_expand_def = Define ‘
+  nth_expand nth ls i =
+    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 tl i0
+        od
+    | ListNil => 
+      Fail Failure
+’             
+
+(* Prove the important theorems *)
+Theorem nth_def_terminates:
+  !ls i.
+  (?n. nth_fuel_P ls i n) ==>
+  nth ls i =
+    nth_expand nth ls i
+Proof
+  rpt strip_tac >>
+  fs [nth_expand_def] >>
+  PURE_ONCE_REWRITE_TAC [nth_def_raw] >>
+  (* Prove that the least upper bound is <= n *)
+  sg ‘$LEAST (nth_fuel_P ls i) <= n’ >-(
+    qspec_then ‘nth_fuel_P (ls :α list_t) (i :u32)’ imp_res_tac whileTheory.LEAST_EXISTS_IMP >>
+    spose_not_then assume_tac >> fs []
+  ) >>
+  (* Use the monotonicity theorem - TODO: ? *)
+  imp_res_tac nth_fuel_least_success_mono >>
+  (* Rewrite only on the left - TODO: easy way ?? *)
+  qspecl_then [‘$LEAST (nth_fuel_P ls i)’, ‘ls’, ‘i’] assume_tac nth_fuel_def >>
+  (* TODO: how to discard assumptions?? *)
+  fs [] >> pop_assum (fn _ => fs []) >>
+  (* Cases on the least upper bound *)
+  Cases_on ‘$LEAST (nth_fuel_P ls i)’ >> rw [] >- (
+    (* The bound is equal to 0: contradiction *)
+    sg ‘nth_fuel 0 ls i = Loop’ >- (PURE_ONCE_REWRITE_TAC [nth_fuel_def] >> rw []) >>
+    fs [nth_fuel_P_def, is_loop_def]
+  ) >>
+  (* Bound not equal to 0 *)
+  fs [nth_fuel_P_def, is_loop_def] >>
+  (* Explore all the paths *)
+  fs [st_ex_bind_def] >>
+  Cases_on ‘ls’ >> rw [] >> fs [] >>
+  Cases_on ‘u32_sub i (int_to_u32 1)’ >> rw [] >> fs [] >>
+  (* Recursive call: use monotonicity - we have an assumption which eliminates the Loop case *)
+  Cases_on ‘nth_fuel n' l a’ >> rw [] >> fs [] >>
+  (sg ‘nth_fuel_P l a n'’ >- fs [nth_fuel_P_def, is_loop_def]) >>
+  (sg ‘$LEAST (nth_fuel_P l a) <= n'’ >-(
+   qspec_then ‘nth_fuel_P l a’ imp_res_tac whileTheory.LEAST_EXISTS_IMP >>
+   spose_not_then assume_tac >> fs [])) >>
+  imp_res_tac nth_fuel_least_success_mono >> fs []
+QED
+
+(* Prove the important theorems *)
+Theorem nth_def_loop:
+  !ls i.
+  (!n. ~nth_fuel_P ls i n) ==>
+  nth ls i =
+    nth_expand nth ls i
+Proof
+  rpt gen_tac >>
+  PURE_ONCE_REWRITE_TAC [nth_def_raw] >>
+  strip_tac >> rw[] >>
+  (* Non-terminating case *)
+  sg ‘∀n. ¬nth_fuel_P ls i (SUC n)’ >- rw [] >>
+  fs [nth_fuel_P_def, is_loop_def] >>
+  pop_assum mp_tac >>
+  PURE_ONCE_REWRITE_TAC [nth_fuel_def] >>
+  rw [] >>  
+  fs [nth_expand_def] >>
+  (* Evaluate all the paths *)
+  fs [st_ex_bind_def] >>
+  Cases_on ‘ls’ >> rw [] >> fs [] >>
+  Cases_on ‘u32_sub i (int_to_u32 1)’ >> rw [] >> fs [] >>
+  (* Use the definition of nth *)
+  rw [nth_def_raw] >>
+  first_x_assum (qspec_then ‘$LEAST (nth_fuel_P l a)’ assume_tac) >>
+  Cases_on ‘nth_fuel ($LEAST (nth_fuel_P l a)) l a’ >> fs []
+QED
+
+(* The final theorem *)
+Theorem nth_def:
+  !ls i.
+  nth ls i =
+    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 tl i0
+        od
+    | ListNil => 
+      Fail Failure
+Proof
+  rpt strip_tac >>
+  Cases_on ‘?n. nth_fuel_P ls i n’ >-(
+    assume_tac nth_def_terminates >>
+    fs [nth_expand_def] >>
+    pop_assum irule >>
+    metis_tac []) >>
+  fs [] >> imp_res_tac nth_def_loop >> fs [nth_expand_def]
+QED
+
+(*
+
+Je viens de finir ma petite expérimentation avec le fuel : ça marche bien. Par exemple, si je pose les définitions suivantes :
+Datatype:
+  result = Return 'a | Fail error | Loop
+End
+
+(* Omitting some definitions like the bind *)
+
+val _ = Define ‘
+ nth_fuel (n : num) (ls : 't list_t) (i : u32) : 't result =
+  case n of
+  | 0 => Loop
+  | SUC n => 
+    do 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_fuel n tl i0
+        od
+    | ListNil => 
+      Fail Failure
+    od
+ ’
+
+val _ = Define 'is_loop r = case r of Loop => T | _ => F'
+ 
+val _ = Define 'nth_fuel_P ls i n = ~is_loop (nth_fuel n ls i)'
+
+(* $LEAST returns the least upper bound for a predicate (if it exists - otherwise it returns an arbitrary number) *)
+val _ = Define ‘
+  nth ls i =
+    if (?n. nth_fuel_P ls i n) then nth_fuel ($LEAST (nth_fuel_P ls i)) ls i
+    else Loop
+’
+J'arrive à montrer (c'est un chouïa technique) :
+Theorem nth_def:
+  !ls i.
+  nth ls i =
+    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 tl i0
+        od
+    | ListNil => 
+      Fail Failure
+
+*)