Stream: Coq users

Topic: 'notypeclasses refine' vs 'autoapply' in large contexts


view this post on Zulip Ike Mulder (Sep 26 2023 at 11:53):

I have a project with some custom automation to construct instances for a type class.
The automation uses 'notypeclasses refine' to apply recursive rules.

I've just noticed that in contexts with a large number of variables (around ~120 in scope in one example), the individual calls to 'notypeclasses refine' become slow. Is this expected? I only recent learned of 'autoapply', which does not seem to suffer from this (or at least, much less). My suspicion is that 'notypeclasses refine (some_term _ _ _ _ _)' will have to create and unify a bunch of evars, and that 'autoapply @some_term' is smarter about this?

I will try to replace 'notypeclasses refine' with 'autoapply' and see if this breaks things (old vs new unification..?). Here is a somewhat minimal example.

Inductive TCEq_par {A : Type} (x : A) : A -> A -> A -> A -> A -> A -> A -> Prop :=
  TCEq_refl y1 y2 y3 y4 y5 y6 : TCEq_par x y1 y2 y3 y4 y5 y6 x.


Lemma TCEq_sym {A : Type} (x x' : A) y1 y2 y3 y4 y5 y6 : TCEq_par x' y1 y2 y3 y4 y5 y6 x -> TCEq_par x y1 y2 y3 y4 y5 y6 x'.
Proof. destruct 1. constructor. Qed.

Existing Class TCEq_par.
#[local] Existing Instance TCEq_refl.


Require Import Vector.

Lemma useless_variable P A :
  (forall (n : nat) (v : Vector.t A n), P) ->
  P.
Proof.
  exact (fun f => f O (Vector.nil _)).
Qed.

Ltac introduce_dep_vars :=
  apply (useless_variable _ nat); intros ??.

Lemma test : exists y1 y2 y3 y4 y5 y6, TCEq_par O y1 y2 y3 y4 y5 y6 O.
Proof.
  do 6 eexists.
  do 100 introduce_dep_vars. (* also try with this line commented out completely *)
  time do 30 (notypeclasses refine (TCEq_sym _ _ _ _ _ _ _ _ _)).
  time do 30 (autoapply @TCEq_sym with typeclass_instances).
Abort.

view this post on Zulip Paolo Giarrusso (Sep 26 2023 at 19:58):

cc @Janno


Last updated: Jun 23 2024 at 04:03 UTC