Merge pull request #419 from AeneasVerif/son/lean1

Reorganize the Lean backend

backends/lean/Aeneas.lean

@@ -0,0 +1,11 @@
+import Aeneas.Arith
+import Aeneas.Diverge
+import Aeneas.List
+import Aeneas.Std
+import Aeneas.Progress
+import Aeneas.SimpLemmas
+import Aeneas.Utils
+import Aeneas.Saturate
+import Aeneas.ScalarNF
+import Aeneas.ScalarTac
+import Aeneas.Termination

backends/lean/Aeneas/Arith.lean

@@ -0,0 +1 @@
+import Aeneas.Arith.Lemmas

backends/lean/Base/Arith/Lemmas.lean → backends/lean/Aeneas/Arith/Lemmas.lean

@@ -1,5 +1,7 @@
-import Base.Arith.Int
-import Base.Arith.Scalar
+import Aeneas.ScalarTac.IntTac
+import Aeneas.ScalarTac.ScalarTac
+
+namespace Aeneas.ScalarTac
 
 @[nonlin_scalar_tac n % m]
 theorem Int.emod_of_pos_disj (n m : Int) : m ≤ 0 ∨ (0 ≤ n % m ∧ n % m < m) := by
@@ -29,3 +31,5 @@ section
   example (x y : Int) (h : 0 ≤ x ∧ 0 ≤ y) : 0 ≤ x * y := by scalar_tac
 
 end
+
+end Aeneas.ScalarTac

backends/lean/Aeneas/Core.lean

@@ -0,0 +1,12 @@
+
+import Lean
+
+namespace Aeneas
+
+namespace Simp
+
+
+
+end Simp
+
+end Aeneas

backends/lean/Base/Diverge.lean → backends/lean/Aeneas/Diverge.lean

@@ -2,5 +2,5 @@ import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
 import Mathlib.Tactic.Linarith
-import Base.Diverge.Base
-import Base.Diverge.Elab
+import Aeneas.Diverge.Core
+import Aeneas.Diverge.Elab

backends/lean/Base/Diverge/Base.lean → backends/lean/Aeneas/Diverge/Core.lean

@@ -1,9 +1,11 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Base.Primitives.Base
-import Base.Arith.Base
-import Base.Diverge.ElabBase
+import Aeneas.Std.Core
+import Aeneas.ScalarTac.Core
+import Aeneas.Diverge.ElabCore
+
+namespace Aeneas
 
 namespace Diverge
 
@@ -14,12 +16,12 @@ namespace Lemmas
     if heq: m = n then True
     else
       f ⟨ m, by simp_all [Nat.lt_iff_le_and_ne] ⟩ ∧
-      for_all_fin_aux f (m + 1) (by simp_all [Arith.add_one_le_iff_le_ne])
+      for_all_fin_aux f (m + 1) (by simp_all [ScalarTac.add_one_le_iff_le_ne])
   termination_by n - m
   decreasing_by
     simp_wf
     apply Nat.sub_add_lt_sub <;> try simp
-    simp_all [Arith.add_one_le_iff_le_ne]
+    simp_all [ScalarTac.add_one_le_iff_le_ne]
 
   def for_all_fin {n : Nat} (f : Fin n → Prop) := for_all_fin_aux f 0 (by simp)
 
@@ -65,7 +67,7 @@ namespace Lemmas
         apply hi <;> simp_all
         . unfold for_all_fin_aux at hf
           simp_all
-        . simp_all [Arith.add_one_le_iff_le_ne]
+        . simp_all [ScalarTac.add_one_le_iff_le_ne]
 
   -- TODO: this is not necessary anymore
   theorem for_all_fin_imp_forall (n : Nat) (f : Fin n → Prop) :
@@ -79,7 +81,7 @@ end Lemmas
 
 namespace Fix
 
-  open Primitives
+  open Std
   open Result
 
   variable {a : Type u} {b : a → Type v}
@@ -504,7 +506,7 @@ namespace FixI
      (it should be a finite type). We make the output type depend on the input
      type because we group the type parameters in the input type.
    -/
-  open Primitives Fix
+  open Std Fix
 
   -- The index type
   variable {id : Type u}
@@ -715,7 +717,7 @@ namespace FixII
   /- Similar to FixI, but we split the input arguments between the type parameters
      and the input values.
    -/
-  open Primitives Fix
+  open Std Fix
 
   -- The index type
   variable {id : Type u}
@@ -930,7 +932,7 @@ end FixII
 
 namespace Ex1
   /- An example of use of the fixed-point -/
-  open Primitives Fix
+  open Std Fix
 
   variable {a : Type} (k : (List a × Int) → Result a)
 
@@ -969,7 +971,7 @@ end Ex1
 namespace Ex2
   /- Same as Ex1, but we make the body of nth non tail-rec (this is mostly
      to see what happens when there are let-bindings) -/
-  open Primitives Fix
+  open Std Fix
 
   variable {a : Type} (k : (List a × Int) → Result a)
 
@@ -1014,7 +1016,7 @@ end Ex2
 
 namespace Ex3
   /- Mutually recursive functions - first encoding (see Ex4 for a better encoding) -/
-  open Primitives Fix
+  open Std Fix
 
   /- Because we have mutually recursive functions, we use a sum for the inputs
      and the output types:
@@ -1121,7 +1123,7 @@ end Ex3
 
 namespace Ex4
   /- Mutually recursive functions - 2nd encoding -/
-  open Primitives FixI
+  open Std FixI
 
   /- We make the input type and output types dependent on a parameter -/
   @[simp] def tys : List in_out_ty := [mk_in_out_ty Int (λ _ => Bool), mk_in_out_ty Int (λ _ => Bool)]
@@ -1196,7 +1198,7 @@ end Ex4
 
 namespace Ex5
   /- Higher-order example -/
-  open Primitives Fix
+  open Std Fix
 
   variable {a b : Type}
 
@@ -1269,7 +1271,7 @@ end Ex5
 
 namespace Ex6
   /- `list_nth` again, but this time we use FixI -/
-  open Primitives FixI
+  open Std FixI
 
   @[simp] def tys.{u} : List in_out_ty :=
     [mk_in_out_ty ((a:Type u) × (List a × Int)) (λ ⟨ a, _ ⟩ => a)]
@@ -1362,7 +1364,7 @@ end Ex6
 
 namespace Ex7
   /- `list_nth` again, but this time we use FixII -/
-  open Primitives FixII
+  open Std FixII
 
   @[simp] def tys.{u} : List in_out_ty :=
     [mk_in_out_ty (Type u) (λ a => List a × Int) (λ a => a)]
@@ -1458,7 +1460,7 @@ end Ex7
 
 namespace Ex8
   /- Higher-order example, with FixII -/
-  open Primitives FixII
+  open Std FixII
 
   variable {id : Type u} {ty : id → Type v}
   variable {a : (i:id) → ty i → Type w} {b : (i:id) → ty i → Type x}
@@ -1504,7 +1506,7 @@ end Ex8
 
 namespace Ex9
   /- An example which uses map -/
-  open Primitives FixII Ex8
+  open Std FixII Ex8
 
   inductive Tree (a : Type u) where
   | leaf (x : a)
@@ -1579,3 +1581,7 @@ namespace Ex9
     Heqix
 
 end Ex9
+
+end Diverge
+
+end Aeneas

backends/lean/Base/Diverge/Elab.lean → backends/lean/Aeneas/Diverge/Elab.lean

@@ -1,16 +1,18 @@
 import Lean
 import Lean.Meta.Tactic.Simp
 import Init.Data.List.Basic
-import Base.Utils
-import Base.Diverge.Base
-import Base.Diverge.ElabBase
+import Aeneas.Utils
+import Aeneas.Diverge.Core
+import Aeneas.Diverge.ElabCore
+
+namespace Aeneas
 
 namespace Diverge
 
 /- Automating the generation of the encoding and the proofs so as to use nice
    syntactic sugar. -/
 
-open Lean Elab Term Meta Primitives Lean.Meta
+open Lean Elab Term Meta Std Lean.Meta
 open Utils
 
 def normalize_let_bindings := true
@@ -362,7 +364,7 @@ private def list_nth_out_ty_inner (a :Type) (scrut1: @Sigma (List a) (fun (_ls :
                  (fun (_ls : List a) => Int)
                  (fun (_scrut1:@Sigma (List a) (fun (_ls : List a) => Int)) => Type)
                  scrut1
-                 (fun (_ls : List a) (_i : Int) => Primitives.Result a)
+                 (fun (_ls : List a) (_i : Int) => Result a)
 
 private def list_nth_out_ty_outer (scrut0 : @Sigma (Type) (fun (a:Type) =>
                       @Sigma (List a) (fun (_ls : List a) => Int))) :=
@@ -1712,7 +1714,7 @@ namespace Tests
   section HigherOrder
     open Ex8
 
-    inductive Tree (a : Type u) :=
+    inductive Tree (a : Type u) where
     | leaf (x : a)
     | node (tl : List (Tree a))
 
@@ -1787,3 +1789,5 @@ namespace Tests
 end Tests
 
 end Diverge
+
+end Aeneas

backends/lean/Base/Diverge/ElabBase.lean → backends/lean/Aeneas/Diverge/ElabCore.lean

@@ -1,7 +1,9 @@
 import Lean
-import Base.Utils
-import Base.Primitives.Base
-import Base.Extensions
+import Aeneas.Utils
+import Aeneas.Std.Primitives
+import Aeneas.Extensions
+
+namespace Aeneas
 
 namespace Diverge
 
@@ -82,3 +84,5 @@ def showStoredDivSpec : MetaM Unit := do
   IO.println s
 
 end Diverge
+
+end Aeneas

backends/lean/Base/Extensions.lean → backends/lean/Aeneas/Extensions.lean

@@ -1,10 +1,12 @@
 import Lean
-import Base.Utils
-import Base.Primitives.Base
+import Aeneas.Utils
+import Aeneas.Std.Core
 
 import Lean.Meta.DiscrTree
 import Lean.Meta.Tactic.Simp
 
+namespace Aeneas
+
 /-! Various state extensions used in the library -/
 namespace Extensions
 
@@ -58,3 +60,5 @@ def mkDiscrTreeExtension [Inhabited α] [BEq α] (name : Name := by exact decl_n
   }
 
 end Extensions
+
+end Aeneas

backends/lean/Aeneas/List.lean

@@ -0,0 +1 @@
+import Aeneas.List.List

backends/lean/Base/List/List.lean → backends/lean/Aeneas/List/List.lean

@@ -1,13 +1,14 @@
-/- Complementary list functions and lemmas which operate on integers rather
-   than natural numbers. -/
+/- Complementary functions and lemmas for the `List` type -/
 
-import Base.Arith
-import Base.Utils
-import Base.Core
+import Aeneas.ScalarTac
+import Aeneas.Utils
+import Aeneas.SimpLemmas
 
-namespace List
+namespace List -- We do not use the `Aeneas` namespace on purpose
 
-open Arith
+open Aeneas
+open Aeneas.ScalarTac
+open Aeneas.Simp
 
 def indexOpt (ls : List α) (i : Nat) : Option α :=
   match ls with
@@ -121,7 +122,7 @@ theorem left_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.length = l1
   revert l1'
   induction l1
   . intro l1'; cases l1' <;> simp [*]
-  . intro l1'; cases l1' <;> simp_all; tauto
+  . intro l1'; cases l1' <;> simp_all
 
 theorem right_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l2.length = l2'.length) :
   l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by

backends/lean/Aeneas/Progress.lean

@@ -0,0 +1 @@
+import Aeneas.Progress.Progress

backends/lean/Base/Progress/Base.lean → backends/lean/Aeneas/Progress/Core.lean

@@ -1,7 +1,9 @@
 import Lean
-import Base.Utils
-import Base.Primitives.Base
-import Base.Extensions
+import Aeneas.Utils
+import Aeneas.Std.Core
+import Aeneas.Extensions
+
+namespace Aeneas
 
 namespace Progress
 
@@ -189,3 +191,5 @@ def showStoredPSpec : MetaM Unit := do
   IO.println s
 
 end Progress
+
+end Aeneas