The Coq mailing list

[frank maltman <frank.maltman AT googlemail.com>]

Hello.

I'm running up against a problem when trying to enforce an
invariant in a data structure. The invariant in question is
in the 'cache' type:

    cache_invariant : forall n, Name_Maps.In (node_name n) cache_name_map ->
      Node_Maps.In (node_frequency n) cache_frequency_map

Apologies for the following pile of boilerplate, but the
majority of it is just to instantiate some FSet modules:

Require Coq.Arith.Compare_dec.
Require Coq.Arith.Peano_dec.
Require Coq.Arith.Lt.
Require Coq.Arith.Le.
Require Coq.Structures.OrderedType.
Require Coq.FSets.FMapAVL.
Require Coq.FSets.FSetAVL.
Require Coq.FSets.FMapFacts.
Require Coq.FSets.FSetProperties.

Lemma lt_not_eq : forall x y,
  lt x y -> ~eq x y.
Proof.
  induction x.
    auto with *.
    induction y.
      auto with *.
      auto with *.
Qed.

Definition eq_dec : forall m n : nat, {eq m n} + {~ eq m n} :=
  Peano_dec.eq_nat_dec.

Definition compare (m n : nat) : OrderedType.Compare lt eq m n.
Proof.
  destruct (Compare_dec.lt_eq_lt_dec m n) as [p|q].
    destruct p as [l|e].
      apply (OrderedType.LT l).
      apply (OrderedType.EQ e).
    apply (OrderedType.GT q).
Qed.

Module Ordered_Nat : OrderedType.OrderedType
  with Definition t  := nat.

  Definition t := nat.
  Definition eq             := @eq nat.
  Definition eq_refl x      := @eq_refl nat x.
  Definition eq_sym x y     := @eq_sym nat x y.
  Definition eq_trans x y z := @eq_trans nat x y z.
  Definition eq_dec         := eq_dec.
  Definition lt             := lt.
  Definition lt_trans x y z := @Lt.lt_trans x y z.
  Definition lt_not_eq      := lt_not_eq.
  Definition compare        := compare.
End Ordered_Nat.

Record node := Node {
  node_frequency : nat;
  node_value     : nat;
  node_name      : nat
}.

Module Ordered_Node : OrderedType.OrderedType
  with Definition t := node.
  Definition t              := node.
  Definition eq (x y : t)   := eq (node_name x) (node_name y).
  Definition lt (x y : t)   := lt (node_name x) (node_name y).
  Definition eq_refl x      := eq_refl (node_name x).
  Definition eq_sym x y     := @eq_sym nat (node_name x) (node_name y).
  Definition eq_trans x y z := @eq_trans nat (node_name x) (node_name y) 
(node_name z).
  Definition eq_dec x y     := Peano_dec.eq_nat_dec (node_name x) (node_name 
y).
  Definition lt_trans x y z := @Lt.lt_trans (node_name x) (node_name y) 
(node_name z).
  Definition lt_not_eq x y  := lt_not_eq (node_name x) (node_name y).
  Parameter compare : forall (u v : t), @OrderedType.Compare t lt eq u v.
End Ordered_Node.

Module Ordered_Name : OrderedType.OrderedType
  with Definition t := nat.

  Definition t := nat.
  Definition eq             := @eq nat.
  Definition eq_refl x      := @eq_refl nat x.
  Definition eq_sym x y     := @eq_sym nat x y.
  Definition eq_trans x y z := @eq_trans nat x y z.
  Definition eq_dec         := eq_dec.
  Definition lt             := lt.
  Definition lt_trans x y z := @Lt.lt_trans x y z.
  Definition lt_not_eq      := lt_not_eq.
  Definition compare        := compare.
End Ordered_Name.

Module Node_Sets       := FSetAVL.Make (Ordered_Node).
Module Node_Sets_Facts := FSetFacts.Facts (Node_Sets).
Module Node_Maps       := FMapAVL.Make (Ordered_Nat).
Module Node_Maps_Facts := FMapFacts.Facts (Node_Maps).
Module Name_Maps       := FMapAVL.Make (Ordered_Name).
Module Name_Maps_Facts := FMapFacts.Facts (Name_Maps).
Module Nat_Sets        := FSetAVL.Make (Ordered_Nat).
Module Nat_Sets_Facts  := FSetFacts.Facts (Nat_Sets).
Module Nat_Sets_Props  := FSetProperties.Properties (Nat_Sets).

Record cache := Cache {
  cache_frequency_map : Node_Maps.t Node_Sets.t;
  cache_name_map      : Name_Maps.t node;
  cache_invariant     : forall n, Name_Maps.In (node_name n) cache_name_map ->
                          Node_Maps.In (node_frequency n) cache_frequency_map
}.

Lemma cache_map_empty_contra : forall n,
  Name_Maps.In (node_name n) (Name_Maps.empty node) ->
    Node_Maps.In (node_frequency n) (Node_Maps.empty Node_Sets.t).
Proof.
  intros n H.
  contradict H.
  rewrite Name_Maps_Facts.empty_in_iff.
  auto.
Qed.

Definition cache_empty := {|
  cache_frequency_map := Node_Maps.empty Node_Sets.t;
  cache_name_map      := Name_Maps.empty _;
  cache_invariant     := cache_map_empty_contra
|}.

Inductive insertion : Prop :=
  | Insertion : forall (c : cache) (n : node),
      Name_Maps.In (node_name n) (cache_name_map c)
        -> insertion.

Module Type Primitives_Signature.

  Parameter insert_node_create_frequency : forall
    (c      : cache)
    (n      : node)
    (H_name : ~Name_Maps.In (node_name n) (cache_name_map c))
    (H_freq : ~Node_Maps.In (node_frequency n) (cache_frequency_map c)),
      insertion.

End Primitives_Signature.

Module Primitives : Primitives_Signature.

  Lemma name_map_add_in : forall n m,
    Name_Maps.In (node_name n) (Name_Maps.add (node_name n) n m).
  Proof.
    intros.
    apply Name_Maps_Facts.add_in_iff.
    left; reflexivity.
  Qed.

  Definition insert_maps_name
    (node_m : Node_Maps.t Node_Sets.t)
    (name_m : Name_Maps.t node)
    (n      : node)
    (H_name : ~Name_Maps.In  (node_name n) name_m)
    (H_node : Node_Maps.In (node_frequency n) node_m)
  : ({p : Node_Maps.t Node_Sets.t | Node_Maps.In (node_frequency n) p} *
     {q : Name_Maps.t node        | Name_Maps.In (node_name n)      q})
  :=
    let name_m' := Name_Maps.add (node_name n) n name_m in
      (exist _ node_m H_node, exist _ name_m' (name_map_add_in _ _)).

  Lemma node_map_add_in : forall n m (s : Node_Sets.t),
    Node_Maps.In (node_frequency n) (Node_Maps.add (node_frequency n) s m).
  Proof.
    intros.
    apply Node_Maps_Facts.add_in_iff.
    left; reflexivity.
  Qed.

  Definition insert_maps_node
    (node_m : Node_Maps.t Node_Sets.t)
    (name_m : Name_Maps.t node)
    (n      : node)
    (H_name : ~Name_Maps.In (node_name n)      name_m)
    (H_node : ~Node_Maps.In (node_frequency n) node_m)
  : ({p : Node_Maps.t Node_Sets.t | Node_Maps.In (node_frequency n) p} *
     {q : Name_Maps.t node        | Name_Maps.In (node_name n)      q})
  :=
    let s       := Node_Sets.singleton n                     in
    let node_m' := Node_Maps.add (node_frequency n) s node_m in
      insert_maps_name node_m' name_m n H_name (node_map_add_in _ _ _).

  Program Definition insert_node_create_frequency
    (c      : cache)
    (n      : node)
    (H_name : ~Name_Maps.In (node_name n) (cache_name_map c))
    (H_freq : ~Node_Maps.In (node_frequency n) (cache_frequency_map c))
  : insertion :=
    match insert_maps_node (cache_frequency_map c) (cache_name_map c) n 
H_name H_freq with
    | (exist node_m H_node_add, exist name_m H_name_add) =>
      let d := {|
        cache_frequency_map := node_m;
        cache_name_map      := name_m;
        cache_invariant     := _
      |} in Insertion d n _
    end.
  Next Obligation.
    (* n0 != n *)
    unfold Node_Maps.In.
    unfold Node_Maps.Raw.In0.
    exists (Node_Sets.singleton n).
    apply Node_Maps.add_1.

--

1 subgoals
c          : cache
n          : node
H_name     : ~ Name_Maps.In (elt:=node) (node_name n) (cache_name_map c)
H_freq     : ~ Node_Maps.In (elt:=Node_Sets.t) (node_frequency n) 
(cache_frequency_map c)
n0         : node
H_name_add : Name_Maps.In (elt:=node) (node_name n) (Name_Maps.add (node_name 
n) n (cache_name_map c))
H          : Name_Maps.In (elt:=node) (node_name n0) (Name_Maps.add 
(node_name n) n (cache_name_map c))
H_node_add : Node_Maps.In (elt:=Node_Sets.t) (node_frequency n) 
(Node_Maps.add (node_frequency n) (Node_Sets.singleton n) 
(cache_frequency_map c))
______________________________________(1/1)
Node_Maps.E.eq (node_frequency n) (node_frequency n0)

It seems, for some reason, that an 'n0' variable has been introduced
into the context and there's no apparent way to prove that it's equal
to n.

Could someone please explain what's going on here?