From b0b613f5ba4e42ba4a476a73a9e33bd3f530620c Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ga=C3=ABtan=20Gilbert?= Date: Fri, 26 Jul 2024 13:22:55 +0200 Subject: [PATCH] speedup wf{3,4}_of_wf by factorizing raw matches to definitions This greatly reduces term size (tree size 1988106 -> 1121651 for wf3_of_wf). Timings before: (Succeed Qed includes some time which isn't in Time Qed, see also https://github.com/coq/coq/pull/19426) wf3 tactics 2.2s qed 1.09s succeed qed 1.25s wf4 tactics 14.5s qed 7.4s succeed qed 8.5s After: wf3 tactics 1.4s qed 0.6s succeed qed 0.65s wf4 tactics 8s qed 3.6s succeed qed 4s --- src/Rewriter/Language/Wf.v | 83 +++++++++++++++++++++++++++++++++----- 1 file changed, 74 insertions(+), 9 deletions(-) diff --git a/src/Rewriter/Language/Wf.v b/src/Rewriter/Language/Wf.v index c8fcbe318..b5f7503c2 100644 --- a/src/Rewriter/Language/Wf.v +++ b/src/Rewriter/Language/Wf.v @@ -1299,12 +1299,39 @@ Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed. variables they use. *) Abort. + Definition wf3_aux1 {var1 var2 var3} + (x:(sigT (fun t : type base_type => var1 t * var2 t * var3 t)%type)) + := match x with + (existT t (v1, v2, v3)) => + existT (fun t => var1 t * (var1 t * var2 t * var3 t))%type + t + (v1, (v1, v2, v3)) + end. + + Definition wf3_aux2 {var1 var2 var3} + (x:(sigT (fun t : type base_type => var1 t * var2 t * var3 t)%type)) + := match x with + (existT t (v1, v2, v3)) => + existT (fun t => var2 t * (var1 t * var2 t * var3 t))%type + t + (v2, (v1, v2, v3)) + end. + + Definition wf3_aux3 {var1 var2 var3} + (x:(sigT (fun t : type base_type => var1 t * var2 t * var3 t)%type)) + := match x with + (existT t (v1, v2, v3)) => + existT (fun t => var3 t * (var1 t * var2 t * var3 t))%type + t + (v3, (v1, v2, v3)) + end. + (* Speeds up Qed by a couple seconds *) Local Strategy -100 [invert_expr.invert_Var invert_expr.invert_LetIn invert_expr.invert_App invert_expr.invert_LetIn invert_expr.invert_Ident invert_expr.invert_Abs invert_expr.invert_App_cps projT1 projT2 fst snd eq_rect]. Lemma wf3_of_wf {var1 var2 var3} G1 G2 G3 G {t} - (HG1 : G1 = List.map (fun '(existT t (v1, v2, v3)) => existT _ t (v1, (v1, v2, v3))) G) - (HG2 : G2 = List.map (fun '(existT t (v1, v2, v3)) => existT _ t (v2, (v1, v2, v3))) G) - (HG3 : G3 = List.map (fun '(existT t (v1, v2, v3)) => existT _ t (v3, (v1, v2, v3))) G) + (HG1 : G1 = List.map wf3_aux1 G) + (HG2 : G2 = List.map wf3_aux2 G) + (HG3 : G3 = List.map wf3_aux3 G) e1 e2 e3 e123 (Hwf1 : @wf var1 _ G1 t e1 e123) (Hwf2 : @wf var2 _ G2 t e2 e123) @@ -1313,7 +1340,8 @@ Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed. Proof using Type. subst G2 G3; revert dependent e3; revert dependent e2; revert dependent G; induction Hwf1; intros. Time all: repeat first [ progress subst - | progress cbn [projT1 projT2 fst snd eq_rect] in * + | progress cbn [projT1 projT2 fst snd eq_rect + wf3_aux1 wf3_aux2 wf3_aux3] in * | progress destruct_head' False | progress destruct_head'_sig | progress destruct_head'_and @@ -1366,11 +1394,47 @@ Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed. : @wf _ _ G1 t e1 e2. Proof using Type. eapply wf_of_wf3_default; eauto. Qed. + Definition wf4_aux1 {var1 var2 var3 var4} + (x:(sigT (fun t : type base_type => var1 t * var2 t * var3 t * var4 t)%type)) + := match x with + (existT t (v1, v2, v3, v4)) => + existT (fun t => var1 t * (var1 t * var2 t * var3 t * var4 t))%type + t + (v1, (v1, v2, v3, v4)) + end. + + Definition wf4_aux2 {var1 var2 var3 var4} + (x:(sigT (fun t : type base_type => var1 t * var2 t * var3 t * var4 t)%type)) + := match x with + (existT t (v1, v2, v3, v4)) => + existT (fun t => var2 t * (var1 t * var2 t * var3 t * var4 t))%type + t + (v2, (v1, v2, v3, v4)) + end. + + Definition wf4_aux3 {var1 var2 var3 var4} + (x:(sigT (fun t : type base_type => var1 t * var2 t * var3 t * var4 t)%type)) + := match x with + (existT t (v1, v2, v3, v4)) => + existT (fun t => var3 t * (var1 t * var2 t * var3 t * var4 t))%type + t + (v3, (v1, v2, v3, v4)) + end. + + Definition wf4_aux4 {var1 var2 var3 var4} + (x:(sigT (fun t : type base_type => var1 t * var2 t * var3 t * var4 t)%type)) + := match x with + (existT t (v1, v2, v3, v4)) => + existT (fun t => var4 t * (var1 t * var2 t * var3 t * var4 t))%type + t + (v4, (v1, v2, v3, v4)) + end. + Lemma wf4_of_wf {var1 var2 var3 var4} G1 G2 G3 G4 G {t} - (HG1 : G1 = List.map (fun '(existT t (v1, v2, v3, v4)) => existT _ t (v1, (v1, v2, v3, v4))) G) - (HG2 : G2 = List.map (fun '(existT t (v1, v2, v3, v4)) => existT _ t (v2, (v1, v2, v3, v4))) G) - (HG3 : G3 = List.map (fun '(existT t (v1, v2, v3, v4)) => existT _ t (v3, (v1, v2, v3, v4))) G) - (HG4 : G4 = List.map (fun '(existT t (v1, v2, v3, v4)) => existT _ t (v4, (v1, v2, v3, v4))) G) + (HG1 : G1 = List.map wf4_aux1 G) + (HG2 : G2 = List.map wf4_aux2 G) + (HG3 : G3 = List.map wf4_aux3 G) + (HG4 : G4 = List.map wf4_aux4 G) e1 e2 e3 e4 e1234 (Hwf1 : @wf var1 _ G1 t e1 e1234) (Hwf2 : @wf var2 _ G2 t e2 e1234) @@ -1380,7 +1444,8 @@ Proof. hnf; etransitivity; eassumption || symmetry; eassumption. Qed. Proof using Type. subst G2 G3 G4; revert dependent e4; revert dependent e3; revert dependent e2; revert dependent G; induction Hwf1; intros. Time all: repeat first [ progress subst - | progress cbn [projT1 projT2 fst snd eq_rect] in * + | progress cbn [projT1 projT2 fst snd eq_rect + wf4_aux1 wf4_aux2 wf4_aux3 wf4_aux4] in * | progress destruct_head' False | progress destruct_head'_sig | progress destruct_head'_and