Ssreflect Users Discussion List

[Georges Gonthier <>]

  Hi there,
 As the manual states p. 52, nosimpl t simplifies to t (eagerly) except at 
the head of a definition. To get nosimpl to work with foo, you should add 
another layer of definitions:
  Fixpoint foo_rec := ...
  Definition foo := nosimpl foo_rec.
There are several instances of this in ssrnat.
You can't make bar unexpandable unless it's a toplevel definition; for your 
example this just means replacing bar by map foo.

  Georges

-----Original Message-----
From:  [] On Behalf Of 
Vincent Siles
Sent: 24 February 2011 16:05
To: 
Subject: issue with nested fixpoint and nosimpl

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