oxilean_std/wellfounded/
types.rs

1//! Auto-generated module
2//!
3//! 🤖 Generated with [SplitRS](https://github.com/cool-japan/splitrs)
4
5use super::functions::*;
6use oxilean_kernel::{BinderInfo, Declaration, Environment, Expr, Level, Name};
7
8/// Sigma-type measure: `f : α → Nat` witnesses well-foundedness of `(<) ∘ f`.
9#[allow(dead_code)]
10#[derive(Debug, Clone)]
11pub struct SizeMeasure {
12    /// Name of the measure function.
13    pub name: String,
14    /// Expected domain type name.
15    pub domain: String,
16}
17impl SizeMeasure {
18    /// Create a measure.
19    #[allow(dead_code)]
20    pub fn new(name: impl Into<String>, domain: impl Into<String>) -> Self {
21        Self {
22            name: name.into(),
23            domain: domain.into(),
24        }
25    }
26    /// Standard measure for lists: the length function.
27    #[allow(dead_code)]
28    pub fn list_length() -> Self {
29        Self::new("List.length", "List")
30    }
31    /// Standard measure for natural numbers: identity.
32    #[allow(dead_code)]
33    pub fn nat_id() -> Self {
34        Self::new("id", "Nat")
35    }
36    /// Standard measure for trees: size function.
37    #[allow(dead_code)]
38    pub fn tree_size() -> Self {
39        Self::new("Tree.size", "Tree")
40    }
41    /// Produce a declaration body for the induced well-founded relation.
42    #[allow(dead_code)]
43    pub fn induced_relation_name(&self) -> String {
44        format!("InvImage.lt_{}", self.name.replace('.', "_"))
45    }
46}
47/// A ranked proof tree for tracking structural recursion depth.
48#[allow(dead_code)]
49#[derive(Debug, Clone)]
50pub enum RecursionTree {
51    /// A base case (leaf).
52    Base { label: String },
53    /// A recursive case with a child proof tree.
54    Rec {
55        label: String,
56        decreasing_arg: String,
57        child: Box<RecursionTree>,
58    },
59    /// A branching point (e.g., `match` with multiple arms).
60    Branch {
61        label: String,
62        arms: Vec<RecursionTree>,
63    },
64}
65impl RecursionTree {
66    /// Return the maximum depth of the recursion tree.
67    #[allow(dead_code)]
68    pub fn depth(&self) -> usize {
69        match self {
70            Self::Base { .. } => 0,
71            Self::Rec { child, .. } => 1 + child.depth(),
72            Self::Branch { arms, .. } => arms.iter().map(|a| a.depth()).max().unwrap_or(0),
73        }
74    }
75    /// Return the number of recursive calls.
76    #[allow(dead_code)]
77    pub fn recursive_calls(&self) -> usize {
78        match self {
79            Self::Base { .. } => 0,
80            Self::Rec { child, .. } => 1 + child.recursive_calls(),
81            Self::Branch { arms, .. } => arms.iter().map(|a| a.recursive_calls()).sum(),
82        }
83    }
84    /// Return `true` if the tree is simply a base case.
85    #[allow(dead_code)]
86    pub fn is_base(&self) -> bool {
87        matches!(self, Self::Base { .. })
88    }
89}
90/// Well-founded relation builder: constructs `InvImage r f` and `Prod.Lex`.
91#[allow(dead_code)]
92pub struct WfRelBuilder;
93impl WfRelBuilder {
94    /// Build the expression for `InvImage r f`:
95    /// a well-founded relation on `α` induced by `f : α → β` and `r` on `β`.
96    #[allow(dead_code)]
97    pub fn inv_image(r: Expr, f: Expr) -> Expr {
98        Expr::App(
99            Box::new(Expr::App(
100                Box::new(Expr::Const(Name::str("InvImage"), vec![])),
101                Box::new(r),
102            )),
103            Box::new(f),
104        )
105    }
106    /// Build `Prod.Lex r s`: lexicographic product of relations.
107    #[allow(dead_code)]
108    pub fn prod_lex(r: Expr, s: Expr) -> Expr {
109        Expr::App(
110            Box::new(Expr::App(
111                Box::new(Expr::Const(Name::str("Prod.Lex"), vec![])),
112                Box::new(r),
113            )),
114            Box::new(s),
115        )
116    }
117    /// The standard `Nat.lt` well-founded relation.
118    #[allow(dead_code)]
119    pub fn nat_lt() -> Expr {
120        Expr::Const(Name::str("Nat.lt"), vec![])
121    }
122    /// The measure-induced relation `InvImage Nat.lt f`.
123    #[allow(dead_code)]
124    pub fn measure(f: Expr) -> Expr {
125        Self::inv_image(Self::nat_lt(), f)
126    }
127}
128/// Heuristic for choosing a termination proof strategy.
129#[allow(dead_code)]
130#[derive(Debug, Clone, Copy, PartialEq, Eq)]
131pub enum TerminationStrategy {
132    /// Recurse on structurally smaller arguments.
133    Structural,
134    /// Use an explicit numeric measure function.
135    Measure,
136    /// Use a lexicographic tuple of measures.
137    Lexicographic,
138    /// Use a well-founded relation other than `<`.
139    WellFounded,
140    /// Multiple-argument mutual recursion.
141    Mutual,
142}
143impl TerminationStrategy {
144    /// Return a description of the strategy.
145    #[allow(dead_code)]
146    pub fn description(self) -> &'static str {
147        match self {
148            Self::Structural => "Structural recursion on an inductive argument",
149            Self::Measure => "Explicit numeric measure function",
150            Self::Lexicographic => "Lexicographic ordering of multiple arguments",
151            Self::WellFounded => "Custom well-founded relation",
152            Self::Mutual => "Mutual recursion with shared termination argument",
153        }
154    }
155    /// Return all available strategies.
156    #[allow(dead_code)]
157    pub fn all() -> &'static [TerminationStrategy] {
158        &[
159            Self::Structural,
160            Self::Measure,
161            Self::Lexicographic,
162            Self::WellFounded,
163            Self::Mutual,
164        ]
165    }
166}
167/// Proof-relevant termination certificates.
168///
169/// A `TerminationCert` pairs a measure function with evidence that the
170/// measure strictly decreases on each recursive call.
171#[allow(dead_code)]
172#[derive(Debug, Clone)]
173pub struct TerminationCert {
174    /// Name of the function being certified.
175    pub fn_name: String,
176    /// Name of the measure function (`measure : domain → Nat`).
177    pub measure_fn: String,
178    /// Human-readable justification.
179    pub justification: String,
180    /// Whether automated verification succeeded.
181    pub verified: bool,
182}
183impl TerminationCert {
184    /// Construct a certificate.
185    #[allow(dead_code)]
186    pub fn new(
187        fn_name: impl Into<String>,
188        measure_fn: impl Into<String>,
189        justification: impl Into<String>,
190        verified: bool,
191    ) -> Self {
192        Self {
193            fn_name: fn_name.into(),
194            measure_fn: measure_fn.into(),
195            justification: justification.into(),
196            verified,
197        }
198    }
199    /// Returns a structural recursion certificate (always verified).
200    #[allow(dead_code)]
201    pub fn structural(fn_name: impl Into<String>) -> Self {
202        let nm = fn_name.into();
203        Self {
204            measure_fn: format!("structural_measure_{}", nm),
205            justification: "Structural recursion on an inductive argument".to_owned(),
206            fn_name: nm,
207            verified: true,
208        }
209    }
210    /// Returns a well-founded recursion certificate.
211    #[allow(dead_code)]
212    pub fn well_founded(fn_name: impl Into<String>, measure_fn: impl Into<String>) -> Self {
213        Self::new(fn_name, measure_fn, "Well-founded recursion", true)
214    }
215    /// Returns a certificate backed by lexicographic ordering.
216    #[allow(dead_code)]
217    pub fn lexicographic(fn_name: impl Into<String>, components: Vec<String>) -> Self {
218        let nm = fn_name.into();
219        let just = format!("Lexicographic order on ({}).", components.join(", "));
220        Self::new(nm.clone(), format!("lex_measure_{}", nm), just, true)
221    }
222    /// Returns `true` if the certificate is valid.
223    #[allow(dead_code)]
224    pub fn is_valid(&self) -> bool {
225        self.verified && !self.fn_name.is_empty() && !self.measure_fn.is_empty()
226    }
227    /// Produce a summary string.
228    #[allow(dead_code)]
229    pub fn summary(&self) -> String {
230        format!(
231            "TerminationCert{{ fn='{}', measure='{}', ok={}, justification='{}' }}",
232            self.fn_name, self.measure_fn, self.verified, self.justification
233        )
234    }
235}
236/// A registry of termination certificates indexed by function name.
237#[allow(dead_code)]
238#[derive(Debug, Default)]
239pub struct TerminationRegistry {
240    certs: Vec<TerminationCert>,
241}
242impl TerminationRegistry {
243    /// Create an empty registry.
244    #[allow(dead_code)]
245    pub fn new() -> Self {
246        Self::default()
247    }
248    /// Register a certificate.
249    #[allow(dead_code)]
250    pub fn register(&mut self, cert: TerminationCert) {
251        self.certs.push(cert);
252    }
253    /// Look up the certificate for a function.
254    #[allow(dead_code)]
255    pub fn lookup(&self, fn_name: &str) -> Option<&TerminationCert> {
256        self.certs.iter().find(|c| c.fn_name == fn_name)
257    }
258    /// Return all verified certificates.
259    #[allow(dead_code)]
260    pub fn verified_certs(&self) -> Vec<&TerminationCert> {
261        self.certs.iter().filter(|c| c.verified).collect()
262    }
263    /// Return the total number of registered certificates.
264    #[allow(dead_code)]
265    pub fn count(&self) -> usize {
266        self.certs.len()
267    }
268}
269/// A combinator for building lexicographic well-founded orderings.
270#[allow(dead_code)]
271#[derive(Debug, Clone)]
272pub struct LexOrder {
273    /// Component measure names in decreasing priority.
274    pub components: Vec<String>,
275}
276impl LexOrder {
277    /// Construct from a list of measure component names.
278    #[allow(dead_code)]
279    pub fn new(components: Vec<impl Into<String>>) -> Self {
280        Self {
281            components: components.into_iter().map(Into::into).collect(),
282        }
283    }
284    /// Add an additional (lowest-priority) component.
285    #[allow(dead_code)]
286    pub fn push(mut self, component: impl Into<String>) -> Self {
287        self.components.push(component.into());
288        self
289    }
290    /// Return the number of components.
291    #[allow(dead_code)]
292    pub fn arity(&self) -> usize {
293        self.components.len()
294    }
295    /// Describe the lex order as a tuple type string.
296    #[allow(dead_code)]
297    pub fn type_string(&self) -> String {
298        format!("({})", self.components.join(" × "))
299    }
300    /// Verify that a concrete sequence of `(before, after)` pairs is
301    /// lexicographically decreasing using the given values for each component.
302    ///
303    /// `values_before[i]` and `values_after[i]` are `u64` values of component `i`.
304    #[allow(dead_code)]
305    pub fn check_decrease(&self, values_before: &[u64], values_after: &[u64]) -> bool {
306        let n = self
307            .components
308            .len()
309            .min(values_before.len())
310            .min(values_after.len());
311        for i in 0..n {
312            if values_before[i] < values_after[i] {
313                return false;
314            }
315            if values_before[i] > values_after[i] {
316                return true;
317            }
318        }
319        false
320    }
321}
oxilean_std/wellfounded/types.rs

oxilean_std/wellfounded/
types.rs
