feat: aesop_contractive tactic to solve Contractive/NonExpansive goals

[arthur-adjedj]

Description

This is a proof of concept that is not meant to be merged as is. This draft implements an aesop_contractive tactic which is meant to help solve Contractive and NonExpansive goals, similar in use to Rocq's f_contractive tactic. This tactic works by building up a custom aesop ruleset, similarly to Mathlib's aesop_cat's. There is a drawback to the tactic:
Many useful Contractive theorems are hidden behind a foo : NonExpansive instance, which means one needs to write a projection foo.ne to access this theorem. However, aesop expects declarations, not arbitrary terms, for its aesop rules, and in particular, one cannot tag such a projection term foo.ne as an aesop rule. To solve this, the PR adds a new a new @[aesop_contractive <rule-type>], generally equivalent to @[aesop safe <rule-type> (rule_sets := [aesop_contractive])], except when tagging a NonExpansive/NonExpansive₂ instance. In that case, it generates the relevant auxiliary theorem and tags that instead.

[markusdemedeiros]

Agreed with adding an aesop_contractive attribute to eliminate the boilerplate

[lzy0505]

Very cool! aesop_contractive sounds like a good idea.

[arthur-adjedj]

Agreed with adding an aesop_contractive attribute to eliminate the boilerplate

That is now implemented. I do not know if it would be useful for the tag to generate such auxiliary declarations for cases other than NonExpansive/NonExpansive₂, so these two are hard-coded for now.

[MackieLoeffel]

I played around with the PR and tweaked the annotations such that aesop_contractive can fully solve the goals. However, it seems like aesop is quite slow. The typeclass instances take around half a second to solve, which is quite slow. When I replace aesop with the solution it finds, it takes around 70ms. I am wondering if a more specialized tactic than aesop could be much faster than using all the power of aesop.

[arthur-adjedj]

However, it seems like aesop is quite slow.

Using set_option aesop.collectStats true and #aesop_stats shows me the following wp.pre.contractive:

Statistics for 1 Aesop calls in current and imported modules
Displaying totals and [averages]
Total Aesop time:      888.6ms [888.6ms]
Config parsing:        10.2ms [10.2ms]
Rule set construction: 7.5ms [7.5ms]
Rule selection:        38.8ms [38.8ms]
Script generation:     0.0ms [0.0ms]
Search:                870.7ms [870.7ms]
Forward state updates: 6.9ms [6.9ms]
Rules:
  <norm simp>:
    total:      30 in 555.2ms [18.5ms]
    successful: 30 in 555.2ms [18.5ms]
    failed:     0 in 0.0ms [0.0ms]
  <norm unfold>:
    total:      32 in 65.2ms [2.0ms]
    successful: 32 in 65.2ms [2.0ms]
    failed:     0 in 0.0ms [0.0ms]
  safe|tactic|global|Aesop.BuiltinRules.assumption:
    total:      21 in 48.4ms [2.3ms]
    successful: 0 in 0.0ms [0.0ms]
    failed:     21 in 48.4ms [2.3ms]
  safe|apply|global|Iris.BI.forall_ne:
    total:      8 in 26.7ms [3.3ms]
    successful: 8 in 26.7ms [3.3ms]
    failed:     0 in 0.0ms [0.0ms]
  norm|tactic|global|Aesop.BuiltinRules.intros:
    total:      42 in 12.4ms [0.2ms]
    successful: 10 in 4.9ms [0.4ms]
    failed:     32 in 7.4ms [0.2ms]
  safe|tactic|global|Aesop.BuiltinRules.splitTarget:
    total:      3 in 11.3ms [3.7ms]
    successful: 1 in 10.7ms [10.7ms]
    failed:     2 in 0.6ms [0.3ms]
  safe|apply|global|Iris.BI.wand_ne._aux_1:
    total:      3 in 9.3ms [3.1ms]
    successful: 3 in 9.3ms [3.1ms]
    failed:     0 in 0.0ms [0.0ms]
  unsafe|tactic|global|Aesop.BuiltinRules.applyHyps:
    total:      2 in 9.1ms [4.5ms]
    successful: 2 in 9.1ms [4.5ms]
    failed:     0 in 0.0ms [0.0ms]
  safe|apply|global|Iris.BIFUpdate.ne._aux_1:
    total:      2 in 7.9ms [3.9ms]
    successful: 2 in 7.9ms [3.9ms]
    failed:     0 in 0.0ms [0.0ms]
  norm|tactic|global|Aesop.BuiltinRules.subst:
    total:      29 in 7.5ms [0.2ms]
    successful: 0 in 0.0ms [0.0ms]
    failed:     29 in 7.5ms [0.2ms]
  safe|apply|global|Iris.BI.sep_ne._aux_1:
    total:      3 in 7.3ms [2.4ms]
    successful: 3 in 7.3ms [2.4ms]
    failed:     0 in 0.0ms [0.0ms]
  safe|apply|global|Iris.step_fupdN_contractive._aux_1:
    total:      1 in 4.6ms [4.6ms]
    successful: 1 in 4.6ms [4.6ms]
    failed:     0 in 0.0ms [0.0ms]
  safe|tactic|global|Aesop.BuiltinRule.preprocess:
    total:      1 in 3.0ms [3.0ms]
    successful: 1 in 3.0ms [3.0ms]
    failed:     0 in 0.0ms [0.0ms]
  safe|apply|global|Iris.BI.BigSepL.bigSepL_dist:
    total:      1 in 1.4ms [1.4ms]
    successful: 1 in 1.4ms [1.4ms]
    failed:     0 in 0.0ms [0.0ms]
  safe|tactic|global|Aesop.BuiltinRules.splitHypotheses:
    total:      2 in 0.6ms [0.3ms]
    successful: 0 in 0.0ms [0.0ms]
    failed:     2 in 0.6ms [0.3ms]

This seems to indicate that more than half of the time is spent running simp normalization rules, and that the various apply rules are cheap in contrast. Between each goal, aesop currently runs simp_all using a simp-set consisting of both aesop_contractive simp-tagged declarations and normal simp declarations. It might be desirable for us to run a weakened version of simp here instead, eg by only accepting aesop_contractive simp declarations (by changing the useDefaultSimpSet in the aesop config).

[arthur-adjedj]

Turning off useDefaultSimpSet makes <norm simp> time on wp.pre.contractive go from ~400ms to ~150ms on my machine. The total execution time of the tactic is still big IMO, but I don't see "obvious" ways to optimize it much further for now.

[MackieLoeffel]

This is a good point, thanks for looking into this! This looks better, but not yet really great. If I have some time, I will look into implementing a specialized tactic for this such that we can compare performance.