The Coq mailing list

[Hugo Herbelin <Hugo.Herbelin AT inria.fr>]

  Dear Antonia,

  Your question points out a default of the typing rule of Cases in
Coq w.r.t. convertibility.

  Actually, the convertibility of two Cases expressions needs the
convertibility of the predicates put in the <..> annotation. But these
predicates may have two forms: actually they can be or not dependent
on the matched term. In "toto", you explicitly give a dependent
predicate (even if the dependency is dummy), while in "toto" a
predicate is automatically inferred which is non dependent (though
hidden -- because automatically inferrable --, it is "nat").  Since
these predicates in <...> are different, the whole expressions are
considered different. This explains the typing error raised by the
Check command.

  Time to make the typing rule of Cases more uniform... which will be
the case in Coq V7.

                                                  Hugo
 
> Dear all,
> 
>       I'm trying to type the expressions: titi and toto (see below),
>  and I would like to know why these two terms do not have the same type.
> The last Check command raises an error. Could you explain me why?
> 
> Best Regards.
>       Antonia
> -----------------------------------------------------------------------------
> 
> Require Arith.
> Require Compare_dec.
> 
> Variable x : nat.
> Variable toto :  O
>         =(<[_:{x=O}+{(lt O x)}]nat>Cases (zerop x) of
>             (left _) => O
>           | (right _) => O
>           end).
> 
> Variable titi : O = (Cases (zerop x) of
>                        (left _) => O
>                      | (right _) => O
>                      end).
> 
> Check (titi::  O
>         =(<[_:{x=O}+{(lt O x)}]nat>Cases (zerop x) of
>             (left _) => O
>           | (right _) => O
>           end)).
> 
> 
>   Antonia
> 
>