Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Data structure invariant problem

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Data structure invariant problem


Chronological Thread 
  • From: AUGER Cédric <sedrikov AT gmail.com>
  • To: frank maltman <frank.maltman AT googlemail.com>
  • Cc: <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Data structure invariant problem
  • Date: Thu, 30 Aug 2012 20:34:45 +0200

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



Archive powered by MHonArc 2.6.18.

Top of Page