The Coq mailing list

[Christine Paulin <christine.paulin AT lri.fr>]

There are indeed examples where this is needed
for instance to have (pred n) < n when (n<>0) or any other destructor 
function
in particular the definition of the fixpoint combinator on well-founded 
relations relies on that.

However there is a simple restriction to the match rule that should 
solve the problem :
    checking the order is done with respect to an inductive definition 
Ind (the type of the recusive variable in the fixpoint)
    the return type of the match (the one gouverning the type of eache 
branch) should produce something in this inductive definition (so be of 
the form (x1:A1)...(xn:An)Ind)
This added condiction should be enough to establish an invariant that 
will guarantee the safety of the condition.

    when doing an elimination on the proof of X=Y to change an object 
of type X into an object of type Y the predicate is fun (p:Prop => p) 
which does not meet the condition. Other useful match constructions that 
I know should pass the test.
Christine





On 12/13/2013 11:04 AM, Viktor Vafeiadis wrote:
> On 13 Dec 2013, at 08:21, Christine Paulin wrote:
>
> > The principle is the recursive call in the definition of f x should be of the 
> > form
> >      f t
> > with t a strict recursive subterm of x
> >
> > there is a rule to accept a term t of the form (match u with t1 .. tn end)
> > whenever all ti are recursive subterms of x
> >      in particular when u has type False (match u with end) is accepted
> [...]
> > So some check needs to be added. A simple idea would be that a recursive 
> > subterm could never be an abstraction, or to add some finer analysis in which 
> > context u should be typable.
> An even simpler fix would be to just drop the rule that accepts (match u with 
> t1 .. tn end) as a subterm.
>
> I wonder whether there are any actual proofs that rely on recursive 
> definitions of such form.
>
>
> Viktor