How to prove theorems about recursive functions of ListMap in coq?

Question

I'm trying to learn to use the ListMap module in Coq. I'm really not sure about proving properties about the keys or values in a ListMap, when the ListMap is created by a recursive function. I feel like I do not know what tactics to use.

(* Me proving statements about maps to understand how to use maps in Coq *)

Require Import FunInd.
Require Import Coq.Lists.List.
Require Import Coq.FSets.FMapInterface.


Require Import
  Coq.FSets.FMapList
  Coq.Structures.OrderedTypeEx.

Module Import MNat := FMapList.Make(Nat_as_OT).
Require Import
        Coq.FSets.FMapFacts.

Definition NatToNat := MNat.t nat.
Definition NatToNatEmpty : NatToNat := MNat.empty nat.

(* We wish to show that map will have only positive values *)
Function insertNats (n: nat)  (mm: NatToNat)  {struct n}: NatToNat :=
  match n with
  | O => mm
  | S (next) => insertNats  next (MNat.add n n mm)
  end.


Definition keys (mm: NatToNat) : list nat :=
  List.map  fst (elements mm).

(* vvvvv How do I prove this? Intuitively it is true *)
Example keys_nonnegative: forall (n: nat),
    forall (k: nat),
      List.In k (keys (insertNats n NatToNatEmpty)) -> k >= 0.
Proof.
  intros n k in_proof.
  induction n.
  simpl in in_proof. tauto.
  (* ??? NOW WHAT *)
Admitted.

Informally, the argument I would use for the below program is that because n >= 0 because it is a nat, the keys inserted into the map by idMapsGo will also always be non-negative.

I need to induct on n for keys_nonnegative. On the nth step, we add a key n, which will be non-negative (due to being a nat). The base case is trivial.

However, I am unable to convert this intuition into a Coq proof :)

Answer 1

You want to look at elements_in_iff and elements_mapsto_iff from Coq.FSets.FMapFacts.

Useful properties on keys:

Here are two useful properties on your definition of keys that might help you simplify your proofs. The code is taken from my own project Aniceto that includes helper properties on maps.

  Definition keys {elt:Type} (m:t elt) : list key :=  fst (split (elements m)).

Fixpoint split_alt {A:Type} {B:Type} (l:list (A*B) %type) : (list A * list B) % type:=
  match l with
    | nil => (nil, nil)
    | (x, y) :: l => (x :: (fst (split_alt l)), y :: (snd (split_alt l)))
  end.

Lemma split_alt_spec:
  forall {A:Type} {B:Type} (l:list (A*B) %type),
  split l = split_alt l.
Proof.
  intros.
  induction l.
  - auto.
  - simpl. intuition.
    rewrite IHl.
    remember (split_alt l) as l'.
    destruct l' as (lhs, rhs).
    auto.
Qed.

Lemma in_fst_split:
  forall {A:Type} {B:Type} (l:list (A*B)%type) (lhs:A),
  List.In lhs (fst (split l)) ->
  exists rhs, List.In (lhs, rhs) l.
Proof.
  intros.
  induction l.
  { inversion H. (* absurd *) }
  destruct a.
  rewrite split_alt_spec in H.
  simpl in H.
  destruct H.
  + subst.
    eauto using in_eq.
  + rewrite <- split_alt_spec in H.
    apply IHl in H; clear IHl.
    destruct H as (r, Hin).
    eauto using in_cons.
Qed.

  Lemma in_elements_to_in:
    forall {elt:Type} k e (m: t elt),
    List.In (k, e) (elements m) ->
    In k m.
  Proof.
    intros.
    rewrite elements_in_iff.
    exists e.
    apply InA_altdef.
    apply Exists_exists.
    exists (k,e).
    intuition.
    unfold eq_key_elt.
    intuition.
  Qed.

  Lemma keys_spec_1:
    forall {elt:Type} (m:t elt) (k:key),
    List.In k (keys m) -> In k m.
  Proof.
    intros.
    unfold keys in *.
    apply in_fst_split in H.
    destruct H as (e, H).
    apply in_elements_to_in with (e0:=e).
    assumption.
  Qed.

  Lemma keys_spec_2:
    forall {elt:Type} (m:t elt) (k:key),
    In k m ->
    exists k', E.eq k k' /\ List.In k' (keys m).
  Proof.
    intros.
    unfold keys in *.
    destruct H as (e, H).
    apply maps_to_impl_in_elements in H.
    destruct H as (k', (Heq, Hin)).
    apply in_split_l in Hin.
    exists k'.
    intuition.
  Qed.