summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--backends/lean/Base/Utils.lean30
-rw-r--r--tests/lean/Hashmap/Properties.lean167
2 files changed, 149 insertions, 48 deletions
diff --git a/backends/lean/Base/Utils.lean b/backends/lean/Base/Utils.lean
index 44590176..f014e112 100644
--- a/backends/lean/Base/Utils.lean
+++ b/backends/lean/Base/Utils.lean
@@ -326,14 +326,6 @@ def firstTac (tacl : List (TacticM Unit)) : TacticM Unit := do
| some _ => pure ()
| none => firstTac tacl -/
--- Split the goal if it is a conjunction
-def splitConjTarget : TacticM Unit := do
- withMainContext do
- let and_intro := Expr.const ``And.intro []
- let mvarIds' ← _root_.Lean.MVarId.apply (← getMainGoal) and_intro
- Term.synthesizeSyntheticMVarsNoPostponing
- replaceMainGoal mvarIds'
-
-- Taken from Lean.Elab.evalAssumption
def assumptionTac : TacticM Unit :=
liftMetaTactic fun mvarId => do mvarId.assumption; pure []
@@ -349,6 +341,24 @@ def optSplitConj (e : Expr) : MetaM (Expr × Option Expr) := do
if f.isConstOf ``And ∧ args.size = 2 then pure (args.get! 0, some (args.get! 1))
else pure (e, none)
+-- Split the goal if it is a conjunction
+def splitConjTarget : TacticM Unit := do
+ withMainContext do
+ let g ← getMainTarget
+ -- 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
+ match r with
+ | none => do throwError "The goal is not a conjunction"
+ | some r => do
+ let lmvar ← mkFreshExprSyntheticOpaqueMVar l
+ let rmvar ← mkFreshExprSyntheticOpaqueMVar r
+ let and_intro ← mkAppM ``And.intro #[lmvar, rmvar]
+ let g ← getMainGoal
+ g.assign and_intro
+ let goals ← getUnsolvedGoals
+ setGoals (lmvar.mvarId! :: rmvar.mvarId! :: goals)
+
-- Destruct an equaliy and return the two sides
def destEq (e : Expr) : MetaM (Expr × Expr) := do
e.withApp fun f args =>
@@ -520,6 +530,10 @@ elab "split_all_exists " n:ident : tactic => do
let fvar := mkFVar decl.fvarId
splitAllExistsTac fvar [] (fun _ _ => pure ())
+elab "split_target_conjs" : tactic =>
+ withMainContext do
+ repeatTac splitConjTarget
+
example (h : a ∧ b) : a := by
split_all_exists h
split_conj h
diff --git a/tests/lean/Hashmap/Properties.lean b/tests/lean/Hashmap/Properties.lean
index e065bb36..66c386f2 100644
--- a/tests/lean/Hashmap/Properties.lean
+++ b/tests/lean/Hashmap/Properties.lean
@@ -3,6 +3,18 @@ import Hashmap.Funs
open Primitives
open Result
+namespace List
+
+-- TODO: we don't want to use the original List.lookup because it uses BEq
+-- TODO: rewrite rule: match x == y with ... -> if x = y then ... else ... ?
+@[simp]
+def lookup' {α : Type} (ls: _root_.List (Usize × α)) (key: Usize) : Option α :=
+ match ls with
+ | [] => none
+ | (k, x) :: tl => if k = key then some x else lookup' tl key
+
+end List
+
namespace hashmap
namespace List
@@ -12,10 +24,15 @@ def v {α : Type} (ls: List α) : _root_.List (Usize × α) :=
| Nil => []
| Cons k x tl => (k, x) :: v tl
-def lookup {α : Type} (ls: _root_.List (Usize × α)) (key: Usize) : Option α :=
- match ls with
- | [] => none
- | (k, x) :: tl => if k = key then some x else lookup tl key
+@[simp] theorem v_nil (α : Type) : (Nil : List α).v = [] := by rfl
+@[simp] theorem v_cons {α : Type} k x (tl: List α) : (Cons k x tl).v = (k, x) :: v tl := by rfl
+
+@[simp]
+abbrev lookup {α : Type} (ls: List α) (key: Usize) : Option α :=
+ ls.v.lookup' key
+
+@[simp]
+abbrev len {α : Type} (ls : List α) : Int := ls.v.len
end List
@@ -23,39 +40,51 @@ namespace HashMap
abbrev Core.List := _root_.List
+namespace List
+
+end List
+
+-- TODO: move
+@[simp] theorem neq_imp_nbeq [BEq α] [LawfulBEq α] (x y : α) (heq : ¬ x = y) : ¬ x == y := by simp [*]
+@[simp] theorem neq_imp_nbeq_rev [BEq α] [LawfulBEq α] (x y : α) (heq : ¬ x = y) : ¬ y == x := by simp [*]
+
+-- TODO: move
+theorem match_lawful_beq [BEq α] [LawfulBEq α] [DecidableEq α] (x y : α) :
+ (x == y) = (if x = y then true else false) := by
+ split <;> simp_all
+
theorem insert_in_list_spec0 {α : Type} (key: Usize) (value: α) (ls: List α) :
∃ b,
insert_in_list α key value ls = ret b ∧
- (b ↔ List.lookup ls.v key = none)
+ (b ↔ ls.lookup key = none)
:= match ls with
- | .Nil => by simp [insert_in_list, insert_in_list_loop, List.lookup]
+ | .Nil => by simp [insert_in_list, insert_in_list_loop]
| .Cons k v tl =>
if h: k = key then -- TODO: The order of k/key matters
by
- simp [insert_in_list, List.lookup]
+ simp [insert_in_list]
rw [insert_in_list_loop]
simp [h]
else
have ⟨ b, hi ⟩ := insert_in_list_spec0 key value tl
by
exists b
- simp [insert_in_list, List.lookup]
+ simp [insert_in_list]
rw [insert_in_list_loop] -- TODO: Using simp leads to infinite recursion
- simp [h]
- simp [insert_in_list] at hi
- exact hi
+ simp only [insert_in_list] at hi
+ simp [*]
-- Variation: use progress
theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α) :
∃ b,
insert_in_list α key value ls = ret b ∧
- (b ↔ List.lookup ls.v key = none)
+ (b ↔ ls.lookup key = none)
:= match ls with
- | .Nil => by simp [insert_in_list, insert_in_list_loop, List.lookup]
+ | .Nil => by simp [insert_in_list, insert_in_list_loop]
| .Cons k v tl =>
if h: k = key then -- TODO: The order of k/key matters
by
- simp [insert_in_list, List.lookup]
+ simp [insert_in_list]
rw [insert_in_list_loop]
simp [h]
else
@@ -66,19 +95,17 @@ theorem insert_in_list_spec1 {α : Type} (key: Usize) (value: α) (ls: List α)
progress keep as heq as ⟨ b hi ⟩
simp only [insert_in_list] at heq
exists b
- simp only [heq, hi]
- simp [*, List.lookup]
-- Variation: use tactics from the beginning
theorem insert_in_list_spec2 {α : Type} (key: Usize) (value: α) (ls: List α) :
∃ b,
insert_in_list α key value ls = ret b ∧
- (b ↔ (List.lookup ls.v key = none))
+ (b ↔ (ls.lookup key = none))
:= by
induction ls
- case Nil => simp [insert_in_list, insert_in_list_loop, List.lookup]
+ case Nil => simp [insert_in_list, insert_in_list_loop]
case Cons k v tl ih =>
- simp only [insert_in_list, List.lookup]
+ simp only [insert_in_list]
rw [insert_in_list_loop]
simp only
if h: k = key then
@@ -94,26 +121,27 @@ theorem insert_in_list_back_spec {α : Type} (key: Usize) (value: α) (l0: List
∃ l1,
insert_in_list_back α key value l0 = ret l1 ∧
-- We update the binding
- List.lookup l1.v key = value ∧
- (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k)
+ l1.lookup key = value ∧
+ (∀ k, k ≠ key → l1.lookup k = l0.lookup k)
:= match l0 with
- | .Nil => by simp [insert_in_list_back, insert_in_list_loop_back, List.lookup]; tauto
+ | .Nil => by
+ simp (config := {contextual := true}) [insert_in_list_back, insert_in_list_loop_back]
| .Cons k v tl =>
if h: k = key then
by
- simp [insert_in_list_back, List.lookup]
+ simp [insert_in_list_back]
rw [insert_in_list_loop_back]
- simp [h, List.lookup]
+ simp [h]
intro k1 h1
simp [*]
else
by
- simp [insert_in_list_back, List.lookup]
+ simp [insert_in_list_back]
rw [insert_in_list_loop_back]
- simp [h, List.lookup]
+ simp [h]
progress keep as heq as ⟨ tl hp1 hp2 ⟩
simp [insert_in_list_back] at heq
- simp (config := {contextual := true}) [*, List.lookup]
+ simp (config := {contextual := true}) [*]
def distinct_keys (ls : Core.List (Usize × α)) := ls.pairwise_rel (λ x y => x.fst ≠ y.fst)
@@ -132,44 +160,103 @@ def slot_s_inv (l i : Int) (ls : Core.List (Usize × α)) : Prop :=
def slot_t_inv (l i : Int) (s : List α) : Prop := slot_s_inv l i s.v
-@[pspec]
-theorem insert_in_list_back_spec1 {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α)
+theorem insert_in_list_back_spec_aux {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α)
(hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v) :
∃ l1,
insert_in_list_back α key value l0 = ret l1 ∧
-- We update the binding
- List.lookup l1.v key = value ∧
- (∀ k, k ≠ key → List.lookup l1.v k = List.lookup l0.v k) ∧
+ l1.lookup key = value ∧
+ (∀ k, k ≠ key → l1.lookup k = l0.lookup k) ∧
-- We preserve part of the key invariant
- slot_s_inv_hash l (hash_mod_key key l) l1.v
+ slot_s_inv_hash l (hash_mod_key key l) l1.v ∧
+ -- Reasoning about the length
+ match l0.lookup key with
+ | none => l1.len = l0.len + 1
+ | some _ => l1.len = l0.len
:= match l0 with
| .Nil => by
- simp [insert_in_list_back, insert_in_list_loop_back, List.lookup, List.v, slot_s_inv_hash]
- tauto
+ simp (config := {contextual := true}) [insert_in_list_back, insert_in_list_loop_back, List.v, slot_s_inv_hash]
| .Cons k v tl0 =>
if h: k = key then
by
- simp [insert_in_list_back, List.lookup]
+ simp [insert_in_list_back]
rw [insert_in_list_loop_back]
- simp [h, List.lookup]
+ simp [h]
constructor
. intros; simp [*]
. simp [List.v, slot_s_inv_hash] at *
simp [*]
else
by
- simp [insert_in_list_back, List.lookup]
+ simp [insert_in_list_back]
rw [insert_in_list_loop_back]
- simp [h, List.lookup]
+ simp [h]
have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by
simp_all [List.v, slot_s_inv_hash]
- progress keep as heq as ⟨ tl1 hp1 hp2 hp3 ⟩
+ progress keep as heq as ⟨ tl1 hp1 hp2 hp3 hp4 ⟩
simp only [insert_in_list_back] at heq
have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by
simp [List.v, slot_s_inv_hash] at *
simp [*]
- simp (config := {contextual := true}) [*, List.lookup]
+ -- TODO: canonize addition by default?
+ simp_all [Int.add_assoc, Int.add_comm, Int.add_left_comm]
+theorem insert_in_list_back_spec_aux1 {α : Type} (l : Int) (key: Usize) (value: α) (l0: List α)
+ (hinv : slot_s_inv_hash l (hash_mod_key key l) l0.v)
+ (hdk : distinct_keys l0.v) :
+ ∃ l1,
+ insert_in_list_back α key value l0 = ret l1 ∧
+ -- We update the binding
+ l1.lookup key = value ∧
+ (∀ k, k ≠ key → l1.lookup k = l0.lookup k) ∧
+ -- We preserve part of the key invariant
+ slot_s_inv_hash l (hash_mod_key key l) l1.v ∧
+ -- Reasoning about the length
+ (match l0.lookup key with
+ | none => l1.len = l0.len + 1
+ | some _ => l1.len = l0.len) ∧
+ -- The keys are distinct
+ distinct_keys l1.v ∧
+ -- We need this auxiliary property to prove that the keys distinct properties is preserved
+ (∀ k, k ≠ key → l0.v.allP (λ (k1, _) => k ≠ k1) → l1.v.allP (λ (k1, _) => k ≠ k1))
+ := match l0 with
+ | .Nil => by
+ simp (config := {contextual := true})
+ [insert_in_list_back, insert_in_list_loop_back,
+ List.v, slot_s_inv_hash, distinct_keys, List.pairwise_rel]
+ | .Cons k v tl0 =>
+ if h: k = key then
+ by
+ simp [insert_in_list_back]
+ rw [insert_in_list_loop_back]
+ simp [h]
+ split_target_conjs
+ . intros; simp [*]
+ . simp [List.v, slot_s_inv_hash] at *
+ simp [*]
+ . simp [*, distinct_keys] at *
+ apply hdk
+ . tauto
+ else
+ by
+ simp [insert_in_list_back]
+ rw [insert_in_list_loop_back]
+ simp [h]
+ have : slot_s_inv_hash l (hash_mod_key key l) (List.v tl0) := by
+ simp_all [List.v, slot_s_inv_hash]
+ have : distinct_keys (List.v tl0) := by
+ simp [distinct_keys] at hdk
+ simp [hdk, distinct_keys]
+ progress keep as heq as ⟨ tl1 hp1 hp2 hp3 hp4 hp5 hp6 ⟩ -- TODO: naming is weird
+ simp only [insert_in_list_back] at heq
+ have : slot_s_inv_hash l (hash_mod_key key l) (List.v (List.Cons k v tl1)) := by
+ simp [List.v, slot_s_inv_hash] at *
+ simp [*]
+ have : distinct_keys ((k, v) :: List.v tl1) := by
+ simp [distinct_keys] at *
+ simp [*]
+ -- TODO: canonize addition by default?
+ simp_all [Int.add_assoc, Int.add_comm, Int.add_left_comm]
end HashMap
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-24 13:13:44 +0000