Stream: Coq users

Topic: Compute record projections?

Shea Levy (Oct 16 2020 at 09:45):

I'm running a Compute command that gives the following output:

= λ (A : Type) (x : domain (cta {| cta := {| domain := A; first_codomain := A |}; func := λ a : A, a |})), x
     : ∀ A : Type, compose_type' 0 (cta {| cta := {| domain := A; first_codomain := A |}; func := λ a : A, a |})

I would expect each of those projections to fully reduce under compute. Is there a way to get that to happen? The result should just be:

= λ (A : Type) (x : A), x
     : ∀ A : Type, A → A

Is the problem that compute doesn't reduce the type by default? Is there a way to force it to?

Janno (Oct 16 2020 at 09:46):

Try Definition type_of {A : Type} (a : A) := A. and Compute type_of <your term>.?

Shea Levy (Oct 16 2020 at 09:48):

Janno said:

Try Definition type_of {A : Type} (a : A) := A. and Compute type_of <your term>.?

That does reduce as desired. Is there a way to get the whole term to do so?

Janno (Oct 16 2020 at 09:52):

Not in a way that generates nice output, I think. You can try reducing (<your_term>, type_of <your_term>) to get both at the same time (plus the type of that expression itself).

Shea Levy (Oct 16 2020 at 09:53):

Janno said:

Not in a way that generates nice output, I think. You can try reducing (<your_term>, type_of <your_term>) to get both at the same time (plus the type of that expression itself).

Ah cool I'll try that

Shea Levy (Oct 16 2020 at 09:57):

This did the trick:

Record type_red_rec := { red_ty : Type; red_val : red_ty }.
Definition type_red {T} t : type_red_rec := {| red_ty := T; red_val := t |}.
Compute (type_red foo).

Gaëtan Gilbert (Oct 16 2020 at 09:58):

cbv vm_compute not reducing in binders may just be a bug

Shea Levy (Oct 16 2020 at 10:00):

Gaëtan Gilbert said:

cbv not reducing in binders may just be a bug

I'm not sure. If the binders were reduced then the term wouldn't (obviously) be of the appropriate type unless the type itself is reduced too.

Shea Levy (Oct 16 2020 at 10:00):

My intuition for the Compute vernacular though is "normalize as far as you can everywhere", which was violated here.

Gaëtan Gilbert (Oct 16 2020 at 10:01):

I don't understand, what does obviously mean here and why does Compute care?

Shea Levy (Oct 16 2020 at 10:08):

I don't have a full intuition for this, but I've seen times where an explicit cast is needed for a term to be accepted, see https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/Need.20eq.20to.20unfold.3F/near/213484692

Shea Levy (Oct 16 2020 at 10:10):

This reduces the term: Compute (foo : ∀ A, A → A).)

Shea Levy (Oct 16 2020 at 10:10):

Which makes me think it's definitely about reducing the type

Gaëtan Gilbert (Oct 16 2020 at 10:19):

removing casts isn't the same as reducing in binders

Gaëtan Gilbert (Oct 16 2020 at 10:20):

and that thread is a unification issue because some of the term contains holes

Shea Levy (Oct 16 2020 at 10:22):

OK. All I know is Compute foo does not reduce and Compute (foo : ∀ A, A → A). does

Last updated: Oct 01 2023 at 17:01 UTC