Ssreflect Users Discussion List

[Aleksandar Nanevski <>]

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