diff options
| author | Son Ho | 2023-11-29 14:26:04 +0100 |
|---|---|---|
| committer | Son Ho | 2023-11-29 14:26:04 +0100 |
| commit | 0273fee7f6b74da1d3b66c3c6a2158c012d04197 (patch) | |
| tree | 5f6db32814f6f0b3a98f2de1db39225ff2c7645d /backends/lean/Base/Arith/Scalar.lean | |
| parent | f4e2c2bb09d9d7b54afc0692b7f690f5ec2eb029 (diff) | |
| parent | 90e42e0e1c1889aabfa66283fb15b43a5852a02a (diff) | |
Merge branch 'main' into afromher_shifts
Diffstat (limited to 'backends/lean/Base/Arith/Scalar.lean')
| -rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 13 |
1 files changed, 12 insertions, 1 deletions
diff --git a/backends/lean/Base/Arith/Scalar.lean b/backends/lean/Base/Arith/Scalar.lean index 47751c8a..2342cce6 100644 --- a/backends/lean/Base/Arith/Scalar.lean +++ b/backends/lean/Base/Arith/Scalar.lean @@ -17,7 +17,7 @@ def scalarTacExtraPreprocess : Tactic.TacticM Unit := do add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Usize []]) add (← mkAppM ``Scalar.cMax_bound #[.const ``ScalarTy.Isize []]) -- Reveal the concrete bounds, simplify calls to [ofInt] - Utils.simpAt [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax, + Utils.simpAt true [``Scalar.min, ``Scalar.max, ``Scalar.cMin, ``Scalar.cMax, ``I8.min, ``I16.min, ``I32.min, ``I64.min, ``I128.min, ``I8.max, ``I16.max, ``I32.max, ``I64.max, ``I128.max, ``U8.min, ``U16.min, ``U32.min, ``U64.min, ``U128.min, @@ -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 |