如何在coq中证明ListMap递归函数的定理？

Question

我正在尝试学习在 Coq 中使用 ListMap 模块。当ListMap 是由递归函数创建时，我真的不确定是否要证明ListMap 中的键或值的属性。我觉得我不知道该使用什么策略。

(* 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.

非正式地，我将用于以下程序的参数是因为n >= 0 因为它是nat，所以idMapsGo 插入到映射中的键也将始终为非负数。

我需要在n 上为keys_nonnegative 进行感应。在nth 步骤中，我们添加一个键n，它是非负的（因为是nat）。基本情况是微不足道的。

但是，我无法将这种直觉转化为 Coq 证明 :)

Answer 1

您想从Coq.FSets.FMapFacts 中查看elements_in_iff 和elements_mapsto_iff。

键的有用属性：

以下是关于密钥定义的两个有用属性，它们可能会帮助您简化证明。代码取自我自​​己的项目Aniceto，其中包括地图上的辅助属性。

  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.