Update the demo

4 files changed, 126 insertions, 30 deletions

diff --git a/tests/coq/demo/Demo.v b/tests/coq/demo/Demo.v
index ec7ca29d..48067c02 100644
--- a/tests/coq/demo/Demo.v
+++ b/tests/coq/demo/Demo.v
@@ -34,8 +34,14 @@ Definition use_mul2_add1 (x : u32) (y : u32) : result u32 :=
 Definition incr (x : u32) : result u32 :=
   u32_add x 1%u32.
 
+(** [demo::use_incr]:
+    Source: 'src/demo.rs', lines 25:0-25:17 *)
+Definition use_incr : result unit :=
+  i <- incr 0%u32; i1 <- incr i; _ <- incr i1; Return tt
+.
+
 (** [demo::CList]
-    Source: 'src/demo.rs', lines 27:0-27:17 *)
+    Source: 'src/demo.rs', lines 34:0-34:17 *)
 Inductive CList_t (T : Type) :=
 | CList_CCons : T -> CList_t T -> CList_t T
 | CList_CNil : CList_t T
@@ -45,7 +51,7 @@ Arguments CList_CCons { _ }.
 Arguments CList_CNil { _ }.
 
 (** [demo::list_nth]:
-    Source: 'src/demo.rs', lines 32:0-32:56 *)
+    Source: 'src/demo.rs', lines 39:0-39:56 *)
 Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
   match n with
   | O => Fail_ OutOfFuel
@@ -61,7 +67,7 @@ Fixpoint list_nth (T : Type) (n : nat) (l : CList_t T) (i : u32) : result T :=
 .
 
 (** [demo::list_nth_mut]:
-    Source: 'src/demo.rs', lines 47:0-47:68 *)
+    Source: 'src/demo.rs', lines 54:0-54:68 *)
 Fixpoint list_nth_mut
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -89,7 +95,7 @@ Fixpoint list_nth_mut
 .
 
 (** [demo::list_nth_mut1]: loop 0:
-    Source: 'src/demo.rs', lines 62:0-71:1 *)
+    Source: 'src/demo.rs', lines 69:0-78:1 *)
 Fixpoint list_nth_mut1_loop
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -116,7 +122,7 @@ Fixpoint list_nth_mut1_loop
 .
 
 (** [demo::list_nth_mut1]:
-    Source: 'src/demo.rs', lines 62:0-62:77 *)
+    Source: 'src/demo.rs', lines 69:0-69:77 *)
 Definition list_nth_mut1
   (T : Type) (n : nat) (l : CList_t T) (i : u32) :
   result (T * (T -> result (CList_t T)))
@@ -125,7 +131,7 @@ Definition list_nth_mut1
 .
 
 (** [demo::i32_id]:
-    Source: 'src/demo.rs', lines 73:0-73:28 *)
+    Source: 'src/demo.rs', lines 80:0-80:28 *)
 Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
   match n with
   | O => Fail_ OutOfFuel
@@ -136,8 +142,30 @@ Fixpoint i32_id (n : nat) (i : i32) : result i32 :=
   end
 .
 
+(** [demo::list_tail]:
+    Source: 'src/demo.rs', lines 88:0-88:64 *)
+Fixpoint list_tail
+  (T : Type) (n : nat) (l : CList_t T) :
+  result ((CList_t T) * (CList_t T -> result (CList_t T)))
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match l with
+    | CList_CCons t tl =>
+      p <- list_tail T n1 tl;
+      let (c, list_tail_back) := p in
+      let back_'a :=
+        fun (ret : CList_t T) =>
+          tl1 <- list_tail_back ret; Return (CList_CCons t tl1) in
+      Return (c, back_'a)
+    | CList_CNil => Return (CList_CNil, Return)
+    end
+  end
+.
+
 (** Trait declaration: [demo::Counter]
-    Source: 'src/demo.rs', lines 83:0-83:17 *)
+    Source: 'src/demo.rs', lines 97:0-97:17 *)
 Record Counter_t (Self : Type) := mkCounter_t {
   Counter_t_incr : Self -> result (usize * Self);
 }.
@@ -146,19 +174,19 @@ Arguments mkCounter_t { _ }.
 Arguments Counter_t_incr { _ }.
 
 (** [demo::{(demo::Counter for usize)}::incr]:
-    Source: 'src/demo.rs', lines 88:4-88:31 *)
+    Source: 'src/demo.rs', lines 102:4-102:31 *)
 Definition counterUsize_incr (self : usize) : result (usize * usize) :=
   self1 <- usize_add self 1%usize; Return (self, self1)
 .
 
 (** Trait implementation: [demo::{(demo::Counter for usize)}]
-    Source: 'src/demo.rs', lines 87:0-87:22 *)
+    Source: 'src/demo.rs', lines 101:0-101:22 *)
 Definition CounterUsize : Counter_t usize := {|
   Counter_t_incr := counterUsize_incr;
 |}.
 
 (** [demo::use_counter]:
-    Source: 'src/demo.rs', lines 95:0-95:59 *)
+    Source: 'src/demo.rs', lines 109:0-109:59 *)
 Definition use_counter
   (T : Type) (counterInst : Counter_t T) (cnt : T) : result (usize * T) :=
   counterInst.(Counter_t_incr) cnt
diff --git a/tests/fstar/demo/Demo.fst b/tests/fstar/demo/Demo.fst
index d13d2ba3..5651b80f 100644
--- a/tests/fstar/demo/Demo.fst
+++ b/tests/fstar/demo/Demo.fst
@@ -28,14 +28,19 @@ let use_mul2_add1 (x : u32) (y : u32) : result u32 =
 let incr (x : u32) : result u32 =
   u32_add x 1
 
+(** [demo::use_incr]:
+    Source: 'src/demo.rs', lines 25:0-25:17 *)
+let use_incr : result unit =
+  let* i = incr 0 in let* i1 = incr i in let* _ = incr i1 in Return ()
+
 (** [demo::CList]
-    Source: 'src/demo.rs', lines 27:0-27:17 *)
+    Source: 'src/demo.rs', lines 34:0-34:17 *)
 type cList_t (t : Type0) =
 | CList_CCons : t -> cList_t t -> cList_t t
 | CList_CNil : cList_t t
 
 (** [demo::list_nth]:
-    Source: 'src/demo.rs', lines 32:0-32:56 *)
+    Source: 'src/demo.rs', lines 39:0-39:56 *)
 let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
   if is_zero n
   then Fail OutOfFuel
@@ -48,7 +53,7 @@ let rec list_nth (t : Type0) (n : nat) (l : cList_t t) (i : u32) : result t =
     end
 
 (** [demo::list_nth_mut]:
-    Source: 'src/demo.rs', lines 47:0-47:68 *)
+    Source: 'src/demo.rs', lines 54:0-54:68 *)
 let rec list_nth_mut
   (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
   result (t & (t -> result (cList_t t)))
@@ -74,7 +79,7 @@ let rec list_nth_mut
     end
 
 (** [demo::list_nth_mut1]: loop 0:
-    Source: 'src/demo.rs', lines 62:0-71:1 *)
+    Source: 'src/demo.rs', lines 69:0-78:1 *)
 let rec list_nth_mut1_loop
   (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
   result (t & (t -> result (cList_t t)))
@@ -99,7 +104,7 @@ let rec list_nth_mut1_loop
     end
 
 (** [demo::list_nth_mut1]:
-    Source: 'src/demo.rs', lines 62:0-62:77 *)
+    Source: 'src/demo.rs', lines 69:0-69:77 *)
 let list_nth_mut1
   (t : Type0) (n : nat) (l : cList_t t) (i : u32) :
   result (t & (t -> result (cList_t t)))
@@ -107,7 +112,7 @@ let list_nth_mut1
   let* (x, back_'a) = list_nth_mut1_loop t n l i in Return (x, back_'a)
 
 (** [demo::i32_id]:
-    Source: 'src/demo.rs', lines 73:0-73:28 *)
+    Source: 'src/demo.rs', lines 80:0-80:28 *)
 let rec i32_id (n : nat) (i : i32) : result i32 =
   if is_zero n
   then Fail OutOfFuel
@@ -117,21 +122,41 @@ let rec i32_id (n : nat) (i : i32) : result i32 =
     then Return 0
     else let* i1 = i32_sub i 1 in let* i2 = i32_id n1 i1 in i32_add i2 1
 
+(** [demo::list_tail]:
+    Source: 'src/demo.rs', lines 88:0-88:64 *)
+let rec list_tail
+  (t : Type0) (n : nat) (l : cList_t t) :
+  result ((cList_t t) & (cList_t t -> result (cList_t t)))
+  =
+  if is_zero n
+  then Fail OutOfFuel
+  else
+    let n1 = decrease n in
+    begin match l with
+    | CList_CCons x tl ->
+      let* (c, list_tail_back) = list_tail t n1 tl in
+      let back_'a =
+        fun ret -> let* tl1 = list_tail_back ret in Return (CList_CCons x tl1)
+        in
+      Return (c, back_'a)
+    | CList_CNil -> Return (CList_CNil, Return)
+    end
+
 (** Trait declaration: [demo::Counter]
-    Source: 'src/demo.rs', lines 83:0-83:17 *)
+    Source: 'src/demo.rs', lines 97:0-97:17 *)
 noeq type counter_t (self : Type0) = { incr : self -> result (usize & self); }
 
 (** [demo::{(demo::Counter for usize)}::incr]:
-    Source: 'src/demo.rs', lines 88:4-88:31 *)
+    Source: 'src/demo.rs', lines 102:4-102:31 *)
 let counterUsize_incr (self : usize) : result (usize & usize) =
   let* self1 = usize_add self 1 in Return (self, self1)
 
 (** Trait implementation: [demo::{(demo::Counter for usize)}]
-    Source: 'src/demo.rs', lines 87:0-87:22 *)
+    Source: 'src/demo.rs', lines 101:0-101:22 *)
 let counterUsize : counter_t usize = { incr = counterUsize_incr; }
 
 (** [demo::use_counter]:
-    Source: 'src/demo.rs', lines 95:0-95:59 *)
+    Source: 'src/demo.rs', lines 109:0-109:59 *)
 let use_counter
   (t : Type0) (counterInst : counter_t t) (cnt : t) : result (usize & t) =
   counterInst.incr cnt
diff --git a/tests/lean/Demo/Demo.lean b/tests/lean/Demo/Demo.lean
index 854b4853..f38b5cd3 100644
--- a/tests/lean/Demo/Demo.lean
+++ b/tests/lean/Demo/Demo.lean
@@ -36,14 +36,23 @@ def use_mul2_add1 (x : U32) (y : U32) : Result U32 :=
 def incr (x : U32) : Result U32 :=
   x + 1#u32
 
+/- [demo::use_incr]:
+   Source: 'src/demo.rs', lines 25:0-25:17 -/
+def use_incr : Result Unit :=
+  do
+  let i ← incr 0#u32
+  let i1 ← incr i
+  let _ ← incr i1
+  Result.ret ()
+
 /- [demo::CList]
-   Source: 'src/demo.rs', lines 27:0-27:17 -/
+   Source: 'src/demo.rs', lines 34:0-34:17 -/
 inductive CList (T : Type) :=
 | CCons : T → CList T → CList T
 | CNil : CList T
 
 /- [demo::list_nth]:
-   Source: 'src/demo.rs', lines 32:0-32:56 -/
+   Source: 'src/demo.rs', lines 39:0-39:56 -/
 divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   match l with
   | CList.CCons x tl =>
@@ -55,7 +64,7 @@ divergent def list_nth (T : Type) (l : CList T) (i : U32) : Result T :=
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut]:
-   Source: 'src/demo.rs', lines 47:0-47:68 -/
+   Source: 'src/demo.rs', lines 54:0-54:68 -/
 divergent def list_nth_mut
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -79,7 +88,7 @@ divergent def list_nth_mut
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]: loop 0:
-   Source: 'src/demo.rs', lines 62:0-71:1 -/
+   Source: 'src/demo.rs', lines 69:0-78:1 -/
 divergent def list_nth_mut1_loop
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -102,7 +111,7 @@ divergent def list_nth_mut1_loop
   | CList.CNil => Result.fail .panic
 
 /- [demo::list_nth_mut1]:
-   Source: 'src/demo.rs', lines 62:0-62:77 -/
+   Source: 'src/demo.rs', lines 69:0-69:77 -/
 def list_nth_mut1
   (T : Type) (l : CList T) (i : U32) :
   Result (T × (T → Result (CList T)))
@@ -112,7 +121,7 @@ def list_nth_mut1
   Result.ret (t, back_'a)
 
 /- [demo::i32_id]:
-   Source: 'src/demo.rs', lines 73:0-73:28 -/
+   Source: 'src/demo.rs', lines 80:0-80:28 -/
 divergent def i32_id (i : I32) : Result I32 :=
   if i = 0#i32
   then Result.ret 0#i32
@@ -121,26 +130,44 @@ divergent def i32_id (i : I32) : Result I32 :=
        let i2 ← i32_id i1
        i2 + 1#i32
 
+/- [demo::list_tail]:
+   Source: 'src/demo.rs', lines 88:0-88:64 -/
+divergent def list_tail
+  (T : Type) (l : CList T) :
+  Result ((CList T) × (CList T → Result (CList T)))
+  :=
+  match l with
+  | CList.CCons t tl =>
+    do
+    let (c, list_tail_back) ← list_tail T tl
+    let back_'a :=
+      fun ret =>
+        do
+        let tl1 ← list_tail_back ret
+        Result.ret (CList.CCons t tl1)
+    Result.ret (c, back_'a)
+  | CList.CNil => Result.ret (CList.CNil, Result.ret)
+
 /- Trait declaration: [demo::Counter]
-   Source: 'src/demo.rs', lines 83:0-83:17 -/
+   Source: 'src/demo.rs', lines 97:0-97:17 -/
 structure Counter (Self : Type) where
   incr : Self → Result (Usize × Self)
 
 /- [demo::{(demo::Counter for usize)}::incr]:
-   Source: 'src/demo.rs', lines 88:4-88:31 -/
+   Source: 'src/demo.rs', lines 102:4-102:31 -/
 def CounterUsize.incr (self : Usize) : Result (Usize × Usize) :=
   do
   let self1 ← self + 1#usize
   Result.ret (self, self1)
 
 /- Trait implementation: [demo::{(demo::Counter for usize)}]
-   Source: 'src/demo.rs', lines 87:0-87:22 -/
+   Source: 'src/demo.rs', lines 101:0-101:22 -/
 def CounterUsize : Counter Usize := {
   incr := CounterUsize.incr
 }
 
 /- [demo::use_counter]:
-   Source: 'src/demo.rs', lines 95:0-95:59 -/
+   Source: 'src/demo.rs', lines 109:0-109:59 -/
 def use_counter
   (T : Type) (CounterInst : Counter T) (cnt : T) : Result (Usize × T) :=
   CounterInst.incr cnt
diff --git a/tests/lean/Demo/Properties.lean b/tests/lean/Demo/Properties.lean
index cdec7332..e514ac3e 100644
--- a/tests/lean/Demo/Properties.lean
+++ b/tests/lean/Demo/Properties.lean
@@ -65,4 +65,20 @@ theorem i32_id_spec (x : I32) (h : 0 ≤ x.val) :
 termination_by x.val.toNat
 decreasing_by scalar_decr_tac
 
+theorem list_tail_spec {T : Type} [Inhabited T] (l : CList T) :
+  ∃ back, list_tail T l = ret (CList.CNil, back) ∧
+  ∀ tl', ∃ l', back tl' = ret l' ∧ l'.to_list = l.to_list ++ tl'.to_list := by
+  rw [list_tail]
+  match l with
+  | CNil =>
+    simp_all
+  | CCons hd tl =>
+    simp_all
+    progress as ⟨ back ⟩
+    simp
+    -- Proving the backward function
+    intro tl'
+    progress
+    simp_all
+
 end demo