rm problematic variables under beta redexes for evar instantiation #19833

Tragicus · 2024-11-14T12:46:44Z

Extracted from #19822 as suggested here.
The unification algorithm sometimes fails on problems of the form ?a = t because variables that are not in the scope of ?a appear in t. We can easily solve the problem when the variable appears in a beta-redex, as in (fun _ => t) x.

Fixes / closes #????

Added / updated test-suite.

Added changelog.
Added / updated documentation.
- Documented any new / changed user messages.
- Updated documented syntax by running make doc_gram_rsts.

Opened overlay pull requests.

JasonGross · 2024-11-14T13:11:33Z

coq/test-suite/bugs/bug_3209.v

Lines 28 to 74 in ac0fd36

    
           (* This used to fail with a Not_found, we fail more graciously but a 
        
              heuristic could be implemented, e.g. in some smart occur-check 
        
              function, to find a solution of then form ?P := fun _ => ?P' *) 
        
           Fail Check (fun e : ?[T] => bar ?[A] ?[P] (fun g : ?[A'] => g e)). 
        
           (* This works and tells which solution we could have inferred *) 
        
           Check (fun e : ?[T] => bar ?[A] (fun _ => ?[P]) (fun g : ?[A'] => g e)). 
        
           (* For the record, here is the trace in the failing example: 
        
           In (fun e : ?T => bar ?[A] ?[P] (fun g : ?A' => g e)), we have the existential variables 
        
           e:?T |- ?A : Prop 
        
           e:?T |- ?P : foo ?A -> Prop 
        
           e:?T |- ?A' : Type 
        
           with constraints 
        
           ?A' == ?A 
        
           ?A' == ?T -> ?P (Foo ?A) 
        
           To type (g e), unification first defines 
        
           ?A := forall x:?B, ?P'{e:=e,x:=x} 
        
           with ?T <= ?B 
        
           and ?P'@{e:=e,x:=e} <= ?P@{e:=e} (Foo (forall x:?B, ?P'{e:=e,x:=x})) 
        
           Then, since ?P'@{e:=e,x:=e} may use "e" in two different ways, it is 
        
           not a pattern and we define a new 
        
           e:?T x:?B|- ?P'' : foo (?B' -> ?P''') -> Prop 
        
           for some ?B' and ?P''', together with 
        
           ?P'@{e,x} := ?P''{e:=e,x:=e} (Foo (?B -> ?P') 
        
           ?P@{e} := ?P''{e:=e,x:=e} 
        
           Moreover, ?B' and ?P''' have to satisfy 
        
           ?B'@{e:=e,x:=e} == ?B@{e:=e} 
        
           ?P'''@{e:=e,x:=e} == ?P'@{e:=e,x:=x} 
        
           and this leads to define ?P' which was the initial existential 
        
           variable to define. 
        
           *)

needs to be fixed
@coqbot run full ci

JasonGross · 2024-11-15T02:48:37Z

@coqbot run full ci

ppedrot · 2024-11-15T10:42:46Z

@coqbot bench

JasonGross · 2024-11-15T21:17:02Z

CI seems to pass, let's see what the bench says

coqbot-app · 2024-11-16T00:11:33Z

🏁 Bench results:

┌─────────────────────────────────────┬─────────────────────────┬───────────────────────────────────────┬─────────────────────────┐
│                                     │      user time [s]      │           CPU instructions            │  max resident mem [KB]  │
│                                     │                         │                                       │                         │
│            package_name             │   NEW      OLD    PDIFF │      NEW             OLD        PDIFF │   NEW      OLD    PDIFF │
├─────────────────────────────────────┼─────────────────────────┼───────────────────────────────────────┼─────────────────────────┤
│              coq-mathcomp-ssreflect │  106.08   107.59  -1.40 │   680455105182    680456711804  -0.00 │ 1646648  1648028  -0.08 │
│             coq-metacoq-safechecker │  346.52   349.01  -0.71 │  2645610883518   2646000577379  -0.01 │ 1712052  1711396   0.04 │
│                coq-mathcomp-algebra │  162.83   163.65  -0.50 │  1097282667500   1097256050751   0.00 │ 1260272  1259704   0.05 │
│              coq-mathcomp-odd-order │  537.04   539.63  -0.48 │  3739284117988   3738888968240   0.01 │ 1576664  1574248   0.15 │
│                           coq-verdi │   44.73    44.89  -0.36 │   301062378805    301100460618  -0.01 │  524420   524608  -0.04 │
│                        coq-coqprime │   52.22    52.40  -0.34 │   363009421675    363000374676   0.00 │  784404   784444  -0.01 │
│                          coq-stdlib │  362.68   363.67  -0.27 │  1258370264321   1258321608859   0.00 │  630008   629900   0.02 │
│         coq-rewriter-perf-SuperFast │  777.36   779.15  -0.23 │  5968773502890   5967062253322   0.03 │ 1393848  1396480  -0.19 │
│                 coq-category-theory │  600.67   601.96  -0.21 │  4467973908545   4467775762310   0.00 │  914368   913828   0.06 │
│                  coq-mathcomp-field │   90.15    90.34  -0.21 │   630098899547    630076093842   0.00 │ 1164356  1161524   0.24 │
│               coq-engine-bench-lite │  131.46   131.48  -0.02 │   968600973495    968845494081  -0.03 │ 1068888  1068984  -0.01 │
│               coq-mathcomp-analysis │  586.69   586.21   0.08 │  4363676866447   4358878319416   0.11 │ 1845164  1844784   0.02 │
│ coq-neural-net-interp-computed-lite │  234.42   234.18   0.10 │  2254120380003   2254163638611  -0.00 │  854696   855476  -0.09 │
│                    coq-fiat-parsers │  276.76   276.38   0.14 │  2141199956520   2141388396179  -0.01 │ 2290084  2287260   0.12 │
│                        coq-rewriter │  338.18   337.62   0.17 │  2519776004935   2519248835894   0.02 │ 1299100  1300012  -0.07 │
│                 coq-metacoq-erasure │  517.24   516.34   0.17 │  3582790457813   3582744597513   0.00 │ 1823952  1824712  -0.04 │
│                   coq-metacoq-pcuic │  674.36   672.99   0.20 │  4387362124169   4387201485256   0.00 │ 2302856  2302404   0.02 │
│                         coq-coqutil │   43.43    43.34   0.21 │   275137496252    275153013865  -0.01 │  555744   554912   0.15 │
│                      coq-verdi-raft │  537.47   536.31   0.22 │  3735672699515   3735658152456   0.00 │  821532   819284   0.27 │
│                coq-metacoq-template │  147.53   147.19   0.23 │   993687386669    993698701814  -0.00 │ 1047052  1046584   0.04 │
│                        coq-compcert │  303.31   302.48   0.27 │  1994772191081   1994670204571   0.01 │ 1168920  1174680  -0.49 │
│                            coq-core │  133.82   133.45   0.28 │   541365975194    541231264578   0.02 │  485804   484624   0.24 │
│                        coq-bedrock2 │  325.94   325.03   0.28 │  2732897843265   2732875245457   0.00 │  852472   852472   0.00 │
│                            coq-hott │  156.82   156.37   0.29 │  1096367835918   1096350128407   0.00 │  467432   468460  -0.22 │
│                   coq-metacoq-utils │   23.36    23.29   0.30 │   153780049798    153735597154   0.03 │  597568   595540   0.34 │
│                         coq-unimath │ 2015.93  2009.36   0.33 │ 16061113777476  16061976968359  -0.01 │ 1108432  1109668  -0.11 │
│               coq-mathcomp-solvable │   95.69    95.36   0.35 │   662112457095    662109577990   0.00 │  881104   879192   0.22 │
│        coq-fiat-crypto-with-bedrock │ 5868.45  5846.58   0.37 │ 47453055140833  47448527035734   0.01 │ 3245472  3245456   0.00 │
│                   coq-iris-examples │  393.66   391.93   0.44 │  2635469290286   2635023323759   0.02 │ 1099276  1090896   0.77 │
│                             coq-vst │  866.77   862.85   0.45 │  6525071846560   6525184701744  -0.00 │ 2192792  2192528   0.01 │
│                            coq-corn │  677.33   672.96   0.65 │  4682139943897   4682228578832  -0.00 │  723280   721468   0.25 │
│                      coq-test-suite │  517.39   513.75   0.71 │  3614346547573   3615746299253  -0.04 │ 2699992  2927400  -7.77 │
│                  coq-metacoq-common │   67.46    66.97   0.73 │   441995506292    441883571297   0.03 │ 1045488  1044864   0.06 │
│                       coq-equations │    7.92     7.86   0.76 │    53182556999     53182569249  -0.00 │  389616   388456   0.30 │
│                           coq-color │  248.07   246.17   0.77 │  1574523347200   1574595055020  -0.00 │ 1123912  1125624  -0.15 │
│              coq-mathcomp-character │   76.11    75.52   0.78 │   504241711349    504362615630  -0.02 │  938212   940188  -0.21 │
│          coq-performance-tests-lite │  915.10   907.54   0.83 │  7321564743699   7321114534850   0.01 │ 2448136  2446832   0.05 │
│                    coq-math-classes │   86.60    85.84   0.89 │   535240274481    535189505608   0.01 │  500196   499308   0.18 │
│                         coq-bignums │   30.43    30.13   1.00 │   194588672133    194635286841  -0.02 │  473460   474448  -0.21 │
│            coq-metacoq-translations │   16.65    16.47   1.09 │   117762285689    117765634884  -0.00 │  779272   776908   0.30 │
│               coq-mathcomp-fingroup │   26.42    26.13   1.11 │   172210881369    172208234747   0.00 │  561832   563912  -0.37 │
│                       coq-fourcolor │ 1365.12  1348.86   1.21 │ 12541627829212  12541542073399   0.00 │  873532   874756  -0.14 │
│                      coq-coquelicot │   38.12    37.62   1.33 │   230545381653    230540569093   0.00 │  808460   804808   0.45 │
│                       coq-fiat-core │   59.04    58.18   1.48 │   360302794837    360265451343   0.01 │  474092   474112  -0.00 │
└─────────────────────────────────────┴─────────────────────────┴───────────────────────────────────────┴─────────────────────────┘

🐢 Top 25 slow downs

┌──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SLOW DOWNS                                                                 │
│                                                                                                                                                  │
│   OLD       NEW      DIFF   %DIFF   Ln                      FILE                                                                                 │
├──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 181.8180  184.5120  2.6940   1.48%  233  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeByExtension.v.html │
│  64.2200   65.4450  1.2250   1.91%  609  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/lightbulb.v.html           │
│ 118.6330  119.8150  1.1820   1.00%   22  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/ArithWithCasts.v.html                                  │
│ 100.8180  101.9350  1.1170   1.11%  968  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│ 100.8290  101.9120  1.0830   1.07%  999  coq-performance-tests-lite/src/fiat_crypto_via_setoid_rewrite_standalone.v.html                         │
│  37.7530   38.6120  0.8590   2.28%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/WithBedrock/fiat_crypto.v.html                     │
│   3.1310    3.8670  0.7360  23.51%  490  coq-stdlib/Reals/Cauchy/ConstructiveCauchyRealsMult.v.html                                              │
│  35.9650   36.6870  0.7220   2.01%    2  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/fiat_crypto.v.html                                 │
│  29.3860   30.0440  0.6580   2.24%   12  coq-fourcolor/theories/proof/job001to106.v.html                                                         │
│  37.9980   38.6500  0.6520   1.72%  548  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/compiler/src/compiler/MMIO.v.html                        │
│  37.7830   38.4160  0.6330   1.68%    3  coq-fiat-crypto-with-bedrock/src/ExtractionJsOfOCaml/bedrock2_fiat_crypto.v.html                        │
│  23.4270   24.0350  0.6080   2.60%   12  coq-fourcolor/theories/proof/job554to562.v.html                                                         │
│ 235.7310  236.3260  0.5950   0.25%  141  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│  28.7890   29.3690  0.5800   2.01%   12  coq-fourcolor/theories/proof/job589to610.v.html                                                         │
│  18.1350   18.7010  0.5660   3.12%   12  coq-fourcolor/theories/proof/job315to318.v.html                                                         │
│  32.5100   33.0020  0.4920   1.51%   12  coq-fourcolor/theories/proof/job439to465.v.html                                                         │
│  28.4150   28.9000  0.4850   1.71%   12  coq-fourcolor/theories/proof/job563to588.v.html                                                         │
│  18.1840   18.6620  0.4780   2.63%   12  coq-fourcolor/theories/proof/job311to314.v.html                                                         │
│  17.1880   17.6420  0.4540   2.64%  841  coq-fiat-crypto-with-bedrock/src/Curves/Weierstrass/Jacobian/CoZ.v.html                                 │
│ 132.9790  133.4320  0.4530   0.34%  155  coq-fiat-crypto-with-bedrock/src/UnsaturatedSolinasHeuristics/Tests.v.html                              │
│  28.8190   29.2710  0.4520   1.57%   12  coq-fourcolor/theories/proof/job323to383.v.html                                                         │
│  21.4710   21.9230  0.4520   2.11%   12  coq-fourcolor/theories/proof/job542to545.v.html                                                         │
│  26.3790   26.8280  0.4490   1.70%   12  coq-fourcolor/theories/proof/job190to206.v.html                                                         │
│  28.1970   28.6430  0.4460   1.58%   32  coq-fiat-crypto-with-bedrock/src/Bedrock/End2End/X25519/MontgomeryLadderRISCV.v.html                    │
│  31.8960   32.3290  0.4330   1.36%   97  coq-vst/veric/binop_lemmas5.v.html                                                                      │
└──────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🐇 Top 25 speed ups

┌─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┐
│                                                                TOP 25 SPEED UPS                                                                 │
│                                                                                                                                                 │
│   OLD      NEW     DIFF     %DIFF    Ln                      FILE                                                                               │
├─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┤
│ 19.9280  18.6320  -1.2960   -6.50%   601  coq-mathcomp-odd-order/theories/PFsection9.v.html                                                     │
│ 94.2060  93.1810  -1.0250   -1.09%    20  coq-fiat-crypto-with-bedrock/src/Rewriter/Passes/NBE.v.html                                           │
│  5.0740   4.3970  -0.6770  -13.34%  2089  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                                │
│  2.3330   1.8280  -0.5050  -21.65%   202  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                              │
│ 11.3080  10.8330  -0.4750   -4.20%  2103  coq-mathcomp-ssreflect/mathcomp/ssreflect/order.v.html                                                │
│ 39.2860  38.8180  -0.4680   -1.19%   835  coq-fiat-crypto-with-bedrock/src/Fancy/Compiler.v.html                                                │
│  1.4590   1.0520  -0.4070  -27.90%  1142  coq-stdlib/FSets/FMapAVL.v.html                                                                       │
│ 46.6240  46.2620  -0.3620   -0.78%   110  coq-bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html                                            │
│ 18.2200  17.9230  -0.2970   -1.63%     6  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/DecodeEncodeCSR.v.html │
│  6.9580   6.6680  -0.2900   -4.17%   872  coq-mathcomp-analysis/theories/derive.v.html                                                          │
│ 24.3850  24.0960  -0.2890   -1.19%   558  coq-bedrock2/bedrock2/src/bedrock2Examples/insertionsort.v.html                                       │
│ 46.7250  46.4400  -0.2850   -0.61%   110  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/bedrock2/src/bedrock2Examples/full_mul.v.html          │
│ 12.7380  12.4710  -0.2670   -2.10%  1555  coq-fiat-crypto-with-bedrock/src/Util/FSets/FMapTrie.v.html                                           │
│  7.8700   7.6060  -0.2640   -3.35%   602  coq-unimath/UniMath/CategoryTheory/EnrichedCats/Limits/Examples/StructureEnrichedLimits.v.html        │
│ 42.4250  42.1630  -0.2620   -0.62%    50  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│  0.7330   0.4720  -0.2610  -35.61%   870  coq-stdlib/MSets/MSetRBT.v.html                                                                       │
│  7.2010   6.9800  -0.2210   -3.07%   130  coq-category-theory/Functor/Strong/Product.v.html                                                     │
│  0.8980   0.6860  -0.2120  -23.61%   204  coq-stdlib/setoid_ring/Ncring_tac.v.html                                                              │
│  5.7890   5.5850  -0.2040   -3.52%   888  coq-vst/veric/binop_lemmas4.v.html                                                                    │
│ 26.9200  26.7170  -0.2030   -0.75%    68  coq-fiat-crypto-with-bedrock/rupicola/bedrock2/deps/riscv-coq/src/riscv/Proofs/VerifyDecode.v.html    │
│  5.7760   5.5770  -0.1990   -3.45%   196  coq-fiat-crypto-with-bedrock/src/Bedrock/Field/Synthesis/Examples/p224_64_new.v.html                  │
│ 43.0720  42.8740  -0.1980   -0.46%   834  coq-vst/veric/binop_lemmas4.v.html                                                                    │
│  0.3340   0.1370  -0.1970  -58.98%    11  coq-stdlib/Reals/Abstract/ConstructiveLimits.v.html                                                   │
│ 18.7530  18.5560  -0.1970   -1.05%    31  coq-engine-bench-lite/coq/PerformanceDemos/pattern.v.html                                             │
│  0.3260   0.1300  -0.1960  -60.12%  1045  coq-stdlib/Reals/Abstract/ConstructiveReals.v.html                                                    │
└─────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────────┘

🪑 GitLab Bench Job

JasonGross · 2024-11-16T00:26:21Z

Bench results look like mostly noise, especially from the CPU column. As far as I'm concerned, this could be good to go with just needs a changelog and a review from @coq/pretyper-maintainers. @Tragicus , could you add a test-suite example that fails on master and passes with this change?

doc/changelog/02-specification-language/19833-evd-inst-beta.rst

Co-authored-by: Jason Gross <jasongross9@gmail.com>

Tragicus requested a review from a team as a code owner November 14, 2024 12:46

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 14, 2024

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 14, 2024

Tragicus mentioned this pull request Nov 14, 2024

rm problematic variables under beta-redexes and evars for evar instantiation #19822

Open

6 tasks

rm problematic variables under beta redexes for evar instantiation

7f21d39

Tragicus force-pushed the evd-inst-beta branch from 249c5fd to 7f21d39 Compare November 14, 2024 17:09

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 14, 2024

coqbot-app bot removed the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 15, 2024

JasonGross added the needs: changelog entry This should be documented in doc/changelog. label Nov 16, 2024

changelog and test-suite example

4477d89

coqbot-app bot added the needs: full CI The latest GitLab pipeline that ran was a light CI. Say "@coqbot run full ci" to get a full CI. label Nov 17, 2024

JasonGross reviewed Nov 17, 2024

View reviewed changes

doc/changelog/02-specification-language/19833-evd-inst-beta.rst Outdated Show resolved Hide resolved

changelog msg

114cf23

Co-authored-by: Jason Gross <jasongross9@gmail.com>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

rm problematic variables under beta redexes for evar instantiation #19833

rm problematic variables under beta redexes for evar instantiation #19833

rm problematic variables under beta redexes for evar instantiation #19833

Are you sure you want to change the base?

rm problematic variables under beta redexes for evar instantiation #19833

Conversation