Ssreflect Users Discussion List

[Vincent Siles <>]

Hi everyone,
I have a function with a nested fixpoint which is unrolled everytime I
do a /= simplification,
and I'd like to prevent this unrolling. Here is a simplification of my code:

Inductive T :Set :=
 | Base
 | Pair of T & T
.

Inductive T' : Set :=
 | Base'
 | Node' of seq T'.

Fixpoint foo (x:T') : T :=
 let fix bar (y:seq T' ) := nosimpl match y with
 | [::] => [::]
 | hd::tl => foo hd :: bar tl
end in
match x with
 | Base' => Base
 | Node' l => foldr (fun xx yy => Pair xx yy) Base (bar l)
end.

Goal (forall l, foo (Node' l) = Base -> False).
move => /=.
Abort.

This print:
foldr (fun xx : T => [eta Pair xx]) Base
 ((fix bar (y : seq T') : seq T :=
     match y with
     | Nil => [::]
     | hd :: tl => foo hd :: bar tl
     end) l) = Base -> False


His there a way to prevent such unrolling of nested fixpoint ?

Best regards,
Vincent

PS: I'm using Coq v8.3 with ssreflect from the v8.3 contrib repository