Merge pull request #36 from AeneasVerif/update_lean

Update the version of Lean and fix a bug in the progress tactic

6 files changed, 36 insertions, 33 deletions

diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean
index 531ec94f..eb6701c2 100644
--- a/backends/lean/Base/Arith/Int.lean
+++ b/backends/lean/Base/Arith/Int.lean
@@ -238,7 +238,7 @@ def intTac (splitGoalConjs : Bool) (extraPreprocess :  Tactic.TacticM Unit) : Ta
   -- the goal. I think before leads to a smaller proof term?
   Tactic.allGoals (intTacPreprocess extraPreprocess)
   -- More preprocessing
-  Tactic.allGoals (Utils.simpAt [] [``nat_zero_eq_int_zero] [] .wildcard)
+  Tactic.allGoals (Utils.tryTac (Utils.simpAt [] [``nat_zero_eq_int_zero] [] .wildcard))
   -- Split the conjunctions in the goal
   if splitGoalConjs then Tactic.allGoals (Utils.repeatTac Utils.splitConjTarget)
   -- Call linarith
diff --git a/backends/lean/Base/Diverge/Base.lean b/backends/lean/Base/Diverge/Base.lean
index 1d548389..6a52387d 100644
--- a/backends/lean/Base/Diverge/Base.lean
+++ b/backends/lean/Base/Diverge/Base.lean
@@ -270,7 +270,7 @@ namespace Fix
     simp [karrow_rel, result_rel]
     have hg := hg Hrgh; simp [result_rel] at hg
     cases heq0: g fg <;> simp_all
-    rename_i y _
+    rename_i _ y
     have hh := hh y Hrgh; simp [result_rel] at hh
     simp_all
 
@@ -546,7 +546,7 @@ namespace FixI
   termination_by for_all_fin_aux n _ m h => n - m
   decreasing_by
     simp_wf
-    apply Nat.sub_add_lt_sub <;> simp
+    apply Nat.sub_add_lt_sub <;> try simp
     simp_all [Arith.add_one_le_iff_le_ne]
 
   def for_all_fin {n : Nat} (f : Fin n → Prop) := for_all_fin_aux f 0 (by simp)
@@ -569,7 +569,6 @@ namespace FixI
       intro i h3; cases i; simp_all
       linarith
     case succ k hi =>
-      simp_all
       intro m hk hmn
       intro hf i hmi
       have hne: m ≠ n := by
@@ -580,7 +579,6 @@ namespace FixI
         -- Yes: simply use the `for_all_fin_aux` hyp
         unfold for_all_fin_aux at hf
         simp_all
-        tauto
       else
         -- No: use the induction hypothesis
         have hlt: m < i := by simp_all [Nat.lt_iff_le_and_ne]
@@ -726,8 +724,8 @@ namespace Ex1
   theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by
     intro k x
     simp [list_nth_body]
-    split <;> simp
-    split <;> simp
+    split <;> try simp
+    split <;> try simp
 
   def list_nth (ls : List a) (i : Int) : Result a := fix list_nth_body (ls, i)
 
@@ -767,8 +765,8 @@ namespace Ex2
   theorem list_nth_body_is_valid: ∀ k x, is_valid_p k (λ k => @list_nth_body a k x) := by
     intro k x
     simp [list_nth_body]
-    split <;> simp
-    split <;> simp
+    split <;> try simp
+    split <;> try simp
     apply is_valid_p_bind <;> intros <;> simp_all
 
   def list_nth (ls : List a) (i : Int) : Result a := fix list_nth_body (ls, i)
@@ -845,7 +843,7 @@ namespace Ex3
     ∀ k x, is_valid_p k (λ k => is_even_is_odd_body k x) := by
     intro k x
     simp [is_even_is_odd_body]
-    split <;> simp <;> split <;> simp
+    split <;> (try simp) <;> split <;> try simp
     apply is_valid_p_bind; simp
     intros; split <;> simp
     apply is_valid_p_bind; simp
@@ -878,7 +876,7 @@ namespace Ex3
     -- inductives on the fly).
     -- The simplest is to repeatedly split then simplify (we identify
     -- the outer match or monadic let-binding, and split on its scrutinee)
-    split <;> simp
+    split <;> try simp
     cases H0 : fix is_even_is_odd_body (Sum.inr (i - 1)) <;> simp
     rename_i v
     split <;> simp
@@ -891,7 +889,7 @@ namespace Ex3
     simp [is_even, is_odd]
     conv => lhs; rw [Heq]; simp; rw [is_even_is_odd_body]; simp
     -- Same remark as for `even`
-    split <;> simp
+    split <;> try simp
     cases H0 : fix is_even_is_odd_body (Sum.inl (i - 1)) <;> simp
     rename_i v
     split <;> simp
@@ -938,7 +936,7 @@ namespace Ex4
     intro k
     apply (Funs.is_valid_p_is_valid_p tys)
     simp [Funs.is_valid_p]
-    (repeat (apply And.intro)) <;> intro x <;> simp at x <;>
+    (repeat (apply And.intro)) <;> intro x <;> (try simp at x) <;>
     simp only [is_even_body, is_odd_body]
     -- Prove the validity of the individual bodies
     . split <;> simp
@@ -995,9 +993,9 @@ namespace Ex5
     (ls : List a) :
     is_valid_p k (λ k => map (f k) ls) := by
     induction ls <;> simp [map]
-    apply is_valid_p_bind <;> simp_all
+    apply is_valid_p_bind <;> try simp_all
     intros
-    apply is_valid_p_bind <;> simp_all
+    apply is_valid_p_bind <;> try simp_all
 
   /- An example which uses map -/
   inductive Tree (a : Type) :=
@@ -1016,8 +1014,8 @@ namespace Ex5
     ∀ k x, is_valid_p k (λ k => @id_body a k x) := by
     intro k x
     simp only [id_body]
-    split <;> simp
-    apply is_valid_p_bind <;> simp [*]
+    split <;> try simp
+    apply is_valid_p_bind <;> try simp [*]
     -- We have to show that `map k tl` is valid
     apply map_is_valid;
     -- Remark: if we don't do the intro, then the last step is expensive:
@@ -1077,12 +1075,11 @@ namespace Ex6
     intro k
     apply (Funs.is_valid_p_is_valid_p tys)
     simp [Funs.is_valid_p]
-    (repeat (apply And.intro)); intro x; simp at x
+    (repeat (apply And.intro)); intro x; try simp at x
     simp only [list_nth_body]
     -- Prove the validity of the individual bodies
     intro k x
-    simp [list_nth_body]
-    split <;> simp
+    split <;> try simp
     split <;> simp
 
   -- Writing the proof terms explicitly
diff --git a/backends/lean/Base/Diverge/Elab.lean b/backends/lean/Base/Diverge/Elab.lean
index f109e847..c6628486 100644
--- a/backends/lean/Base/Diverge/Elab.lean
+++ b/backends/lean/Base/Diverge/Elab.lean
@@ -1089,7 +1089,7 @@ namespace Tests
       intro i hpos h
       -- We can directly use `rw [list_nth]`!
       rw [list_nth]; simp
-      split <;> simp [*]
+      split <;> try simp [*]
       . tauto
       . -- TODO: we shouldn't have to do that
         have hneq : 0 < i := by cases i <;> rename_i a _ <;> simp_all; cases a <;> simp_all
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean
index 0b483e90..a940da25 100644
--- a/backends/lean/Base/IList/IList.lean
+++ b/backends/lean/Base/IList/IList.lean
@@ -239,7 +239,6 @@ open Arith in
     have := tl.len_pos
     linarith
   else
-    simp at hineq
     have : 0 < i := by int_tac
     simp [*]
     apply hi
@@ -364,8 +363,8 @@ theorem index_itake_append_end [Inhabited α] (i j : Int) (l0 l1 : List α)
   match l0 with
   | [] => by
     simp at *
-    have := index_itake i j l1 (by simp_all) (by simp_all) (by simp_all; int_tac)
-    simp [*]
+    have := index_itake i j l1 (by simp_all) (by simp_all) (by int_tac)
+    try simp [*]
   | hd :: tl =>
     have : ¬ i = 0 := by simp at *; int_tac
     if hj : j = 0 then by simp_all; int_tac -- Contradiction
diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean
index 6a4729dc..4fd88e36 100644
--- a/backends/lean/Base/Progress/Progress.lean
+++ b/backends/lean/Base/Progress/Progress.lean
@@ -110,8 +110,9 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal)
     -- then continue splitting the post-condition
     splitEqAndPost fun hEq hPost ids => do
     trace[Progress] "eq and post:\n{hEq} : {← inferType hEq}\n{hPost}"
-    simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
-           [hEq.fvarId!] (.targets #[] true)
+    tryTac (
+      simpAt [] [``Primitives.bind_tc_ret, ``Primitives.bind_tc_fail, ``Primitives.bind_tc_div]
+             [hEq.fvarId!] (.targets #[] true))
     -- Clear the equality, unless the user requests not to do so
     let mgoal ← do
       if keep.isSome then getMainGoal
@@ -314,12 +315,14 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do
     else pure none
   let ids :=
     let args := asArgs.getArgs
-    let args := (args.get! 2).getSepArgs
-    args.map (λ s => if s.isIdent then some s.getId else none)
+    if args.size > 2 then
+      let args := (args.get! 2).getSepArgs
+      args.map (λ s => if s.isIdent then some s.getId else none)
+    else #[]
   trace[Progress] "User-provided ids: {ids}"
   let splitPost : Bool :=
     let args := asArgs.getArgs
-    (args.get! 3).getArgs.size > 0
+    args.size > 3 ∧ (args.get! 3).getArgs.size > 0
   trace[Progress] "Split post: {splitPost}"
   /- For scalarTac we have a fast track: if the goal is not a linear
      arithmetic goal, we skip (note that otherwise, scalarTac would try
@@ -343,11 +346,11 @@ elab "progress" args:progressArgs : tactic =>
 namespace Test
   open Primitives Result
 
-  set_option trace.Progress true
-  set_option pp.rawOnError true
+  -- set_option trace.Progress true
+  -- set_option pp.rawOnError true
 
-  #eval showStoredPSpec
-  #eval showStoredPSpecClass
+  -- #eval showStoredPSpec
+  -- #eval showStoredPSpecClass
 
   example {ty} {x y : Scalar ty}
     (hmin : Scalar.min ty ≤ x.val + y.val)
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 1f8f1455..5224e1c3 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -301,6 +301,10 @@ example : Nat := by
 example (x : Bool) : Nat := by
   cases x <;> custom_let x := 3 <;> apply x
 
+-- Attempt to apply a tactic
+def tryTac (tac : TacticM Unit) : TacticM Unit := do
+  let _ ← tryTactic tac
+
 -- Repeatedly apply a tactic
 partial def repeatTac (tac : TacticM Unit) : TacticM Unit := do
   try