@[rspec] Attribute for Automatic Relational Spec Lookup

This file provides a @[rspec] attribute that registers rHoare lemmas in a discrimination tree, keyed on the goal type. The ssprove_sim tactic queries this tree when head-matching fails, enabling automatic spec application.

Main definitions

• rspecExt - discrimination tree storing registered rspec lemmas
• @[rspec] - attribute to register a lemma for automatic lookup
• rspecLookup - query the tree for lemmas matching a goal

opaque CatCrypt.Tactics.rspecExt : Lean.SimpleScopedEnvExtension (Lean.Name × Array Lean.Meta.DiscrTree.Key) (Lean.Meta.DiscrTree Lean.Name)

Extension storing rspec lemmas indexed by goal pattern.

def CatCrypt.Tactics.addRSpecLemma (declName : Lean.Name) (kind : Lean.AttributeKind) : Lean.MetaM Unit

Register a lemma in the rspec discrimination tree. Extracts the conclusion (an rHoare judgment) and indexes on it.

Equations

• One or more equations did not get rendered due to their size.

def CatCrypt.Tactics.rspecLookup (goal : Lean.Expr) : Lean.MetaM (Array Lean.Name)

Query the rspec tree for lemmas matching the current goal expression.

Equations

• CatCrypt.Tactics.rspecLookup goal = do let __do_lift ← Lean.getEnv (Lean.ScopedEnvExtension.getState CatCrypt.Tactics.rspecExt __do_lift).getMatch goal