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 | |
parent | 2ec2e374302c772ff2c6a26e39451b4e49e13a16 (diff) |
Implement tactics for termination proofs which involve arithmetic
Diffstat (limited to 'backends/lean/Base')
-rw-r--r-- | backends/lean/Base/Arith/Base.lean | 12 | ||||
-rw-r--r-- | backends/lean/Base/Arith/Int.lean | 11 | ||||
-rw-r--r-- | backends/lean/Base/Arith/Scalar.lean | 11 | ||||
-rw-r--r-- | backends/lean/Base/IList/IList.lean | 24 |
4 files changed, 37 insertions, 21 deletions
diff --git a/backends/lean/Base/Arith/Base.lean b/backends/lean/Base/Arith/Base.lean index 9c11ed45..8ada4171 100644 --- a/backends/lean/Base/Arith/Base.lean +++ b/backends/lean/Base/Arith/Base.lean @@ -57,4 +57,16 @@ theorem int_pos_ind (p : Int → Prop) : -- TODO: there is probably something more general to do theorem nat_zero_eq_int_zero : (0 : Nat) = (0 : Int) := by simp +-- This is mostly used in termination proofs +theorem to_int_to_nat_lt (x y : ℤ) (h0 : 0 ≤ x) (h1 : x < y) : + ↑(x.toNat) < y := by + simp [*] + +-- This is mostly used in termination proofs +theorem to_int_sub_to_nat_lt (x y : ℤ) (x' : ℕ) + (h0 : ↑x' ≤ x) (h1 : x - ↑x' < y) : + ↑(x.toNat - x') < y := by + have : 0 ≤ x := by linarith + simp [Int.toNat_sub_of_le, *] + end Arith diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index 3359ecdb..2959e245 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -270,6 +270,17 @@ elab "int_tac" args:(" split_goal"?): tactic => let split := args.raw.getArgs.size > 0 intTac split (do pure ()) +-- For termination proofs +syntax "int_decr_tac" : tactic +macro_rules + | `(tactic| int_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 <;> int_tac) + example (x : Int) (h0: 0 ≤ x) (h1: x ≠ 0) : 0 < x := by int_tac_preprocess linarith 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 diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean index 79de93d5..f71f2de2 100644 --- a/backends/lean/Base/IList/IList.lean +++ b/backends/lean/Base/IList/IList.lean @@ -118,13 +118,7 @@ def ireplicate {α : Type u} (i : ℤ) (x : α) : List α := if i ≤ 0 then [] else x :: ireplicate (i - 1) x termination_by ireplicate i x => i.toNat -decreasing_by - simp_wf - -- TODO: simplify this kind of proofs - simp at * - have : 0 ≤ i := by linarith - have : 1 ≤ i := by linarith - simp [Int.toNat_sub_of_le, *] +decreasing_by int_decr_tac @[simp] theorem update_nil : update ([] : List α) i y = [] := by simp [update] @[simp] theorem update_zero_cons : update ((x :: tl) : List α) 0 y = y :: tl := by simp [update] @@ -173,13 +167,7 @@ theorem ireplicate_replicate {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : cases hl: l.toNat <;> simp_all conv => rhs; rw[hl] termination_by ireplicate_replicate l x h => l.toNat -decreasing_by - simp_wf - -- TODO: simplify this kind of proofs - simp at * - have : 0 ≤ l := by linarith - have : 1 ≤ l := by linarith - simp [Int.toNat_sub_of_le, *] +decreasing_by int_decr_tac @[simp] theorem ireplicate_len {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : @@ -191,13 +179,7 @@ theorem ireplicate_len {α : Type u} (l : ℤ) (x : α) (h : 0 ≤ l) : have hr := ireplicate_len (l - 1) x (by int_tac) simp [*] termination_by ireplicate_len l x h => l.toNat -decreasing_by - simp_wf - -- TODO: simplify this kind of proofs - simp at * - have : 0 ≤ l := by linarith - have : 1 ≤ l := by linarith - simp [Int.toNat_sub_of_le, *] +decreasing_by int_decr_tac theorem len_eq_length (ls : List α) : ls.len = ls.length := by induction ls |