Stream: Coq users

Topic: Setoid_rewrite: slow down between Prop and Type


view this post on Zulip Olivier Laurent (Jun 03 2021 at 16:25):

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.

view this post on Zulip Pierre-Marie Pédrot (Jun 03 2021 at 17:39):

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

view this post on Zulip Olivier Laurent (Jun 03 2021 at 18:04):

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

view this post on Zulip Pierre-Marie Pédrot (Jun 03 2021 at 18:08):

I don't know any magic trick unfortunately.

view this post on Zulip Pierre-Marie Pédrot (Jun 03 2021 at 18:09):

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

view this post on Zulip Olivier Laurent (Jun 03 2021 at 18:20):

Any idea why the problem here does not occur with rewrite H instead of rewrite H at 1?

view this post on Zulip Guillaume Melquiond (Jun 03 2021 at 18:30):

If I am not mistaken, rewrite at is setoid_rewrite, so a completely different beast from rewrite.

view this post on Zulip Olivier Laurent (Jun 03 2021 at 18:32):

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

view this post on Zulip Kenji Maillard (Jun 03 2021 at 18:34):

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

view this post on Zulip Guillaume Melquiond (Jun 03 2021 at 18:35):

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


Last updated: Jan 31 2023 at 14:03 UTC