Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hi Alex,
   There are probably several things wrong in your example, but the thing 
that is most likely stumping you is that in Coq 8.2 canonical structure 
unification subproblems are processed in an unnatural order -- Coq tries to 
fully unify the projection value BEFORE unifying the projection parameters. 
This makes it impossible to program a list search naively as you have done -- 
the search parameter is simply not passed to the recursive calls. You can 
take a peek at the "quote.v" file to see the shenanigans that must be used to 
work around that problem. Fortunately, this is one bugfix we (specifically, 
Cyril Cohen) were able to sneak back into the mainstream Coq: in Coq 8.3 this 
sort of thing should be way easier to do.
  Another issue you might have is that you seem to be doing searches on the 
lists contained in the "find" structures returned by previous search. These 
will have stripped some of the "wrap" markers used to introduce non 
determinism in the (normally deterministic) canonical projection search 
procedure, thereby spoiling future searches. Your quote function should 
traverse the returned list to make sure it has the right markers in the right 
places (or you could use the self-inserting/collapsible markers provided by 
the wrapped type in ssrfun).

  Cheers,
Georges

-----Original Message-----
From: Aleksandar Nanevski [] 
Sent: 30 November 2010 13:15
To: 
Subject: puzzle with canonical structures

Hi,

I've been playing a bit with canonical structures, trying to experiment 
with the ideas from quote.v and mxalgebra.v, when I ran into a puzzling 
behavior of Coq unification.

The problem I set out to do was build canonical structures to search for 
an element in a list, and return its index (size + 1 if the element does 
not exist). I used the code below, where the comments describe my 
intuition how each of the definitions is supposed to behave.

-------------------------------------------------------------------------

Require Import ssreflect ssrfun ssrbool ssrnat seq.
Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.

(* how to use canonical structures to find an element in a list *)
(* and return its index; size + 1 if no element found. *)
Module SillyLists.
Variable A : Set.

(* a structure packaging a list with the index of the element x in the 
list *)
(* for now, we drop the proof that x is in index position, since it's not *)
(* needed to illustrate the problem *)
Structure find (x : A) :=  Find {list_of : seq A; index : nat}.

Definition wrap := @id (seq A).

(* first we check if x is already at the head *)
(* ensure that this is the first check by putting a wrap around. *)
(* the returned index is 0 *)
Canonical Structure found x s := Find x (wrap (x :: s)) 0.

(* if not, the wrap is removed by unfolding its definition *)
(* then check if the unwrapped list is empty *)
(* if so, the element does not exist; return index 1 *)
Canonical Structure notfound x := Find x [::] 1.

(* if non-empty, recurse by solving for s whose list is one shorter *)
Canonical Structure drop x y (s : find x) :=
   Find x (y :: list_of s) (index s).+1.

(* start it all up *)
Definition quote (s : seq A) (i : nat) := s.

Lemma search_for x (f : find x) s :
         quote (list_of f) (index f) = s -> list_of f = s.
Proof. by []. Qed.

Implicit Arguments search_for [].

------------------------------------------------------------------------

However, I encountered a problem in that the system is willing to infer 
the structure drop (that is, recurse) at most once.
Hence, the above setting can only find an element if it is in the first 
or the second position in the list, but not if it is further down.

Here are a couple of examples that are showing the behavior.

------------------------------------------------------------------------

Example ex1 (x1 x2 x3 x4 : A) :
           wrap (x1 :: wrap (x2 :: wrap (x3 :: wrap nil))) = [::].
move=>x1 x2 x3 x4.
apply: (search_for x1). simpl. (* works *)
apply: (search_for x2). simpl. (* works *)
try apply: (search_for x3). simpl. (* doesn't work *)
admit.
Qed.

Example ex2 (x1 x2 x3 x4 : A) : wrap (x1 :: wrap nil) = [::].
move=>x1 x2 x3 x4.
apply: (search_for x2). simpl. (* works *)
admit.
Qed.

(* funny things start happening once you remove some wrap's *)
Example ex3 (x1 x2 x3 x4 : A) :
           wrap (x1 :: x2 :: wrap (x3 :: wrap nil)) = [::].
move=>x1 x2 x3 x4.
apply: (search_for x1). simpl. (* works *)
try apply: (search_for x2). simpl. (* doesn't works *)
apply: (search_for x3). simpl. (* now it allows calling drop twice, and 
works *)
try apply: (search_for x4). simpl. (* doesn't works *)
admit.
Qed.

-------------------------------------------------------------------

Does anyone know why the structures behave this way, and how to work 
around the problem?

Thanks,
Aleks