1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
//! `aesop`-style rule-set search: turn `auto`'s fixed cascade into an
//! extensible, best-first search over registered rules.
//!
//! Lean's `aesop` lets you register lemmas as intro/elim/forward/destruct rules
//! with priorities and a safe/unsafe classification, then searches best-first.
//! This is that shape, built on the existing tactic combinators and the cheap
//! [`ProofState`] clone that already powers backtracking: SAFE rules are applied
//! whenever they fire (no branching — they never lose information); UNSAFE rules
//! fork the search, ordered by priority. A node budget bounds the search, and
//! [`SearchStats`] exposes how much was explored — so a best-first strategy can
//! be shown to expand fewer nodes than blind depth-first `first`/`repeat`.
//!
//! `auto` becomes one rule among many (an unsafe fallback), completing the
//! inversion the tactic framework was built for.
use crate::tactic::{ProofState, Tactic};
/// How a rule participates in search.
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum Safety {
/// Never loses provability — applied eagerly, no branch point.
Safe,
/// May not lead to a proof — forks the search; higher priority tried first.
Unsafe(u8),
}
/// The role a rule plays (currently advisory metadata for ordering/diagnostics;
/// the tactic itself encodes the actual transformation).
#[derive(Clone, Copy, Debug, PartialEq, Eq)]
pub enum RuleKind {
Intro,
Elim,
Forward,
Destruct,
}
/// A search rule: a named tactic with a role and a safety classification.
pub struct Rule {
pub name: String,
pub kind: RuleKind,
pub safety: Safety,
pub tactic: Tactic,
}
impl Rule {
pub fn new(name: &str, kind: RuleKind, safety: Safety, tactic: Tactic) -> Self {
Rule { name: name.to_string(), kind, safety, tactic }
}
}
/// An extensible collection of search rules.
#[derive(Default)]
pub struct RuleSet {
rules: Vec<Rule>,
}
/// What the search explored.
#[derive(Clone, Copy, Debug, Default, PartialEq, Eq)]
pub struct SearchStats {
pub nodes_expanded: usize,
pub succeeded: bool,
}
/// Default node budget for a best-first search.
const DEFAULT_NODE_BUDGET: usize = 2000;
impl RuleSet {
pub fn new() -> Self {
Self::default()
}
pub fn register(&mut self, rule: Rule) {
self.rules.push(rule);
}
pub fn len(&self) -> usize {
self.rules.len()
}
pub fn is_empty(&self) -> bool {
self.rules.is_empty()
}
/// Best-first search from `st`. Applies safe rules eagerly at each node,
/// then forks on unsafe rules in priority order. Succeeds (leaving `st` at
/// a closed proof state) when some branch drives the open goals to zero.
pub fn search(&self, st: &mut ProofState) -> SearchStats {
self.search_bounded(st, DEFAULT_NODE_BUDGET)
}
pub fn search_bounded(&self, st: &mut ProofState, budget: usize) -> SearchStats {
let mut stats = SearchStats::default();
// A best-first frontier of `(path-cost, state)`; the next node expanded
// is the one with the fewest open goals, then the cheapest path. The
// frontier stays small for the goal sizes this targets.
let mut frontier: Vec<(usize, ProofState)> = vec![(0, st.clone())];
let rules = self.rules_by_priority();
while let Some(best_idx) = pick_best(&frontier) {
if stats.nodes_expanded >= budget {
break;
}
let (cost, node) = frontier.swap_remove(best_idx);
stats.nodes_expanded += 1;
if node.open_goals() == 0 {
*st = node;
stats.succeeded = true;
return stats;
}
// Fork on each rule, highest priority (and safe) first. A safe rule
// adds no path-cost (it never loses provability), so its branch is
// explored ahead of any unsafe alternative.
for rule in &rules {
let mut child = node.clone();
if (rule.tactic)(&mut child).is_ok() && !state_eq(&child, &node) {
frontier.push((cost + rule_cost(rule), child));
}
}
}
stats
}
/// Rules ordered for expansion: safe first, then unsafe by descending priority.
fn rules_by_priority(&self) -> Vec<&Rule> {
let mut r: Vec<&Rule> = self.rules.iter().collect();
r.sort_by_key(|rule| std::cmp::Reverse(priority_of(rule)));
r
}
}
/// The path-cost of taking a rule: zero for safe rules (free), and the inverse
/// of priority for unsafe ones, so high-priority unsafe branches are cheaper.
fn rule_cost(rule: &Rule) -> usize {
match rule.safety {
Safety::Safe => 0,
Safety::Unsafe(p) => (255 - p as usize) + 1,
}
}
fn priority_of(rule: &Rule) -> u8 {
match rule.safety {
Safety::Unsafe(p) => p,
Safety::Safe => 255,
}
}
/// Cheap progress check: two states differ if their open-goal count or focused
/// target differ (enough to avoid enqueuing a no-op rule application).
fn state_eq(a: &ProofState, b: &ProofState) -> bool {
a.open_goals() == b.open_goals() && a.focused_target() == b.focused_target()
}
/// The frontier node to expand next: fewest open goals, then cheapest path.
fn pick_best(frontier: &[(usize, ProofState)]) -> Option<usize> {
frontier
.iter()
.enumerate()
.min_by_key(|(_, (cost, st))| (st.open_goals(), *cost))
.map(|(i, _)| i)
}
/// The default rule set: `auto` as the sole unsafe fallback — so a default
/// `search` closes exactly what `auto` closes, the regression baseline.
pub fn default_ruleset() -> RuleSet {
let mut rs = RuleSet::new();
rs.register(Rule::new(
"auto",
RuleKind::Elim,
Safety::Unsafe(10),
crate::tactic::combinators::auto(),
));
rs
}