diff options
| author | Ryan Lahfa | 2024-06-12 13:59:11 +0200 |
|---|---|---|
| committer | Ryan Lahfa | 2024-06-12 14:27:11 +0200 |
| commit | f3b22b5cca9bc1154f55a81c9a82dc491074067d (patch) | |
| tree | 4a3f54ee8e95dbeed37a3f3d78ec0d0ac1de7883 /backends/lean/Base/IList | |
| parent | e60d525fe3dffa035d2a551af624747dca6e1c1e (diff) | |
backends/lean: introduce `HasIntPred` automation
`HasIntPred` enable generation of facts based on specific terms in the
context rather than their types, e.g. if the "length of a list" occurs
in the context, generate the fact 0 ≤ length of that list, which can be
further used for `scalar_tac` automation to discharge bounds goals.
The aim is to use it to simplify various height related computations,
e.g. whenever "height of a (left ; right) tree" is encountered, generate
"height left < height of a (left ; right) tree", etc.
Signed-off-by: Ryan Lahfa <ryan.lahfa@inria.fr>
Diffstat (limited to 'backends/lean/Base/IList')
| -rw-r--r-- | backends/lean/Base/IList/IList.lean | 8 |
1 files changed, 5 insertions, 3 deletions
diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean index ca5ee266..9fe2297f 100644 --- a/backends/lean/Base/IList/IList.lean +++ b/backends/lean/Base/IList/IList.lean @@ -19,9 +19,11 @@ theorem len_pos : 0 ≤ (ls : List α).len := by induction ls <;> simp [*] linarith -instance (a : Type u) : Arith.HasIntProp (List a) where - prop_ty := λ ls => 0 ≤ ls.len - prop := λ ls => ls.len_pos +instance (l: List a) : Arith.HasIntPred (l.len) where + concl := 0 ≤ l.len + prop := l.len_pos + +example (l: List a): 0 ≤ l.len := by scalar_tac -- Remark: if i < 0, then the result is none def indexOpt (ls : List α) (i : Int) : Option α := |