From f3b22b5cca9bc1154f55a81c9a82dc491074067d Mon Sep 17 00:00:00 2001 From: Ryan Lahfa Date: Wed, 12 Jun 2024 13:59:11 +0200 Subject: 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 --- backends/lean/Base/IList/IList.lean | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) (limited to 'backends/lean/Base/IList') 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 α := -- cgit v1.2.3