Anomaly "Uncaught exception Not_found"

[TDiazT]

trafficstars

Hi, I was trying to define a function with some nested where clauses, in which one of them uses a wf recursion. I get the following error when trying to define it :

Error: Anomaly "Uncaught exception Not_found."
Please report at http://coq.inria.fr/bugs/.

The example I have is a little convoluted so I'll try to sketch the structure at least. I use a tree as in the RoseTree example, as well as some definitions from there (map_In, size, etc.). I carry some proofs of some properties along the way (between the where clauses).

 Section list_size.
    Context {A : Type} (f : A -> nat).
    Equations list_size (l : list A) : nat :=
      {
        list_size nil := 0;
        list_size (cons x xs) := S (f x + list_size xs)
      }.
  End list_size.

Variable (U : Type).

Inductive Result : Type :=
  | ULeaf : U -> Result
  | UNode : list Result -> Result.
  Derive NoConfusion for Result.

 Fixpoint rsize (r : Result) :=
    match r with
    | ULeaf a => 0
    | UNode l => S (list_size rsize l)
    end.


Equations? foo : p1 -> p2 -> ... -> rty :=
    {
      foo _ ... _ := map_in lst (fun x Hin => f3 x _ _)

      where f1 (res : Result) : rty by wf (rsize res) :=
              {
                f1 (ULeaf v) := ...;
                f1 (UNode rs) := ... (map_in rs (fun r Hin2 => f1 r)));
               }            
                
      where f2 p1 p2 (H1 : P p1) (H2 : P' p2) : rty :=
              {
                f2 ... := f1 params
              }
                
      where f3 p1 ... :=
              {
                f3 ... := f2 params
              }
    }.

[TDiazT]

I rewrote my code to not use any recursive call and I am still getting the error message, so I am guessing it has nothing to do with it haha.

I will try and pinpoint what is causing it.

[TDiazT]

So far I've noticed it is happening whenever there is a 3rd where clause (even if it is not being called). Simple examples such as the following :

Equations test : nat -> bool :=
    {
      test _ := foo3 1
               where foo1 : nat -> bool :=
                       {
                         foo1 _ := false
                       }
               where foo2 : nat -> bool :=
                       {
                         foo2 _ := foo1 3
                       }
               where foo3 : nat -> bool :=
                       {
                         foo3 _ := foo2 2
                       }

    }.

Are ok... So I am guessing it might have to do with the dep types I am using? Not sure...

[TDiazT]

I ended up collapsing the three where clauses into a single one, which itself has another nested where clause (2 where clauses in total). Thing is that this version is not capable of proving the unfold lemma automatically... And I get huuuge terms when proving some of the obligations.

I also tried with those two where clauses at the same level (instead of one nested inside the other), but this actually gives me a type error, which is quite similar to the one in #74 (The 3rd term has type "X" which should be coercible to "Y"). This is most probably another issue though...