logicaffeine_proof/
tactic_script.rs

1//! A tiny proof-script language over the [`crate::tactic`] combinators — proofs as
2//! TEXT, the way a Lean/Coq proof reads. This is the self-contained seam toward a
3//! full English vernacular: it has no dependency on the surface language, so it
4//! compiles a script string straight into a composed [`Tactic`].
5//!
6//! Grammar (precedence low → high):
7//!
8//! ```text
9//! script  := seq
10//! seq     := chain (';' chain)*          // run in order
11//! chain   := atom ('<;>' atom)*          // `t1 <;> t2`: t2 on every goal t1 spawns
12//! atom    := '(' script ')'
13//!          | 'first' '[' script ('|' script)* ']'   // first that applies (backtracks)
14//!          | 'try' atom                              // run if it applies, else no-op
15//!          | 'repeat' atom                           // apply until it stops applying
16//!          | NAME ARG?                               // a primitive tactic
17//! ```
18//!
19//! Primitive tactics: `intro h`, `exact h`, `cases h`, `rewrite h`, `exists W`,
20//! `assumption`, `split`, `left`, `right`, `auto`, `induction`.
21
22use std::collections::HashMap;
23
24use crate::tactic::combinators as c;
25use crate::tactic::{ProofState, Tactic};
26use crate::verify::{citation_order, LibraryResult, LibraryTheorem};
27use crate::{ProofExpr, ProofTerm};
28
29/// A script parse error, with a human-readable reason.
30#[derive(Debug, Clone, PartialEq)]
31pub struct ScriptError(pub String);
32
33impl std::fmt::Display for ScriptError {
34    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
35        write!(f, "tactic script error: {}", self.0)
36    }
37}
38
39#[derive(Debug, Clone, PartialEq)]
40enum Tok {
41    Word(String),
42    Semi,
43    ThenAll,
44    LParen,
45    RParen,
46    LBracket,
47    RBracket,
48    Bar,
49}
50
51fn lex(src: &str) -> Result<Vec<Tok>, ScriptError> {
52    let mut toks = Vec::new();
53    let bytes = src.as_bytes();
54    let mut i = 0;
55    while i < bytes.len() {
56        let ch = bytes[i] as char;
57        match ch {
58            c if c.is_whitespace() => i += 1,
59            // Sentence punctuation reads as a step separator, so prose flows: a proof
60            // can be written `Assume h. By cases on h, …` and parse the same as `;`.
61            ';' | '.' | ',' => {
62                toks.push(Tok::Semi);
63                i += 1;
64            }
65            '(' => {
66                toks.push(Tok::LParen);
67                i += 1;
68            }
69            ')' => {
70                toks.push(Tok::RParen);
71                i += 1;
72            }
73            '[' => {
74                toks.push(Tok::LBracket);
75                i += 1;
76            }
77            ']' => {
78                toks.push(Tok::RBracket);
79                i += 1;
80            }
81            '|' => {
82                toks.push(Tok::Bar);
83                i += 1;
84            }
85            '<' if src[i..].starts_with("<;>") => {
86                toks.push(Tok::ThenAll);
87                i += 3;
88            }
89            c if c.is_alphanumeric() || c == '_' => {
90                let start = i;
91                while i < bytes.len() {
92                    let cc = bytes[i] as char;
93                    if cc.is_alphanumeric() || cc == '_' {
94                        i += 1;
95                    } else {
96                        break;
97                    }
98                }
99                toks.push(Tok::Word(src[start..i].to_string()));
100            }
101            other => return Err(ScriptError(format!("unexpected character {other:?}"))),
102        }
103    }
104    Ok(toks)
105}
106
107/// A registry of USER-DEFINED tactics (M) — the metaprogramming seam. A user names a
108/// composite tactic (built from primitives and combinators) with [`TacticEnv::define`], and
109/// may then reference it BY NAME in any later script, including from within other
110/// user-defined tactics. This is "write your own tactic in the language", without Rust —
111/// the definitions are stored as source and re-expanded (depth-bounded, so a recursive
112/// definition is rejected rather than looping) wherever the name appears.
113#[derive(Clone, Default)]
114pub struct TacticEnv {
115    defs: std::collections::HashMap<String, String>,
116}
117
118impl TacticEnv {
119    pub fn new() -> Self {
120        Self::default()
121    }
122    /// Define a named tactic from a script source. Names are case-insensitive.
123    pub fn define(&mut self, name: &str, script: &str) {
124        self.defs.insert(name.to_ascii_lowercase(), script.to_string());
125    }
126    fn get(&self, name: &str) -> Option<&String> {
127        self.defs.get(&name.to_ascii_lowercase())
128    }
129}
130
131/// Depth bound on user-tactic expansion — a recursive definition (`t := … t …`) is refused
132/// at this depth rather than looping forever.
133const MAX_TACTIC_DEPTH: usize = 128;
134
135struct Parser {
136    toks: Vec<Tok>,
137    pos: usize,
138    env: TacticEnv,
139    depth: usize,
140}
141
142impl Parser {
143    fn peek(&self) -> Option<&Tok> {
144        self.toks.get(self.pos)
145    }
146    fn bump(&mut self) -> Option<Tok> {
147        let t = self.toks.get(self.pos).cloned();
148        if t.is_some() {
149            self.pos += 1;
150        }
151        t
152    }
153    fn expect(&mut self, t: &Tok) -> Result<(), ScriptError> {
154        match self.bump() {
155            Some(got) if &got == t => Ok(()),
156            other => Err(ScriptError(format!("expected {t:?}, found {other:?}"))),
157        }
158    }
159
160    /// True if the next token ends a step: `;`/`.`/`,` (lexed to `Semi`) or the word
161    /// `then`. Lets prose read `Assume h, then by cases on h.`
162    fn at_separator(&self) -> bool {
163        matches!(self.peek(), Some(Tok::Semi))
164            || matches!(self.peek(), Some(Tok::Word(w)) if w.eq_ignore_ascii_case("then"))
165    }
166
167    /// Skip purely connective filler words (`by`, `the`, `on`, …) so a tactic can be
168    /// stated as `by cases on h` and mean `cases h`.
169    fn skip_filler(&mut self) {
170        while matches!(self.peek(), Some(Tok::Word(w)) if is_filler(w)) {
171            self.bump();
172        }
173    }
174
175    /// `script := chain (sep+ chain)*` — a *run* of separators (`.`/`,`/`;`/`then`,
176    /// e.g. the `, then` in `Assume h, then …`) counts as one.
177    fn parse_seq(&mut self) -> Result<Tactic, ScriptError> {
178        let mut steps = vec![self.parse_chain()?];
179        loop {
180            let mut consumed = false;
181            while self.at_separator() {
182                self.bump();
183                consumed = true;
184            }
185            if !consumed {
186                break;
187            }
188            // Allow a trailing separator (a closing `.`) before `)`/`]`/`|`/EOF.
189            if matches!(self.peek(), None | Some(Tok::RParen) | Some(Tok::RBracket) | Some(Tok::Bar)) {
190                break;
191            }
192            steps.push(self.parse_chain()?);
193        }
194        Ok(if steps.len() == 1 {
195            steps.into_iter().next().unwrap()
196        } else {
197            c::seq(steps)
198        })
199    }
200
201    /// `chain := atom ('<;>' atom)*` — left-associative `then_all`.
202    fn parse_chain(&mut self) -> Result<Tactic, ScriptError> {
203        let mut acc = self.parse_atom()?;
204        while matches!(self.peek(), Some(Tok::ThenAll)) {
205            self.bump();
206            let rhs = self.parse_atom()?;
207            acc = c::then_all(acc, rhs);
208        }
209        Ok(acc)
210    }
211
212    fn parse_atom(&mut self) -> Result<Tactic, ScriptError> {
213        self.skip_filler();
214        match self.peek() {
215            Some(Tok::LParen) => {
216                self.bump();
217                let inner = self.parse_seq()?;
218                self.expect(&Tok::RParen)?;
219                Ok(inner)
220            }
221            Some(Tok::Word(w)) if w == "first" => {
222                self.bump();
223                self.expect(&Tok::LBracket)?;
224                let mut alts = vec![self.parse_seq()?];
225                while matches!(self.peek(), Some(Tok::Bar)) {
226                    self.bump();
227                    alts.push(self.parse_seq()?);
228                }
229                self.expect(&Tok::RBracket)?;
230                Ok(c::first(alts))
231            }
232            Some(Tok::Word(w)) if w == "try" => {
233                self.bump();
234                Ok(c::try_(self.parse_atom()?))
235            }
236            Some(Tok::Word(w)) if w == "repeat" => {
237                self.bump();
238                Ok(c::repeat(self.parse_atom()?))
239            }
240            Some(Tok::Word(_)) => self.parse_primitive(),
241            other => Err(ScriptError(format!("expected a tactic, found {other:?}"))),
242        }
243    }
244
245    fn parse_primitive(&mut self) -> Result<Tactic, ScriptError> {
246        let raw = match self.bump() {
247            Some(Tok::Word(w)) => w,
248            other => return Err(ScriptError(format!("expected a tactic name, found {other:?}"))),
249        };
250        // A USER-DEFINED tactic (M) takes PRECEDENCE — an explicit `define` is authoritative,
251        // so a user tactic may even shadow a built-in alias (`both`, `split`, …). Expand its
252        // stored source in place, one level deeper (recursion is depth-bounded).
253        if let Some(src) = self.env.get(&raw).cloned() {
254            if self.depth >= MAX_TACTIC_DEPTH {
255                return Err(ScriptError(format!(
256                    "user tactic `{raw}` expands too deeply (recursive definition?)"
257                )));
258            }
259            return parse_with_env(&src, &self.env, self.depth + 1);
260        }
261        let name = canonical(&raw)
262            .ok_or_else(|| ScriptError(format!("unknown tactic `{raw}`")))?;
263        // Filler may sit between the verb and its object: `cases on h`, `rewrite with eq`.
264        let mut arg = || -> Result<String, ScriptError> {
265            self.skip_filler();
266            match self.peek() {
267                Some(Tok::Word(w)) => {
268                    let w = w.clone();
269                    self.bump();
270                    Ok(w)
271                }
272                _ => Err(ScriptError(format!("tactic `{name}` expects an argument"))),
273            }
274        };
275        match name {
276            "intro" => Ok(c::intro(&arg()?)),
277            "exact" => Ok(c::exact(&arg()?)),
278            "cases" => Ok(c::cases(&arg()?)),
279            "rewrite" => Ok(c::rewrite(&arg()?)),
280            "exists" => Ok(c::exists(ProofTerm::Constant(arg()?))),
281            "assumption" => Ok(c::assumption()),
282            "simp" => Ok(c::simp()),
283            "decide" => Ok(c::decide()),
284            "omega" => Ok(c::omega()),
285            "crush" => Ok(c::crush()),
286            "split" => Ok(c::split()),
287            "left" => Ok(c::left()),
288            "right" => Ok(c::right()),
289            "auto" => Ok(c::auto()),
290            "induction" => Ok(c::induction()),
291            _ => Err(ScriptError(format!("unknown tactic `{name}`"))),
292        }
293    }
294}
295
296/// Connective filler words that carry no tactic meaning — skipped so a step can be
297/// phrased as prose (`by cases on h`, `then by assumption`).
298fn is_filler(w: &str) -> bool {
299    matches!(
300        w.to_ascii_lowercase().as_str(),
301        "by" | "the" | "on" | "that" | "now" | "with" | "we" | "it" | "a" | "an" | "of" | "to" | "and"
302    )
303}
304
305/// Map an English-esque verb to its canonical tactic name. `Suppose`/`assume`/`let`
306/// all mean `intro`; `automatically`/`trivially` mean `auto`; and so on — the
307/// vocabulary that lets a proof read like prose. Case-insensitive.
308fn canonical(word: &str) -> Option<&'static str> {
309    match word.to_ascii_lowercase().as_str() {
310        "intro" | "assume" | "suppose" | "let" | "introduce" | "given" | "fix" => Some("intro"),
311        "exact" | "from" | "because" => Some("exact"),
312        "cases" | "destruct" | "consider" | "casework" => Some("cases"),
313        "rewrite" | "rw" | "substitute" | "subst" => Some("rewrite"),
314        "exists" | "use" | "witness" | "choose" | "provide" => Some("exists"),
315        "assumption" | "done" | "trivial" | "established" | "hypothesis" => Some("assumption"),
316        "simp" | "simplify" | "normalize" | "simplification" => Some("simp"),
317        "decide" | "compute" | "evaluate" | "calculate" => Some("decide"),
318        "omega" | "arithmetic" | "linarith" | "integers" => Some("omega"),
319        "crush" | "grind" | "blast" => Some("crush"),
320        "split" | "constructor" | "both" | "conjunction" => Some("split"),
321        "left" => Some("left"),
322        "right" => Some("right"),
323        "auto" | "tauto" | "automatically" | "automation" | "trivially" | "directly" => Some("auto"),
324        "induction" | "induct" => Some("induction"),
325        _ => None,
326    }
327}
328
329/// Compile a proof-script string into a composed [`Tactic`] (no user-defined tactics).
330pub fn parse_script(src: &str) -> Result<Tactic, ScriptError> {
331    parse_with_env(src, &TacticEnv::new(), 0)
332}
333
334/// Compile a proof-script string with USER-DEFINED tactics resolved from `env` (M).
335pub fn parse_script_with_env(src: &str, env: &TacticEnv) -> Result<Tactic, ScriptError> {
336    parse_with_env(src, env, 0)
337}
338
339fn parse_with_env(src: &str, env: &TacticEnv, depth: usize) -> Result<Tactic, ScriptError> {
340    let toks = lex(src)?;
341    if toks.is_empty() {
342        return Err(ScriptError("empty script".to_string()));
343    }
344    let mut p = Parser { toks, pos: 0, env: env.clone(), depth };
345    let t = p.parse_seq()?;
346    if p.pos != p.toks.len() {
347        return Err(ScriptError(format!(
348            "trailing tokens after the script: {:?}",
349            &p.toks[p.pos..]
350        )));
351    }
352    Ok(t)
353}
354
355impl ProofState {
356    /// Parse and run a proof script against this state. The state is unchanged on a
357    /// parse error; a tactic that fails mid-run leaves whatever it had committed.
358    pub fn run_script(&mut self, src: &str) -> Result<&mut Self, ScriptError> {
359        let tactic = parse_script(src)?;
360        tactic(self).map_err(|e| ScriptError(format!("{e:?}")))?;
361        Ok(self)
362    }
363
364    /// Parse and run a proof script that may reference USER-DEFINED tactics from `env` (M).
365    pub fn run_script_with_env(
366        &mut self,
367        src: &str,
368        env: &TacticEnv,
369    ) -> Result<&mut Self, ScriptError> {
370        let tactic = parse_script_with_env(src, env)?;
371        tactic(self).map_err(|e| ScriptError(format!("{e:?}")))?;
372        Ok(self)
373    }
374}
375
376// =============================================================================
377// The certified scripted library (ROOT R6) — a Mathlib-analog seam: theorems
378// proved BY TACTIC SCRIPTS accumulate into a dependency-ordered library, each
379// proved lemma becoming a citable premise for later ones, every step kernel-checked.
380// =============================================================================
381
382/// One theorem of a scripted library: proved from its own `premises` plus the
383/// conclusions of the theorems it `cites`, by running `script` to a kernel-checked
384/// proof. The unit the [`prove_scripted_library`] driver discharges in citation order.
385pub struct ScriptedTheorem {
386    pub name: String,
387    pub premises: Vec<ProofExpr>,
388    pub goal: ProofExpr,
389    /// An English-esque proof script (see [`parse_script`]).
390    pub script: String,
391    /// Names of earlier theorems whose conclusions this proof relies on.
392    pub cites: Vec<String>,
393    /// `[simp]`-tagged: once proved, this conclusion joins the simp pool and
394    /// is in scope for every LATER theorem's `simp` even without a citation.
395    pub simp: bool,
396}
397
398/// Discharge a library of scripted theorems in citation order, on a shared `axioms`
399/// base. Each theorem is proved by its [`ScriptedTheorem::script`] from its premises,
400/// the axioms, and the conclusions of the theorems it cites (already proved); a proved
401/// conclusion becomes a citable lemma for later theorems — the scraped-Euclid-graph
402/// discipline, now driven by tactic scripts. Results come back in INPUT order.
403pub fn prove_scripted_library(
404    axioms: &[ProofExpr],
405    theorems: &[ScriptedTheorem],
406) -> Vec<LibraryResult> {
407    // `citation_order` works off names + cites; stub the rest.
408    let stubs: Vec<LibraryTheorem> = theorems
409        .iter()
410        .map(|t| LibraryTheorem {
411            name: t.name.clone(),
412            premises: Vec::new(),
413            goal: t.goal.clone(),
414            cites: t.cites.clone(),
415        })
416        .collect();
417
418    let mut proved: HashMap<String, ProofExpr> = HashMap::new();
419    let mut by_name: HashMap<String, LibraryResult> = HashMap::new();
420    // Conclusions of proved `[simp]`-tagged theorems, in proof order: in scope
421    // for every later theorem without an explicit citation.
422    let mut simp_pool: Vec<ProofExpr> = Vec::new();
423
424    for &i in &citation_order(&stubs) {
425        let t = &theorems[i];
426        let mut premises = axioms.to_vec();
427        premises.extend(t.premises.iter().cloned());
428        for cite in &t.cites {
429            if let Some(goal) = proved.get(cite) {
430                premises.push(goal.clone());
431            }
432        }
433        for lemma in &simp_pool {
434            if !premises.contains(lemma) {
435                premises.push(lemma.clone());
436            }
437        }
438
439        let mut st = ProofState::start(premises, t.goal.clone());
440        let (verified, error) = match st.run_script(&t.script).err() {
441            Some(e) => (false, Some(e.0)),
442            None => match st.qed() {
443                Ok(vp) => (vp.verified, vp.verification_error),
444                Err(e) => (false, Some(format!("{e:?}"))),
445            },
446        };
447        if verified {
448            proved.insert(t.name.clone(), t.goal.clone());
449            if t.simp {
450                simp_pool.push(t.goal.clone());
451            }
452        }
453        by_name.insert(
454            t.name.clone(),
455            LibraryResult { name: t.name.clone(), verified, verification_error: error },
456        );
457    }
458
459    theorems
460        .iter()
461        .map(|t| by_name.remove(&t.name).expect("every theorem produces a result"))
462        .collect()
463}
logicaffeine_proof/tactic_script.rs

logicaffeine_proof/
tactic_script.rs
