Stream: Coq users

Topic: Compute record projections?


view this post on Zulip 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?

view this post on Zulip Janno (Oct 16 2020 at 09:46):

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

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Gaëtan Gilbert (Oct 16 2020 at 09:58):

cbv vm_compute not reducing in binders may just be a bug

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Gaëtan Gilbert (Oct 16 2020 at 10:01):

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

view this post on Zulip 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

view this post on Zulip Shea Levy (Oct 16 2020 at 10:10):

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

view this post on Zulip Shea Levy (Oct 16 2020 at 10:10):

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

view this post on Zulip Gaëtan Gilbert (Oct 16 2020 at 10:19):

removing casts isn't the same as reducing in binders

view this post on Zulip Gaëtan Gilbert (Oct 16 2020 at 10:20):

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

view this post on Zulip 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: Jan 29 2023 at 01:02 UTC