## Stream: Coq users

### Topic: ✔ How to proof `In (k, v) m -> find k m = Some v`

#### 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
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 *)
``````

#### Daniel Hilst Selli (Apr 17 2022 at 04:35):

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`

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.
``````

#### Notification Bot (Apr 17 2022 at 05:05):

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 04 2023 at 23:01 UTC