The Coq mailing list

[Randy Pollack <rpollack AT inf.ed.ac.uk>]

Hi Matthieu

>
> The cast is a term constructor.
>

What are the rules for typing and computation of cast terms?  That
would answer my questions.

Randy
--
On Tue, Apr 28, 2015 at 1:16 PM, Matthieu Sozeau 
<mattam AT mattam.org>
 wrote:
> Hi Randy,
>
> On Tue, Apr 28, 2015 at 7:46 AM Randy Pollack 
> <rpollack AT inf.ed.ac.uk>
>  wrote:
>>
>> I am unclear about Coq's type casting.
>>
>> Consider
>>
>> Check (cons: forall (A:Set), A -> list A -> list A).
>> (fun A : Set => cons (A:=A)):forall A : Set, A -> list A -> list A
>>      : forall A : Set, A -> list A -> list A
>>
>> It looks like the cast [ (cons: forall (A:Set), A -> list A -> list A).]
>> is
>> a meta-notation for the eta-expansion.  Then why is the cast still in the
>> term?
>
>
> The cast is a term constructor.
>
>>
>>
>> Now consider
>>
>> Goal (cons: forall (A:Set), A -> list A -> list A) =
>>        (cons: forall (A:Set), A -> list A -> list A).
>> cbv beta.
>>
>> Goal is:
>>
>>    (fun A : Set => cons (A:=A)) = (fun A : Set => cons (A:=A))
>>
>> The cast was removed even though no beta steps were taken.  What is
>> the official story about when casts are removed in Coq?
>
>
> The story is you shouldn't expect any tactic to preserve them. They're
> "just" hints to drive conversion.
>
>> Finally consider
>>
>> Goal (cons: forall (A:Set), A -> list A -> list A) = cons.
>>
>> The Goal is
>>
>> ((fun A : Set => cons (A:=A)):forall A : Set, A -> list A -> list A) =
>> (fun A : Set => cons (A:=A))
>>
>> Why was the RHS eta expanded in this way?  This is not the goal I
>> entered; this goal is true (solved by reflexivity), but the tactic
>
>
> The coercion mechanism introduces those eta-expansions on the fly during
> refinement even though no actual coercion could be found after the
> expansion, i.e A -> list A -> list A becomes simply convertible with A ->
> list A -> list A. The coercion goes from Π A : Type, ... to Π A : Set ...
> here.
>
>> constr_eq (cons: forall (A:Set), A -> list A -> list A) cons.
>
>
> They aren't: the lhs is actually eta-expanded to match the casts' type,
> while the rhs stays a cons : forall A : Type, A -> list A -> list A.
> constr_eq rightly says they're different terms.
>
> Hope this helps,
> -- Matthieu