Ssreflect Users Discussion List

[Cyril Cohen <>]

Hi Vincent,

On 12/04/2012 10:11, Vincent Siles wrote:
> sometimes, I have to define function over non-trivial matrices (let's
> say f: forall n, 'M[R]_n.+1 -> T).
> When I try to prove properties about f by induction, the recursive
> case usually unfold too much because
> now my size is some n.+2 and the goal because unreadable.
> 
> In such cases, is there a known solution to "block" the unfolding ?

What I do in these kind of situation (although I do not know if they are the 
best
solutions), is
1/ Either I lock n.+1 manually (using [n.+1]lock) in the recursive case, 
before
doing /=.
2/ Or I prove f: forall n, 0 < n -> 'M[R]_n -> T instead and when I need n to 
be
something.+1, I use prednK.

Best,
-- 
Cyril
désolé pour le doublon