diff options
Diffstat (limited to '')
-rw-r--r-- | backends/lean/Base/Arith/Int.lean | 1 | ||||
-rw-r--r-- | backends/lean/Base/IList/IList.lean | 41 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Base.lean | 2 | ||||
-rw-r--r-- | backends/lean/Base/Primitives/Vec.lean | 20 | ||||
-rw-r--r-- | backends/lean/Base/Progress/Progress.lean | 34 | ||||
-rw-r--r-- | backends/lean/Base/Utils.lean | 36 | ||||
-rw-r--r-- | tests/lean/Hashmap/Properties.lean | 116 |
7 files changed, 216 insertions, 34 deletions
diff --git a/backends/lean/Base/Arith/Int.lean b/backends/lean/Base/Arith/Int.lean index bc0676d8..48a30a49 100644 --- a/backends/lean/Base/Arith/Int.lean +++ b/backends/lean/Base/Arith/Int.lean @@ -43,6 +43,7 @@ instance (x y : Int) : IsLinearIntProp (x > y) where instance (x y : Int) : IsLinearIntProp (x ≤ y) where instance (x y : Int) : IsLinearIntProp (x ≥ y) where instance (x y : Int) : IsLinearIntProp (x ≥ y) where +instance (x y : Int) : IsLinearIntProp (x = y) where /- It seems we don't need to do any special preprocessing when the *goal* has the following shape - I guess `linarith` automatically calls `intro` -/ instance (x y : Int) : IsLinearIntProp (¬ x = y) where diff --git a/backends/lean/Base/IList/IList.lean b/backends/lean/Base/IList/IList.lean index 2443b1a6..93047a1b 100644 --- a/backends/lean/Base/IList/IList.lean +++ b/backends/lean/Base/IList/IList.lean @@ -123,6 +123,10 @@ theorem length_update (ls : List α) (i : Int) (x : α) : (ls.update i x).length theorem len_update (ls : List α) (i : Int) (x : α) : (ls.update i x).len = ls.len := by simp [len_eq_length] +@[simp] +theorem len_map (ls : List α) (f : α → β) : (ls.map f).len = ls.len := by + simp [len_eq_length] + theorem left_length_eq_append_eq (l1 l2 l1' l2' : List α) (heq : l1.length = l1'.length) : l1 ++ l2 = l1' ++ l2' ↔ l1 = l1' ∧ l2 = l2' := by revert l1' @@ -210,6 +214,43 @@ theorem index_eq simp at * apply index_eq <;> scalar_tac +theorem update_map_eq {α : Type u} {β : Type v} (ls : List α) (i : Int) (x : α) (f : α → β) : + (ls.update i x).map f = (ls.map f).update i (f x) := + match ls with + | [] => by simp + | hd :: tl => + if h : i = 0 then by simp [*] + else + have hi := update_map_eq tl (i - 1) x f + by simp [*] + +theorem len_flatten_update_eq {α : Type u} (ls : List (List α)) (i : Int) (x : List α) + (h0 : 0 ≤ i) (h1 : i < ls.len) : + (ls.update i x).flatten.len = ls.flatten.len + x.len - (ls.index i).len := + match ls with + | [] => by simp at h1; int_tac + | hd :: tl => by + simp at h1 + if h : i = 0 then simp [*]; int_tac + else + have hi := len_flatten_update_eq tl (i - 1) x (by int_tac) (by int_tac) + simp [*] + int_tac + +@[simp] +theorem index_map_eq {α : Type u} {β : Type v} [Inhabited α] [Inhabited β] (ls : List α) (i : Int) (f : α → β) + (h0 : 0 ≤ i) (h1 : i < ls.len) : + (ls.map f).index i = f (ls.index i) := + match ls with + | [] => by simp at h1; int_tac + | hd :: tl => + if h : i = 0 then by + simp [*] + else + have hi := index_map_eq tl (i - 1) f (by int_tac) (by simp at h1; int_tac) + by + simp [*] + def allP {α : Type u} (l : List α) (p: α → Prop) : Prop := foldr (fun a r => p a ∧ r) True l diff --git a/backends/lean/Base/Primitives/Base.lean b/backends/lean/Base/Primitives/Base.lean index db462c38..7c0fa3bb 100644 --- a/backends/lean/Base/Primitives/Base.lean +++ b/backends/lean/Base/Primitives/Base.lean @@ -76,7 +76,7 @@ def eval_global {α: Type u} (x: Result α) (_: ret? x): α := /- DO-DSL SUPPORT -/ -def bind {α : Type u} {β : Type v} (x: Result α) (f: α -> Result β) : Result β := +def bind {α : Type u} {β : Type v} (x: Result α) (f: α → Result β) : Result β := match x with | ret v => f v | fail v => fail v diff --git a/backends/lean/Base/Primitives/Vec.lean b/backends/lean/Base/Primitives/Vec.lean index 5a709566..523372bb 100644 --- a/backends/lean/Base/Primitives/Vec.lean +++ b/backends/lean/Base/Primitives/Vec.lean @@ -75,10 +75,9 @@ def Vec.insert (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Vec α) := .fail arrayOutOfBounds @[pspec] -theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α) : - i.val < v.length → +theorem Vec.insert_spec {α : Type u} (v: Vec α) (i: Usize) (x: α) + (hbound : i.val < v.length) : ∃ nv, v.insert α i x = ret nv ∧ nv.val = v.val.update i.val x := by - intro h simp [insert, *] def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α := @@ -87,10 +86,9 @@ def Vec.index (α : Type u) (v: Vec α) (i: Usize) : Result α := | some x => ret x @[pspec] -theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) : - i.val < v.length → +theorem Vec.index_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) + (hbound : i.val < v.length) : v.index α i = ret (v.val.index i.val) := by - intro simp only [index] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) @@ -109,10 +107,9 @@ def Vec.index_mut (α : Type u) (v: Vec α) (i: Usize) : Result α := | some x => ret x @[pspec] -theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) : - i.val < v.length → +theorem Vec.index_mut_spec {α : Type u} [Inhabited α] (v: Vec α) (i: Usize) + (hbound : i.val < v.length) : v.index_mut α i = ret (v.val.index i.val) := by - intro simp only [index_mut] -- TODO: dependent rewrite have h := List.indexOpt_eq_index v.val i.val (by scalar_tac) (by simp [*]) @@ -129,12 +126,11 @@ def Vec.index_mut_back (α : Type u) (v: Vec α) (i: Usize) (x: α) : Result (Ve .ret ⟨ v.val.update i.val x, by have := v.property; simp [*] ⟩ @[pspec] -theorem Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α) : - i.val < v.length → +theorem Vec.index_mut_back_spec {α : Type u} (v: Vec α) (i: Usize) (x : α) + (hbound : i.val < v.length) : ∃ nv, v.index_mut_back α i x = ret nv ∧ nv.val = v.val.update i.val x := by - intro simp only [index_mut_back] have h := List.indexOpt_bounds v.val i.val split diff --git a/backends/lean/Base/Progress/Progress.lean b/backends/lean/Base/Progress/Progress.lean index a2c7764f..4a406bdf 100644 --- a/backends/lean/Base/Progress/Progress.lean +++ b/backends/lean/Base/Progress/Progress.lean @@ -1,6 +1,7 @@ import Lean import Base.Arith import Base.Progress.Base +import Base.Primitives -- TODO: remove? namespace Progress @@ -41,7 +42,12 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) match th with | .Theorem thName => let thDecl := env.constants.find! thName - pure thDecl.type + -- We have to introduce fresh meta-variables for the universes already + let ul : List (Name × Level) ← + thDecl.levelParams.mapM (λ x => do pure (x, ← mkFreshLevelMVar)) + let ulMap : HashMap Name Level := HashMap.ofList ul + let thTy := thDecl.type.instantiateLevelParamsCore (λ x => ulMap.find! x) + pure thTy | .Local asmDecl => pure asmDecl.type trace[Progress] "Looked up theorem/assumption type: {thTy}" -- TODO: the tactic fails if we uncomment withNewMCtxDepth @@ -129,15 +135,16 @@ def progressWith (fExpr : Expr) (th : TheoremOrLocal) Split the remaining conjunctions by using fresh ids if the user instructed to fully split the post-condition, otherwise stop -/ if splitPost then - splitFullConjTac hPost (λ _ => pure .Ok) + splitFullConjTac true hPost (λ _ => pure .Ok) else pure .Ok | nid :: ids => do - trace[Progress] "Splitting post: {hPost}" + trace[Progress] "Splitting post: {← inferType hPost}" -- Split let nid ← do match nid with | none => mkFreshUserName `h | some nid => pure nid + trace[Progress] "\n- prevId: {prevId}\n- nid: {nid}\n- remaining ids: {ids}" if ← isConj (← inferType hPost) then splitConjTac hPost (some (prevId, nid)) (λ _ nhPost => splitPostWithIds nid nhPost ids) else return (.Error m!"Too many ids provided ({ids0}) not enough conjuncts to split in the postcondition") @@ -323,7 +330,7 @@ def evalProgress (args : TSyntax `Progress.progressArgs) : TacticM Unit := do elab "progress" args:progressArgs : tactic => evalProgress args -/- namespace Test +namespace Test open Primitives Result set_option trace.Progress true @@ -336,10 +343,25 @@ elab "progress" args:progressArgs : tactic => (hmin : Scalar.min ty ≤ x.val + y.val) (hmax : x.val + y.val ≤ Scalar.max ty) : ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by --- progress keep as h with Scalar.add_spec as ⟨ z ⟩ progress keep as h as ⟨ x, h1 .. ⟩ simp [*] -end Test -/ + example {ty} {x y : Scalar ty} + (hmin : Scalar.min ty ≤ x.val + y.val) + (hmax : x.val + y.val ≤ Scalar.max ty) : + ∃ z, x + y = ret z ∧ z.val = x.val + y.val := by + progress keep as h with Scalar.add_spec as ⟨ z ⟩ + simp [*] + + /- Checking that universe instantiation works: the original spec uses + `α : Type u` where u is quantified, while here we use `α : Type 0` -/ + example {α : Type} (v: Vec α) (i: Usize) (x : α) + (hbounds : i.val < v.length) : + ∃ nv, v.index_mut_back α i x = ret nv ∧ + nv.val = v.val.update i.val x := by + progress + simp [*] + +end Test end Progress diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean index 66497a49..f6dc45c7 100644 --- a/backends/lean/Base/Utils.lean +++ b/backends/lean/Base/Utils.lean @@ -1,6 +1,7 @@ import Lean import Mathlib.Tactic.Core import Mathlib.Tactic.LeftRight +import Base.UtilsBase /- Mathlib tactics: @@ -331,13 +332,13 @@ def assumptionTac : TacticM Unit := liftMetaTactic fun mvarId => do mvarId.assumption; pure [] def isConj (e : Expr) : MetaM Bool := - e.withApp fun f args => pure (f.isConstOf ``And ∧ args.size = 2) + e.consumeMData.withApp fun f args => pure (f.isConstOf ``And ∧ args.size = 2) -- Return the first conjunct if the expression is a conjunction, or the -- expression itself otherwise. Also return the second conjunct if it is a -- conjunction. def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do - e.withApp fun f args => + e.consumeMData.withApp fun f args => if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1)) else pure (e, none) @@ -345,6 +346,7 @@ def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do def splitConjTarget : TacticM Unit := do withMainContext do let g ← getMainTarget + trace[Utils] "splitConjTarget: goal: {g}" -- The tactic was initially implemened with `_root_.Lean.MVarId.apply` -- but it tended to mess the goal by unfolding terms, even when it failed let (l, r) ← optSplitConj g @@ -525,18 +527,26 @@ def splitConjTac (h : Expr) (optIds : Option (Name × Name)) (k : Expr → Expr throwError "Not a conjunction" -- Tactic to fully split a conjunction -partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (l : List Expr) (h : Expr) (k : List Expr → TacticM α) : TacticM α := do +partial def splitFullConjTacAux [Inhabited α] [Nonempty α] (keepCurrentName : Bool) (l : List Expr) (h : Expr) (k : List Expr → TacticM α) : TacticM α := do try - splitConjTac h none (λ h1 h2 => - splitFullConjTacAux l h1 (λ l1 => - splitFullConjTacAux l1 h2 (λ l2 => + let ids ← do + if keepCurrentName then do + let cur := (← h.fvarId!.getDecl).userName + let nid ← mkFreshUserName `h + pure (some (cur, nid)) + else + pure none + splitConjTac h ids (λ h1 h2 => + splitFullConjTacAux keepCurrentName l h1 (λ l1 => + splitFullConjTacAux keepCurrentName l1 h2 (λ l2 => k l2))) catch _ => k (h :: l) -- Tactic to fully split a conjunction -def splitFullConjTac [Inhabited α] [Nonempty α] (h : Expr) (k : List Expr → TacticM α) : TacticM α := do - splitFullConjTacAux [] h (λ l => k l.reverse) +-- `keepCurrentName`: if `true`, then the first conjunct has the name of the original assumption +def splitFullConjTac [Inhabited α] [Nonempty α] (keepCurrentName : Bool) (h : Expr) (k : List Expr → TacticM α) : TacticM α := do + splitFullConjTacAux keepCurrentName [] h (λ l => k l.reverse) syntax optAtArgs := ("at" ident)? def elabOptAtArgs (args : TSyntax `Utils.optAtArgs) : TacticM (Option Expr) := do @@ -553,17 +563,21 @@ def elabOptAtArgs (args : TSyntax `Utils.optAtArgs) : TacticM (Option Expr) := d elab "split_conj" args:optAtArgs : tactic => do withMainContext do match ← elabOptAtArgs args with - | some fvar => + | some fvar => do + trace[Utils] "split at {fvar}" splitConjTac fvar none (fun _ _ => pure ()) - | none => + | none => do + trace[Utils] "split goal" splitConjTarget elab "split_conjs" args:optAtArgs : tactic => do withMainContext do match ← elabOptAtArgs args with | some fvar => - splitFullConjTac fvar (fun _ => pure ()) + trace[Utils] "split at {fvar}" + splitFullConjTac false fvar (fun _ => pure ()) | none => + trace[Utils] "split goal" repeatTac splitConjTarget elab "split_existsl" " at " n:ident : tactic => do diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean index b2d5570a..92285c0d 100644 --- a/tests/lean/Hashmap/Properties.lean +++ b/tests/lean/Hashmap/Properties.lean @@ -55,6 +55,7 @@ theorem match_lawful_beq [BEq α] [LawfulBEq α] [DecidableEq α] (x y : α) : (x == y) = (if x = y then true else false) := by split <;> simp_all +@[pspec] theorem insert_in_list_spec0 {α : Type} (key: Usize) (value: α) (ls: List α) : ∃ b, insert_in_list α key value ls = ret b ∧ @@ -126,6 +127,10 @@ def hash_mod_key (k : Usize) (l : Int) : Int := | .ret k => k.val % l | _ => 0 +@[simp] +theorem hash_mod_key_eq : hash_mod_key k l = k.val % l := by + simp [hash_mod_key, hash_key] + def slot_s_inv_hash (l i : Int) (ls : Core.List (Usize × α)) : Prop := ls.allP (λ (k, _) => hash_mod_key k l = i) @@ -246,6 +251,7 @@ theorem insert_in_list_back_spec {α : Type} (l : Int) (key: Usize) (value: α) progress with insert_in_list_back_spec_aux as ⟨ l1 .. ⟩ exists l1 +@[simp] def slots_t_lookup (s : Core.List (List α)) (k : Usize) : Option α := let i := hash_mod_key k s.len let slot := s.index i @@ -260,7 +266,15 @@ abbrev len_s (hm : HashMap α) : Int := hm.al_v.len set_option trace.Progress true /-set_option pp.explicit true set_option pp.universes true -set_option pp.notation false-/ +set_option pp.notation false -/ + +-- Remark: α and β must live in the same universe, otherwise the +-- bind doesn't work +theorem if_update_eq + {α β : Type u} (b : Bool) (y : α) (e : Result α) (f : α → Result β) : + (if b then Bind.bind e f else f y) = Bind.bind (if b then e else pure y) f + := by + split <;> simp [Pure.pure] theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value : α) (hinv : hm.inv) (hnsat : hm.lookup key = none → hm.len_s < Usize.max) : @@ -270,18 +284,112 @@ theorem insert_no_resize_spec {α : Type} (hm : HashMap α) (key : Usize) (value -- We updated the binding for key nhm.lookup key = some value ∧ -- We left the other bindings unchanged - (∀ k, k ≠ key → nhm.lookup k = hm.lookup k) ∧ + (∀ k, ¬ k = key → nhm.lookup k = hm.lookup k) ∧ -- Reasoning about the length (match hm.lookup key with | none => nhm.len_s = hm.len_s + 1 | some _ => nhm.len_s = hm.len_s) := by rw [insert_no_resize] simp [hash_key] - have : (Vec.len (List α) hm.slots).val ≠ 0 := by + have _ : (Vec.len (List α) hm.slots).val ≠ 0 := by checkpoint intro simp_all [inv] - progress as ⟨ hash_mod ⟩ + -- TODO: progress keep as ⟨ ... ⟩ : conflict + progress keep as h as ⟨ hash_mod, hhm ⟩ + have _ : 0 ≤ hash_mod.val := by checkpoint scalar_tac + have _ : hash_mod.val < Vec.length hm.slots := by sorry + -- have h := Primitives.Vec.index_mut_spec hm.slots hash_mod + -- TODO: change the spec of Vec.index_mut to introduce a let-binding. + -- or: make progress introduce the let-binding by itself (this is clearer) progress + -- TODO: make progress use the names written in the goal + progress as ⟨ inserted ⟩ + rw [if_update_eq] -- TODO: necessary because we don't have a join + -- TODO: progress to ... + have hipost : + ∃ i0, (if inserted = true then hm.num_entries + Usize.ofInt 1 else pure hm.num_entries) = ret i0 ∧ + i0.val = if inserted then hm.num_entries.val + 1 else hm.num_entries.val + := by sorry + progress as ⟨ i0 ⟩ + -- TODO: progress "eager" to match premises with assumptions while instantiating + -- meta-variables + have h_slot : slot_s_inv_hash hm.slots.length hash_mod.val (hm.slots.v.index hash_mod.val).v := by sorry + have hd : distinct_keys (hm.slots.v.index hash_mod.val).v := by checkpoint + simp [inv, slots_t_inv, slot_t_inv] at hinv + have h := hinv.right.left hash_mod.val (by assumption) (by assumption) + simp [h] + -- TODO: hide the variables and only keep the props + -- TODO: allow providing terms to progress to instantiate the meta variables + -- which are not propositions + progress as ⟨ l0, _, _, _, hlen .. ⟩ + . checkpoint exact hm.slots.length + . checkpoint simp_all + . -- Finishing the proof + progress as ⟨ v ⟩ + -- TODO: update progress to automate that + let nhm : HashMap α := { num_entries := i0, max_load_factor := hm.max_load_factor, max_load := hm.max_load, slots := v } + exists nhm + have hupdt : lookup nhm key = some value := by checkpoint + simp [lookup, List.lookup] at * + simp_all + have hlkp : ∀ k, ¬ k = key → nhm.lookup k = hm.lookup k := by checkpoint + simp [lookup, List.lookup] at * + intro k hk + -- We have to make a case disjunction: either the hashes are different, + -- in which case we don't even lookup the same slots, or the hashes + -- are the same, in which case we have to reason about what happens + -- in one slot + let k_hash_mod := k.val % v.val.len + have _ : 0 ≤ k_hash_mod := by sorry + have _ : k_hash_mod < Vec.length hm.slots := by sorry + if h_hm : k_hash_mod = hash_mod.val then + simp_all + else + simp_all + have _ : + match hm.lookup key with + | none => nhm.len_s = hm.len_s + 1 + | some _ => nhm.len_s = hm.len_s := by checkpoint + simp only [lookup, List.lookup, len_s, al_v, HashMap.v, slots_t_lookup] at * + -- We have to do a case disjunction + simp_all + simp [_root_.List.update_map_eq] + -- TODO: dependent rewrites + have _ : key.val % hm.slots.val.len < (List.map List.v hm.slots.val).len := by + simp [*] + simp [_root_.List.len_flatten_update_eq, *] + split <;> + rename_i heq <;> + simp [heq] at hlen <;> + -- TODO: canonize addition by default? We need a tactic to simplify arithmetic equalities + -- with addition and substractions ((ℤ, +) is a ring or something - there should exist a tactic + -- somewhere in mathlib?) + simp [Int.add_assoc, Int.add_comm, Int.add_left_comm] <;> + int_tac + have hinv : inv nhm := by + simp [inv] at * + split_conjs + . match h: lookup hm key with + | none => + simp [h, lookup] at * + simp_all + | some _ => + simp_all [lookup] + . simp [slots_t_inv, slot_t_inv] at * + intro i hipos _ + have hs := hinv.right.left i hipos (by simp_all) + -- We need a case disjunction + if i = key.val % _root_.List.len hm.slots.val then + simp_all + else + simp_all + . match h: lookup hm key with + | none => + simp [h] at * + simp [*] + | some _ => + simp_all + simp_all end HashMap |