diff options
| author | Son Ho | 2023-10-17 09:36:55 +0200 |
|---|---|---|
| committer | Son Ho | 2023-10-17 09:48:47 +0200 |
| commit | 584726e9c4e4378129a35f6cfbbbf934448d10a9 (patch) | |
| tree | 4e9c385d1115e71acb7581ab998320af867830bc /backends/lean/Base/Arith/Scalar.lean | |
| parent | 2ec2e374302c772ff2c6a26e39451b4e49e13a16 (diff) | |
Implement tactics for termination proofs which involve arithmetic
Diffstat (limited to 'backends/lean/Base/Arith/Scalar.lean')
| -rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 11 |
1 files changed, 11 insertions, 0 deletions
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean index 47751c8a..66c31129 100644 --- a/backends/lean/Base/Arith/Scalar.lean +++ b/backends/lean/Base/Arith/Scalar.lean @@ -36,6 +36,17 @@ def scalarTac (splitGoalConjs : Bool) : Tactic.TacticM Unit := do elab "scalar_tac" : tactic => scalarTac false +-- For termination proofs +syntax "scalar_decr_tac" : tactic +macro_rules + | `(tactic| scalar_decr_tac) => + `(tactic| + simp_wf; + -- TODO: don't use a macro (namespace problems) + (first | apply Arith.to_int_to_nat_lt + | apply Arith.to_int_sub_to_nat_lt) <;> + simp_all <;> scalar_tac) + instance (ty : ScalarTy) : HasIntProp (Scalar ty) where -- prop_ty is inferred prop := λ x => And.intro x.hmin x.hmax |