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`

Hint: consider `[("a", 1); ("a", 2)]`

.

Yeah, so it's not provable because the values may differ in the `In`

Thanks Li-yao

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.

FWIW, you could add `NoDup (map fst m)`

as a side condition

Hmm, thanks I didn't know about NoDup

Last updated: Jun 24 2024 at 14:01 UTC