Make minor updates (#298)

backends/lean/Base/Arith/Int.lean

@@ -29,6 +29,9 @@ macro "scalar_tac" pat:term : attr =>
 macro "nonlin_scalar_tac" pat:term : attr =>
   `(attr|aesop safe forward (rule_sets := [$(Lean.mkIdent `Aeneas.ScalarTacNonLin):ident]) (pattern := $pat))
 
+-- This is useful especially in the termination proofs
+attribute [scalar_tac a.toNat] Int.toNat_eq_max
+
 /- Check if a proposition is a linear integer proposition.
    We notably use this to check the goals: this is useful to filter goals that
    are unlikely to be solvable with arithmetic tactics. -/

backends/lean/Base/Termination.lean

@@ -86,7 +86,8 @@ macro_rules
       simp_wf <;>
       -- Simplify the context - otherwise simp_all below will blow up
       remove_invImage_assumptions <;>
-      -- Transform the goal a bit
+      -- Transform the goal a bit to get rid of `Int.toNat` if there is
+      -- (note that this is actually not necessary anymore).
       scalar_decr_tac_apply_lemmas <;>
       -- Finish
       simp_all <;> scalar_tac)

tests/lean/Tutorial.lean

@@ -382,8 +382,7 @@ decreasing_by
   -- We first need to "massage" the goal (in practice, all the proofs of [decreasing_by]
   -- should start with a call to [simp_wf]).
   simp_wf
-  -- Finish the proof
-  have : 1 ≤ x.val := by scalar_tac
-  simp [Int.toNat_sub_of_le, *]
+  -- This is just a linear arithmetic goal so we conclude with [scalar_tac]
+  scalar_tac
 
 end Tutorial