Any reason why there is such a huge slowdown when moving from `Prop`

to `Type`

?

```
From Coq Require Import Setoid Morphisms CMorphisms.
Inductive IdentityList A : list A -> list A -> Prop :=
| IdentityList_nil : IdentityList A nil nil
| IdentityList_cons x l l' : IdentityList A l l' -> IdentityList A (x::l) (x::l').
Theorem IdentityList_refl A l : IdentityList A l l.
Proof. now induction l; constructor. Qed.
Instance IIdentityList_refl A : Reflexive (IdentityList A).
Proof. intros x; apply IdentityList_refl. Qed.
Instance IIdentityList_cons A :
Proper (eq ==> (IdentityList A) ==> (IdentityList A)) cons.
Proof. now intros x y -> l1 l2 HP; apply IdentityList_cons. Qed.
Inductive IdentityList_Type A : list A -> list A -> Type :=
| IdentityList_Type_nil : IdentityList_Type A nil nil
| IdentityList_Type_cons x l l' : IdentityList_Type A l l' -> IdentityList_Type A (x::l) (x::l').
Theorem IdentityList_Type_refl A l : IdentityList_Type A l l.
Proof. now induction l; constructor. Qed.
Instance IIdentityList_Type_refl A : Reflexive (IdentityList_Type A).
Proof. intros x; apply IdentityList_Type_refl. Qed.
Instance IIdentityList_Type_cons A :
Proper (eq ==> (IdentityList_Type A) ==> (IdentityList_Type A)) cons.
Proof. now intros x y -> l1 l2 HP; apply IdentityList_Type_cons. Qed.
Lemma fastProp T (P : list T -> Prop) A B (H : A = B) : P (cons B (cons A nil)).
Proof.
Time rewrite H at 1. (* Finished transaction in 0.035 secs (0.035u,0.s) (successful) *)
Abort.
Lemma slowType T (P : list T -> Type) A B (H : A = B) : P (cons B (cons A nil)).
Proof.
Time rewrite H at 1. (* Finished transaction in 0.776 secs (0.769u,0.006s) (successful) *)
Abort.
```

Blanket explanation: *universes*. As usual, unification is generating many universes and it's very costly to keep them around.

Any way to control it in specific cases to get speed back? (I mostly know nothing about universes).

I don't know any magic trick unfortunately.

Coq generates a literal metric ton of universes without thinking twice, and this is terrible for performance.

Any idea why the problem here does not occur with `rewrite H`

instead of `rewrite H at 1`

?

If I am not mistaken, `rewrite at`

is `setoid_rewrite`

, so a completely different beast from `rewrite`

.

Any way to specify occurrences without paying the complexity of `setoid_rewrite`

?

ssreflect's rewrite ? (I was thinking of `rewrite {1}H.`

)

`pattern ... at ... ; rewrite ...`

Last updated: Jun 18 2024 at 09:02 UTC