Daniel Hilst Selli (Apr 17 2022 at 04:25): Daniel Hilst Selli (Apr 17 2022 at 04:25):I'm implementing a map with lists for fun and I was trying to prove In (k, v) m -> find k m = Some v but I got stuck with the \/. I'm starting to think that this can't be proved but I'm not sure. My hypothesis are that this is because In uses (k, v) and find uses only k so that v may differ, but I'm kind of confused still, anyway, is this lemma provable in the way that it is stated?
Require Import String.
Require Import List.
Open Scope string_scope.
Open Scope list_scope.
Import ListNotations.
Module Map.
Definition t (a : Set) : Set := list (string * a).
Definition empty (a : Set) : t a := [].
Fixpoint add {a : Set} (k : string) (v : a) (m : t a) :=
match m with
| [] => [(k, v)]
| (key, val) :: tl =>
if String.eqb key k
then (k, v) :: tl
else add k v tl
end.
Fixpoint find {a : Set} (k : string) (m : t a) : option a :=
match m with
| [] => None
| (key, value) :: tl =>
if String.eqb k key
then Some value
else find k tl
end.
Lemma find_In_eq {a : Set} k v m :
In (k, v) m -> find (a := a) k m = Some v.
Proof.
intros.
destruct m; [easy|].
destruct p.
simpl.
destruct (_ =? _) eqn:?.
apply eqb_eq in Heqb. rewrite Heqb in H.
simpl in H.
destruct H.
{ injection H as H. now rewrite H. }
{ (* stuck in showing that a0 = v *)
If I take another path :
Lemma find_In_eq {a : Set} k v m :
In (k, v) m -> find (a := a) k m = Some v.
Proof.
intros.
induction m; [easy|].
destruct a0.
simpl in *.
At this point I have the goal
a : Set
k : string
v : a
s : string
a0 : a
m : list (string * a)
H : (s, a0) = (k, v) \/ In (k, v) m
IHm : In (k, v) m -> find k m = Some v
============================
(if k =? s then Some a0 else find k m) = Some v
The left side of H corresponds to the then and the right side corresponds to the else. But if I destruct both H and =? When proving with the right side of \/ I need something in my context saying that k <> s so I can branch to the else, but I do not think this is possible because A \/ B, B = True do not implies that A is False
Li-yao (Apr 17 2022 at 04:45):Hint: consider [("a", 1); ("a", 2)].
Daniel Hilst Selli (Apr 17 2022 at 04:56):Yeah, so it's not provable because the values may differ in the In
Daniel Hilst Selli (Apr 17 2022 at 04:58):Thanks Li-yao
Daniel Hilst Selli (Apr 17 2022 at 05:05):Yeah, here is the counter example
Lemma counter_example :
let l := [("a", 2); ("a", 1)] in
let v := ("a", 1) in
In v l -> find "a" l = Some 1 -> False.
Proof.
intros.
simpl in *.
inversion H0.
Qed.
Daniel Hilst Selli has marked this topic as resolved.
Paolo Giarrusso (Apr 17 2022 at 10:39):FWIW, you could add NoDup (map fst m) as a side condition
Daniel Hilst Selli (Apr 18 2022 at 13:11):Hmm, thanks I didn't know about NoDup
Last updated: Oct 13 2024 at 01:02 UTC