The Coq mailing list

[AUGER Cédric <sedrikov AT gmail.com>]

Le Thu, 30 Aug 2012 17:55:18 +0000,
frank maltman 
<frank.maltman AT googlemail.com>
 a écrit :

> 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?
> 

Run the following to understand where your n0 comes from :


  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.

refine (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 ci := _ in
          Insertion {|cache_frequency_map := node_m;
                      cache_name_map := name_m;
                      cache_invariant := ci|} n _
        end).
clear s s0.

(** Check the head of your goal, and you'll find your [n0] *)

It is the your ci