aac_reflexivity leads to QED blow up in trivial case (just one unit removed)

[MSoegtropIMC]

Dear AAC-tactics Team,

I added AAC instances for the sepcon type in Princeton VST - which was straight forward. Only if I use aac_reflexivity it leads to very long QED times, at least one million times slower than when directly rewriting with the one lemma required. Below please find example code (using the versions from Coq Platform 2023.11.0). I waited for QED for more than 30 minutes (embedded in a larger proof) and it did not succeed. In below example the direct proof QED time is 1ms, the aac_reflexivity QED timeouts with 10s limit.

I wrote a few reflexive tactics myself and I would expect that one can write the tactic such that the QED time is similar to the tactic run time. What I usually need to make QED fast is a specific eval lazy on the interpretation of the reified term. If I just apply the correctness lemma and leave the unification of the interpretation of the reified term with the original goal term to the unifier, I usually also experience very bad QED blow up. See e.g. metaprogramming-rosetta-stone-real-simplifier. This evaluation makes the interpretation of the reified term identical to the goal, so that unification is trivial (also for the kernel during QED). If this evaluation is removed, the tactic still works, but QED times can be very bad (also tactic run times are slower). This is just a wild guess, but maybe this is the issue with aac-tactics. Note that I would do a lazy now instead of a cbv.

Require Import VST.floyd.proofauto.
Require Import VST.floyd.library.

Require Import AAC_tactics.AAC.

Lemma sepcon'Associative: Associative eq sepcon.
Proof.
  unfold Associative.
  intros x y z.
  symmetry.
  apply sepcon_assoc.
Qed.

Lemma sepcon'Commutative: Commutative eq sepcon.
Proof.
  unfold Commutative.
  intros x y.
  apply sepcon_comm.
Qed.

Lemma sepcon'Unit_emp: Unit eq sepcon emp.
Proof.
  constructor; intros x.
  apply emp_sepcon.
  apply sepcon_emp.
Qed.

#[export] Instance sepcon'aac_assoc : Associative eq sepcon := sepcon'Associative.
#[export] Instance sepcon'aac_comm : Commutative eq sepcon := sepcon'Commutative.
#[export] Instance sepcon'aac_emp_Unit : Unit eq sepcon emp := sepcon'Unit_emp.

Example Fast: forall {cs : compspecs} (sh : Share.t) (t : type) (gfs1 : list gfield) (v : reptype (nested_field_type t gfs1)) (p : val),
  field_at sh t gfs1 v p = (field_at sh t gfs1 v p * emp)%logic.
Proof.
  intros.
  rewrite sepcon_emp.
  reflexivity.
Time Qed. 

Example Slow: forall {cs : compspecs} (sh : Share.t) (t : type) (gfs1 : list gfield) (v : reptype (nested_field_type t gfs1)) (p : val),
  field_at sh t gfs1 v p = (field_at sh t gfs1 v p * emp)%logic.
Proof.
  intros.
  aac_reflexivity.
Timeout 10 Qed.

[palmskog]

@MSoegtropIMC I have no idea about what the bottleneck could be here, but if you need an expert opinion, you may want to consider trying to contact one of the original authors, Damien Pous: https://perso.ens-lyon.fr/damien.pous/

[MSoegtropIMC]

@palmskog : if PRs messing with the guts of the tactic are welcome, I can also have a look. As I said I have some experience with this.

[palmskog]

PRs are welcome in general, but my priority is to preserve the "regular" behavior of AAC Tactics on the tutorial examples and the "caveat" examples. Standalone examples/benchmarks are also very welcome and encouraged as part of PRs.

[MSoegtropIMC]

I expect that a single well placed "eval lazy" with a tailored delta does the trick. It might be, that I have to duplicate some standard library functions like list append in case such things are used in the interpretation function. If the interpretation uses Z arithmetic, things might get messy.

[MSoegtropIMC]

@palmskog : I wasn't aware that the tactic is written in OCaml - I have little experience with this. What - as far as I can see - needs to be done is to do an explicit lazy eval in the type of decision_thm after:

aac-tactics/src/aac_rewrite.ml

Line 127 in 3fc2fb1

let decision_thm = mkApp (Coq.get_efresh Theory.Stubs.decide_thm,

expanding eval, eval_aux, fold_map and the projections of the record Bin.pack + maybe a few things I overlooked, but it looks all very neat and clean.

This should make the proof statement identical to the original goal - not just unifiable. What likely happens here is that the kernel unifier chokes on terms which are the arguments of the AAC relation. If the type of decision_thm is identical to the goal, the unifier has nothing to do.

[SkySkimmer]

Consider this example of blowup:

From Coq Require ZArith.
From AAC_tactics Require Import AAC.
From AAC_tactics Require Instances.
Import ZArith.
Import Instances.Z.

Fixpoint mkevil n := match n with 0%nat => 1 | S k => 2 * mkevil k end.
(* 2 ^ n in Z *)

Definition evil := mkevil 25%nat.

Time Eval vm_compute in evil.
(* ~instant *)

Lemma test a : a + evil = evil + a.
Proof.
  Time aac_reflexivity.
  (* n = 32 -> 0.015s
     n = 25 -> 0.016s
     n = 20 -> 0.015s
     n = 16 -> 0.014s
   *)

 Time Qed.
(* (memory usage seems negligible)
   n = 32 -> too long
   n = 25 -> 37s
   n = 20 -> 1.15s
   n = 16 -> 0.08s
 *)

The proof is

test =
fun a : Z =>
@lift_reflexivity Z (@eq Z) (@eq Z)
  (@aac_lift_subrelation Z (@eq Z) (@eq Z) (@eq_equivalence Z) (@eq_Transitive Z)
     (@subrelation_refl Z (@eq Z))) (@eq_Reflexive Z) (Z.add a evil) (Z.add evil a)
  (let env_sym :=
     sigma_get
       {| Internal.Sym.ar := 0; Internal.Sym.value := evil; Internal.Sym.morph := proper_eq evil |}
       (sigma_add 1%positive
          {| Internal.Sym.ar := 0; Internal.Sym.value := a; Internal.Sym.morph := proper_eq a |}
          (sigma_empty Internal.Sym.pack)) in
   let env_bin :=
     sigma_get
       {|
         Internal.Bin.value := Z.add;
         Internal.Bin.compat := reflexive_proper Z.add;
         Internal.Bin.assoc := aac_Z_add_Assoc;
         Internal.Bin.comm := Some aac_Z_add_Comm;
         Internal.Bin.idem := None
       |} (sigma_empty Internal.Bin.pack) in
   let env_units :=
     sigma_get
       {|
         Internal.u_value := 0;
         Internal.u_desc := {| Internal.uf_idx := 1; Internal.uf_desc := aac_Z_add_0_Unit |} :: nil
       |} (sigma_empty (Internal.unit_pack env_bin)) in
   let tty := Internal.T env_sym in
   let rsum := Internal.sum (e_sym:=env_sym) in
   let rprd := Internal.prd (e_sym:=env_sym) in
   let rsym := Internal.sym (e_sym:=env_sym) in
   let vnil := Internal.vnil env_sym in
   let vcons := Internal.vcons (e_sym:=env_sym) in
   let eval := Internal.eval (e_sym:=env_sym) env_units in
   let left :=
     rsum 1%positive
       (Utils.cons (rsym 1%positive vnil, 1%positive) (Utils.nil (rsym 2%positive vnil, 1%positive)))
     in
   let right :=
     rsum 1%positive
       (Utils.cons (rsym 2%positive vnil, 1%positive) (Utils.nil (rsym 1%positive vnil, 1%positive)))
     in
   Internal.decide env_units left right
     (eq_refl : Internal.compare (Internal.norm env_units left) (Internal.norm env_units right) = Eq)
   <: (* VM CAST HERE, inferred type "Internal.eval env_units left = Internal.eval env_units right" *)
   a + evil = evil + a)
     : forall a : Z, a + evil = evil + a

Using vm cast here seems just wrong, it should be a default cast (or even nothing since this is an argument of lift_reflexivity so the expected type is already known).

The eq_refl : Internal.compare ... = Eq maybe should be vmcast, OTOH in cbv it will end up computing evil (eg left uses rsum uses env_sym uses evil) so maybe not.

[SkySkimmer]

#134