咨询Coq中递归函数生成的ListMap键性质的证明方法

Great question! Let's break this down step by step. First, I want to point out a quick win here, then walk through the inductive proof you were trying to write (since it's a great way to practice reasoning about FMapList structures in Coq).

The Trivial Proof (Because of Nat's Definition) #

First, let's recognize that every natural number is non-negative in Coq. The nat type is defined inductively as O (zero) or S n (successor of n), so every k : nat satisfies k >= 0 by definition. Coq even has a built-in lemma for this: Nat.le_0_l, which states forall n : nat, 0 <= n.

This means your entire proposition is trivially true—you don't even need to use the in_proof hypothesis! Here's the one-line proof:

Example keys_nonnegative: forall (n: nat), forall (k: nat),
List.In k (keys (insertNats n NatToNatEmpty)) -> k >= 0.
Proof.
intros n k _. (* We ignore the membership hypothesis entirely *)
apply Nat.le_0_l. (* All natural numbers are >= 0 *)
Qed.

The Inductive Proof (For Practice) #

If you want to go through the inductive proof to learn how to reason about FMapList structures, here's how to complete it. The key is to use lemmas about FMapList's add and elements functions, plus list membership properties.

Here's the full proof with explanations:

Example keys_nonnegative_inductive: forall (n: nat), forall (k: nat),
List.In k (keys (insertNats n NatToNatEmpty)) -> k >= 0.
Proof.
intros n k in_proof.
induction n as [| next IHnext].
- (* Base case: n = O *)
  simpl in in_proof. (* insertNats O empty is empty, so keys is nil *)
  tauto. (* List.In k nil is False, so the implication holds vacuously *)
- (* Inductive step: n = S next *)
  (* First, unfold the definitions to see what we're working with *)
  simpl insertNats in in_proof.
  unfold keys in in_proof.
  (* Now in_proof is: List.In k (map fst (elements (add (S next) (S next) (insertNats next empty)))) *)
  
  (* Use the list map membership lemma: In y (map f l) ↔ ∃x, In x l ∧ y = f x *)
  apply List.In_map in in_proof.
  destruct in_proof as [[kv in_elements] eq_k]. (* kv is (k', v'), k = k' *)
  
  (* Use FMapList's lemma linking elements to map membership *)
  apply MNat.elements_iff in in_elements.
  rewrite eq_k in in_elements. (* Replace k' with k in the hypothesis *)
  destruct in_elements as [in_map find_eq].
  
  (* Use the lemma for membership in an added map: In k' (add k v m) ↔ k' = k ∨ In k' m *)
  apply MNat.In_add_iff in in_map.
  destruct in_map as [eq_k_snext | in_map_next].
  
  + (* Case 1: k = S next *)
    (* S next is a natural number, so it's >= 0 *)
    apply Nat.le_0_l.
  + (* Case 2: k is in the map from insertNats next empty *)
    (* We need to link map membership to key list membership *)
    assert (List.In k (keys (insertNats next NatToNatEmpty))).
    {
      unfold keys.
      apply List.In_map.
      exists (k, MNat.find k (insertNats next NatToNatEmpty)).
      split.
      - (* Prove (k, find k m) is in elements m *)
        apply MNat.elements_iff.
        split.
        * exact in_map_next.
        * apply MNat.find_iff; exact in_map_next.
      - reflexivity. (* fst (k, _) = k *)
    }
    (* Now use the inductive hypothesis *)
    apply IHnext in H.
    exact H.
Qed.

Key Takeaways for Working with FMapList #

• Lemmas are your friends: Coq's FMapList and FMapFacts modules have tons of useful lemmas like In_add_iff (membership after add) and elements_iff (linking elements to map membership). You can browse these modules to find lemmas that match your needs.
• Unfold definitions first: When stuck, unfold functions like keys or insertNats to see the underlying list/map operations.
• List properties apply: Since elements returns a list, you can use standard list lemmas like In_map to reason about key membership.

内容的提问来源于stack exchange，提问作者Siddharth Bhat