The Coq mailing list

[Randy Pollack <rpollack0 AT gmail.com>]

This "answer" doesn't explain either of the observations I asked about:

> Type inference is as you would expect: Γ |- t : A  /\ A =c B ----> Γ |- (t
> :c B) : B. The :c can be just regular kernel conversion or call to a VM
> (bytecode or native). Reduction ignores casts entirely (AFAICT).

Type inference apparently causes eta-expansion of the term t, but
Matthieu's purported type inference rule doesn't change t.

Apparently reduction causes the cast "term constructor" to be dropped,
at least in some cases, which is not the same as ignoring casts
entirely.

Finally, consider again the goal command

   Goal (cons: forall (A:Set), A -> list A -> list A) = cons.

Coq shows the goal to be

    ((fun A : Set => cons (A:=A)):forall A : Set, A -> list A -> list A) =
    (fun A : Set => cons (A:=A))

Why is the RHS eta-expanded?

--Randy
> -- Matthieu
>
> On Tue, Apr 28, 2015 at 9:17 AM Randy Pollack 
> <rpollack AT inf.ed.ac.uk>
>  wrote:
>>
>> 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