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?

Try `Definition type_of {A : Type} (a : A) := A.`

and `Compute type_of <your term>.`

?

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?

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).

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

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).
```

~~cbv~~ vm_compute not reducing in binders may just be a bug

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.

My intuition for the `Compute`

vernacular though is "normalize as far as you can everywhere", which was violated here.

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

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

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

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

removing casts isn't the same as reducing in binders

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

OK. All I know is `Compute foo`

does not reduce and `Compute (foo : ∀ A, A → A).`

does

Last updated: Jun 16 2024 at 01:42 UTC