Improve the extraction and the Lean backend

backends/lean/Aeneas/List/List.lean

@@ -51,7 +51,6 @@ theorem indexOpt_eq_index [Inhabited α] (ls : List α) (i : Nat) :
     else by
       have hi := indexOpt_eq_index tl (i - 1)
       simp [*]; intros
-      -- TODO: there seems to be syntax errors if we don't put the parentheses below??
       apply hi; int_tac
 
 -- Remark: the list is unchanged if the index is not in bounds
@@ -313,27 +312,12 @@ theorem length_flatten_update_as_int_eq {α : Type u} (ls : List (List α)) (i :
 @[simp]
 theorem index_map_eq {α : Type u} {β : Type v} [Inhabited α] [Inhabited β]
   (ls : List α) (i : Nat) (f : α → β)
-  (h1 : i < ls.length) :
+  (h1 : i < ls.length) : -- We need the bound because otherwise we have to prove that: `(default : β) = f (default : α)`
   (ls.map f).index i = f (ls.index i) := by
   revert i; induction ls <;> simp_all
   intro i h
   cases i <;> simp_all
 
-@[simp]
-theorem index_nat_map_eq {α : Type u} {β : Type v} [Inhabited α] [Inhabited β]
-  (ls : List α) (i : Nat) (f : α → β)
-  (h1 : i < ls.length) :
-  (ls.map f).index i = f (ls.index i) := by
-  match ls with
-  | [] => simp at h1
-  | hd :: tl =>
-    if h : i = 0 then
-      simp [*]
-    else
-      have hi := index_nat_map_eq tl (i - 1) f (by simp at h1; int_tac)
-      have : (i : Nat) - 1 < tl.length := by simp_all; scalar_tac
-      simp [*]
-
 theorem replace_slice_index [Inhabited α] (start end_ : Nat) (l nl : List α)
   (_ : start < end_) (_ : end_ ≤ l.length) (_ : nl.length = end_ - start) :
   let l1 := l.replace_slice start end_ nl

backends/lean/Aeneas/Progress/Progress.lean

@@ -585,7 +585,7 @@ namespace Test
   def add (x y : U32) : Result U32 := x + y
 
   @[pspec] -- TODO: give the possibility of using pspec as a local attribute
-  theorem add_spec x y (h : x.val + y.val ≤ U32.max) :
+  theorem add_spec (x y : U32) (h : x.val + y.val ≤ U32.max) :
     let tot := x.val + y.val
     ∃ z, add x y = ok z ∧ z.val = tot := by
     rw [add]

backends/lean/Aeneas/ScalarTac/ScalarTac.lean

@@ -87,11 +87,11 @@ example (x : U32 × U32) : 0 ≤ x.fst.val := by
   scalar_tac
 
 -- Checking that we properly handle [ofInt]
-example : U32.ofInt 1 ≤ U32.max := by
+example : (U32.ofInt 1).val ≤ U32.max := by
   scalar_tac
 
 example (x : Int) (h0 : 0 ≤ x) (h1 : x ≤ U32.max) :
-  U32.ofIntCore x (by constructor <;> scalar_tac) ≤ U32.max := by
+  (U32.ofIntCore x (by constructor <;> scalar_tac)).val ≤ U32.max := by
   scalar_tac_preprocess
   scalar_tac
 
@@ -119,8 +119,8 @@ example (x y : Nat) (z : Int) (h : Int.subNatNat x y + z = 0) : (x : Int) - (y :
   scalar_tac_preprocess
   omega
 
-example (x : U32) (h : 16 * ↑x ≤ U32.max) :
-  4 * U32.ofInt (4 * x.val) (by scalar_tac) ≤ U32.max := by
+example (x : U32) (h : 16 * x.val ≤ U32.max) :
+  4 * (U32.ofInt (4 * x.val) (by scalar_tac)).val ≤ U32.max := by
   scalar_tac
 
 example (b : Bool) (x y : Int) (h : if b then P ∧ x + y < 3 else x + y < 4) : x + y < 5 := by
@@ -134,10 +134,10 @@ example
   (_ : c0u.val = c0.val)
   (s1 : U32)
   (c1 : Bool)
-  (hConv1 : if ↑xi + ↑c0u > U32.max then ↑s1 = ↑xi + ↑c0u - U32.max - 1 ∧ c1 = true else s1 = xi.val + c0u ∧ c1 = false)
+  (hConv1 : if xi.val + c0u.val > U32.max then s1.val = ↑xi + ↑c0u - U32.max - 1 ∧ c1 = true else s1 = xi.val + c0u ∧ c1 = false)
   (s2 : U32)
   (c2 : Bool)
-  (hConv2 : if ↑s1 + ↑yi > U32.max then ↑s2 = ↑s1 + ↑yi - U32.max - 1 ∧ c2 = true else s2 = s1.val + yi ∧ c2 = false)
+  (hConv2 : if s1.val + yi.val > U32.max then s2.val = ↑s1 + ↑yi - U32.max - 1 ∧ c2 = true else s2 = s1.val + yi ∧ c2 = false)
   (c1u : U8)
   (_ : c1u.val = if c1 = true then 1 else 0)
   (c2u : U8)

backends/lean/Aeneas/Std/ArraySlice.lean

@@ -119,14 +119,14 @@ theorem Array.update_length {α : Type u} {n : Usize} (v: Array α n) (i: Usize)
 theorem Array.update_usize_spec {α : Type u} {n : Usize} (v: Array α n) (i: Usize) (x : α)
   (hbound : i.toNat < v.length) :
   ∃ nv, v.update_usize i x = ok nv ∧
-  nv.val = v.val.update i.toNat x
+  nv = v.update i x
   := by
   simp only [update_usize]
   have h := List.indexOpt_bounds v.val i.toNat
   split
   . simp_all [length]
     scalar_tac
-  . simp_all
+  . simp [Array.update]
 
 def Array.index_mut_usize {α : Type u} {n : Usize} (v: Array α n) (i: Usize) :
   Result (α × (α -> Array α n)) := do
@@ -171,7 +171,7 @@ abbrev Slice.v {α : Type u} (v : Slice α) : List α := v.val
 example {a: Type u} (v : Slice a) : v.length ≤ Scalar.max ScalarTy.Usize := by
   scalar_tac
 
-def Slice.new (α : Type u) : Slice α := ⟨ [], by apply Scalar.cMax_suffices .Usize; simp ⟩
+def Slice.new (α : Type u) : Slice α := ⟨ [], by simp ⟩
 
 -- TODO: very annoying that the α is an explicit parameter
 abbrev Slice.len {α : Type u} (v : Slice α) : Usize :=
@@ -230,13 +230,13 @@ theorem Slice.update_length {α : Type u} (v: Slice α) (i: Usize) (x: α) :
 theorem Slice.update_usize_spec {α : Type u} (v: Slice α) (i: Usize) (x : α)
   (hbound : i.toNat < v.length) :
   ∃ nv, v.update_usize i x = ok nv ∧
-  nv.val = v.val.update i.toNat x
+  nv = v.update i x
   := by
   simp only [update_usize]
   have h := List.indexOpt_bounds v.val i.toNat
   split
   . simp_all [length]; scalar_tac
-  . simp_all
+  . simp [Slice.update]
 
 def Slice.index_mut_usize {α : Type u} (v: Slice α) (i: Usize) :
   Result (α × (α → Slice α)) := do

backends/lean/Aeneas/Std/Scalar.lean

@@ -392,27 +392,27 @@ theorem Scalar.add_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
   apply add_spec <;> assumption
 
 /- Fine-grained theorems -/
-@[pspec] theorem Usize.add_spec {x y : Usize} (hmax : ↑x + ↑y ≤ Usize.max) :
+@[pspec] theorem Usize.add_spec {x y : Usize} (hmax : x.val + y.val ≤ Usize.max) :
   ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
-@[pspec] theorem U8.add_spec {x y : U8} (hmax : ↑x + ↑y ≤ U8.max) :
+@[pspec] theorem U8.add_spec {x y : U8} (hmax : x.val + y.val ≤ U8.max) :
   ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
-@[pspec] theorem U16.add_spec {x y : U16} (hmax : ↑x + ↑y ≤ U16.max) :
+@[pspec] theorem U16.add_spec {x y : U16} (hmax : x.val + y.val ≤ U16.max) :
   ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
-@[pspec] theorem U32.add_spec {x y : U32} (hmax : ↑x + ↑y ≤ U32.max) :
+@[pspec] theorem U32.add_spec {x y : U32} (hmax : x.val + y.val ≤ U32.max) :
   ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
-@[pspec] theorem U64.add_spec {x y : U64} (hmax : ↑x + ↑y ≤ U64.max) :
+@[pspec] theorem U64.add_spec {x y : U64} (hmax : x.val + y.val ≤ U64.max) :
   ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
-@[pspec] theorem U128.add_spec {x y : U128} (hmax : ↑x + ↑y ≤ U128.max) :
+@[pspec] theorem U128.add_spec {x y : U128} (hmax : x.val + y.val ≤ U128.max) :
   ∃ z, x + y = ok z ∧ (↑z : Int) = ↑x + ↑y := by
   apply Scalar.add_unsigned_spec <;> simp [ScalarTy.isSigned, Scalar.max, *]
 
@@ -487,27 +487,27 @@ theorem Scalar.sub_unsigned_spec {ty : ScalarTy} (s : ¬ ty.isSigned)
   apply sub_spec <;> assumption
 
 /- Fine-grained theorems -/
-@[pspec] theorem Usize.sub_spec {x y : Usize} (hmin : Usize.min ≤ ↑x - ↑y) :
+@[pspec] theorem Usize.sub_spec {x y : Usize} (hmin : Usize.min ≤ x.val - y.val) :
   ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
-  apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
+  apply Scalar.sub_unsigned_spec <;> simp [Scalar.min, ScalarTy.isSigned]; omega
 
-@[pspec] theorem U8.sub_spec {x y : U8} (hmin : U8.min ≤ ↑x - ↑y) :
+@[pspec] theorem U8.sub_spec {x y : U8} (hmin : U8.min ≤ x.val - y.val) :
   ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
-@[pspec] theorem U16.sub_spec {x y : U16} (hmin : U16.min ≤ ↑x - ↑y) :
+@[pspec] theorem U16.sub_spec {x y : U16} (hmin : U16.min ≤ x.val - y.val) :
   ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
-@[pspec] theorem U32.sub_spec {x y : U32} (hmin : U32.min ≤ ↑x - ↑y) :
+@[pspec] theorem U32.sub_spec {x y : U32} (hmin : U32.min ≤ x.val - y.val) :
   ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
-@[pspec] theorem U64.sub_spec {x y : U64} (hmin : U64.min ≤ ↑x - ↑y) :
+@[pspec] theorem U64.sub_spec {x y : U64} (hmin : U64.min ≤ x.val - y.val) :
   ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
-@[pspec] theorem U128.sub_spec {x y : U128} (hmin : U128.min ≤ ↑x - ↑y) :
+@[pspec] theorem U128.sub_spec {x y : U128} (hmin : U128.min ≤ x.val - y.val) :
   ∃ z, x - y = ok z ∧ (↑z : Int) = ↑x - ↑y := by
   apply Scalar.sub_unsigned_spec <;> simp_all [Scalar.min, ScalarTy.isSigned]
 
@@ -583,27 +583,27 @@ theorem Scalar.mul_unsigned_spec {ty} (s: ¬ ty.isSigned) {x y : Scalar ty}
   apply mul_spec <;> assumption
 
 /- Fine-grained theorems -/
-@[pspec] theorem Usize.mul_spec {x y : Usize} (hmax : ↑x * ↑y ≤ Usize.max) :
+@[pspec] theorem Usize.mul_spec {x y : Usize} (hmax : x.val * y.val ≤ Usize.max) :
   ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
-@[pspec] theorem U8.mul_spec {x y : U8} (hmax : ↑x * ↑y ≤ U8.max) :
+@[pspec] theorem U8.mul_spec {x y : U8} (hmax : x.val * y.val ≤ U8.max) :
   ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
-@[pspec] theorem U16.mul_spec {x y : U16} (hmax : ↑x * ↑y ≤ U16.max) :
+@[pspec] theorem U16.mul_spec {x y : U16} (hmax : x.val * y.val ≤ U16.max) :
   ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
-@[pspec] theorem U32.mul_spec {x y : U32} (hmax : ↑x * ↑y ≤ U32.max) :
+@[pspec] theorem U32.mul_spec {x y : U32} (hmax : x.val * y.val ≤ U32.max) :
   ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
-@[pspec] theorem U64.mul_spec {x y : U64} (hmax : ↑x * ↑y ≤ U64.max) :
+@[pspec] theorem U64.mul_spec {x y : U64} (hmax : x.val * y.val ≤ U64.max) :
   ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
-@[pspec] theorem U128.mul_spec {x y : U128} (hmax : ↑x * ↑y ≤ U128.max) :
+@[pspec] theorem U128.mul_spec {x y : U128} (hmax : x.val * y.val ≤ U128.max) :
   ∃ z, x * y = ok z ∧ (↑z : Int) = ↑x * ↑y := by
   apply Scalar.mul_unsigned_spec <;> simp_all [Scalar.max, ScalarTy.isSigned]
 
@@ -1349,81 +1349,81 @@ theorem core.num.Usize.saturating_sub_spec (x y : Usize) :
 def Scalar.wrapping_add {ty} (x y : Scalar ty) : Scalar ty := sorry
 
 /- [core::num::{u8}::wrapping_add] -/
-def core.num.U8.wrapping_add := @Scalar.wrapping_add ScalarTy.U8
+def core.num.U8.wrapping_add : U8 → U8 → U8 := @Scalar.wrapping_add ScalarTy.U8
 
 /- [core::num::{u16}::wrapping_add] -/
-def core.num.U16.wrapping_add := @Scalar.wrapping_add ScalarTy.U16
+def core.num.U16.wrapping_add : U16 → U16 → U16  := @Scalar.wrapping_add ScalarTy.U16
 
 /- [core::num::{u32}::wrapping_add] -/
-def core.num.U32.wrapping_add := @Scalar.wrapping_add ScalarTy.U32
+def core.num.U32.wrapping_add : U32 → U32 → U32  := @Scalar.wrapping_add ScalarTy.U32
 
 /- [core::num::{u64}::wrapping_add] -/
-def core.num.U64.wrapping_add := @Scalar.wrapping_add ScalarTy.U64
+def core.num.U64.wrapping_add : U64 → U64 → U64  := @Scalar.wrapping_add ScalarTy.U64
 
 /- [core::num::{u128}::wrapping_add] -/
-def core.num.U128.wrapping_add := @Scalar.wrapping_add ScalarTy.U128
+def core.num.U128.wrapping_add : U128 → U128 → U128 := @Scalar.wrapping_add ScalarTy.U128
 
 /- [core::num::{usize}::wrapping_add] -/
-def core.num.Usize.wrapping_add := @Scalar.wrapping_add ScalarTy.Usize
+def core.num.Usize.wrapping_add : Usize → Usize → Usize  := @Scalar.wrapping_add ScalarTy.Usize
 
 /- [core::num::{i8}::wrapping_add] -/
-def core.num.I8.wrapping_add := @Scalar.wrapping_add ScalarTy.I8
+def core.num.I8.wrapping_add : I8 → I8 → I8  := @Scalar.wrapping_add ScalarTy.I8
 
 /- [core::num::{i16}::wrapping_add] -/
-def core.num.I16.wrapping_add := @Scalar.wrapping_add ScalarTy.I16
+def core.num.I16.wrapping_add : I16 → I16 → I16  := @Scalar.wrapping_add ScalarTy.I16
 
 /- [core::num::{i32}::wrapping_add] -/
-def core.num.I32.wrapping_add := @Scalar.wrapping_add ScalarTy.I32
+def core.num.I32.wrapping_add : I32 → I32 → I32  := @Scalar.wrapping_add ScalarTy.I32
 
 /- [core::num::{i64}::wrapping_add] -/
-def core.num.I64.wrapping_add := @Scalar.wrapping_add ScalarTy.I64
+def core.num.I64.wrapping_add : I64 → I64 → I64 := @Scalar.wrapping_add ScalarTy.I64
 
 /- [core::num::{i128}::wrapping_add] -/
-def core.num.I128.wrapping_add := @Scalar.wrapping_add ScalarTy.I128
+def core.num.I128.wrapping_add : I128 → I128 → I128  := @Scalar.wrapping_add ScalarTy.I128
 
 /- [core::num::{isize}::wrapping_add] -/
-def core.num.Isize.wrapping_add := @Scalar.wrapping_add ScalarTy.Isize
+def core.num.Isize.wrapping_add : Isize → Isize → Isize  := @Scalar.wrapping_add ScalarTy.Isize
 
 -- TODO: reasoning lemmas for wrapping add
 
 -- Wrapping sub
 def Scalar.wrapping_sub {ty} (x y : Scalar ty) : Scalar ty := sorry
 
 /- [core::num::{u8}::wrapping_sub] -/
-def core.num.U8.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U8
+def core.num.U8.wrapping_sub : U8 → U8 → U8 := @Scalar.wrapping_sub ScalarTy.U8
 
 /- [core::num::{u16}::wrapping_sub] -/
-def core.num.U16.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U16
+def core.num.U16.wrapping_sub : U16 → U16 → U16 := @Scalar.wrapping_sub ScalarTy.U16
 
 /- [core::num::{u32}::wrapping_sub] -/
-def core.num.U32.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U32
+def core.num.U32.wrapping_sub : U32 → U32 → U32 := @Scalar.wrapping_sub ScalarTy.U32
 
 /- [core::num::{u64}::wrapping_sub] -/
-def core.num.U64.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U64
+def core.num.U64.wrapping_sub : U64 → U64 → U64 := @Scalar.wrapping_sub ScalarTy.U64
 
 /- [core::num::{u128}::wrapping_sub] -/
-def core.num.U128.wrapping_sub := @Scalar.wrapping_sub ScalarTy.U128
+def core.num.U128.wrapping_sub : U128 → U128 → U128 := @Scalar.wrapping_sub ScalarTy.U128
 
 /- [core::num::{usize}::wrapping_sub] -/
-def core.num.Usize.wrapping_sub := @Scalar.wrapping_sub ScalarTy.Usize
+def core.num.Usize.wrapping_sub : Usize → Usize → Usize := @Scalar.wrapping_sub ScalarTy.Usize
 
 /- [core::num::{i8}::wrapping_sub] -/
-def core.num.I8.wrapping_sub := @Scalar.wrapping_sub ScalarTy.I8
+def core.num.I8.wrapping_sub : I8 → I8 → I8 := @Scalar.wrapping_sub ScalarTy.I8
 
 /- [core::num::{i16}::wrapping_sub] -/
-def core.num.I16.wrapping_sub := @Scalar.wrapping_sub ScalarTy.I16
+def core.num.I16.wrapping_sub : I16 → I16 → I16 := @Scalar.wrapping_sub ScalarTy.I16
 
 /- [core::num::{i32}::wrapping_sub] -/
-def core.num.I32.wrapping_sub := @Scalar.wrapping_sub ScalarTy.I32
+def core.num.I32.wrapping_sub : I32 → I32 → I32 := @Scalar.wrapping_sub ScalarTy.I32
 
 /- [core::num::{i64}::wrapping_sub] -/
-def core.num.I64.wrapping_sub := @Scalar.wrapping_sub ScalarTy.I64
+def core.num.I64.wrapping_sub : I64 → I64 → I64 := @Scalar.wrapping_sub ScalarTy.I64
 
 /- [core::num::{i128}::wrapping_sub] -/
-def core.num.I128.wrapping_sub := @Scalar.wrapping_sub ScalarTy.I128
+def core.num.I128.wrapping_sub : I128 → I128 → I128 := @Scalar.wrapping_sub ScalarTy.I128
 
 /- [core::num::{isize}::wrapping_sub] -/
-def core.num.Isize.wrapping_sub := @Scalar.wrapping_sub ScalarTy.Isize
+def core.num.Isize.wrapping_sub : Isize → Isize → Isize := @Scalar.wrapping_sub ScalarTy.Isize
 
 -- TODO: reasoning lemmas for wrapping sub