feat: aesop_contractive tactic to solve Contractive/NonExpansive goals

Iris/Iris/Algebra/OFE.lean

@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
 module
-
 public meta import Iris.Std.RocqPorting
+public meta import Iris.Std.AesopContractive
 
 @[expose] public section
 
@@ -106,7 +106,7 @@ theorem NonExpansive₂.ne_left [OFE α] [OFE β] [OFE γ] (f : α → β → γ
   ⟨fun {_ _ _} h => ne h Dist.rfl⟩
 
 /-- `DistLater n x y` means that `x` and `y` are `m`-equivalent for all `m < n`. -/
-@[rocq_alias dist_later]
+@[rocq_alias dist_later, aesop_contractive safe unfold]
 def DistLater [OFE α] (n : Nat) (x y : α) : Prop := ∀ m, m < n → x ≡{m}≡ y
 
 @[simp, refl] theorem DistLater.rfl [OFE α] {n} {x : α} : DistLater n x x := fun _ _ => .rfl

Iris/Iris/BI/DerivedLaws.lean

@@ -119,6 +119,7 @@ theorem imp_congr_l [BI PROP] {P P' Q : PROP} (h : P ⊣⊢ P') : (P → Q) ⊣
 theorem imp_congr_r [BI PROP] {P Q Q' : PROP} (h : Q ⊣⊢ Q') : (P → Q) ⊣⊢ (P → Q') :=
   imp_congr .rfl h
 
+@[aesop_contractive safe apply]
 theorem forall_ne [BI PROP] {Φ Ψ : α → PROP} (h : ∀ a, Φ a ≡{n}≡ Ψ a) :
     iprop(∀ a, Φ a) ≡{n}≡ iprop(∀ a, Ψ a) := sForall_ne <| by
   constructor <;> rintro _ ⟨a, rfl⟩ <;> exact ⟨_, ⟨a, rfl⟩, h _⟩

Iris/Iris/BI/Updates.lean

@@ -160,6 +160,8 @@ class BIUpdate (PROP : Type _) [BI PROP] extends BUpd PROP where
   trans {P : PROP} : |==> |==> P ⊢ |==> P
   frame_r {P R : PROP} : (|==> P) ∗ R ⊢ |==> (P ∗ R)
 
+attribute [instance] BIUpdate.bupd_ne
+
 class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
   [ne {E1 E2 : CoPset} : OFE.NonExpansive (iprop(|={E1,E2}=> · : PROP))]
   subset {E1 E2 : CoPset} : E2 ⊆ E1 → ⊢ |={E1,E2}=> |={E2,E1}=> (emp : PROP)
@@ -170,6 +172,8 @@ class BIFUpdate (PROP : Type _) [BI PROP] extends FUpd PROP where
     E1 ## Ef → (|={E1,E2}=> ⌜E2 ## Ef⌝ → P) ⊢ |={E1 ∪ Ef,E2 ∪ Ef}=> P
   frame_r {E1 E2 : CoPset} {P R : PROP} : (|={E1,E2}=> P) ∗ R ⊢ |={E1,E2}=> P ∗ R
 
+attribute [instance] BIFUpdate.ne
+
 class BIUpdateFUpdate (PROP : Type _) [BI PROP] [BIUpdate PROP] [BIFUpdate PROP] where
   fupd_of_bupd {P : PROP} {E : CoPset} : (|==> P) ⊢ |={E}=> P
 
@@ -424,6 +428,8 @@ theorem step_fupdN_contractive {E1 E2 : CoPset} {n : Nat} [ι : BILaterContracti
     | zero => exact ne.ne (ι.distLater_dist (ne.ne <| xy_i · ·))
     | succ n IH => exact ne.ne (later_ne.ne (ne.ne IH))
 
+-- unsafe since it can make contractive goals unprovable if n > 0
+-- @[aesop_contractive unsafe 90% apply]
 theorem step_fupdN_ne {E1 E2 : CoPset} {n : Nat} :
     OFE.NonExpansive (iprop(|={E1}[E2]▷=>^[n] · : PROP)) where
   ne {i x y} xy_i := by

Iris/Iris/ProgramLogic/WeakestPre.lean

@@ -78,37 +78,26 @@ def wp.pre (s : Stuckness) (wp : CoPset -> Expr -> (Val -> IProp GF) -> IProp GF
       stateInterp σ₂ (ns + 1) obs' (nt + eₜ.length) ∗
       wp E e₂ Φ ∗ [∗list] e' ∈ eₜ, wp ⊤ e' ι.forkPost)
 
-@[rocq_alias wp_pre_contractive]
+open BI
+
+attribute [aesop_contractive safe apply] wand_ne sep_ne BIFUpdate.ne step_fupdN_contractive BigSepL.bigSepL_dist
+-- the following makes aesop_contractive quite slow and does not allow prioritization of Contractive instances over NonExpansive instances
+-- attribute [aesop_contractive safe apply] OFE.NonExpansive.ne OFE.NonExpansive₂.ne
+attribute [aesop_contractive safe forward (immediate := [h])] OFE.Dist.le
+attribute [aesop_contractive simp] Nat.le_iff_lt_or_eq
+attribute [aesop_contractive simp] OFE.Dist.rfl
+
+-- time: was 580ms, is 350ms now
+#time @[rocq_alias wp_pre_contractive, aesop_contractive safe apply]
 instance wp.pre.contractive s : OFE.Contractive (wp.pre s (ι := ι)) where
   distLater_dist := by
-    intros n wp wp' Hwp E e₁ Φ
-    unfold pre
-    cases toVal e₁
-    case some _ =>
-      exact .rfl
-    case none =>
-      refine BI.forall_ne (fun σ₁ => ?_)
-      refine BI.forall_ne (fun ns => ?_)
-      refine BI.forall_ne (fun obs => ?_)
-      refine BI.forall_ne (fun obs' => ?_)
-      refine BI.forall_ne (fun nt => ?_)
-      refine BI.wand_ne.ne .rfl ?_
-      refine BIFUpdate.ne.ne ?_
-      refine BI.sep_ne.ne .rfl ?_
-      refine BI.forall_ne (fun e₂  => ?_)
-      refine BI.forall_ne (fun σ₂ => ?_)
-      refine BI.forall_ne (fun eₜ => ?_)
-      refine BI.wand_ne.ne .rfl ?_
-      refine BI.wand_ne.ne .rfl ?_
-      refine BIFUpdate.ne.ne ?_
-      refine OFE.Contractive.distLater_dist fun m m_n => ?_
-      refine BIFUpdate.ne.ne ?_
-      refine step_fupdN_ne.ne ?_
-      refine BIFUpdate.ne.ne ?_
-      refine BI.sep_ne.ne .rfl ?_
-      refine BI.sep_ne.ne ?_ ?_
-      · exact Hwp m m_n _ _ _
-      · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp m m_n _ _ _
+    intros; unfold pre; intros _ _ _;
+    aesop_contractive
+    -- set_option trace.aesop true in
+    -- aesop (config := { introsTransparency? := none, warnOnNonterminal := false })
+            -- (rule_sets := [aesop_contractive]) (erase Aesop.BuiltinRules.rfl)
+    -- · exact Hwp _ ‹_› _ _ _
+    -- · exact BI.BigSepL.bigSepL_dist <| fun _ => Hwp _ ‹_› _ _ _
 
 @[rocq_alias wp_def]
 instance wp.def : Wp (IProp GF) (Expr) (Val) Stuckness where
@@ -125,63 +114,32 @@ theorem wp_unfold {s E} {e : Expr} {Φ : Val → IProp GF} :
     WP e @ s ; E {{ Φ }} ⊣⊢ wp.pre s (Wp.wp (PROP := IProp GF) s) E e Φ :=
   BI.equiv_iff.1 <| fixpoint_unfold (f := (wp.pre s).toContractiveHom) E e Φ
 
-@[rocq_alias wp_ne]
+-- time: was 780ms, is 540ms now
+#time @[rocq_alias wp_ne, aesop_contractive safe apply]
 instance wp_ne {s : Stuckness} {E} {e : Expr} :
     OFE.NonExpansive (Wp.wp (PROP := IProp GF) s E e) where
   ne {n Φ₁ Φ₂} HΦ := by
     induction n using Nat.strongRecOn generalizing e E Φ₁ Φ₂ with | ind n IH =>
     simp only [wp_unfold.to_eq]
     dsimp only [wp.pre]
-    cases toVal e
-    case some v =>
-      exact BIFUpdate.ne.ne <| HΦ v
-    case none =>
-      refine BI.forall_ne fun σ₁ => ?_
-      refine BI.forall_ne fun ns => ?_
-      refine BI.forall_ne fun obs => ?_
-      refine BI.forall_ne fun obs' => ?_
-      refine BI.forall_ne fun nt => ?_
-      refine BI.wand_ne.ne .rfl ?_
-      refine BIFUpdate.ne.ne ?_
-      refine BI.sep_ne.ne .rfl ?_
-      refine BI.forall_ne fun e₂  => ?_
-      refine BI.forall_ne fun σ₂ => ?_
-      refine BI.forall_ne fun eₜ => ?_
-      refine BI.wand_ne.ne .rfl ?_
-      refine BI.wand_ne.ne .rfl ?_
-      refine step_fupdN_contractive.distLater_dist fun m n_m => ?_
-      refine BIFUpdate.ne.ne ?_
-      refine BI.sep_ne.ne .rfl ?_
-      refine BI.sep_ne.ne ?_ .rfl
-      exact IH m n_m <| OFE.dist_lt HΦ n_m
+    aesop_contractive
+    -- · aesop_contractive
+    -- · apply IH
+      -- · aesop_contractive
+      -- · apply fwd; aesop_contractive
 
 #rocq_ignore wp_proper "Derivable using NonExpansive.eqv"
 
-@[rocq_alias wp_contractive]
+-- time: was 480ms, is 260ms now
+#time @[rocq_alias wp_contractive]
 instance wp_contractive (s : Stuckness) E (e : Expr) (h : toVal e = none) :
     OFE.Contractive (Wp.wp (PROP := IProp GF) s E e) where
   distLater_dist {n Φ₁ Φ₂} HΦ := by
     simp only [wp_unfold.to_eq]
-    simp only [wp.pre, h]
-    refine BI.forall_ne fun σ₁ => ?_
-    refine BI.forall_ne fun ns => ?_
-    refine BI.forall_ne fun obs => ?_
-    refine BI.forall_ne fun obs' => ?_
-    refine BI.forall_ne fun nt => ?_
-    refine BI.wand_ne.ne .rfl ?_
-    refine BIFUpdate.ne.ne ?_
-    refine BI.sep_ne.ne .rfl ?_
-    refine BI.forall_ne fun e₂  => ?_
-    refine BI.forall_ne fun σ₂ => ?_
-    refine BI.forall_ne fun eₜ => ?_
-    refine BI.wand_ne.ne .rfl ?_
-    refine BI.wand_ne.ne .rfl ?_
-    refine step_fupdN_contractive.distLater_dist fun m n_m => ?_
-    refine BIFUpdate.ne.ne ?_
-    refine BI.sep_ne.ne .rfl ?_
-    refine BI.sep_ne.ne ?_ .rfl
-    refine wp_ne.ne ?_
-    exact HΦ m n_m
+    unfold wp.pre
+    aesop_contractive
+    -- refine wp_ne.ne ?_
+    -- exact HΦ _ ‹_›
 
 @[rocq_alias wp_value_fupd']
 theorem wp_value_fupd' {s : Stuckness} {E} {Φ : Val → IProp GF} {v : Val} :

Iris/Iris/Std/AesopContractive.lean

@@ -0,0 +1,70 @@
+module
+public meta import Aesop
+public meta import Lean
+
+open Lean Elab Meta
+
+declare_aesop_rule_sets [aesop_contractive]
+
+macro (name := aesop_cat) "aesop_contractive" c:Aesop.tactic_clause* : tactic =>
+`(tactic|
+  aesop $c* (config := { warnOnNonterminal := true, useDefaultSimpSet := false})
+            (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]) (erase Aesop.BuiltinRules.rfl))
+
+-- attribute [simp] Nat.repeat
+
+syntax (name := aesop_contractive_attr) "aesop_contractive " Aesop.attr_rules : attr
+
+open Aesop Frontend
+
+meta def elabConfig (stx : Syntax) : TermElabM AttrConfig :=
+  withRef stx do
+    match stx with
+    | `(attr| aesop_contractive $e:Aesop.rule_expr) => do
+      let e ← `(Aesop.rule_expr| (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]) $e:Aesop.rule_expr)
+      let r ← RuleExpr.elab e |>.run $ ← ElabM.Context.forAdditionalGlobalRules
+      return { rules := #[r] }
+    | `(attr| aesop_contractive [ $es:Aesop.rule_expr,* ]) => do
+      let es ← es.getElems.mapM fun e => `(Aesop.rule_expr| (rule_sets := [$(Lean.mkIdent `aesop_contractive):ident]) $e:Aesop.rule_expr)
+      let ctx ← ElabM.Context.forAdditionalGlobalRules
+      let rs ← (es : Array Syntax).mapM λ e => RuleExpr.elab e |>.run ctx
+      return { rules := rs }
+    | _ => throwUnsupportedSyntax
+
+meta def auxIfIsNonExpansiveDecl (declName : Name) : TermElabM Name := do
+  let decl ← getConstInfo declName
+  forallTelescope decl.type fun xs ty => do
+    let .const fnName _ := ty.getAppFn | return declName
+    let projName ←
+      if fnName == `Iris.OFE.NonExpansive ||
+         fnName == `Iris.OFE.NonExpansive₂ then
+        pure `ne
+      else if fnName == `Iris.OFE.Contractive then
+        pure `distLater_dist
+      else
+        do return declName
+    let declLvls := decl.levelParams.map Level.param
+    let declWithArgs := mkAppN (mkConst declName declLvls) xs
+    let proj ←  mkProjection declWithArgs projName
+    withDeclNameForAuxNaming declName do
+      let auxName ← mkAuxDeclName
+      let e ← mkAuxDefinitionFor auxName proj
+      trace[aesop] m!"{e}"
+      return auxName
+
+meta initialize registerBuiltinAttribute {
+    name := `aesop_contractive_attr
+    descr := "Adds a given declaration to the ruleset for the `aesop_contractive` tactic."
+    applicationTime := .afterCompilation
+    add := fun declName stx kind ↦ withRef stx do Aesop.runTermElabMAsCoreM do
+      let declName ← auxIfIsNonExpansiveDecl declName
+      let config ← elabConfig stx
+      let rules ← config.rules.flatMapM (·.buildAdditionalGlobalRules declName)
+      for (rule, rsNames) in rules do
+        for rsName in rsNames do
+          addGlobalRule rsName rule kind (checkNotExists := true)
+    erase := λ decl =>
+      let ruleFilter :=
+        { name := decl, scope := .global, builders := #[], phases := #[] }
+      eraseGlobalRules RuleSetNameFilter.all ruleFilter (checkExists := true)
+  }

Iris/lake-manifest.json

@@ -1,7 +1,17 @@
 {"version": "1.2.0",
  "packagesDir": ".lake/packages",
  "packages":
- [{"url": "https://github.com/leanprover-community/batteries",
+ [{"url": "https://github.com/leanprover-community/aesop",
+   "type": "git",
+   "subDir": null,
+   "scope": "leanprover-community",
+   "rev": "558915ae105bfd8074e22d597613d1961822adc2",
+   "name": "aesop",
+   "manifestFile": "lake-manifest.json",
+   "inputRev": "v4.30.0",
+   "inherited": false,
+   "configFile": "lakefile.toml"},
+  {"url": "https://github.com/leanprover-community/batteries",
    "type": "git",
    "subDir": null,
    "scope": "leanprover-community",

Iris/lakefile.toml

@@ -11,6 +11,11 @@ name = "batteries"
 scope = "leanprover-community"
 rev = "v4.30.0"
 
+[[require]]
+name = "aesop"
+scope = "leanprover-community"
+rev = "v4.30.0"
+
 [[lean_lib]]
 name = "Iris"