Stream: Coq users

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


view this post on Zulip 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 *)

view this post on Zulip 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

view this post on Zulip Li-yao (Apr 17 2022 at 04:45):

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

view this post on Zulip Daniel Hilst Selli (Apr 17 2022 at 04:56):

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

view this post on Zulip Daniel Hilst Selli (Apr 17 2022 at 04:58):

Thanks Li-yao

view this post on Zulip 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.

view this post on Zulip Notification Bot (Apr 17 2022 at 05:05):

Daniel Hilst Selli has marked this topic as resolved.

view this post on Zulip Paolo Giarrusso (Apr 17 2022 at 10:39):

FWIW, you could add NoDup (map fst m) as a side condition

view this post on Zulip Daniel Hilst Selli (Apr 18 2022 at 13:11):

Hmm, thanks I didn't know about NoDup


Last updated: Feb 04 2023 at 21:02 UTC