logicaffeine_kernel/
reduction.rs

1//! Term reduction for the Calculus of Constructions.
2//!
3//! This module implements the evaluation semantics of the kernel. Terms are
4//! reduced to normal form using a call-by-name strategy.
5//!
6//! # Reduction Rules
7//!
8//! ## Beta Reduction
9//! Function application: `(λx. body) arg → body[x := arg]`
10//!
11//! ## Iota Reduction
12//! Pattern matching: `match (Cᵢ args) { ... caseᵢ ... } → caseᵢ(args)`
13//!
14//! ## Fix Unfolding (Guarded)
15//! Recursive definitions: `(fix f. body) (Cᵢ args) → body[f := fix f. body] (Cᵢ args)`
16//!
17//! Fix unfolding is guarded by requiring the argument to be in constructor form.
18//! This ensures termination by structural recursion.
19//!
20//! ## Delta Reduction
21//! Global definitions are expanded when needed during normalization.
22//!
23//! # Primitive Operations
24//!
25//! The reducer handles built-in operations on literals:
26//! - Arithmetic: `add`, `sub`, `mul`, `div`, `mod`
27//! - Comparison: `lt`, `le`, `gt`, `ge`, `eq`
28//! - Boolean: `ite` (if-then-else)
29//!
30//! # Reflection Builtins
31//!
32//! Special operations for the deep embedding (Syntax type):
33//! - `syn_size`: Compute the size of a syntax tree
34//! - `syn_max_var`: Find the maximum variable index
35//! - `syn_step`, `syn_eval`: Bounded evaluation
36//! - `syn_quote`, `syn_diag`: Reification and diagonalization
37//!
38//! # Fuel Limit
39//!
40//! Normalization uses a fuel counter (default 10000) to prevent infinite loops.
41//! If fuel is exhausted, the current term is returned as-is.
42
43use crate::context::Context;
44use crate::omega;
45use crate::term::{Literal, Term, Universe};
46use crate::type_checker::substitute;
47
48/// Normalize a term to its normal form.
49///
50/// Repeatedly applies reduction rules until no more reductions are possible.
51/// This is a full normalization that reduces under binders.
52pub fn normalize(ctx: &Context, term: &Term) -> Term {
53    let mut current = term.clone();
54    let mut fuel = 10000; // Safety limit to prevent infinite loops
55
56    loop {
57        if fuel == 0 {
58            // If we hit the fuel limit, return what we have
59            return current;
60        }
61        fuel -= 1;
62
63        let reduced = reduce_step(ctx, &current);
64        if reduced == current {
65            return current;
66        }
67        current = reduced;
68    }
69}
70
71/// Single-step reduction.
72///
73/// Reduces the outermost redex first (call-by-name), then recurses
74/// into subterms for full normalization.
75fn reduce_step(ctx: &Context, term: &Term) -> Term {
76    match term {
77        // Literals are in normal form
78        Term::Lit(_) => term.clone(),
79
80        // Beta: (λx. body) arg → body[x := arg]
81        Term::App(func, arg) => {
82            // First try primitive reduction (add, sub, mul, etc.)
83            if let Some(result) = try_primitive_reduce(func, arg) {
84                return result;
85            }
86
87            // Try reflection builtins (syn_size, syn_max_var)
88            if let Some(result) = try_reflection_reduce(ctx, func, arg) {
89                return result;
90            }
91
92            // Then try to reduce at the head
93            match func.as_ref() {
94                Term::Lambda { param, body, .. } => {
95                    // Beta reduction
96                    substitute(body, param, arg)
97                }
98                // Fix application: (fix f. body) arg
99                // We need to check if arg is a constructor to unfold
100                Term::Fix { name, body } => {
101                    if is_constructor_form(ctx, arg) {
102                        // Unfold: (fix f. body) arg → body[f := fix f. body] arg
103                        let fix_term = Term::Fix {
104                            name: name.clone(),
105                            body: body.clone(),
106                        };
107                        let unfolded = substitute(body, name, &fix_term);
108                        Term::App(Box::new(unfolded), arg.clone())
109                    } else {
110                        // Try reducing the argument first
111                        let reduced_arg = reduce_step(ctx, arg);
112                        if reduced_arg != **arg {
113                            Term::App(func.clone(), Box::new(reduced_arg))
114                        } else {
115                            term.clone()
116                        }
117                    }
118                }
119                // Nested application: ((f x) y) - reduce inner first
120                Term::App(_, _) => {
121                    let reduced_func = reduce_step(ctx, func);
122                    if reduced_func != **func {
123                        Term::App(Box::new(reduced_func), arg.clone())
124                    } else {
125                        // Try reducing argument
126                        let reduced_arg = reduce_step(ctx, arg);
127                        Term::App(func.clone(), Box::new(reduced_arg))
128                    }
129                }
130                // Other function forms - try reducing function position
131                _ => {
132                    let reduced_func = reduce_step(ctx, func);
133                    if reduced_func != **func {
134                        Term::App(Box::new(reduced_func), arg.clone())
135                    } else {
136                        // Try reducing argument
137                        let reduced_arg = reduce_step(ctx, arg);
138                        Term::App(func.clone(), Box::new(reduced_arg))
139                    }
140                }
141            }
142        }
143
144        // Iota: match (Cᵢ a₁...aₙ) with cases → caseᵢ a₁ ... aₙ
145        Term::Match {
146            discriminant,
147            motive,
148            cases,
149        } => {
150            if let Some((ctor_idx, args)) = extract_constructor(ctx, discriminant) {
151                // Select the corresponding case
152                let case = &cases[ctor_idx];
153                // Apply case to constructor arguments
154                let mut result = case.clone();
155                for arg in args {
156                    result = Term::App(Box::new(result), Box::new(arg));
157                }
158                // Reduce the result
159                reduce_step(ctx, &result)
160            } else {
161                // Try reducing the discriminant
162                let reduced_disc = reduce_step(ctx, discriminant);
163                if reduced_disc != **discriminant {
164                    Term::Match {
165                        discriminant: Box::new(reduced_disc),
166                        motive: motive.clone(),
167                        cases: cases.clone(),
168                    }
169                } else {
170                    term.clone()
171                }
172            }
173        }
174
175        // Reduce under lambdas (deep normalization)
176        Term::Lambda {
177            param,
178            param_type,
179            body,
180        } => {
181            let reduced_param_type = reduce_step(ctx, param_type);
182            let reduced_body = reduce_step(ctx, body);
183            if reduced_param_type != **param_type || reduced_body != **body {
184                Term::Lambda {
185                    param: param.clone(),
186                    param_type: Box::new(reduced_param_type),
187                    body: Box::new(reduced_body),
188                }
189            } else {
190                term.clone()
191            }
192        }
193
194        // Reduce under Pi types
195        Term::Pi {
196            param,
197            param_type,
198            body_type,
199        } => {
200            let reduced_param_type = reduce_step(ctx, param_type);
201            let reduced_body_type = reduce_step(ctx, body_type);
202            if reduced_param_type != **param_type || reduced_body_type != **body_type {
203                Term::Pi {
204                    param: param.clone(),
205                    param_type: Box::new(reduced_param_type),
206                    body_type: Box::new(reduced_body_type),
207                }
208            } else {
209                term.clone()
210            }
211        }
212
213        // Reduce under Fix
214        Term::Fix { name, body } => {
215            let reduced_body = reduce_step(ctx, body);
216            if reduced_body != **body {
217                Term::Fix {
218                    name: name.clone(),
219                    body: Box::new(reduced_body),
220                }
221            } else {
222                term.clone()
223            }
224        }
225
226        // Base cases: already in normal form
227        Term::Sort(_) | Term::Var(_) | Term::Hole => term.clone(),
228
229        // Delta reduction: unfold definitions (but not axioms, constructors, or inductives)
230        Term::Global(name) => {
231            if let Some(body) = ctx.get_definition_body(name) {
232                // Definition found - unfold to body
233                body.clone()
234            } else {
235                // Axiom, constructor, or inductive - no reduction
236                term.clone()
237            }
238        }
239    }
240}
241
242/// Check if a term is a constructor (possibly applied to arguments).
243fn is_constructor_form(ctx: &Context, term: &Term) -> bool {
244    extract_constructor(ctx, term).is_some()
245}
246
247/// Extract constructor index and VALUE arguments from a term (skipping type arguments).
248///
249/// Returns `Some((constructor_index, [value_arg1, value_arg2, ...]))` if term is `Cᵢ(type_args..., value_args...)`
250/// where `Cᵢ` is the i-th constructor of some inductive type.
251///
252/// For polymorphic constructors like `Cons A h t`, this returns only [h, t], not [A, h, t].
253fn extract_constructor(ctx: &Context, term: &Term) -> Option<(usize, Vec<Term>)> {
254    let mut args = Vec::new();
255    let mut current = term;
256
257    // Collect arguments from nested applications
258    while let Term::App(func, arg) = current {
259        args.push((**arg).clone());
260        current = func;
261    }
262    args.reverse();
263
264    // Check if head is a constructor
265    if let Term::Global(name) = current {
266        if let Some(inductive) = ctx.constructor_inductive(name) {
267            let ctors = ctx.get_constructors(inductive);
268            for (idx, (ctor_name, ctor_type)) in ctors.iter().enumerate() {
269                if *ctor_name == name {
270                    // Count type parameters (leading Pis where param_type is a Sort)
271                    let num_type_params = count_type_params(ctor_type);
272
273                    // Skip type arguments, return only value arguments
274                    let value_args = if num_type_params < args.len() {
275                        args[num_type_params..].to_vec()
276                    } else {
277                        vec![]
278                    };
279
280                    return Some((idx, value_args));
281                }
282            }
283        }
284    }
285    None
286}
287
288/// Count leading type parameters in a constructor type.
289///
290/// Type parameters are Pis where the param_type is a Sort (Type n or Prop).
291/// For `Π(A:Type). Π(_:A). Π(_:List A). List A`, this returns 1.
292fn count_type_params(ty: &Term) -> usize {
293    let mut count = 0;
294    let mut current = ty;
295
296    while let Term::Pi { param_type, body_type, .. } = current {
297        if is_sort(param_type) {
298            count += 1;
299            current = body_type;
300        } else {
301            break;
302        }
303    }
304
305    count
306}
307
308/// Check if a term is a Sort (Type n or Prop).
309fn is_sort(term: &Term) -> bool {
310    matches!(term, Term::Sort(_))
311}
312
313/// Try to reduce a primitive operation.
314///
315/// Returns Some(result) if this is a fully applied primitive like (add 3 4).
316/// Pattern: ((op x) y) where op is a builtin and x, y are literals.
317fn try_primitive_reduce(func: &Term, arg: &Term) -> Option<Term> {
318    // We need func = (op x) and arg = y
319    if let Term::App(op_term, x) = func {
320        if let Term::Global(op_name) = op_term.as_ref() {
321            if let (Term::Lit(Literal::Int(x_val)), Term::Lit(Literal::Int(y_val))) =
322                (x.as_ref(), arg)
323            {
324                let result = match op_name.as_str() {
325                    "add" => x_val.checked_add(*y_val)?,
326                    "sub" => x_val.checked_sub(*y_val)?,
327                    "mul" => x_val.checked_mul(*y_val)?,
328                    "div" => x_val.checked_div(*y_val)?,
329                    "mod" => x_val.checked_rem(*y_val)?,
330                    _ => return None,
331                };
332                return Some(Term::Lit(Literal::Int(result)));
333            }
334        }
335    }
336    None
337}
338
339// -------------------------------------------------------------------------
340// Reflection Builtins
341// -------------------------------------------------------------------------
342
343/// Try to reduce reflection builtins (syn_size, syn_max_var, syn_lift, syn_subst, syn_beta, syn_step).
344///
345/// Pattern: (syn_size arg) or (syn_max_var arg) or (syn_step arg) where arg is a Syntax constructor.
346/// Pattern: ((syn_beta body) arg) for two-argument builtins.
347/// Pattern: (((syn_lift amount) cutoff) term) for three-argument builtins.
348/// Pattern: (((syn_subst replacement) index) term) for substitution.
349fn try_reflection_reduce(ctx: &Context, func: &Term, arg: &Term) -> Option<Term> {
350    // First, check for single-argument builtins
351    if let Term::Global(op_name) = func {
352        match op_name.as_str() {
353            "syn_size" => {
354                // Normalize the argument first
355                let norm_arg = normalize(ctx, arg);
356                return try_syn_size_reduce(ctx, &norm_arg);
357            }
358            "syn_max_var" => {
359                // Normalize the argument first
360                let norm_arg = normalize(ctx, arg);
361                return try_syn_max_var_reduce(ctx, &norm_arg, 0);
362            }
363            "syn_step" => {
364                // Normalize the argument first
365                let norm_arg = normalize(ctx, arg);
366                return try_syn_step_reduce(ctx, &norm_arg);
367            }
368            "syn_quote" => {
369                // Normalize the argument first
370                let norm_arg = normalize(ctx, arg);
371                return try_syn_quote_reduce(ctx, &norm_arg);
372            }
373            "syn_diag" => {
374                // Normalize the argument first
375                let norm_arg = normalize(ctx, arg);
376                return try_syn_diag_reduce(ctx, &norm_arg);
377            }
378            "concludes" => {
379                // Normalize the argument first
380                let norm_arg = normalize(ctx, arg);
381                return try_concludes_reduce(ctx, &norm_arg);
382            }
383            "try_refl" => {
384                // Normalize the argument first
385                let norm_arg = normalize(ctx, arg);
386                return try_try_refl_reduce(ctx, &norm_arg);
387            }
388            "tact_fail" => {
389                // tact_fail always returns error derivation
390                return Some(make_error_derivation());
391            }
392            "try_compute" => {
393                // try_compute goal = DCompute goal
394                // The validation happens in concludes
395                let norm_arg = normalize(ctx, arg);
396                return Some(Term::App(
397                    Box::new(Term::Global("DCompute".to_string())),
398                    Box::new(norm_arg),
399                ));
400            }
401            "try_ring" => {
402                // Ring tactic: prove polynomial equalities by normalization
403                let norm_arg = normalize(ctx, arg);
404                return try_try_ring_reduce(ctx, &norm_arg);
405            }
406            "try_lia" => {
407                // LIA tactic: prove linear inequalities by Fourier-Motzkin
408                let norm_arg = normalize(ctx, arg);
409                return try_try_lia_reduce(ctx, &norm_arg);
410            }
411            "try_cc" => {
412                // CC tactic: prove equalities by congruence closure
413                let norm_arg = normalize(ctx, arg);
414                return try_try_cc_reduce(ctx, &norm_arg);
415            }
416            "try_simp" => {
417                // Simp tactic: prove equalities by simplification and arithmetic
418                let norm_arg = normalize(ctx, arg);
419                return try_try_simp_reduce(ctx, &norm_arg);
420            }
421            "try_omega" => {
422                // Omega tactic: prove integer inequalities with proper rounding
423                let norm_arg = normalize(ctx, arg);
424                return try_try_omega_reduce(ctx, &norm_arg);
425            }
426            "try_auto" => {
427                // Auto tactic: tries all tactics in sequence
428                let norm_arg = normalize(ctx, arg);
429                return try_try_auto_reduce(ctx, &norm_arg);
430            }
431            "try_bitblast" => {
432                // Bitblast tactic: prove Bit equalities by normalization
433                let norm_arg = normalize(ctx, arg);
434                return try_try_bitblast_reduce(ctx, &norm_arg);
435            }
436            "try_tabulate" => {
437                // Tabulate tactic: prove universal Bit goals by exhaustion
438                let norm_arg = normalize(ctx, arg);
439                return try_try_tabulate_reduce(ctx, &norm_arg);
440            }
441            "try_hw_auto" => {
442                // Hardware auto: tries bitblast, then tabulate, then auto
443                let norm_arg = normalize(ctx, arg);
444                return try_try_hw_auto_reduce(ctx, &norm_arg);
445            }
446            "try_inversion" => {
447                // Inversion tactic: derives False if no constructor can match
448                let norm_arg = normalize(ctx, arg);
449                return try_try_inversion_reduce(ctx, &norm_arg);
450            }
451            "induction_num_cases" => {
452                // Returns number of constructors for an inductive type
453                let norm_arg = normalize(ctx, arg);
454                return try_induction_num_cases_reduce(ctx, &norm_arg);
455            }
456            _ => {}
457        }
458    }
459
460    // For multi-argument builtins like syn_lift and syn_subst,
461    // we need to check if func is a partial application
462
463    // syn_lift amount cutoff term
464    // Structure: (((syn_lift amount) cutoff) term) = App(App(App(syn_lift, amount), cutoff), term)
465    // When reduced: func = App(App(syn_lift, amount), cutoff), arg = term
466    if let Term::App(partial2, cutoff) = func {
467        if let Term::App(partial1, amount) = partial2.as_ref() {
468            if let Term::Global(op_name) = partial1.as_ref() {
469                if op_name == "syn_lift" {
470                    if let (Term::Lit(Literal::Int(amt)), Term::Lit(Literal::Int(cut))) =
471                        (amount.as_ref(), cutoff.as_ref())
472                    {
473                        let norm_term = normalize(ctx, arg);
474                        return try_syn_lift_reduce(ctx, *amt, *cut, &norm_term);
475                    }
476                }
477            }
478        }
479    }
480
481    // syn_subst replacement index term
482    // Structure: (((syn_subst replacement) index) term)
483    if let Term::App(partial2, index) = func {
484        if let Term::App(partial1, replacement) = partial2.as_ref() {
485            if let Term::Global(op_name) = partial1.as_ref() {
486                if op_name == "syn_subst" {
487                    if let Term::Lit(Literal::Int(idx)) = index.as_ref() {
488                        let norm_replacement = normalize(ctx, replacement);
489                        let norm_term = normalize(ctx, arg);
490                        return try_syn_subst_reduce(ctx, &norm_replacement, *idx, &norm_term);
491                    }
492                }
493            }
494        }
495    }
496
497    // syn_beta body arg (2 arguments)
498    // Structure: ((syn_beta body) arg)
499    if let Term::App(partial1, body) = func {
500        if let Term::Global(op_name) = partial1.as_ref() {
501            if op_name == "syn_beta" {
502                let norm_body = normalize(ctx, body);
503                let norm_arg = normalize(ctx, arg);
504                return try_syn_beta_reduce(ctx, &norm_body, &norm_arg);
505            }
506        }
507    }
508
509    // try_cong context eq_proof (2 arguments)
510    // Structure: ((try_cong context) eq_proof)
511    // Returns: DCong context eq_proof
512    if let Term::App(partial1, context) = func {
513        if let Term::Global(op_name) = partial1.as_ref() {
514            if op_name == "try_cong" {
515                let norm_context = normalize(ctx, context);
516                let norm_proof = normalize(ctx, arg);
517                return Some(Term::App(
518                    Box::new(Term::App(
519                        Box::new(Term::Global("DCong".to_string())),
520                        Box::new(norm_context),
521                    )),
522                    Box::new(norm_proof),
523                ));
524            }
525        }
526    }
527
528    // try_rewrite eq_proof goal (2 arguments)
529    // Structure: ((try_rewrite eq_proof) goal)
530    // Given eq_proof : Eq A x y, rewrites goal by replacing x with y
531    if let Term::App(partial1, eq_proof) = func {
532        if let Term::Global(op_name) = partial1.as_ref() {
533            if op_name == "try_rewrite" {
534                let norm_eq_proof = normalize(ctx, eq_proof);
535                let norm_goal = normalize(ctx, arg);
536                return try_try_rewrite_reduce(ctx, &norm_eq_proof, &norm_goal, false);
537            }
538            if op_name == "try_rewrite_rev" {
539                let norm_eq_proof = normalize(ctx, eq_proof);
540                let norm_goal = normalize(ctx, arg);
541                return try_try_rewrite_reduce(ctx, &norm_eq_proof, &norm_goal, true);
542            }
543        }
544    }
545
546    // syn_eval fuel term (2 arguments)
547    // Structure: ((syn_eval fuel) term)
548    if let Term::App(partial1, fuel_term) = func {
549        if let Term::Global(op_name) = partial1.as_ref() {
550            if op_name == "syn_eval" {
551                if let Term::Lit(Literal::Int(fuel)) = fuel_term.as_ref() {
552                    let norm_term = normalize(ctx, arg);
553                    return try_syn_eval_reduce(ctx, *fuel, &norm_term);
554                }
555            }
556        }
557    }
558
559    // induction_base_goal ind_type motive (2 arguments)
560    // Structure: ((induction_base_goal ind_type) motive)
561    if let Term::App(partial1, ind_type) = func {
562        if let Term::Global(op_name) = partial1.as_ref() {
563            if op_name == "induction_base_goal" {
564                let norm_ind_type = normalize(ctx, ind_type);
565                let norm_motive = normalize(ctx, arg);
566                return try_induction_base_goal_reduce(ctx, &norm_ind_type, &norm_motive);
567            }
568        }
569    }
570
571    // tact_orelse t1 t2 goal (3 arguments)
572    // Structure: (((tact_orelse t1) t2) goal)
573    // Here: func = App(App(tact_orelse, t1), t2), arg = goal
574    if let Term::App(partial1, t2) = func {
575        if let Term::App(combinator, t1) = partial1.as_ref() {
576            if let Term::Global(name) = combinator.as_ref() {
577                if name == "tact_orelse" {
578                    return try_tact_orelse_reduce(ctx, t1, t2, arg);
579                }
580                // tact_then t1 t2 goal (3 arguments)
581                if name == "tact_then" {
582                    return try_tact_then_reduce(ctx, t1, t2, arg);
583                }
584            }
585        }
586    }
587
588    // tact_try t goal (2 arguments)
589    // Structure: ((tact_try t) goal)
590    if let Term::App(combinator, t) = func {
591        if let Term::Global(name) = combinator.as_ref() {
592            if name == "tact_try" {
593                return try_tact_try_reduce(ctx, t, arg);
594            }
595            // tact_repeat t goal (2 arguments)
596            if name == "tact_repeat" {
597                return try_tact_repeat_reduce(ctx, t, arg);
598            }
599            // tact_solve t goal (2 arguments)
600            if name == "tact_solve" {
601                return try_tact_solve_reduce(ctx, t, arg);
602            }
603            // tact_first tactics goal (2 arguments)
604            if name == "tact_first" {
605                return try_tact_first_reduce(ctx, t, arg);
606            }
607        }
608    }
609
610    // induction_step_goal ind_type motive ctor_idx (3 arguments)
611    // Structure: (((induction_step_goal ind_type) motive) ctor_idx)
612    // Returns the goal for the given constructor index
613    if let Term::App(partial1, motive) = func {
614        if let Term::App(combinator, ind_type) = partial1.as_ref() {
615            if let Term::Global(name) = combinator.as_ref() {
616                if name == "induction_step_goal" {
617                    let norm_ind_type = normalize(ctx, ind_type);
618                    let norm_motive = normalize(ctx, motive);
619                    let norm_idx = normalize(ctx, arg);
620                    return try_induction_step_goal_reduce(ctx, &norm_ind_type, &norm_motive, &norm_idx);
621                }
622            }
623        }
624    }
625
626    // try_induction ind_type motive cases (3 arguments)
627    // Structure: (((try_induction ind_type) motive) cases)
628    // Returns DElim ind_type motive cases (delegating to existing infrastructure)
629    if let Term::App(partial1, motive) = func {
630        if let Term::App(combinator, ind_type) = partial1.as_ref() {
631            if let Term::Global(name) = combinator.as_ref() {
632                if name == "try_induction" {
633                    let norm_ind_type = normalize(ctx, ind_type);
634                    let norm_motive = normalize(ctx, motive);
635                    let norm_cases = normalize(ctx, arg);
636                    return try_try_induction_reduce(ctx, &norm_ind_type, &norm_motive, &norm_cases);
637                }
638            }
639        }
640    }
641
642    // try_destruct ind_type motive cases (3 arguments)
643    // Structure: (((try_destruct ind_type) motive) cases)
644    // Case analysis without induction hypotheses
645    if let Term::App(partial1, motive) = func {
646        if let Term::App(combinator, ind_type) = partial1.as_ref() {
647            if let Term::Global(name) = combinator.as_ref() {
648                if name == "try_destruct" {
649                    let norm_ind_type = normalize(ctx, ind_type);
650                    let norm_motive = normalize(ctx, motive);
651                    let norm_cases = normalize(ctx, arg);
652                    return try_try_destruct_reduce(ctx, &norm_ind_type, &norm_motive, &norm_cases);
653                }
654            }
655        }
656    }
657
658    // try_apply hyp_name hyp_proof goal (3 arguments)
659    // Structure: (((try_apply hyp_name) hyp_proof) goal)
660    // Manual backward chaining
661    if let Term::App(partial1, hyp_proof) = func {
662        if let Term::App(combinator, hyp_name) = partial1.as_ref() {
663            if let Term::Global(name) = combinator.as_ref() {
664                if name == "try_apply" {
665                    let norm_hyp_name = normalize(ctx, hyp_name);
666                    let norm_hyp_proof = normalize(ctx, hyp_proof);
667                    let norm_goal = normalize(ctx, arg);
668                    return try_try_apply_reduce(ctx, &norm_hyp_name, &norm_hyp_proof, &norm_goal);
669                }
670            }
671        }
672    }
673
674    None
675}
676
677/// Compute size of a Syntax term.
678///
679/// SVar n -> 1
680/// SGlobal n -> 1
681/// SSort u -> 1
682/// SApp f x -> 1 + size(f) + size(x)
683/// SLam A b -> 1 + size(A) + size(b)
684/// SPi A B -> 1 + size(A) + size(B)
685fn try_syn_size_reduce(ctx: &Context, term: &Term) -> Option<Term> {
686    // Match on the constructor form
687    // Unary constructors: (SVar n), (SGlobal n), (SSort u)
688    // Binary constructors: ((SApp f) x), ((SLam A) b), ((SPi A) B)
689
690    // Check for unary constructor: (Ctor arg)
691    if let Term::App(ctor_term, _inner_arg) = term {
692        if let Term::Global(ctor_name) = ctor_term.as_ref() {
693            match ctor_name.as_str() {
694                "SVar" | "SGlobal" | "SSort" | "SLit" | "SName" => {
695                    return Some(Term::Lit(Literal::Int(1)));
696                }
697                _ => {}
698            }
699        }
700
701        // Check for binary constructor: ((Ctor a) b)
702        if let Term::App(inner, a) = ctor_term.as_ref() {
703            if let Term::Global(ctor_name) = inner.as_ref() {
704                match ctor_name.as_str() {
705                    "SApp" | "SLam" | "SPi" => {
706                        // Get sizes of both children
707                        let a_size = try_syn_size_reduce(ctx, a)?;
708                        let b_size = try_syn_size_reduce(ctx, _inner_arg)?;
709
710                        if let (Term::Lit(Literal::Int(a_n)), Term::Lit(Literal::Int(b_n))) =
711                            (a_size, b_size)
712                        {
713                            return Some(Term::Lit(Literal::Int(1 + a_n + b_n)));
714                        }
715                    }
716                    _ => {}
717                }
718            }
719        }
720    }
721
722    None
723}
724
725/// Compute maximum free variable index in a Syntax term.
726///
727/// The `depth` parameter tracks how many binders we're under.
728/// SVar k -> k - depth (returns -1 if bound, k - depth if free)
729/// SGlobal _ -> -1 (no free variables)
730/// SSort _ -> -1 (no free variables)
731/// SApp f x -> max(max_var(f), max_var(x))
732/// SLam A b -> max(max_var(A), max_var(b, depth+1))
733/// SPi A B -> max(max_var(A), max_var(B, depth+1))
734fn try_syn_max_var_reduce(ctx: &Context, term: &Term, depth: i64) -> Option<Term> {
735    // Check for unary constructor: (Ctor arg)
736    if let Term::App(ctor_term, inner_arg) = term {
737        if let Term::Global(ctor_name) = ctor_term.as_ref() {
738            match ctor_name.as_str() {
739                "SVar" => {
740                    // SVar k -> if k >= depth then k - depth else -1
741                    if let Term::Lit(Literal::Int(k)) = inner_arg.as_ref() {
742                        if *k >= depth {
743                            // Free variable with adjusted index
744                            return Some(Term::Lit(Literal::Int(*k - depth)));
745                        } else {
746                            // Bound variable
747                            return Some(Term::Lit(Literal::Int(-1)));
748                        }
749                    }
750                }
751                "SGlobal" | "SSort" | "SLit" | "SName" => {
752                    // No free variables
753                    return Some(Term::Lit(Literal::Int(-1)));
754                }
755                _ => {}
756            }
757        }
758
759        // Check for binary constructor: ((Ctor a) b)
760        if let Term::App(inner, a) = ctor_term.as_ref() {
761            if let Term::Global(ctor_name) = inner.as_ref() {
762                match ctor_name.as_str() {
763                    "SApp" => {
764                        // SApp f x -> max(max_var(f), max_var(x))
765                        let a_max = try_syn_max_var_reduce(ctx, a, depth)?;
766                        let b_max = try_syn_max_var_reduce(ctx, inner_arg, depth)?;
767
768                        if let (Term::Lit(Literal::Int(a_n)), Term::Lit(Literal::Int(b_n))) =
769                            (a_max, b_max)
770                        {
771                            return Some(Term::Lit(Literal::Int(a_n.max(b_n))));
772                        }
773                    }
774                    "SLam" | "SPi" => {
775                        // SLam A b -> max(max_var(A, depth), max_var(b, depth+1))
776                        // The body 'b' is under one additional binder
777                        let a_max = try_syn_max_var_reduce(ctx, a, depth)?;
778                        let b_max = try_syn_max_var_reduce(ctx, inner_arg, depth + 1)?;
779
780                        if let (Term::Lit(Literal::Int(a_n)), Term::Lit(Literal::Int(b_n))) =
781                            (a_max, b_max)
782                        {
783                            return Some(Term::Lit(Literal::Int(a_n.max(b_n))));
784                        }
785                    }
786                    _ => {}
787                }
788            }
789        }
790    }
791
792    None
793}
794
795// -------------------------------------------------------------------------
796// Substitution Builtins
797// -------------------------------------------------------------------------
798
799/// Lift De Bruijn indices in a Syntax term.
800///
801/// syn_lift amount cutoff term:
802/// - Variables with index < cutoff are bound -> unchanged
803/// - Variables with index >= cutoff are free -> add amount
804fn try_syn_lift_reduce(ctx: &Context, amount: i64, cutoff: i64, term: &Term) -> Option<Term> {
805    // Check for unary constructor: (Ctor arg)
806    if let Term::App(ctor_term, inner_arg) = term {
807        if let Term::Global(ctor_name) = ctor_term.as_ref() {
808            match ctor_name.as_str() {
809                "SVar" => {
810                    if let Term::Lit(Literal::Int(k)) = inner_arg.as_ref() {
811                        if *k >= cutoff {
812                            // Free variable, shift
813                            return Some(Term::App(
814                                Box::new(Term::Global("SVar".to_string())),
815                                Box::new(Term::Lit(Literal::Int(*k + amount))),
816                            ));
817                        } else {
818                            // Bound variable, no shift
819                            return Some(term.clone());
820                        }
821                    }
822                }
823                "SGlobal" | "SSort" | "SLit" | "SName" => {
824                    // No free variables
825                    return Some(term.clone());
826                }
827                _ => {}
828            }
829        }
830
831        // Check for binary constructor: ((Ctor a) b)
832        if let Term::App(inner, a) = ctor_term.as_ref() {
833            if let Term::Global(ctor_name) = inner.as_ref() {
834                match ctor_name.as_str() {
835                    "SApp" => {
836                        // No binding, same cutoff for both
837                        let a_lifted = try_syn_lift_reduce(ctx, amount, cutoff, a)?;
838                        let b_lifted = try_syn_lift_reduce(ctx, amount, cutoff, inner_arg)?;
839                        return Some(Term::App(
840                            Box::new(Term::App(
841                                Box::new(Term::Global("SApp".to_string())),
842                                Box::new(a_lifted),
843                            )),
844                            Box::new(b_lifted),
845                        ));
846                    }
847                    "SLam" | "SPi" => {
848                        // Binder: param type at current cutoff, body at cutoff+1
849                        let param_lifted = try_syn_lift_reduce(ctx, amount, cutoff, a)?;
850                        let body_lifted =
851                            try_syn_lift_reduce(ctx, amount, cutoff + 1, inner_arg)?;
852                        return Some(Term::App(
853                            Box::new(Term::App(
854                                Box::new(Term::Global(ctor_name.clone())),
855                                Box::new(param_lifted),
856                            )),
857                            Box::new(body_lifted),
858                        ));
859                    }
860                    _ => {}
861                }
862            }
863        }
864    }
865
866    None
867}
868
869/// Substitute a term for a variable in a Syntax term.
870///
871/// syn_subst replacement index term:
872/// - If term is SVar k and k == index, return replacement
873/// - If term is SVar k and k != index, return term unchanged
874/// - For binders, increment index and lift replacement
875fn try_syn_subst_reduce(
876    ctx: &Context,
877    replacement: &Term,
878    index: i64,
879    term: &Term,
880) -> Option<Term> {
881    // Check for unary constructor: (Ctor arg)
882    if let Term::App(ctor_term, inner_arg) = term {
883        if let Term::Global(ctor_name) = ctor_term.as_ref() {
884            match ctor_name.as_str() {
885                "SVar" => {
886                    if let Term::Lit(Literal::Int(k)) = inner_arg.as_ref() {
887                        if *k == index {
888                            // Match! Return replacement
889                            return Some(replacement.clone());
890                        } else {
891                            // No match, return unchanged
892                            return Some(term.clone());
893                        }
894                    }
895                }
896                "SGlobal" | "SSort" | "SLit" | "SName" => {
897                    // No variables to substitute
898                    return Some(term.clone());
899                }
900                _ => {}
901            }
902        }
903
904        // Check for binary constructor: ((Ctor a) b)
905        if let Term::App(inner, a) = ctor_term.as_ref() {
906            if let Term::Global(ctor_name) = inner.as_ref() {
907                match ctor_name.as_str() {
908                    "SApp" => {
909                        // No binding, same index and replacement
910                        let a_subst = try_syn_subst_reduce(ctx, replacement, index, a)?;
911                        let b_subst = try_syn_subst_reduce(ctx, replacement, index, inner_arg)?;
912                        return Some(Term::App(
913                            Box::new(Term::App(
914                                Box::new(Term::Global("SApp".to_string())),
915                                Box::new(a_subst),
916                            )),
917                            Box::new(b_subst),
918                        ));
919                    }
920                    "SLam" | "SPi" => {
921                        // Binder: param type at current index, body at index+1
922                        // Lift replacement when going under binder
923                        let param_subst = try_syn_subst_reduce(ctx, replacement, index, a)?;
924
925                        // Lift the replacement by 1 when going under the binder
926                        let lifted_replacement = try_syn_lift_reduce(ctx, 1, 0, replacement)?;
927                        let body_subst = try_syn_subst_reduce(
928                            ctx,
929                            &lifted_replacement,
930                            index + 1,
931                            inner_arg,
932                        )?;
933
934                        return Some(Term::App(
935                            Box::new(Term::App(
936                                Box::new(Term::Global(ctor_name.clone())),
937                                Box::new(param_subst),
938                            )),
939                            Box::new(body_subst),
940                        ));
941                    }
942                    _ => {}
943                }
944            }
945        }
946    }
947
948    None
949}
950
951// -------------------------------------------------------------------------
952// Computation Builtins
953// -------------------------------------------------------------------------
954
955/// Beta reduction: substitute arg for variable 0 in body.
956///
957/// syn_beta body arg = syn_subst arg 0 body
958fn try_syn_beta_reduce(ctx: &Context, body: &Term, arg: &Term) -> Option<Term> {
959    // syn_beta is just syn_subst with index 0
960    try_syn_subst_reduce(ctx, arg, 0, body)
961}
962
963/// Try to reduce arithmetic on Syntax literals.
964///
965/// Handles: SApp (SApp (SName op) (SLit n)) (SLit m) → SLit result
966/// where op is one of: add, sub, mul, div, mod
967fn try_syn_arith_reduce(func: &Term, arg: &Term) -> Option<Term> {
968    // func should be: SApp (SName op) (SLit n)
969    // Pattern: App(App(Global("SApp"), App(Global("SName"), Lit(Text(op)))), App(Global("SLit"), Lit(Int(n))))
970    if let Term::App(inner_ctor, n_term) = func {
971        if let Term::App(sapp_ctor, op_term) = inner_ctor.as_ref() {
972            // Check for SApp constructor
973            if let Term::Global(ctor_name) = sapp_ctor.as_ref() {
974                if ctor_name != "SApp" {
975                    return None;
976                }
977            } else {
978                return None;
979            }
980
981            // Extract op from SName op
982            let op = if let Term::App(sname_ctor, op_str) = op_term.as_ref() {
983                if let Term::Global(name) = sname_ctor.as_ref() {
984                    if name == "SName" {
985                        if let Term::Lit(Literal::Text(op)) = op_str.as_ref() {
986                            op.clone()
987                        } else {
988                            return None;
989                        }
990                    } else {
991                        return None;
992                    }
993                } else {
994                    return None;
995                }
996            } else {
997                return None;
998            };
999
1000            // Extract n from SLit n
1001            let n = if let Term::App(slit_ctor, n_val) = n_term.as_ref() {
1002                if let Term::Global(name) = slit_ctor.as_ref() {
1003                    if name == "SLit" {
1004                        if let Term::Lit(Literal::Int(n)) = n_val.as_ref() {
1005                            *n
1006                        } else {
1007                            return None;
1008                        }
1009                    } else {
1010                        return None;
1011                    }
1012                } else {
1013                    return None;
1014                }
1015            } else {
1016                return None;
1017            };
1018
1019            // Extract m from SLit m (the arg)
1020            let m = if let Term::App(slit_ctor, m_val) = arg {
1021                if let Term::Global(name) = slit_ctor.as_ref() {
1022                    if name == "SLit" {
1023                        if let Term::Lit(Literal::Int(m)) = m_val.as_ref() {
1024                            *m
1025                        } else {
1026                            return None;
1027                        }
1028                    } else {
1029                        return None;
1030                    }
1031                } else {
1032                    return None;
1033                }
1034            } else {
1035                return None;
1036            };
1037
1038            // Compute result based on operator
1039            let result = match op.as_str() {
1040                "add" => n.checked_add(m),
1041                "sub" => n.checked_sub(m),
1042                "mul" => n.checked_mul(m),
1043                "div" => {
1044                    if m == 0 {
1045                        return None; // Division by zero: remain stuck
1046                    }
1047                    n.checked_div(m)
1048                }
1049                "mod" => {
1050                    if m == 0 {
1051                        return None; // Mod by zero: remain stuck
1052                    }
1053                    n.checked_rem(m)
1054                }
1055                _ => None,
1056            };
1057
1058            // Build SLit result
1059            if let Some(r) = result {
1060                return Some(Term::App(
1061                    Box::new(Term::Global("SLit".to_string())),
1062                    Box::new(Term::Lit(Literal::Int(r))),
1063                ));
1064            }
1065        }
1066    }
1067
1068    None
1069}
1070
1071/// Single-step head reduction.
1072///
1073/// Looks for the leftmost-outermost beta redex and reduces it.
1074/// - If SApp (SLam T body) arg: perform beta reduction
1075/// - If SApp f x where f is reducible: reduce f
1076/// - Otherwise: return unchanged (stuck or value)
1077fn try_syn_step_reduce(ctx: &Context, term: &Term) -> Option<Term> {
1078    // Check for SApp (binary constructor)
1079    if let Term::App(ctor_term, arg) = term {
1080        if let Term::App(inner, func) = ctor_term.as_ref() {
1081            if let Term::Global(ctor_name) = inner.as_ref() {
1082                if ctor_name == "SApp" {
1083                    // We have SApp func arg
1084                    // First, check for arithmetic primitives: SApp (SApp (SName op) (SLit n)) (SLit m)
1085                    if let Some(result) = try_syn_arith_reduce(func.as_ref(), arg.as_ref()) {
1086                        return Some(result);
1087                    }
1088
1089                    // Check if func is SLam (beta redex)
1090                    if let Term::App(lam_inner, body) = func.as_ref() {
1091                        if let Term::App(lam_ctor, _param_type) = lam_inner.as_ref() {
1092                            if let Term::Global(lam_name) = lam_ctor.as_ref() {
1093                                if lam_name == "SLam" {
1094                                    // Beta redex! (SApp (SLam T body) arg) → syn_beta body arg
1095                                    return try_syn_beta_reduce(ctx, body.as_ref(), arg.as_ref());
1096                                }
1097                            }
1098                        }
1099                    }
1100
1101                    // Delta reduction via kernel normalization:
1102                    // When the entire SApp tree represents a reducible expression
1103                    // (e.g., SApp(SApp(SName("bit_and"), SName("B1")), SName("B0"))),
1104                    // reify to kernel Term, normalize, and convert back to Syntax.
1105                    // This leverages the kernel's full reduction machinery (delta + iota + beta)
1106                    // without needing Match support in the Syntax representation.
1107                    {
1108                        let full_app = term; // The entire SApp(func, arg) Syntax term
1109                        if let Some(kernel_term) = syntax_to_term(full_app) {
1110                            let normalized = normalize(ctx, &kernel_term);
1111                            if normalized != kernel_term {
1112                                if let Some(result_syntax) = term_to_syntax(&normalized) {
1113                                    return Some(result_syntax);
1114                                }
1115                            }
1116                        }
1117                    }
1118
1119                    // Not a beta redex or reducible application. Try to step the function.
1120                    if let Some(stepped_func) = try_syn_step_reduce(ctx, func.as_ref()) {
1121                        // Check if func actually changed
1122                        if &stepped_func != func.as_ref() {
1123                            // func reduced, reconstruct SApp stepped_func arg
1124                            return Some(Term::App(
1125                                Box::new(Term::App(
1126                                    Box::new(Term::Global("SApp".to_string())),
1127                                    Box::new(stepped_func),
1128                                )),
1129                                Box::new(arg.as_ref().clone()),
1130                            ));
1131                        }
1132                    }
1133
1134                    // func is stuck. Try to step the argument.
1135                    if let Some(stepped_arg) = try_syn_step_reduce(ctx, arg.as_ref()) {
1136                        if &stepped_arg != arg.as_ref() {
1137                            // arg reduced, reconstruct SApp func stepped_arg
1138                            return Some(Term::App(
1139                                Box::new(Term::App(
1140                                    Box::new(Term::Global("SApp".to_string())),
1141                                    Box::new(func.as_ref().clone()),
1142                                )),
1143                                Box::new(stepped_arg),
1144                            ));
1145                        }
1146                    }
1147
1148                    // Both func and arg are stuck, return original term
1149                    return Some(term.clone());
1150                }
1151            }
1152        }
1153    }
1154
1155    // Not an application - it's a value or stuck term
1156    // Return unchanged
1157    Some(term.clone())
1158}
1159
1160// -------------------------------------------------------------------------
1161// Bounded Evaluation
1162// -------------------------------------------------------------------------
1163
1164/// Bounded evaluation: reduce for up to N steps.
1165///
1166/// syn_eval fuel term:
1167/// - If fuel <= 0: return term unchanged
1168/// - Otherwise: step and repeat until normal form or fuel exhausted
1169fn try_syn_eval_reduce(ctx: &Context, fuel: i64, term: &Term) -> Option<Term> {
1170    if fuel <= 0 {
1171        return Some(term.clone());
1172    }
1173
1174    // Try one step
1175    let stepped = try_syn_step_reduce(ctx, term)?;
1176
1177    // If term didn't change, it's in normal form (or stuck)
1178    if &stepped == term {
1179        return Some(term.clone());
1180    }
1181
1182    // Continue with reduced fuel
1183    try_syn_eval_reduce(ctx, fuel - 1, &stepped)
1184}
1185
1186// -------------------------------------------------------------------------
1187// Reification (Quote)
1188// -------------------------------------------------------------------------
1189
1190/// Quote a Syntax value: produce Syntax that constructs it.
1191///
1192/// syn_quote term:
1193/// - SVar n → SApp (SName "SVar") (SLit n)
1194/// - SGlobal n → SApp (SName "SGlobal") (SLit n)
1195/// - SSort u → SApp (SName "SSort") (quote_univ u)
1196/// - SApp f x → SApp (SApp (SName "SApp") (quote f)) (quote x)
1197/// - SLam T b → SApp (SApp (SName "SLam") (quote T)) (quote b)
1198/// - SPi T B → SApp (SApp (SName "SPi") (quote T)) (quote B)
1199/// - SLit n → SApp (SName "SLit") (SLit n)
1200/// - SName s → SName s (self-quoting)
1201#[allow(dead_code)]
1202fn try_syn_quote_reduce(ctx: &Context, term: &Term) -> Option<Term> {
1203    // Helper to build SApp (SName name) arg
1204    fn sname_app(name: &str, arg: Term) -> Term {
1205        Term::App(
1206            Box::new(Term::App(
1207                Box::new(Term::Global("SApp".to_string())),
1208                Box::new(Term::App(
1209                    Box::new(Term::Global("SName".to_string())),
1210                    Box::new(Term::Lit(Literal::Text(name.to_string()))),
1211                )),
1212            )),
1213            Box::new(arg),
1214        )
1215    }
1216
1217    // Helper to build SLit n
1218    fn slit(n: i64) -> Term {
1219        Term::App(
1220            Box::new(Term::Global("SLit".to_string())),
1221            Box::new(Term::Lit(Literal::Int(n))),
1222        )
1223    }
1224
1225    // Helper to build SName s
1226    fn sname(s: &str) -> Term {
1227        Term::App(
1228            Box::new(Term::Global("SName".to_string())),
1229            Box::new(Term::Lit(Literal::Text(s.to_string()))),
1230        )
1231    }
1232
1233    // Helper to build SApp (SApp (SName name) a) b
1234    fn sname_app2(name: &str, a: Term, b: Term) -> Term {
1235        Term::App(
1236            Box::new(Term::App(
1237                Box::new(Term::Global("SApp".to_string())),
1238                Box::new(sname_app(name, a)),
1239            )),
1240            Box::new(b),
1241        )
1242    }
1243
1244    // Match on Syntax constructors
1245    if let Term::App(ctor_term, inner_arg) = term {
1246        if let Term::Global(ctor_name) = ctor_term.as_ref() {
1247            match ctor_name.as_str() {
1248                "SVar" => {
1249                    if let Term::Lit(Literal::Int(n)) = inner_arg.as_ref() {
1250                        return Some(sname_app("SVar", slit(*n)));
1251                    }
1252                }
1253                "SGlobal" => {
1254                    if let Term::Lit(Literal::Int(n)) = inner_arg.as_ref() {
1255                        return Some(sname_app("SGlobal", slit(*n)));
1256                    }
1257                }
1258                "SSort" => {
1259                    // Quote the universe
1260                    let quoted_univ = quote_univ(inner_arg)?;
1261                    return Some(sname_app("SSort", quoted_univ));
1262                }
1263                "SLit" => {
1264                    if let Term::Lit(Literal::Int(n)) = inner_arg.as_ref() {
1265                        return Some(sname_app("SLit", slit(*n)));
1266                    }
1267                }
1268                "SName" => {
1269                    // SName is self-quoting
1270                    return Some(term.clone());
1271                }
1272                _ => {}
1273            }
1274        }
1275
1276        // Binary constructors: ((Ctor a) b)
1277        if let Term::App(inner, a) = ctor_term.as_ref() {
1278            if let Term::Global(ctor_name) = inner.as_ref() {
1279                match ctor_name.as_str() {
1280                    "SApp" | "SLam" | "SPi" => {
1281                        let quoted_a = try_syn_quote_reduce(ctx, a)?;
1282                        let quoted_b = try_syn_quote_reduce(ctx, inner_arg)?;
1283                        return Some(sname_app2(ctor_name, quoted_a, quoted_b));
1284                    }
1285                    _ => {}
1286                }
1287            }
1288        }
1289    }
1290
1291    None
1292}
1293
1294/// Quote a Univ value.
1295///
1296/// UProp → SName "UProp"
1297/// UType n → SApp (SName "UType") (SLit n)
1298fn quote_univ(term: &Term) -> Option<Term> {
1299    fn sname(s: &str) -> Term {
1300        Term::App(
1301            Box::new(Term::Global("SName".to_string())),
1302            Box::new(Term::Lit(Literal::Text(s.to_string()))),
1303        )
1304    }
1305
1306    fn slit(n: i64) -> Term {
1307        Term::App(
1308            Box::new(Term::Global("SLit".to_string())),
1309            Box::new(Term::Lit(Literal::Int(n))),
1310        )
1311    }
1312
1313    fn sname_app(name: &str, arg: Term) -> Term {
1314        Term::App(
1315            Box::new(Term::App(
1316                Box::new(Term::Global("SApp".to_string())),
1317                Box::new(sname(name)),
1318            )),
1319            Box::new(arg),
1320        )
1321    }
1322
1323    if let Term::Global(name) = term {
1324        if name == "UProp" {
1325            return Some(sname("UProp"));
1326        }
1327    }
1328
1329    if let Term::App(ctor, arg) = term {
1330        if let Term::Global(name) = ctor.as_ref() {
1331            if name == "UType" {
1332                if let Term::Lit(Literal::Int(n)) = arg.as_ref() {
1333                    return Some(sname_app("UType", slit(*n)));
1334                }
1335            }
1336        }
1337    }
1338
1339    None
1340}
1341
1342// -------------------------------------------------------------------------
1343// Diagonalization (Self-Reference)
1344// -------------------------------------------------------------------------
1345
1346/// The diagonal function: syn_diag x = syn_subst (syn_quote x) 0 x
1347///
1348/// This takes a term x with free variable 0, quotes x to get its construction
1349/// code, then substitutes that code for variable 0 in x.
1350fn try_syn_diag_reduce(ctx: &Context, term: &Term) -> Option<Term> {
1351    // Step 1: Quote the term
1352    let quoted = try_syn_quote_reduce(ctx, term)?;
1353
1354    // Step 2: Substitute the quoted form for variable 0 in the original term
1355    try_syn_subst_reduce(ctx, &quoted, 0, term)
1356}
1357
1358// -------------------------------------------------------------------------
1359// Inference Rules
1360// -------------------------------------------------------------------------
1361
1362/// Extract the conclusion from a derivation.
1363///
1364/// concludes d:
1365/// - DAxiom P → P
1366/// - DModusPonens d_impl d_ant → extract B from (Implies A B) if A matches antecedent
1367/// - DUnivIntro d → wrap conclusion in Forall
1368/// - DUnivElim d term → substitute term into forall body
1369/// - DRefl T a → Eq T a a
1370fn try_concludes_reduce(ctx: &Context, deriv: &Term) -> Option<Term> {
1371    // DAxiom P → P
1372    if let Term::App(ctor_term, p) = deriv {
1373        if let Term::Global(ctor_name) = ctor_term.as_ref() {
1374            if ctor_name == "DAxiom" {
1375                return Some(p.as_ref().clone());
1376            }
1377            if ctor_name == "DUnivIntro" {
1378                // Get conclusion of inner derivation
1379                let inner_conc = try_concludes_reduce(ctx, p)?;
1380                // Lift it by 1 and wrap in Forall
1381                let lifted = try_syn_lift_reduce(ctx, 1, 0, &inner_conc)?;
1382                return Some(make_forall_syntax(&lifted));
1383            }
1384            if ctor_name == "DCompute" {
1385                // DCompute goal: verify goal is Eq T A B and eval(A) == eval(B)
1386                return try_dcompute_conclude(ctx, p);
1387            }
1388            if ctor_name == "DRingSolve" {
1389                // DRingSolve goal: verify goal is Eq T A B and polynomials are equal
1390                return try_dring_solve_conclude(ctx, p);
1391            }
1392            if ctor_name == "DLiaSolve" {
1393                // DLiaSolve goal: verify goal is an inequality and LIA proves it
1394                return try_dlia_solve_conclude(ctx, p);
1395            }
1396            if ctor_name == "DccSolve" {
1397                // DccSolve goal: verify goal by congruence closure
1398                return try_dcc_solve_conclude(ctx, p);
1399            }
1400            if ctor_name == "DSimpSolve" {
1401                // DSimpSolve goal: verify goal by simplification
1402                return try_dsimp_solve_conclude(ctx, p);
1403            }
1404            if ctor_name == "DOmegaSolve" {
1405                // DOmegaSolve goal: verify goal by integer arithmetic
1406                return try_domega_solve_conclude(ctx, p);
1407            }
1408            if ctor_name == "DAutoSolve" {
1409                // DAutoSolve goal: verify goal by trying all tactics
1410                return try_dauto_solve_conclude(ctx, p);
1411            }
1412            if ctor_name == "DBitblastSolve" {
1413                // DBitblastSolve goal: verify Eq Bit by normalization
1414                return try_dbitblast_solve_conclude(ctx, p);
1415            }
1416            if ctor_name == "DTabulateSolve" {
1417                // DTabulateSolve goal: verify universal Bit by exhaustion
1418                return try_dtabulate_solve_conclude(ctx, p);
1419            }
1420            if ctor_name == "DHwAutoSolve" {
1421                // DHwAutoSolve goal: verify by hw tactic chain
1422                return try_dhw_auto_solve_conclude(ctx, p);
1423            }
1424            if ctor_name == "DInversion" {
1425                // DInversion hyp_type: verify no constructor can match, return False
1426                return try_dinversion_conclude(ctx, p);
1427            }
1428        }
1429    }
1430
1431    // DRewrite eq_proof old_goal new_goal → new_goal (if verified)
1432    // Pattern: App(App(App(DRewrite, eq_proof), old_goal), new_goal)
1433    if let Term::App(partial1, new_goal) = deriv {
1434        if let Term::App(partial2, old_goal) = partial1.as_ref() {
1435            if let Term::App(ctor_term, eq_proof) = partial2.as_ref() {
1436                if let Term::Global(ctor_name) = ctor_term.as_ref() {
1437                    if ctor_name == "DRewrite" {
1438                        return try_drewrite_conclude(ctx, eq_proof, old_goal, new_goal);
1439                    }
1440                }
1441            }
1442        }
1443    }
1444
1445    // DDestruct ind_type motive cases → Forall ind_type motive (if verified)
1446    // Pattern: App(App(App(DDestruct, ind_type), motive), cases)
1447    if let Term::App(partial1, cases) = deriv {
1448        if let Term::App(partial2, motive) = partial1.as_ref() {
1449            if let Term::App(ctor_term, ind_type) = partial2.as_ref() {
1450                if let Term::Global(ctor_name) = ctor_term.as_ref() {
1451                    if ctor_name == "DDestruct" {
1452                        return try_ddestruct_conclude(ctx, ind_type, motive, cases);
1453                    }
1454                }
1455            }
1456        }
1457    }
1458
1459    // DApply hyp_name hyp_proof old_goal new_goal → new_goal (if verified)
1460    // Pattern: App(App(App(App(DApply, hyp_name), hyp_proof), old_goal), new_goal)
1461    if let Term::App(partial1, new_goal) = deriv {
1462        if let Term::App(partial2, old_goal) = partial1.as_ref() {
1463            if let Term::App(partial3, hyp_proof) = partial2.as_ref() {
1464                if let Term::App(ctor_term, hyp_name) = partial3.as_ref() {
1465                    if let Term::Global(ctor_name) = ctor_term.as_ref() {
1466                        if ctor_name == "DApply" {
1467                            return try_dapply_conclude(ctx, hyp_name, hyp_proof, old_goal, new_goal);
1468                        }
1469                    }
1470                }
1471            }
1472        }
1473    }
1474
1475    // DRefl T a → Eq T a a
1476    if let Term::App(partial, a) = deriv {
1477        if let Term::App(ctor_term, t) = partial.as_ref() {
1478            if let Term::Global(ctor_name) = ctor_term.as_ref() {
1479                if ctor_name == "DRefl" {
1480                    return Some(make_eq_syntax(t.as_ref(), a.as_ref()));
1481                }
1482                if ctor_name == "DCong" {
1483                    // DCong context eq_proof → Eq T (f a) (f b)
1484                    // where context = SLam T body, eq_proof proves Eq T a b
1485                    return try_dcong_conclude(ctx, t, a);
1486                }
1487            }
1488        }
1489    }
1490
1491    // DModusPonens d_impl d_ant
1492    if let Term::App(partial, d_ant) = deriv {
1493        if let Term::App(ctor_term, d_impl) = partial.as_ref() {
1494            if let Term::Global(ctor_name) = ctor_term.as_ref() {
1495                if ctor_name == "DModusPonens" {
1496                    // Get conclusions of both derivations
1497                    let impl_conc = try_concludes_reduce(ctx, d_impl)?;
1498                    let ant_conc = try_concludes_reduce(ctx, d_ant)?;
1499
1500                    // Check if impl_conc = SApp (SApp (SName "Implies") A) B
1501                    if let Some((a, b)) = extract_implication(&impl_conc) {
1502                        // Check if ant_conc equals A
1503                        if syntax_equal(&ant_conc, &a) {
1504                            return Some(b);
1505                        }
1506                    }
1507                    // Invalid modus ponens
1508                    return Some(make_sname_error());
1509                }
1510                if ctor_name == "DUnivElim" {
1511                    // d_impl is the derivation, d_ant is the term to substitute
1512                    let conc = try_concludes_reduce(ctx, d_impl)?;
1513                    if let Some(body) = extract_forall_body(&conc) {
1514                        // Substitute d_ant for var 0 in body
1515                        return try_syn_subst_reduce(ctx, d_ant, 0, &body);
1516                    }
1517                    // Invalid universal elimination
1518                    return Some(make_sname_error());
1519                }
1520            }
1521        }
1522    }
1523
1524    // DInduction motive base step → Forall Nat motive (if verified)
1525    // Pattern: App(App(App(DInduction, motive), base), step)
1526    if let Term::App(partial1, step) = deriv {
1527        if let Term::App(partial2, base) = partial1.as_ref() {
1528            if let Term::App(ctor_term, motive) = partial2.as_ref() {
1529                if let Term::Global(ctor_name) = ctor_term.as_ref() {
1530                    if ctor_name == "DInduction" {
1531                        return try_dinduction_reduce(ctx, motive, base, step);
1532                    }
1533                }
1534            }
1535        }
1536    }
1537
1538    // DElim ind_type motive cases → Forall ind_type motive (if verified)
1539    // Pattern: App(App(App(DElim, ind_type), motive), cases)
1540    if let Term::App(partial1, cases) = deriv {
1541        if let Term::App(partial2, motive) = partial1.as_ref() {
1542            if let Term::App(ctor_term, ind_type) = partial2.as_ref() {
1543                if let Term::Global(ctor_name) = ctor_term.as_ref() {
1544                    if ctor_name == "DElim" {
1545                        return try_delim_conclude(ctx, ind_type, motive, cases);
1546                    }
1547                }
1548            }
1549        }
1550    }
1551
1552    None
1553}
1554
1555/// Extract (A, B) from SApp (SApp (SName "Implies") A) B
1556///
1557/// In kernel representation:
1558/// SApp X Y = App(App(SApp, X), Y)
1559/// So SApp (SApp (SName "Implies") A) B =
1560///   App(App(SApp, App(App(SApp, App(SName, "Implies")), A)), B)
1561fn extract_implication(term: &Term) -> Option<(Term, Term)> {
1562    // term = App(App(SApp, X), B)
1563    if let Term::App(outer, b) = term {
1564        if let Term::App(sapp_outer, x) = outer.as_ref() {
1565            if let Term::Global(ctor) = sapp_outer.as_ref() {
1566                if ctor == "SApp" {
1567                    // x = App(App(SApp, App(SName, "Implies")), A)
1568                    if let Term::App(inner, a) = x.as_ref() {
1569                        if let Term::App(sapp_inner, sname_implies) = inner.as_ref() {
1570                            if let Term::Global(ctor2) = sapp_inner.as_ref() {
1571                                if ctor2 == "SApp" {
1572                                    // sname_implies = App(SName, "Implies")
1573                                    if let Term::App(sname, text) = sname_implies.as_ref() {
1574                                        if let Term::Global(sname_ctor) = sname.as_ref() {
1575                                            if sname_ctor == "SName" {
1576                                                if let Term::Lit(Literal::Text(s)) = text.as_ref() {
1577                                                    if s == "Implies" || s == "implies" {
1578                                                        return Some((
1579                                                            a.as_ref().clone(),
1580                                                            b.as_ref().clone(),
1581                                                        ));
1582                                                    }
1583                                                }
1584                                            }
1585                                        }
1586                                    }
1587                                }
1588                            }
1589                        }
1590                    }
1591                }
1592            }
1593        }
1594    }
1595    None
1596}
1597
1598/// Extract all hypotheses from a chain of nested implications.
1599///
1600/// For `A -> B -> C`, returns `([A, B], C)`.
1601/// For non-implications, returns `([], term)`.
1602fn extract_implications(term: &Term) -> Option<(Vec<Term>, Term)> {
1603    let mut hyps = Vec::new();
1604    let mut current = term.clone();
1605
1606    while let Some((hyp, rest)) = extract_implication(&current) {
1607        hyps.push(hyp);
1608        current = rest;
1609    }
1610
1611    if hyps.is_empty() {
1612        None
1613    } else {
1614        Some((hyps, current))
1615    }
1616}
1617
1618/// Extract body from SApp (SApp (SName "Forall") T) (SLam T body)
1619///
1620/// In kernel representation:
1621/// Extract body from Forall syntax (two forms supported):
1622/// Form 1: SApp (SName "Forall") (SLam T body)
1623/// Form 2: SApp (SApp (SName "Forall") T) (SLam T body)
1624fn extract_forall_body(term: &Term) -> Option<Term> {
1625    // term = App(App(SApp, X), lam)
1626    if let Term::App(outer, lam) = term {
1627        if let Term::App(sapp_outer, x) = outer.as_ref() {
1628            if let Term::Global(ctor) = sapp_outer.as_ref() {
1629                if ctor == "SApp" {
1630                    // Form 1: X = App(SName, "Forall")
1631                    if let Term::App(sname, text) = x.as_ref() {
1632                        if let Term::Global(sname_ctor) = sname.as_ref() {
1633                            if sname_ctor == "SName" {
1634                                if let Term::Lit(Literal::Text(s)) = text.as_ref() {
1635                                    if s == "Forall" {
1636                                        // Extract body from SLam
1637                                        return extract_slam_body(lam);
1638                                    }
1639                                }
1640                            }
1641                        }
1642                    }
1643
1644                    // Form 2: X = App(App(SApp, App(SName, "Forall")), T)
1645                    if let Term::App(inner, _t) = x.as_ref() {
1646                        if let Term::App(sapp_inner, sname_forall) = inner.as_ref() {
1647                            if let Term::Global(ctor2) = sapp_inner.as_ref() {
1648                                if ctor2 == "SApp" {
1649                                    if let Term::App(sname, text) = sname_forall.as_ref() {
1650                                        if let Term::Global(sname_ctor) = sname.as_ref() {
1651                                            if sname_ctor == "SName" {
1652                                                if let Term::Lit(Literal::Text(s)) = text.as_ref() {
1653                                                    if s == "Forall" {
1654                                                        return extract_slam_body(lam);
1655                                                    }
1656                                                }
1657                                            }
1658                                        }
1659                                    }
1660                                }
1661                            }
1662                        }
1663                    }
1664                }
1665            }
1666        }
1667    }
1668    None
1669}
1670
1671/// Extract body from ((SLam T) body)
1672fn extract_slam_body(term: &Term) -> Option<Term> {
1673    if let Term::App(inner, body) = term {
1674        if let Term::App(slam, _t) = inner.as_ref() {
1675            if let Term::Global(name) = slam.as_ref() {
1676                if name == "SLam" {
1677                    return Some(body.as_ref().clone());
1678                }
1679            }
1680        }
1681    }
1682    None
1683}
1684
1685/// Structural equality check for Syntax terms
1686fn syntax_equal(a: &Term, b: &Term) -> bool {
1687    a == b
1688}
1689
1690/// Build SName "Error"
1691fn make_sname_error() -> Term {
1692    Term::App(
1693        Box::new(Term::Global("SName".to_string())),
1694        Box::new(Term::Lit(Literal::Text("Error".to_string()))),
1695    )
1696}
1697
1698/// Build SName from a string
1699fn make_sname(s: &str) -> Term {
1700    Term::App(
1701        Box::new(Term::Global("SName".to_string())),
1702        Box::new(Term::Lit(Literal::Text(s.to_string()))),
1703    )
1704}
1705
1706/// Build SLit from an integer
1707fn make_slit(n: i64) -> Term {
1708    Term::App(
1709        Box::new(Term::Global("SLit".to_string())),
1710        Box::new(Term::Lit(Literal::Int(n))),
1711    )
1712}
1713
1714/// Build SApp f x
1715fn make_sapp(f: Term, x: Term) -> Term {
1716    Term::App(
1717        Box::new(Term::App(
1718            Box::new(Term::Global("SApp".to_string())),
1719            Box::new(f),
1720        )),
1721        Box::new(x),
1722    )
1723}
1724
1725/// Build SPi A B
1726fn make_spi(a: Term, b: Term) -> Term {
1727    Term::App(
1728        Box::new(Term::App(
1729            Box::new(Term::Global("SPi".to_string())),
1730            Box::new(a),
1731        )),
1732        Box::new(b),
1733    )
1734}
1735
1736/// Build SLam A b
1737fn make_slam(a: Term, b: Term) -> Term {
1738    Term::App(
1739        Box::new(Term::App(
1740            Box::new(Term::Global("SLam".to_string())),
1741            Box::new(a),
1742        )),
1743        Box::new(b),
1744    )
1745}
1746
1747/// Build SSort u
1748fn make_ssort(u: Term) -> Term {
1749    Term::App(
1750        Box::new(Term::Global("SSort".to_string())),
1751        Box::new(u),
1752    )
1753}
1754
1755/// Build SVar n
1756fn make_svar(n: i64) -> Term {
1757    Term::App(
1758        Box::new(Term::Global("SVar".to_string())),
1759        Box::new(Term::Lit(Literal::Int(n))),
1760    )
1761}
1762
1763/// Convert a kernel Term to Syntax encoding (S* form).
1764///
1765/// This converts semantic Terms to their syntactic representation:
1766/// - Global(n) → SName n
1767/// - Var(n) → SName n (for named variables)
1768/// - App(f, x) → SApp (convert f) (convert x)
1769/// - Pi { param, param_type, body_type } → SPi (convert param_type) (convert body_type)
1770/// - Lambda { param, param_type, body } → SLam (convert param_type) (convert body)
1771/// - Sort(Type n) → SSort (UType n)
1772/// - Sort(Prop) → SSort UProp
1773/// - Lit(Int n) → SLit n
1774/// - Lit(Text s) → SName s
1775fn term_to_syntax(term: &Term) -> Option<Term> {
1776    match term {
1777        Term::Global(name) => Some(make_sname(name)),
1778
1779        Term::Var(name) => {
1780            // Named variables become SName in syntax representation
1781            Some(make_sname(name))
1782        }
1783
1784        Term::App(f, x) => {
1785            let sf = term_to_syntax(f)?;
1786            let sx = term_to_syntax(x)?;
1787            Some(make_sapp(sf, sx))
1788        }
1789
1790        Term::Pi { param_type, body_type, .. } => {
1791            let sp = term_to_syntax(param_type)?;
1792            let sb = term_to_syntax(body_type)?;
1793            Some(make_spi(sp, sb))
1794        }
1795
1796        Term::Lambda { param_type, body, .. } => {
1797            let sp = term_to_syntax(param_type)?;
1798            let sb = term_to_syntax(body)?;
1799            Some(make_slam(sp, sb))
1800        }
1801
1802        Term::Sort(Universe::Type(n)) => {
1803            let u = Term::App(
1804                Box::new(Term::Global("UType".to_string())),
1805                Box::new(Term::Lit(Literal::Int(*n as i64))),
1806            );
1807            Some(make_ssort(u))
1808        }
1809
1810        Term::Sort(Universe::Prop) => {
1811            let u = Term::Global("UProp".to_string());
1812            Some(make_ssort(u))
1813        }
1814
1815        Term::Lit(Literal::Int(n)) => Some(make_slit(*n)),
1816
1817        Term::Lit(Literal::Text(s)) => Some(make_sname(s)),
1818
1819        // Float, Duration, Date, and Moment literals - skip for now as they're rarely used in proofs
1820        Term::Lit(Literal::Float(_))
1821        | Term::Lit(Literal::Duration(_))
1822        | Term::Lit(Literal::Date(_))
1823        | Term::Lit(Literal::Moment(_)) => None,
1824
1825        // Match expressions, Fix, and Hole are complex - skip for now
1826        Term::Match { .. } | Term::Fix { .. } | Term::Hole => None,
1827    }
1828}
1829
1830/// Build DHint derivation that references a hint by name.
1831///
1832/// Uses DAxiom (SName "hint_name") to indicate the proof uses this hint.
1833fn make_hint_derivation(hint_name: &str, goal: &Term) -> Term {
1834    // Build: DAxiom (SApp (SName "Hint") (SName hint_name))
1835    // This distinguishes hints from error derivations
1836    let hint_marker = make_sapp(make_sname("Hint"), make_sname(hint_name));
1837
1838    // Actually, let's use a simpler approach: DAutoSolve goal
1839    // This indicates auto succeeded, and we can trace which hint was used through debugging
1840    Term::App(
1841        Box::new(Term::Global("DAutoSolve".to_string())),
1842        Box::new(goal.clone()),
1843    )
1844}
1845
1846/// Try to apply a hint to prove a goal.
1847///
1848/// Returns Some(derivation) if the hint's type matches the goal,
1849/// otherwise returns None.
1850fn try_apply_hint(ctx: &Context, hint_name: &str, hint_type: &Term, goal: &Term) -> Option<Term> {
1851    // Convert hint type to syntax form
1852    let hint_syntax = term_to_syntax(hint_type)?;
1853
1854    // Normalize both for comparison
1855    let norm_hint = normalize(ctx, &hint_syntax);
1856    let norm_goal = normalize(ctx, goal);
1857
1858    // Direct match: hint type equals goal
1859    if syntax_equal(&norm_hint, &norm_goal) {
1860        return Some(make_hint_derivation(hint_name, goal));
1861    }
1862
1863    // Try backward chaining for implications: if hint is P → Q and goal is Q,
1864    // try to prove P using auto and then apply the hint
1865    if let Term::App(outer, q) = &hint_syntax {
1866        if let Term::App(pi_ctor, p) = outer.as_ref() {
1867            if let Term::Global(name) = pi_ctor.as_ref() {
1868                if name == "SPi" {
1869                    // hint_type is SPi P Q, goal might be Q
1870                    let norm_q = normalize(ctx, q);
1871                    if syntax_equal(&norm_q, &norm_goal) {
1872                        // Need to prove P first, then apply hint
1873                        // This would require recursive auto call - skip for now
1874                        // to avoid infinite recursion
1875                    }
1876                }
1877            }
1878        }
1879    }
1880
1881    None
1882}
1883
1884/// Build Forall Type0 (SLam Type0 body)
1885fn make_forall_syntax(body: &Term) -> Term {
1886    let type0 = Term::App(
1887        Box::new(Term::Global("SSort".to_string())),
1888        Box::new(Term::App(
1889            Box::new(Term::Global("UType".to_string())),
1890            Box::new(Term::Lit(Literal::Int(0))),
1891        )),
1892    );
1893
1894    // SLam Type0 body
1895    let slam = Term::App(
1896        Box::new(Term::App(
1897            Box::new(Term::Global("SLam".to_string())),
1898            Box::new(type0.clone()),
1899        )),
1900        Box::new(body.clone()),
1901    );
1902
1903    // SApp (SApp (SName "Forall") Type0) slam
1904    Term::App(
1905        Box::new(Term::App(
1906            Box::new(Term::Global("SApp".to_string())),
1907            Box::new(Term::App(
1908                Box::new(Term::App(
1909                    Box::new(Term::Global("SApp".to_string())),
1910                    Box::new(Term::App(
1911                        Box::new(Term::Global("SName".to_string())),
1912                        Box::new(Term::Lit(Literal::Text("Forall".to_string()))),
1913                    )),
1914                )),
1915                Box::new(type0),
1916            )),
1917        )),
1918        Box::new(slam),
1919    )
1920}
1921
1922// -------------------------------------------------------------------------
1923// Core Tactics
1924// -------------------------------------------------------------------------
1925
1926/// Build SApp (SApp (SApp (SName "Eq") type_s) term) term
1927///
1928/// Constructs the Syntax representation of (Eq type_s term term)
1929fn make_eq_syntax(type_s: &Term, term: &Term) -> Term {
1930    let eq_name = Term::App(
1931        Box::new(Term::Global("SName".to_string())),
1932        Box::new(Term::Lit(Literal::Text("Eq".to_string()))),
1933    );
1934
1935    // SApp (SName "Eq") type_s
1936    let app1 = Term::App(
1937        Box::new(Term::App(
1938            Box::new(Term::Global("SApp".to_string())),
1939            Box::new(eq_name),
1940        )),
1941        Box::new(type_s.clone()),
1942    );
1943
1944    // SApp (SApp (SName "Eq") type_s) term
1945    let app2 = Term::App(
1946        Box::new(Term::App(
1947            Box::new(Term::Global("SApp".to_string())),
1948            Box::new(app1),
1949        )),
1950        Box::new(term.clone()),
1951    );
1952
1953    // SApp (SApp (SApp (SName "Eq") type_s) term) term
1954    Term::App(
1955        Box::new(Term::App(
1956            Box::new(Term::Global("SApp".to_string())),
1957            Box::new(app2),
1958        )),
1959        Box::new(term.clone()),
1960    )
1961}
1962
1963/// Extract (T, a, b) from SApp (SApp (SApp (SName "Eq") T) a) b
1964///
1965/// Pattern matches against the Syntax representation of (Eq T a b)
1966fn extract_eq(term: &Term) -> Option<(Term, Term, Term)> {
1967    // term = App(App(SApp, X), b)
1968    if let Term::App(outer, b) = term {
1969        if let Term::App(sapp_outer, x) = outer.as_ref() {
1970            if let Term::Global(ctor) = sapp_outer.as_ref() {
1971                if ctor == "SApp" {
1972                    // x = App(App(SApp, Y), a)
1973                    if let Term::App(inner, a) = x.as_ref() {
1974                        if let Term::App(sapp_inner, y) = inner.as_ref() {
1975                            if let Term::Global(ctor2) = sapp_inner.as_ref() {
1976                                if ctor2 == "SApp" {
1977                                    // y = App(App(SApp, eq_name), t)
1978                                    if let Term::App(inner2, t) = y.as_ref() {
1979                                        if let Term::App(sapp_inner2, sname_eq) = inner2.as_ref() {
1980                                            if let Term::Global(ctor3) = sapp_inner2.as_ref() {
1981                                                if ctor3 == "SApp" {
1982                                                    // sname_eq = App(SName, "Eq")
1983                                                    if let Term::App(sname, text) = sname_eq.as_ref()
1984                                                    {
1985                                                        if let Term::Global(sname_ctor) =
1986                                                            sname.as_ref()
1987                                                        {
1988                                                            if sname_ctor == "SName" {
1989                                                                if let Term::Lit(Literal::Text(s)) =
1990                                                                    text.as_ref()
1991                                                                {
1992                                                                    if s == "Eq" {
1993                                                                        return Some((
1994                                                                            t.as_ref().clone(),
1995                                                                            a.as_ref().clone(),
1996                                                                            b.as_ref().clone(),
1997                                                                        ));
1998                                                                    }
1999                                                                }
2000                                                            }
2001                                                        }
2002                                                    }
2003                                                }
2004                                            }
2005                                        }
2006                                    }
2007                                }
2008                            }
2009                        }
2010                    }
2011                }
2012            }
2013        }
2014    }
2015    None
2016}
2017
2018/// Build DRefl type_s term
2019fn make_drefl(type_s: &Term, term: &Term) -> Term {
2020    let drefl = Term::Global("DRefl".to_string());
2021    let app1 = Term::App(Box::new(drefl), Box::new(type_s.clone()));
2022    Term::App(Box::new(app1), Box::new(term.clone()))
2023}
2024
2025/// Build DAxiom (SName "Error")
2026fn make_error_derivation() -> Term {
2027    let daxiom = Term::Global("DAxiom".to_string());
2028    let error = make_sname_error();
2029    Term::App(Box::new(daxiom), Box::new(error))
2030}
2031
2032/// Build DAxiom goal (identity derivation)
2033fn make_daxiom(goal: &Term) -> Term {
2034    let daxiom = Term::Global("DAxiom".to_string());
2035    Term::App(Box::new(daxiom), Box::new(goal.clone()))
2036}
2037
2038/// Reflexivity tactic: try to prove a goal by reflexivity.
2039///
2040/// try_refl goal:
2041/// - If goal matches (Eq T a b) and a == b, return DRefl T a
2042/// - Otherwise return DAxiom (SName "Error")
2043fn try_try_refl_reduce(ctx: &Context, goal: &Term) -> Option<Term> {
2044    // Normalize the goal first
2045    let norm_goal = normalize(ctx, goal);
2046
2047    // Pattern match: SApp (SApp (SApp (SName "Eq") T) a) b
2048    if let Some((type_s, left, right)) = extract_eq(&norm_goal) {
2049        // Check if left == right (structural equality)
2050        if syntax_equal(&left, &right) {
2051            // Success! Return DRefl T a
2052            return Some(make_drefl(&type_s, &left));
2053        }
2054    }
2055
2056    // Failure: return error derivation
2057    Some(make_error_derivation())
2058}
2059
2060// =============================================================================
2061// RING TACTIC (POLYNOMIAL EQUALITY)
2062// =============================================================================
2063
2064use crate::ring;
2065use crate::lia;
2066use crate::cc;
2067use crate::simp;
2068
2069/// Ring tactic: try to prove a goal by polynomial normalization.
2070///
2071/// try_ring goal:
2072/// - If goal matches (Eq T a b) where T is Int or Nat
2073/// - And poly(a) == poly(b) after normalization
2074/// - Returns DRingSolve goal
2075/// - Otherwise returns DAxiom (SName "Error")
2076fn try_try_ring_reduce(ctx: &Context, goal: &Term) -> Option<Term> {
2077    // Normalize the goal first
2078    let norm_goal = normalize(ctx, goal);
2079
2080    // Pattern match: SApp (SApp (SApp (SName "Eq") T) a) b
2081    if let Some((type_s, left, right)) = extract_eq(&norm_goal) {
2082        // Check type is Int or Nat (ring types)
2083        if !is_ring_type(&type_s) {
2084            return Some(make_error_derivation());
2085        }
2086
2087        // Reify both sides to polynomials
2088        let poly_left = match ring::reify(&left) {
2089            Ok(p) => p,
2090            Err(_) => return Some(make_error_derivation()),
2091        };
2092        let poly_right = match ring::reify(&right) {
2093            Ok(p) => p,
2094            Err(_) => return Some(make_error_derivation()),
2095        };
2096
2097        // Check canonical equality
2098        if poly_left.canonical_eq(&poly_right) {
2099            // Success! Return DRingSolve goal
2100            return Some(Term::App(
2101                Box::new(Term::Global("DRingSolve".to_string())),
2102                Box::new(norm_goal),
2103            ));
2104        }
2105    }
2106
2107    // Failure: return error derivation
2108    Some(make_error_derivation())
2109}
2110
2111/// Verify DRingSolve proof.
2112///
2113/// DRingSolve goal → goal (if verified)
2114fn try_dring_solve_conclude(ctx: &Context, goal: &Term) -> Option<Term> {
2115    let norm_goal = normalize(ctx, goal);
2116
2117    // Extract T, lhs, rhs from Eq T lhs rhs
2118    if let Some((type_s, left, right)) = extract_eq(&norm_goal) {
2119        // Verify type is a ring type
2120        if !is_ring_type(&type_s) {
2121            return Some(make_sname_error());
2122        }
2123
2124        // Reify and verify
2125        let poly_left = match ring::reify(&left) {
2126            Ok(p) => p,
2127            Err(_) => return Some(make_sname_error()),
2128        };
2129        let poly_right = match ring::reify(&right) {
2130            Ok(p) => p,
2131            Err(_) => return Some(make_sname_error()),
2132        };
2133
2134        if poly_left.canonical_eq(&poly_right) {
2135            return Some(norm_goal);
2136        }
2137    }
2138
2139    Some(make_sname_error())
2140}
2141
2142/// Check if a Syntax type is a ring type (Int or Nat)
2143fn is_ring_type(type_term: &Term) -> bool {
2144    if let Some(name) = extract_sname_from_syntax(type_term) {
2145        return name == "Int" || name == "Nat";
2146    }
2147    false
2148}
2149
2150/// Extract name from SName term
2151fn extract_sname_from_syntax(term: &Term) -> Option<String> {
2152    if let Term::App(ctor, arg) = term {
2153        if let Term::Global(name) = ctor.as_ref() {
2154            if name == "SName" {
2155                if let Term::Lit(Literal::Text(s)) = arg.as_ref() {
2156                    return Some(s.clone());
2157                }
2158            }
2159        }
2160    }
2161    None
2162}
2163
2164// =============================================================================
2165// LIA TACTIC (LINEAR INTEGER ARITHMETIC)
2166// =============================================================================
2167
2168/// LIA tactic: try to prove a goal by Fourier-Motzkin elimination.
2169///
2170/// try_lia goal:
2171/// - If goal matches (Lt/Le/Gt/Ge a b)
2172/// - And Fourier-Motzkin shows the negation is unsatisfiable
2173/// - Returns DLiaSolve goal
2174/// - Otherwise returns DAxiom (SName "Error")
2175fn try_try_lia_reduce(ctx: &Context, goal: &Term) -> Option<Term> {
2176    // Normalize the goal first
2177    let norm_goal = normalize(ctx, goal);
2178
2179    // Extract comparison: (SApp (SApp (SName "Lt"|"Le"|etc) a) b)
2180    if let Some((rel, lhs_term, rhs_term)) = lia::extract_comparison(&norm_goal) {
2181        // Reify both sides to linear expressions
2182        let lhs = match lia::reify_linear(&lhs_term) {
2183            Ok(l) => l,
2184            Err(_) => return Some(make_error_derivation()),
2185        };
2186        let rhs = match lia::reify_linear(&rhs_term) {
2187            Ok(r) => r,
2188            Err(_) => return Some(make_error_derivation()),
2189        };
2190
2191        // Convert to negated constraint for validity checking
2192        if let Some(negated) = lia::goal_to_negated_constraint(&rel, &lhs, &rhs) {
2193            // If the negation is unsatisfiable, the goal is valid
2194            if lia::fourier_motzkin_unsat(&[negated]) {
2195                // Success! Return DLiaSolve goal
2196                return Some(Term::App(
2197                    Box::new(Term::Global("DLiaSolve".to_string())),
2198                    Box::new(norm_goal),
2199                ));
2200            }
2201        }
2202    }
2203
2204    // Failure: return error derivation
2205    Some(make_error_derivation())
2206}
2207
2208/// Verify DLiaSolve proof.
2209///
2210/// DLiaSolve goal → goal (if verified)
2211fn try_dlia_solve_conclude(ctx: &Context, goal: &Term) -> Option<Term> {
2212    let norm_goal = normalize(ctx, goal);
2213
2214    // Extract comparison and verify
2215    if let Some((rel, lhs_term, rhs_term)) = lia::extract_comparison(&norm_goal) {
2216        // Reify both sides
2217        let lhs = match lia::reify_linear(&lhs_term) {
2218            Ok(l) => l,
2219            Err(_) => return Some(make_sname_error()),
2220        };
2221        let rhs = match lia::reify_linear(&rhs_term) {
2222            Ok(r) => r,
2223            Err(_) => return Some(make_sname_error()),
2224        };
2225
2226        // Verify via Fourier-Motzkin
2227        if let Some(negated) = lia::goal_to_negated_constraint(&rel, &lhs, &rhs) {
2228            if lia::fourier_motzkin_unsat(&[negated]) {
2229                return Some(norm_goal);
2230            }
2231        }
2232    }
2233
2234    Some(make_sname_error())
2235}
2236
2237// =============================================================================
2238// CONGRUENCE CLOSURE TACTIC
2239// =============================================================================
2240
2241/// CC tactic: try to prove a goal by congruence closure.
2242///
2243/// try_cc goal:
2244/// - If goal is a direct equality (Eq a b) or an implication with hypotheses
2245/// - And congruence closure shows the conclusion follows
2246/// - Returns DccSolve goal
2247/// - Otherwise returns DAxiom (SName "Error")
2248fn try_try_cc_reduce(ctx: &Context, goal: &Term) -> Option<Term> {
2249    // Normalize the goal first
2250    let norm_goal = normalize(ctx, goal);
2251
2252    // Use cc::check_goal which handles both:
2253    // - Direct equalities: (Eq a b)
2254    // - Implications: (implies (Eq x y) (Eq (f x) (f y)))
2255    if cc::check_goal(&norm_goal) {
2256        // Success! Return DccSolve goal
2257        return Some(Term::App(
2258            Box::new(Term::Global("DccSolve".to_string())),
2259            Box::new(norm_goal),
2260        ));
2261    }
2262
2263    // Failure: return error derivation
2264    Some(make_error_derivation())
2265}
2266
2267/// Verify DccSolve proof.
2268///
2269/// DccSolve goal → goal (if verified)
2270fn try_dcc_solve_conclude(ctx: &Context, goal: &Term) -> Option<Term> {
2271    let norm_goal = normalize(ctx, goal);
2272
2273    // Re-verify using congruence closure
2274    if cc::check_goal(&norm_goal) {
2275        return Some(norm_goal);
2276    }
2277
2278    Some(make_sname_error())
2279}
2280
2281// =============================================================================
2282// SIMP TACTIC (SIMPLIFICATION)
2283// =============================================================================
2284
2285/// try_simp goal:
2286/// - Prove equalities by simplification and arithmetic evaluation
2287/// - Handles hypotheses via implications: (implies (Eq x 0) (Eq (add x 1) 1))
2288/// - Returns DSimpSolve goal on success
2289/// - Otherwise returns DAxiom (SName "Error")
2290fn try_try_simp_reduce(ctx: &Context, goal: &Term) -> Option<Term> {
2291    // Normalize the goal first
2292    let norm_goal = normalize(ctx, goal);
2293
2294    // Use simp::check_goal which handles:
2295    // - Reflexive equalities: (Eq a a)
2296    // - Constant folding: (Eq (add 2 3) 5)
2297    // - Hypothesis substitution: (implies (Eq x 0) (Eq (add x 1) 1))
2298    if simp::check_goal(&norm_goal) {
2299        // Success! Return DSimpSolve goal
2300        return Some(Term::App(
2301            Box::new(Term::Global("DSimpSolve".to_string())),
2302            Box::new(norm_goal),
2303        ));
2304    }
2305
2306    // Failure: return error derivation
2307    Some(make_error_derivation())
2308}
2309
2310/// Verify DSimpSolve proof.
2311///
2312/// DSimpSolve goal → goal (if verified)
2313fn try_dsimp_solve_conclude(ctx: &Context, goal: &Term) -> Option<Term> {
2314    let norm_goal = normalize(ctx, goal);
2315
2316    // Re-verify using simplification
2317    if simp::check_goal(&norm_goal) {
2318        return Some(norm_goal);
2319    }
2320
2321    Some(make_sname_error())
2322}
2323
2324// =============================================================================
2325// OMEGA TACTIC (TRUE INTEGER ARITHMETIC)
2326// =============================================================================
2327
2328/// try_omega goal:
2329///
2330/// Omega tactic using integer-aware Fourier-Motzkin elimination.
2331/// Unlike lia (which uses rationals), omega handles integers properly:
2332/// - x > 1 means x >= 2 (strict-to-nonstrict conversion)
2333/// - 3x <= 10 means x <= 3 (floor division)
2334///
2335/// - Extracts comparison (Lt, Le, Gt, Ge) from goal
2336/// - Reifies to integer linear expressions
2337/// - Converts to negated constraint (validity = negation is unsat)
2338/// - Applies omega test
2339/// - Returns DOmegaSolve goal on success
2340fn try_try_omega_reduce(ctx: &Context, goal: &Term) -> Option<Term> {
2341    let norm_goal = normalize(ctx, goal);
2342
2343    // Handle implications: extract hypotheses and check conclusion
2344    if let Some((hyps, conclusion)) = extract_implications(&norm_goal) {
2345        // Convert hypotheses to constraints
2346        let mut constraints = Vec::new();
2347
2348        for hyp in &hyps {
2349            // Try to extract a comparison from the hypothesis
2350            if let Some((rel, lhs_term, rhs_term)) = omega::extract_comparison(hyp) {
2351                if let (Some(lhs), Some(rhs)) =
2352                    (omega::reify_int_linear(&lhs_term), omega::reify_int_linear(&rhs_term))
2353                {
2354                    // Add hypothesis as a constraint (it's given, so it's a fact)
2355                    // For Lt(a, b): a - b < 0, i.e., (a - b) < 0
2356                    // Constraint form: (a - b + 1) <= 0 for integers (since a < b means a <= b - 1)
2357                    match rel.as_str() {
2358                        "Lt" | "lt" => {
2359                            // a < b means a - b <= -1, i.e., (a - b + 1) <= 0
2360                            let mut expr = lhs.sub(&rhs);
2361                            expr.constant += 1;
2362                            constraints.push(omega::IntConstraint { expr, strict: false });
2363                        }
2364                        "Le" | "le" => {
2365                            // a <= b means a - b <= 0
2366                            constraints.push(omega::IntConstraint {
2367                                expr: lhs.sub(&rhs),
2368                                strict: false,
2369                            });
2370                        }
2371                        "Gt" | "gt" => {
2372                            // a > b means a - b >= 1, i.e., (b - a + 1) <= 0
2373                            let mut expr = rhs.sub(&lhs);
2374                            expr.constant += 1;
2375                            constraints.push(omega::IntConstraint { expr, strict: false });
2376                        }
2377                        "Ge" | "ge" => {
2378                            // a >= b means b - a <= 0
2379                            constraints.push(omega::IntConstraint {
2380                                expr: rhs.sub(&lhs),
2381                                strict: false,
2382                            });
2383                        }
2384                        _ => {}
2385                    }
2386                }
2387            }
2388        }
2389
2390        // Now check if the conclusion is provable given the constraints
2391        if let Some((rel, lhs_term, rhs_term)) = omega::extract_comparison(&conclusion) {
2392            if let (Some(lhs), Some(rhs)) =
2393                (omega::reify_int_linear(&lhs_term), omega::reify_int_linear(&rhs_term))
2394            {
2395                // To prove the conclusion, check if its negation is unsat
2396                if let Some(neg_constraint) = omega::goal_to_negated_constraint(&rel, &lhs, &rhs) {
2397                    let mut all_constraints = constraints;
2398                    all_constraints.push(neg_constraint);
2399
2400                    if omega::omega_unsat(&all_constraints) {
2401                        return Some(Term::App(
2402                            Box::new(Term::Global("DOmegaSolve".to_string())),
2403                            Box::new(norm_goal),
2404                        ));
2405                    }
2406                }
2407            }
2408        }
2409
2410        // Failure
2411        return Some(make_error_derivation());
2412    }
2413
2414    // Direct comparison (no hypotheses)
2415    if let Some((rel, lhs_term, rhs_term)) = omega::extract_comparison(&norm_goal) {
2416        if let (Some(lhs), Some(rhs)) =
2417            (omega::reify_int_linear(&lhs_term), omega::reify_int_linear(&rhs_term))
2418        {
2419            if let Some(constraint) = omega::goal_to_negated_constraint(&rel, &lhs, &rhs) {
2420                if omega::omega_unsat(&[constraint]) {
2421                    return Some(Term::App(
2422                        Box::new(Term::Global("DOmegaSolve".to_string())),
2423                        Box::new(norm_goal),
2424                    ));
2425                }
2426            }
2427        }
2428    }
2429
2430    Some(make_error_derivation())
2431}
2432
2433/// Verify DOmegaSolve proof.
2434///
2435/// DOmegaSolve goal → goal (if verified)
2436fn try_domega_solve_conclude(ctx: &Context, goal: &Term) -> Option<Term> {
2437    let norm_goal = normalize(ctx, goal);
2438
2439    // Re-verify using omega test
2440    // Handle implications
2441    if let Some((hyps, conclusion)) = extract_implications(&norm_goal) {
2442        let mut constraints = Vec::new();
2443
2444        for hyp in &hyps {
2445            if let Some((rel, lhs_term, rhs_term)) = omega::extract_comparison(hyp) {
2446                if let (Some(lhs), Some(rhs)) =
2447                    (omega::reify_int_linear(&lhs_term), omega::reify_int_linear(&rhs_term))
2448                {
2449                    match rel.as_str() {
2450                        "Lt" | "lt" => {
2451                            let mut expr = lhs.sub(&rhs);
2452                            expr.constant += 1;
2453                            constraints.push(omega::IntConstraint { expr, strict: false });
2454                        }
2455                        "Le" | "le" => {
2456                            constraints.push(omega::IntConstraint {
2457                                expr: lhs.sub(&rhs),
2458                                strict: false,
2459                            });
2460                        }
2461                        "Gt" | "gt" => {
2462                            let mut expr = rhs.sub(&lhs);
2463                            expr.constant += 1;
2464                            constraints.push(omega::IntConstraint { expr, strict: false });
2465                        }
2466                        "Ge" | "ge" => {
2467                            constraints.push(omega::IntConstraint {
2468                                expr: rhs.sub(&lhs),
2469                                strict: false,
2470                            });
2471                        }
2472                        _ => {}
2473                    }
2474                }
2475            }
2476        }
2477
2478        if let Some((rel, lhs_term, rhs_term)) = omega::extract_comparison(&conclusion) {
2479            if let (Some(lhs), Some(rhs)) =
2480                (omega::reify_int_linear(&lhs_term), omega::reify_int_linear(&rhs_term))
2481            {
2482                if let Some(neg_constraint) = omega::goal_to_negated_constraint(&rel, &lhs, &rhs) {
2483                    let mut all_constraints = constraints;
2484                    all_constraints.push(neg_constraint);
2485
2486                    if omega::omega_unsat(&all_constraints) {
2487                        return Some(norm_goal);
2488                    }
2489                }
2490            }
2491        }
2492
2493        return Some(make_sname_error());
2494    }
2495
2496    // Direct comparison
2497    if let Some((rel, lhs_term, rhs_term)) = omega::extract_comparison(&norm_goal) {
2498        if let (Some(lhs), Some(rhs)) =
2499            (omega::reify_int_linear(&lhs_term), omega::reify_int_linear(&rhs_term))
2500        {
2501            if let Some(constraint) = omega::goal_to_negated_constraint(&rel, &lhs, &rhs) {
2502                if omega::omega_unsat(&[constraint]) {
2503                    return Some(norm_goal);
2504                }
2505            }
2506        }
2507    }
2508
2509    Some(make_sname_error())
2510}
2511
2512// =============================================================================
2513// AUTO TACTIC (THE INFINITY GAUNTLET)
2514// =============================================================================
2515
2516/// Check if a derivation is an error derivation.
2517///
2518/// Error derivations have the pattern: DAxiom (SApp (SName "Error") ...)
2519fn is_error_derivation(term: &Term) -> bool {
2520    // Check for DAxiom constructor
2521    if let Term::App(ctor, arg) = term {
2522        if let Term::Global(name) = ctor.as_ref() {
2523            if name == "DAxiom" {
2524                // Check if arg is SName "Error" or SApp (SName "Error") ...
2525                if let Term::App(sname, inner) = arg.as_ref() {
2526                    if let Term::Global(sn) = sname.as_ref() {
2527                        if sn == "SName" {
2528                            if let Term::Lit(Literal::Text(s)) = inner.as_ref() {
2529                                return s == "Error";
2530                            }
2531                        }
2532                        if sn == "SApp" {
2533                            // Recursively check - could be SApp (SName "Error") ...
2534                            return true; // For now, treat any DAxiom as potential error
2535                        }
2536                    }
2537                }
2538                // DAxiom with SName "Error"
2539                if let Term::Global(sn) = arg.as_ref() {
2540                    // This shouldn't happen but just in case
2541                    return sn == "Error";
2542                }
2543                return true; // Any DAxiom is treated as error for auto purposes
2544            }
2545        }
2546    }
2547    false
2548}
2549
2550/// Auto tactic: tries each decision procedure in sequence.
2551///
2552/// Order: True/False → simp → ring → cc → omega → lia
2553/// Returns the first successful derivation, or error if all fail.
2554// =============================================================================
2555// HARDWARE TACTICS (bitblast, tabulate, hw_auto)
2556// =============================================================================
2557
2558/// Bitblast tactic: prove Eq Bit lhs rhs by normalizing both sides.
2559///
2560/// Operates on Syntax terms: SApp(SApp(SApp(SName("Eq"), SName("Bit")), lhs), rhs)
2561/// Normalizes lhs and rhs to concrete Bit values (B0/B1) and checks equality.
2562fn try_try_bitblast_reduce(ctx: &Context, goal: &Term) -> Option<Term> {
2563    let norm_goal = normalize(ctx, goal);
2564
2565    // Extract Eq T lhs rhs from Syntax
2566    if let Some((type_s, left, right)) = extract_eq_syntax_parts(&norm_goal) {
2567        // Check type is Bit (or BVec — for future extension)
2568        if !is_bit_type(&type_s) {
2569            return Some(make_error_derivation());
2570        }
2571
2572        // Evaluate both sides using syn_eval with delta reduction support.
2573        // syn_step now handles definition unfolding (delta reduction),
2574        // so syn_eval correctly reduces expressions like
2575        // SApp(SApp(SName("bit_and"), SName("B1")), SName("B0")) → SName("B0")
2576        let fuel = 1000;
2577        let left_eval = try_syn_eval_reduce(ctx, fuel, &left)?;
2578        let right_eval = try_syn_eval_reduce(ctx, fuel, &right)?;
2579
2580        if syntax_equal(&left_eval, &right_eval) {
2581            return Some(Term::App(
2582                Box::new(Term::Global("DBitblastSolve".to_string())),
2583                Box::new(norm_goal),
2584            ));
2585        }
2586    }
2587
2588    Some(make_error_derivation())
2589}
2590
2591/// Convert a Syntax deep embedding back to a kernel Term.
2592///
2593/// This is the proper bridge between the reflected Syntax representation
2594/// and the kernel's native Term language. The kernel normalizer handles
2595/// all reduction strategies (delta, iota, beta, fix), so reifying to Term
2596/// and normalizing there gives correct results for hardware gate expressions.
2597///
2598/// Handles: SName, SApp, SLit, SVar, SLam, SPi, SSort, SMatch
2599fn syntax_to_term(syntax: &Term) -> Option<Term> {
2600    if let Term::App(ctor, inner) = syntax {
2601        if let Term::Global(name) = ctor.as_ref() {
2602            match name.as_str() {
2603                "SName" => {
2604                    if let Term::Lit(Literal::Text(s)) = inner.as_ref() {
2605                        return Some(Term::Global(s.clone()));
2606                    }
2607                }
2608                "SLit" => {
2609                    if let Term::Lit(Literal::Int(n)) = inner.as_ref() {
2610                        return Some(Term::Lit(Literal::Int(*n)));
2611                    }
2612                }
2613                "SVar" => {
2614                    if let Term::Lit(Literal::Int(n)) = inner.as_ref() {
2615                        return Some(Term::Var(format!("v{}", n)));
2616                    }
2617                }
2618                "SGlobal" => {
2619                    if let Term::Lit(Literal::Int(n)) = inner.as_ref() {
2620                        return Some(Term::Var(format!("g{}", n)));
2621                    }
2622                }
2623                _ => {}
2624            }
2625        }
2626    }
2627
2628    // Two-argument constructors: SApp, SLam, SPi
2629    if let Term::App(outer, second) = syntax {
2630        if let Term::App(sctor, first) = outer.as_ref() {
2631            if let Term::Global(name) = sctor.as_ref() {
2632                match name.as_str() {
2633                    "SApp" => {
2634                        let f = syntax_to_term(first)?;
2635                        let x = syntax_to_term(second)?;
2636                        return Some(Term::App(Box::new(f), Box::new(x)));
2637                    }
2638                    "SLam" => {
2639                        let param_type = syntax_to_term(first)?;
2640                        let body = syntax_to_term(second)?;
2641                        return Some(Term::Lambda {
2642                            param: "_".to_string(),
2643                            param_type: Box::new(param_type),
2644                            body: Box::new(body),
2645                        });
2646                    }
2647                    "SPi" => {
2648                        let param_type = syntax_to_term(first)?;
2649                        let body_type = syntax_to_term(second)?;
2650                        return Some(Term::Pi {
2651                            param: "_".to_string(),
2652                            param_type: Box::new(param_type),
2653                            body_type: Box::new(body_type),
2654                        });
2655                    }
2656                    _ => {}
2657                }
2658            }
2659        }
2660    }
2661
2662    // Three-argument: SMatch discriminant motive cases
2663    // (SApp (SApp (SApp (SName "SMatch") disc) motive) cases)
2664    if let Term::App(outer, third) = syntax {
2665        if let Term::App(mid, second) = outer.as_ref() {
2666            if let Term::App(inner, first) = mid.as_ref() {
2667                if let Term::Global(name) = inner.as_ref() {
2668                    if name == "SMatch" {
2669                        let disc = syntax_to_term(first)?;
2670                        let motive = syntax_to_term(second)?;
2671                        // cases would need list handling — skip for now
2672                        let _ = third;
2673                        return Some(Term::Match {
2674                            discriminant: Box::new(disc),
2675                            motive: Box::new(motive),
2676                            cases: vec![],
2677                        });
2678                    }
2679                }
2680            }
2681        }
2682    }
2683
2684    None
2685}
2686
2687/// Check if a Syntax type term represents Bit.
2688fn is_bit_type(term: &Term) -> bool {
2689    // SName "Bit"
2690    if let Term::App(ctor, inner) = term {
2691        if let Term::Global(name) = ctor.as_ref() {
2692            if name == "SName" {
2693                if let Term::Lit(Literal::Text(s)) = inner.as_ref() {
2694                    return s == "Bit";
2695                }
2696            }
2697        }
2698    }
2699    false
2700}
2701
2702/// Tabulate tactic: prove universally quantified Bit goals by exhaustion.
2703/// Currently a stub — will be implemented with full enumeration later.
2704fn try_try_tabulate_reduce(_ctx: &Context, _goal: &Term) -> Option<Term> {
2705    // TODO: Detect SPi(SName("Bit"), body), enumerate B0/B1, verify each
2706    Some(make_error_derivation())
2707}
2708
2709/// Verify DBitblastSolve proof by re-evaluating via syn_eval.
2710fn try_dbitblast_solve_conclude(ctx: &Context, goal: &Term) -> Option<Term> {
2711    let norm_goal = normalize(ctx, goal);
2712    if let Some((type_s, left, right)) = extract_eq_syntax_parts(&norm_goal) {
2713        if is_bit_type(&type_s) {
2714            let fuel = 1000;
2715            let left_eval = try_syn_eval_reduce(ctx, fuel, &left)?;
2716            let right_eval = try_syn_eval_reduce(ctx, fuel, &right)?;
2717            if syntax_equal(&left_eval, &right_eval) {
2718                return Some(norm_goal);
2719            }
2720        }
2721    }
2722    None
2723}
2724
2725/// Verify DTabulateSolve proof.
2726fn try_dtabulate_solve_conclude(_ctx: &Context, goal: &Term) -> Option<Term> {
2727    // TODO: Re-verify exhaustive enumeration
2728    Some(normalize(_ctx, goal))
2729}
2730
2731/// Verify DHwAutoSolve proof by re-running hw tactic chain.
2732fn try_dhw_auto_solve_conclude(ctx: &Context, goal: &Term) -> Option<Term> {
2733    // Try bitblast conclude first
2734    if let Some(result) = try_dbitblast_solve_conclude(ctx, goal) {
2735        return Some(result);
2736    }
2737    // Fall back to auto conclude
2738    try_dauto_solve_conclude(ctx, goal)
2739}
2740
2741/// Hardware auto: tries bitblast, then tabulate, then falls back to auto.
2742fn try_try_hw_auto_reduce(ctx: &Context, goal: &Term) -> Option<Term> {
2743    let norm_goal = normalize(ctx, goal);
2744
2745    // Try bitblast first (fast, for concrete Bit equalities)
2746    if let Some(result) = try_try_bitblast_reduce(ctx, &norm_goal) {
2747        if !is_error_derivation(&result) {
2748            return Some(result);
2749        }
2750    }
2751
2752    // Try tabulate (for universal Bit quantification)
2753    if let Some(result) = try_try_tabulate_reduce(ctx, &norm_goal) {
2754        if !is_error_derivation(&result) {
2755            return Some(result);
2756        }
2757    }
2758
2759    // Fall back to auto
2760    try_try_auto_reduce(ctx, &norm_goal)
2761}
2762
2763fn try_try_auto_reduce(ctx: &Context, goal: &Term) -> Option<Term> {
2764    let norm_goal = normalize(ctx, goal);
2765
2766    // Handle trivial cases: True and False
2767    // SName "True" is trivially provable
2768    if let Term::App(ctor, inner) = &norm_goal {
2769        if let Term::Global(name) = ctor.as_ref() {
2770            if name == "SName" {
2771                if let Term::Lit(Literal::Text(s)) = inner.as_ref() {
2772                    if s == "True" {
2773                        // True is always provable - use DAutoSolve
2774                        return Some(Term::App(
2775                            Box::new(Term::Global("DAutoSolve".to_string())),
2776                            Box::new(norm_goal),
2777                        ));
2778                    }
2779                    if s == "False" {
2780                        // False is never provable
2781                        return Some(make_error_derivation());
2782                    }
2783                }
2784            }
2785        }
2786    }
2787
2788    // Try simp (handles equalities with simplification)
2789    if let Some(result) = try_try_simp_reduce(ctx, &norm_goal) {
2790        if !is_error_derivation(&result) {
2791            return Some(result);
2792        }
2793    }
2794
2795    // Try ring (polynomial equalities)
2796    if let Some(result) = try_try_ring_reduce(ctx, &norm_goal) {
2797        if !is_error_derivation(&result) {
2798            return Some(result);
2799        }
2800    }
2801
2802    // Try cc (congruence closure)
2803    if let Some(result) = try_try_cc_reduce(ctx, &norm_goal) {
2804        if !is_error_derivation(&result) {
2805            return Some(result);
2806        }
2807    }
2808
2809    // Try omega (integer arithmetic - most precise)
2810    if let Some(result) = try_try_omega_reduce(ctx, &norm_goal) {
2811        if !is_error_derivation(&result) {
2812            return Some(result);
2813        }
2814    }
2815
2816    // Try lia (linear arithmetic - fallback)
2817    if let Some(result) = try_try_lia_reduce(ctx, &norm_goal) {
2818        if !is_error_derivation(&result) {
2819            return Some(result);
2820        }
2821    }
2822
2823    // Try registered hints
2824    for hint_name in ctx.get_hints() {
2825        if let Some(hint_type) = ctx.get_global(hint_name) {
2826            if let Some(result) = try_apply_hint(ctx, hint_name, hint_type, &norm_goal) {
2827                return Some(result);
2828            }
2829        }
2830    }
2831
2832    // All tactics failed
2833    Some(make_error_derivation())
2834}
2835
2836/// Verify DAutoSolve proof by re-running tactic search.
2837fn try_dauto_solve_conclude(ctx: &Context, goal: &Term) -> Option<Term> {
2838    let norm_goal = normalize(ctx, goal);
2839
2840    // Handle trivial cases: True
2841    if let Term::App(ctor, inner) = &norm_goal {
2842        if let Term::Global(name) = ctor.as_ref() {
2843            if name == "SName" {
2844                if let Term::Lit(Literal::Text(s)) = inner.as_ref() {
2845                    if s == "True" {
2846                        return Some(norm_goal.clone());
2847                    }
2848                }
2849            }
2850        }
2851    }
2852
2853    // Try each tactic - if any succeeds, the proof is valid
2854    if let Some(result) = try_try_simp_reduce(ctx, &norm_goal) {
2855        if !is_error_derivation(&result) {
2856            return Some(norm_goal.clone());
2857        }
2858    }
2859    if let Some(result) = try_try_ring_reduce(ctx, &norm_goal) {
2860        if !is_error_derivation(&result) {
2861            return Some(norm_goal.clone());
2862        }
2863    }
2864    if let Some(result) = try_try_cc_reduce(ctx, &norm_goal) {
2865        if !is_error_derivation(&result) {
2866            return Some(norm_goal.clone());
2867        }
2868    }
2869    if let Some(result) = try_try_omega_reduce(ctx, &norm_goal) {
2870        if !is_error_derivation(&result) {
2871            return Some(norm_goal.clone());
2872        }
2873    }
2874    if let Some(result) = try_try_lia_reduce(ctx, &norm_goal) {
2875        if !is_error_derivation(&result) {
2876            return Some(norm_goal.clone());
2877        }
2878    }
2879
2880    // Try registered hints
2881    for hint_name in ctx.get_hints() {
2882        if let Some(hint_type) = ctx.get_global(hint_name) {
2883            if try_apply_hint(ctx, hint_name, hint_type, &norm_goal).is_some() {
2884                return Some(norm_goal);
2885            }
2886        }
2887    }
2888
2889    Some(make_sname_error())
2890}
2891
2892// =============================================================================
2893// GENERIC INDUCTION HELPERS (induction_num_cases, induction_base_goal, etc.)
2894// =============================================================================
2895
2896/// Returns the number of constructors for an inductive type.
2897///
2898/// induction_num_cases (SName "Nat") → Succ (Succ Zero) = 2
2899/// induction_num_cases (SName "Bool") → Succ (Succ Zero) = 2
2900/// induction_num_cases (SApp (SName "List") A) → Succ (Succ Zero) = 2
2901fn try_induction_num_cases_reduce(ctx: &Context, ind_type: &Term) -> Option<Term> {
2902    // Extract inductive name from Syntax
2903    let ind_name = match extract_inductive_name_from_syntax(ind_type) {
2904        Some(name) => name,
2905        None => {
2906            // Not a valid inductive type syntax
2907            return Some(Term::Global("Zero".to_string()));
2908        }
2909    };
2910
2911    // Look up constructors
2912    let constructors = ctx.get_constructors(&ind_name);
2913    let num_ctors = constructors.len();
2914
2915    // Build Nat representation: Succ (Succ (... Zero))
2916    let mut result = Term::Global("Zero".to_string());
2917    for _ in 0..num_ctors {
2918        result = Term::App(
2919            Box::new(Term::Global("Succ".to_string())),
2920            Box::new(result),
2921        );
2922    }
2923
2924    Some(result)
2925}
2926
2927/// Returns the base case goal for induction (first constructor).
2928///
2929/// Given ind_type and motive (SLam T body), returns motive[ctor0/var].
2930fn try_induction_base_goal_reduce(
2931    ctx: &Context,
2932    ind_type: &Term,
2933    motive: &Term,
2934) -> Option<Term> {
2935    // Extract inductive name
2936    let ind_name = match extract_inductive_name_from_syntax(ind_type) {
2937        Some(name) => name,
2938        None => return Some(make_sname_error()),
2939    };
2940
2941    // Get constructors
2942    let constructors = ctx.get_constructors(&ind_name);
2943    if constructors.is_empty() {
2944        return Some(make_sname_error());
2945    }
2946
2947    // Extract motive body
2948    let motive_body = match extract_slam_body(motive) {
2949        Some(body) => body,
2950        None => return Some(make_sname_error()),
2951    };
2952
2953    // Build goal for first constructor (base case)
2954    let (ctor_name, _) = constructors[0];
2955    build_case_expected(ctx, ctor_name, &constructors, &motive_body, ind_type)
2956}
2957
2958/// Returns the goal for a specific constructor index.
2959///
2960/// Given ind_type, motive, and constructor index (as Nat), returns the case goal.
2961fn try_induction_step_goal_reduce(
2962    ctx: &Context,
2963    ind_type: &Term,
2964    motive: &Term,
2965    ctor_idx: &Term,
2966) -> Option<Term> {
2967    // Extract inductive name
2968    let ind_name = match extract_inductive_name_from_syntax(ind_type) {
2969        Some(name) => name,
2970        None => return Some(make_sname_error()),
2971    };
2972
2973    // Get constructors
2974    let constructors = ctx.get_constructors(&ind_name);
2975    if constructors.is_empty() {
2976        return Some(make_sname_error());
2977    }
2978
2979    // Convert Nat to index
2980    let idx = nat_to_usize(ctor_idx)?;
2981    if idx >= constructors.len() {
2982        return Some(make_sname_error());
2983    }
2984
2985    // Extract motive body
2986    let motive_body = match extract_slam_body(motive) {
2987        Some(body) => body,
2988        None => return Some(make_sname_error()),
2989    };
2990
2991    // Build goal for the specified constructor
2992    let (ctor_name, _) = constructors[idx];
2993    build_case_expected(ctx, ctor_name, &constructors, &motive_body, ind_type)
2994}
2995
2996/// Convert a Nat term to usize.
2997///
2998/// Zero → 0
2999/// Succ Zero → 1
3000/// Succ (Succ Zero) → 2
3001fn nat_to_usize(term: &Term) -> Option<usize> {
3002    match term {
3003        Term::Global(name) if name == "Zero" => Some(0),
3004        Term::App(succ, inner) => {
3005            if let Term::Global(name) = succ.as_ref() {
3006                if name == "Succ" {
3007                    return nat_to_usize(inner).map(|n| n + 1);
3008                }
3009            }
3010            None
3011        }
3012        _ => None,
3013    }
3014}
3015
3016/// Generic induction tactic.
3017///
3018/// try_induction ind_type motive cases → DElim ind_type motive cases
3019///
3020/// Delegates to existing DElim infrastructure after basic validation.
3021fn try_try_induction_reduce(
3022    ctx: &Context,
3023    ind_type: &Term,
3024    motive: &Term,
3025    cases: &Term,
3026) -> Option<Term> {
3027    // Extract inductive name to validate
3028    let ind_name = match extract_inductive_name_from_syntax(ind_type) {
3029        Some(name) => name,
3030        None => return Some(make_error_derivation()),
3031    };
3032
3033    // Get constructors to validate count
3034    let constructors = ctx.get_constructors(&ind_name);
3035    if constructors.is_empty() {
3036        return Some(make_error_derivation());
3037    }
3038
3039    // Extract case proofs to validate count
3040    let case_proofs = match extract_case_proofs(cases) {
3041        Some(proofs) => proofs,
3042        None => return Some(make_error_derivation()),
3043    };
3044
3045    // Verify case count matches constructor count
3046    if case_proofs.len() != constructors.len() {
3047        return Some(make_error_derivation());
3048    }
3049
3050    // Build DElim term (delegates verification to existing infrastructure)
3051    Some(Term::App(
3052        Box::new(Term::App(
3053            Box::new(Term::App(
3054                Box::new(Term::Global("DElim".to_string())),
3055                Box::new(ind_type.clone()),
3056            )),
3057            Box::new(motive.clone()),
3058        )),
3059        Box::new(cases.clone()),
3060    ))
3061}
3062
3063// -------------------------------------------------------------------------
3064// Deep Induction
3065// -------------------------------------------------------------------------
3066
3067/// DInduction reduction with verification.
3068///
3069/// DInduction motive base step → Forall Nat motive (if verified)
3070///
3071/// Verification:
3072/// 1. Extract motive body from SLam Nat body
3073/// 2. Check that concludes(base) = motive[Zero/0]
3074/// 3. Check that concludes(step) = ∀k:Nat. P(k) → P(Succ k)
3075/// 4. If all checks pass, return Forall Nat motive
3076/// 5. Otherwise, return Error
3077fn try_dinduction_reduce(
3078    ctx: &Context,
3079    motive: &Term,
3080    base: &Term,
3081    step: &Term,
3082) -> Option<Term> {
3083    // Normalize all inputs
3084    let norm_motive = normalize(ctx, motive);
3085    let norm_base = normalize(ctx, base);
3086    let norm_step = normalize(ctx, step);
3087
3088    // 1. Extract motive body (should be SLam (SName "Nat") body)
3089    let motive_body = match extract_slam_body(&norm_motive) {
3090        Some(body) => body,
3091        None => return Some(make_sname_error()),
3092    };
3093
3094    // 2. Compute expected base: motive body with Zero substituted for SVar 0
3095    let zero = make_sname("Zero");
3096    let expected_base = match try_syn_subst_reduce(ctx, &zero, 0, &motive_body) {
3097        Some(b) => b,
3098        None => return Some(make_sname_error()),
3099    };
3100
3101    // 3. Get actual base conclusion
3102    let base_conc = match try_concludes_reduce(ctx, &norm_base) {
3103        Some(c) => c,
3104        None => return Some(make_sname_error()),
3105    };
3106
3107    // 4. Verify base matches expected
3108    if !syntax_equal(&base_conc, &expected_base) {
3109        return Some(make_sname_error());
3110    }
3111
3112    // 5. Build expected step formula: ∀k:Nat. P(k) → P(Succ k)
3113    let expected_step = match build_induction_step_formula(ctx, &motive_body) {
3114        Some(s) => s,
3115        None => return Some(make_sname_error()),
3116    };
3117
3118    // 6. Get actual step conclusion
3119    let step_conc = match try_concludes_reduce(ctx, &norm_step) {
3120        Some(c) => c,
3121        None => return Some(make_sname_error()),
3122    };
3123
3124    // 7. Verify step matches expected
3125    if !syntax_equal(&step_conc, &expected_step) {
3126        return Some(make_sname_error());
3127    }
3128
3129    // 8. Return conclusion: Forall Nat motive
3130    Some(make_forall_nat_syntax(&norm_motive))
3131}
3132
3133/// Build step formula: ∀k:Nat. P(k) → P(Succ k)
3134///
3135/// Given motive body P (which uses SVar 0 for k), builds:
3136/// Forall (SName "Nat") (SLam (SName "Nat") (Implies P P[Succ(SVar 0)/SVar 0]))
3137fn build_induction_step_formula(ctx: &Context, motive_body: &Term) -> Option<Term> {
3138    // P(k) = motive_body (uses SVar 0 for k)
3139    let p_k = motive_body.clone();
3140
3141    // P(Succ k) = motive_body with (SApp (SName "Succ") (SVar 0)) substituted
3142    let succ_var = Term::App(
3143        Box::new(Term::App(
3144            Box::new(Term::Global("SApp".to_string())),
3145            Box::new(make_sname("Succ")),
3146        )),
3147        Box::new(Term::App(
3148            Box::new(Term::Global("SVar".to_string())),
3149            Box::new(Term::Lit(Literal::Int(0))),
3150        )),
3151    );
3152    let p_succ_k = try_syn_subst_reduce(ctx, &succ_var, 0, motive_body)?;
3153
3154    // Implies P(k) P(Succ k)
3155    let implies_body = make_implies_syntax(&p_k, &p_succ_k);
3156
3157    // SLam (SName "Nat") implies_body
3158    let slam = Term::App(
3159        Box::new(Term::App(
3160            Box::new(Term::Global("SLam".to_string())),
3161            Box::new(make_sname("Nat")),
3162        )),
3163        Box::new(implies_body),
3164    );
3165
3166    // Forall (SName "Nat") slam
3167    Some(make_forall_syntax_with_type(&make_sname("Nat"), &slam))
3168}
3169
3170/// Build SApp (SApp (SName "Implies") a) b
3171fn make_implies_syntax(a: &Term, b: &Term) -> Term {
3172    // SApp (SName "Implies") a
3173    let app1 = Term::App(
3174        Box::new(Term::App(
3175            Box::new(Term::Global("SApp".to_string())),
3176            Box::new(make_sname("Implies")),
3177        )),
3178        Box::new(a.clone()),
3179    );
3180
3181    // SApp (SApp (SName "Implies") a) b
3182    Term::App(
3183        Box::new(Term::App(
3184            Box::new(Term::Global("SApp".to_string())),
3185            Box::new(app1),
3186        )),
3187        Box::new(b.clone()),
3188    )
3189}
3190
3191/// Build SApp (SApp (SName "Forall") (SName "Nat")) motive
3192fn make_forall_nat_syntax(motive: &Term) -> Term {
3193    make_forall_syntax_with_type(&make_sname("Nat"), motive)
3194}
3195
3196/// Build SApp (SApp (SName "Forall") type_s) body
3197fn make_forall_syntax_with_type(type_s: &Term, body: &Term) -> Term {
3198    // SApp (SName "Forall") type_s
3199    let app1 = Term::App(
3200        Box::new(Term::App(
3201            Box::new(Term::Global("SApp".to_string())),
3202            Box::new(make_sname("Forall")),
3203        )),
3204        Box::new(type_s.clone()),
3205    );
3206
3207    // SApp (SApp (SName "Forall") type_s) body
3208    Term::App(
3209        Box::new(Term::App(
3210            Box::new(Term::Global("SApp".to_string())),
3211            Box::new(app1),
3212        )),
3213        Box::new(body.clone()),
3214    )
3215}
3216
3217// -------------------------------------------------------------------------
3218// Solver (Computational Reflection)
3219// -------------------------------------------------------------------------
3220
3221/// DCompute reduction with verification.
3222///
3223/// DCompute goal → goal (if verified by computation)
3224///
3225/// Verification:
3226/// 1. Check that goal is (Eq T A B) as Syntax
3227/// 2. Evaluate A and B using syn_eval with bounded fuel
3228/// 3. If eval(A) == eval(B), return goal
3229/// 4. Otherwise, return Error
3230fn try_dcompute_conclude(ctx: &Context, goal: &Term) -> Option<Term> {
3231    let norm_goal = normalize(ctx, goal);
3232
3233    // Extract T, A, B from Eq T A B (as Syntax)
3234    // Pattern: SApp (SApp (SApp (SName "Eq") T) A) B
3235    let parts = extract_eq_syntax_parts(&norm_goal);
3236    if parts.is_none() {
3237        // Goal is not an equality - return Error
3238        return Some(make_sname_error());
3239    }
3240    let (_, a, b) = parts.unwrap();
3241
3242    // Evaluate A and B with generous fuel
3243    let fuel = 1000;
3244    let a_eval = match try_syn_eval_reduce(ctx, fuel, &a) {
3245        Some(e) => e,
3246        None => return Some(make_sname_error()),
3247    };
3248    let b_eval = match try_syn_eval_reduce(ctx, fuel, &b) {
3249        Some(e) => e,
3250        None => return Some(make_sname_error()),
3251    };
3252
3253    // Compare normalized results
3254    if syntax_equal(&a_eval, &b_eval) {
3255        Some(norm_goal)
3256    } else {
3257        Some(make_sname_error())
3258    }
3259}
3260
3261/// Extract T, A, B from Eq T A B (as Syntax)
3262///
3263/// Pattern: SApp (SApp (SApp (SName "Eq") T) A) B
3264fn extract_eq_syntax_parts(term: &Term) -> Option<(Term, Term, Term)> {
3265    // term = SApp X B where X = SApp Y A where Y = SApp (SName "Eq") T
3266    // Structure: App(App(SApp, App(App(SApp, App(App(SApp, App(SName, "Eq")), T)), A)), B)
3267    if let Term::App(partial2, b) = term {
3268        if let Term::App(sapp2, inner2) = partial2.as_ref() {
3269            if let Term::Global(sapp2_name) = sapp2.as_ref() {
3270                if sapp2_name != "SApp" {
3271                    return None;
3272                }
3273            } else {
3274                return None;
3275            }
3276
3277            if let Term::App(partial1, a) = inner2.as_ref() {
3278                if let Term::App(sapp1, inner1) = partial1.as_ref() {
3279                    if let Term::Global(sapp1_name) = sapp1.as_ref() {
3280                        if sapp1_name != "SApp" {
3281                            return None;
3282                        }
3283                    } else {
3284                        return None;
3285                    }
3286
3287                    if let Term::App(eq_t, t) = inner1.as_ref() {
3288                        if let Term::App(sapp0, eq_sname) = eq_t.as_ref() {
3289                            if let Term::Global(sapp0_name) = sapp0.as_ref() {
3290                                if sapp0_name != "SApp" {
3291                                    return None;
3292                                }
3293                            } else {
3294                                return None;
3295                            }
3296
3297                            // Check if eq_sname is SName "Eq"
3298                            if let Term::App(sname_ctor, eq_str) = eq_sname.as_ref() {
3299                                if let Term::Global(ctor) = sname_ctor.as_ref() {
3300                                    if ctor == "SName" {
3301                                        if let Term::Lit(Literal::Text(s)) = eq_str.as_ref() {
3302                                            if s == "Eq" {
3303                                                return Some((
3304                                                    t.as_ref().clone(),
3305                                                    a.as_ref().clone(),
3306                                                    b.as_ref().clone(),
3307                                                ));
3308                                            }
3309                                        }
3310                                    }
3311                                }
3312                            }
3313                        }
3314                    }
3315                }
3316            }
3317        }
3318    }
3319    None
3320}
3321
3322// -------------------------------------------------------------------------
3323// Tactic Combinators
3324// -------------------------------------------------------------------------
3325
3326/// Reduce tact_orelse t1 t2 goal
3327///
3328/// - Apply t1 to goal
3329/// - If concludes returns Error, apply t2 to goal
3330/// - Otherwise return t1's result
3331fn try_tact_orelse_reduce(
3332    ctx: &Context,
3333    t1: &Term,
3334    t2: &Term,
3335    goal: &Term,
3336) -> Option<Term> {
3337    let norm_goal = normalize(ctx, goal);
3338
3339    // Apply t1 to goal
3340    let d1_app = Term::App(Box::new(t1.clone()), Box::new(norm_goal.clone()));
3341    let d1 = normalize(ctx, &d1_app);
3342
3343    // Check if t1 succeeded by looking at concludes
3344    if let Some(conc1) = try_concludes_reduce(ctx, &d1) {
3345        if is_error_syntax(&conc1) {
3346            // t1 failed, try t2
3347            let d2_app = Term::App(Box::new(t2.clone()), Box::new(norm_goal));
3348            return Some(normalize(ctx, &d2_app));
3349        } else {
3350            // t1 succeeded
3351            return Some(d1);
3352        }
3353    }
3354
3355    // Couldn't evaluate concludes - return error
3356    Some(make_error_derivation())
3357}
3358
3359/// Check if a Syntax term is SName "Error"
3360fn is_error_syntax(term: &Term) -> bool {
3361    // Pattern: SName "Error" = App(Global("SName"), Lit(Text("Error")))
3362    if let Term::App(ctor, arg) = term {
3363        if let Term::Global(name) = ctor.as_ref() {
3364            if name == "SName" {
3365                if let Term::Lit(Literal::Text(s)) = arg.as_ref() {
3366                    return s == "Error";
3367                }
3368            }
3369        }
3370    }
3371    false
3372}
3373
3374/// Reduce tact_try t goal
3375///
3376/// - Apply t to goal
3377/// - If concludes returns Error, return identity (DAxiom goal)
3378/// - Otherwise return t's result
3379fn try_tact_try_reduce(ctx: &Context, t: &Term, goal: &Term) -> Option<Term> {
3380    let norm_goal = normalize(ctx, goal);
3381
3382    // Apply t to goal
3383    let d_app = Term::App(Box::new(t.clone()), Box::new(norm_goal.clone()));
3384    let d = normalize(ctx, &d_app);
3385
3386    // Check if t succeeded by looking at concludes
3387    if let Some(conc) = try_concludes_reduce(ctx, &d) {
3388        if is_error_syntax(&conc) {
3389            // t failed, return identity (DAxiom goal)
3390            return Some(make_daxiom(&norm_goal));
3391        } else {
3392            // t succeeded
3393            return Some(d);
3394        }
3395    }
3396
3397    // Couldn't evaluate concludes - return identity
3398    Some(make_daxiom(&norm_goal))
3399}
3400
3401/// Reduce tact_repeat t goal
3402///
3403/// Apply t repeatedly until it fails or makes no progress.
3404/// Returns the accumulated derivation or identity if first application fails.
3405fn try_tact_repeat_reduce(ctx: &Context, t: &Term, goal: &Term) -> Option<Term> {
3406    const MAX_ITERATIONS: usize = 100;
3407
3408    let norm_goal = normalize(ctx, goal);
3409    let mut current_goal = norm_goal.clone();
3410    let mut last_successful_deriv: Option<Term> = None;
3411
3412    for _ in 0..MAX_ITERATIONS {
3413        // Apply t to current goal
3414        let d_app = Term::App(Box::new(t.clone()), Box::new(current_goal.clone()));
3415        let d = normalize(ctx, &d_app);
3416
3417        // Check result
3418        if let Some(conc) = try_concludes_reduce(ctx, &d) {
3419            if is_error_syntax(&conc) {
3420                // Tactic failed - stop and return what we have
3421                break;
3422            }
3423
3424            // Check for no-progress (fixed point)
3425            if syntax_equal(&conc, &current_goal) {
3426                // No progress made - stop
3427                break;
3428            }
3429
3430            // Progress made - continue
3431            current_goal = conc;
3432            last_successful_deriv = Some(d);
3433        } else {
3434            // Couldn't evaluate concludes - stop
3435            break;
3436        }
3437    }
3438
3439    // Return final derivation or identity
3440    last_successful_deriv.or_else(|| Some(make_daxiom(&norm_goal)))
3441}
3442
3443/// Reduce tact_then t1 t2 goal
3444///
3445/// - Apply t1 to goal
3446/// - If t1 fails, return Error
3447/// - Otherwise apply t2 to the result of t1
3448fn try_tact_then_reduce(
3449    ctx: &Context,
3450    t1: &Term,
3451    t2: &Term,
3452    goal: &Term,
3453) -> Option<Term> {
3454    let norm_goal = normalize(ctx, goal);
3455
3456    // Apply t1 to goal
3457    let d1_app = Term::App(Box::new(t1.clone()), Box::new(norm_goal.clone()));
3458    let d1 = normalize(ctx, &d1_app);
3459
3460    // Check if t1 succeeded
3461    if let Some(conc1) = try_concludes_reduce(ctx, &d1) {
3462        if is_error_syntax(&conc1) {
3463            // t1 failed
3464            return Some(make_error_derivation());
3465        }
3466
3467        // t1 succeeded - apply t2 to the new goal (conc1)
3468        let d2_app = Term::App(Box::new(t2.clone()), Box::new(conc1));
3469        let d2 = normalize(ctx, &d2_app);
3470
3471        // The result is d2 (which may succeed or fail)
3472        return Some(d2);
3473    }
3474
3475    // Couldn't evaluate concludes - return error
3476    Some(make_error_derivation())
3477}
3478
3479/// Reduce tact_first tactics goal
3480///
3481/// Try each tactic in the list until one succeeds.
3482/// Returns Error if all fail or list is empty.
3483fn try_tact_first_reduce(ctx: &Context, tactics: &Term, goal: &Term) -> Option<Term> {
3484    let norm_goal = normalize(ctx, goal);
3485
3486    // Extract tactics from TList
3487    let tactic_vec = extract_tlist(tactics)?;
3488
3489    for tactic in tactic_vec {
3490        // Apply this tactic to goal
3491        let d_app = Term::App(Box::new(tactic), Box::new(norm_goal.clone()));
3492        let d = normalize(ctx, &d_app);
3493
3494        // Check if it succeeded
3495        if let Some(conc) = try_concludes_reduce(ctx, &d) {
3496            if !is_error_syntax(&conc) {
3497                // Success!
3498                return Some(d);
3499            }
3500            // Failed - try next
3501        }
3502    }
3503
3504    // All failed
3505    Some(make_error_derivation())
3506}
3507
3508/// Extract elements from a TList term
3509///
3510/// TList is polymorphic: TNil A and TCons A h t
3511/// So the structure is:
3512/// - TNil A = App(Global("TNil"), type)
3513/// - TCons A h t = App(App(App(Global("TCons"), type), head), tail)
3514fn extract_tlist(term: &Term) -> Option<Vec<Term>> {
3515    let mut result = Vec::new();
3516    let mut current = term.clone();
3517
3518    loop {
3519        match &current {
3520            // TNil A = App(Global("TNil"), type)
3521            Term::App(tnil, _type) => {
3522                if let Term::Global(name) = tnil.as_ref() {
3523                    if name == "TNil" {
3524                        // Empty list
3525                        break;
3526                    }
3527                }
3528                // Try TCons A h t = App(App(App(Global("TCons"), type), head), tail)
3529                if let Term::App(partial2, tail) = &current {
3530                    if let Term::App(partial1, head) = partial2.as_ref() {
3531                        if let Term::App(tcons, _type) = partial1.as_ref() {
3532                            if let Term::Global(name) = tcons.as_ref() {
3533                                if name == "TCons" {
3534                                    result.push(head.as_ref().clone());
3535                                    current = tail.as_ref().clone();
3536                                    continue;
3537                                }
3538                            }
3539                        }
3540                    }
3541                }
3542                // Not a valid TList structure
3543                return None;
3544            }
3545            // Bare Global("TNil") without type argument - also valid
3546            Term::Global(name) if name == "TNil" => {
3547                break;
3548            }
3549            _ => {
3550                // Not a valid TList
3551                return None;
3552            }
3553        }
3554    }
3555
3556    Some(result)
3557}
3558
3559/// Reduce tact_solve t goal
3560///
3561/// - Apply t to goal
3562/// - If t fails (Error), return Error
3563/// - If t succeeds, return its result
3564fn try_tact_solve_reduce(ctx: &Context, t: &Term, goal: &Term) -> Option<Term> {
3565    let norm_goal = normalize(ctx, goal);
3566
3567    // Apply t to goal
3568    let d_app = Term::App(Box::new(t.clone()), Box::new(norm_goal.clone()));
3569    let d = normalize(ctx, &d_app);
3570
3571    // Check if t succeeded
3572    if let Some(conc) = try_concludes_reduce(ctx, &d) {
3573        if is_error_syntax(&conc) {
3574            // t failed
3575            return Some(make_error_derivation());
3576        }
3577        // t succeeded - return its derivation
3578        return Some(d);
3579    }
3580
3581    // Couldn't evaluate concludes - return error
3582    Some(make_error_derivation())
3583}
3584
3585// -------------------------------------------------------------------------
3586// Congruence Closure
3587// -------------------------------------------------------------------------
3588
3589/// Validate DCong proof by congruence.
3590///
3591/// DCong context eq_proof where:
3592/// - context is SLam param_type body
3593/// - eq_proof proves Eq T a b
3594/// Returns: Eq param_type (body[0:=a]) (body[0:=b])
3595fn try_dcong_conclude(ctx: &Context, context: &Term, eq_proof: &Term) -> Option<Term> {
3596    // Get the conclusion of the equality proof
3597    let eq_conc = try_concludes_reduce(ctx, eq_proof)?;
3598
3599    // Extract T, a, b from Eq T a b
3600    let parts = extract_eq_syntax_parts(&eq_conc);
3601    if parts.is_none() {
3602        // Not an equality proof
3603        return Some(make_sname_error());
3604    }
3605    let (_type_term, lhs, rhs) = parts.unwrap();
3606
3607    // Normalize context and check it's a lambda
3608    let norm_context = normalize(ctx, context);
3609
3610    // Extract (param_type, body) from SLam param_type body
3611    let slam_parts = extract_slam_parts(&norm_context);
3612    if slam_parts.is_none() {
3613        // Not a lambda context
3614        return Some(make_sname_error());
3615    }
3616    let (param_type, body) = slam_parts.unwrap();
3617
3618    // Substitute lhs and rhs into body at index 0
3619    let fa = try_syn_subst_reduce(ctx, &lhs, 0, &body)?;
3620    let fb = try_syn_subst_reduce(ctx, &rhs, 0, &body)?;
3621
3622    // Build result: Eq param_type fa fb
3623    Some(make_eq_syntax_three(&param_type, &fa, &fb))
3624}
3625
3626/// Extract (param_type, body) from SLam param_type body
3627///
3628/// Pattern: App(App(Global("SLam"), param_type), body)
3629fn extract_slam_parts(term: &Term) -> Option<(Term, Term)> {
3630    if let Term::App(inner, body) = term {
3631        if let Term::App(slam_ctor, param_type) = inner.as_ref() {
3632            if let Term::Global(name) = slam_ctor.as_ref() {
3633                if name == "SLam" {
3634                    return Some((param_type.as_ref().clone(), body.as_ref().clone()));
3635                }
3636            }
3637        }
3638    }
3639    None
3640}
3641
3642/// Build SApp (SApp (SApp (SName "Eq") type_s) a) b
3643///
3644/// Constructs the Syntax representation of (Eq type_s a b)
3645fn make_eq_syntax_three(type_s: &Term, a: &Term, b: &Term) -> Term {
3646    let eq_name = Term::App(
3647        Box::new(Term::Global("SName".to_string())),
3648        Box::new(Term::Lit(Literal::Text("Eq".to_string()))),
3649    );
3650
3651    // SApp (SName "Eq") type_s
3652    let app1 = Term::App(
3653        Box::new(Term::App(
3654            Box::new(Term::Global("SApp".to_string())),
3655            Box::new(eq_name),
3656        )),
3657        Box::new(type_s.clone()),
3658    );
3659
3660    // SApp (SApp (SName "Eq") type_s) a
3661    let app2 = Term::App(
3662        Box::new(Term::App(
3663            Box::new(Term::Global("SApp".to_string())),
3664            Box::new(app1),
3665        )),
3666        Box::new(a.clone()),
3667    );
3668
3669    // SApp (SApp (SApp (SName "Eq") type_s) a) b
3670    Term::App(
3671        Box::new(Term::App(
3672            Box::new(Term::Global("SApp".to_string())),
3673            Box::new(app2),
3674        )),
3675        Box::new(b.clone()),
3676    )
3677}
3678
3679// -------------------------------------------------------------------------
3680// Generic Elimination
3681// -------------------------------------------------------------------------
3682
3683/// DElim reduction with verification.
3684///
3685/// DElim ind_type motive cases → Forall ind_type motive (if verified)
3686///
3687/// Verification:
3688/// 1. Extract inductive name from ind_type Syntax
3689/// 2. Look up constructors for that inductive
3690/// 3. Extract case proofs from DCase chain
3691/// 4. Verify case count matches constructor count
3692/// 5. For each constructor, verify case conclusion matches expected
3693/// 6. Return Forall ind_type motive
3694fn try_delim_conclude(
3695    ctx: &Context,
3696    ind_type: &Term,
3697    motive: &Term,
3698    cases: &Term,
3699) -> Option<Term> {
3700    // Normalize inputs
3701    let norm_ind_type = normalize(ctx, ind_type);
3702    let norm_motive = normalize(ctx, motive);
3703    let norm_cases = normalize(ctx, cases);
3704
3705    // 1. Extract inductive name from Syntax
3706    let ind_name = match extract_inductive_name_from_syntax(&norm_ind_type) {
3707        Some(name) => name,
3708        None => return Some(make_sname_error()),
3709    };
3710
3711    // 2. Look up constructors for this inductive
3712    let constructors = ctx.get_constructors(&ind_name);
3713    if constructors.is_empty() {
3714        // Unknown inductive type
3715        return Some(make_sname_error());
3716    }
3717
3718    // 3. Extract case proofs from DCase chain
3719    let case_proofs = match extract_case_proofs(&norm_cases) {
3720        Some(proofs) => proofs,
3721        None => return Some(make_sname_error()),
3722    };
3723
3724    // 4. Verify case count matches constructor count
3725    if case_proofs.len() != constructors.len() {
3726        return Some(make_sname_error());
3727    }
3728
3729    // 5. Extract motive body (should be SLam param_type body)
3730    let motive_body = match extract_slam_body(&norm_motive) {
3731        Some(body) => body,
3732        None => return Some(make_sname_error()),
3733    };
3734
3735    // 6. For each constructor, verify case conclusion matches expected
3736    for (i, (ctor_name, _ctor_type)) in constructors.iter().enumerate() {
3737        let case_proof = &case_proofs[i];
3738
3739        // Get actual conclusion of this case proof
3740        let case_conc = match try_concludes_reduce(ctx, case_proof) {
3741            Some(c) => c,
3742            None => return Some(make_sname_error()),
3743        };
3744
3745        // Build expected conclusion based on constructor
3746        // For base case (0-ary constructor): motive[ctor/var]
3747        // For step case (recursive constructor): requires IH pattern
3748        let expected = match build_case_expected(ctx, ctor_name, &constructors, &motive_body, &norm_ind_type) {
3749            Some(e) => e,
3750            None => return Some(make_sname_error()),
3751        };
3752
3753        // Verify conclusion matches expected
3754        if !syntax_equal(&case_conc, &expected) {
3755            return Some(make_sname_error());
3756        }
3757    }
3758
3759    // 7. Return conclusion: Forall ind_type motive
3760    Some(make_forall_syntax_generic(&norm_ind_type, &norm_motive))
3761}
3762
3763/// Extract inductive name from Syntax term.
3764///
3765/// Handles:
3766/// - SName "Nat" → "Nat"
3767/// - SApp (SName "List") A → "List"
3768fn extract_inductive_name_from_syntax(term: &Term) -> Option<String> {
3769    // Case 1: SName "X"
3770    if let Term::App(sname, text) = term {
3771        if let Term::Global(ctor) = sname.as_ref() {
3772            if ctor == "SName" {
3773                if let Term::Lit(Literal::Text(name)) = text.as_ref() {
3774                    return Some(name.clone());
3775                }
3776            }
3777        }
3778    }
3779
3780    // Case 2: SApp (SName "X") args → extract "X" from the function position
3781    if let Term::App(inner, _arg) = term {
3782        if let Term::App(sapp, func) = inner.as_ref() {
3783            if let Term::Global(ctor) = sapp.as_ref() {
3784                if ctor == "SApp" {
3785                    // Recursively extract from the function
3786                    return extract_inductive_name_from_syntax(func);
3787                }
3788            }
3789        }
3790    }
3791
3792    None
3793}
3794
3795/// Extract case proofs from DCase chain.
3796///
3797/// DCase p1 (DCase p2 DCaseEnd) → [p1, p2]
3798fn extract_case_proofs(term: &Term) -> Option<Vec<Term>> {
3799    let mut proofs = Vec::new();
3800    let mut current = term;
3801
3802    loop {
3803        // DCaseEnd - end of list
3804        if let Term::Global(name) = current {
3805            if name == "DCaseEnd" {
3806                return Some(proofs);
3807            }
3808        }
3809
3810        // DCase head tail - Pattern: App(App(DCase, head), tail)
3811        if let Term::App(inner, tail) = current {
3812            if let Term::App(dcase, head) = inner.as_ref() {
3813                if let Term::Global(name) = dcase.as_ref() {
3814                    if name == "DCase" {
3815                        proofs.push(head.as_ref().clone());
3816                        current = tail.as_ref();
3817                        continue;
3818                    }
3819                }
3820            }
3821        }
3822
3823        // Unrecognized structure
3824        return None;
3825    }
3826}
3827
3828/// Build expected case conclusion for a constructor.
3829///
3830/// For base case constructors (no recursive args): motive[ctor/var]
3831/// For recursive constructors: ∀args. IH → motive[ctor args/var]
3832fn build_case_expected(
3833    ctx: &Context,
3834    ctor_name: &str,
3835    _constructors: &[(&str, &Term)],
3836    motive_body: &Term,
3837    ind_type: &Term,
3838) -> Option<Term> {
3839    // Extract inductive name to determine constructor patterns
3840    let ind_name = extract_inductive_name_from_syntax(ind_type)?;
3841
3842    // Special case for Nat - we know its structure
3843    if ind_name == "Nat" {
3844        if ctor_name == "Zero" {
3845            // Base case: motive[Zero/var]
3846            let zero = make_sname("Zero");
3847            return try_syn_subst_reduce(ctx, &zero, 0, motive_body);
3848        } else if ctor_name == "Succ" {
3849            // Step case: ∀k:Nat. P(k) → P(Succ k)
3850            // Use the same logic as DInduction
3851            return build_induction_step_formula(ctx, motive_body);
3852        }
3853    }
3854
3855    // For other inductives, use heuristic based on constructor type
3856    // Build the constructor as Syntax: SName "CtorName"
3857    let ctor_syntax = make_sname(ctor_name);
3858
3859    // For polymorphic types, we need to apply the type argument to the constructor
3860    // e.g., for List A, Nil becomes (SApp (SName "Nil") A)
3861    let ctor_applied = apply_type_args_to_ctor(&ctor_syntax, ind_type);
3862
3863    // Get constructor type from context to determine if it's recursive
3864    if let Some(ctor_ty) = ctx.get_global(ctor_name) {
3865        // Check if constructor type contains the inductive type (recursive)
3866        if is_recursive_constructor(ctx, ctor_ty, &ind_name, ind_type) {
3867            // For recursive constructors, build the IH pattern
3868            return build_recursive_case_formula(ctx, ctor_name, ctor_ty, motive_body, ind_type, &ind_name);
3869        }
3870    }
3871
3872    // Simple base case: substitute ctor into motive body
3873    try_syn_subst_reduce(ctx, &ctor_applied, 0, motive_body)
3874}
3875
3876/// Apply type arguments from ind_type to a constructor.
3877///
3878/// If ind_type = SApp (SName "List") A, and ctor = SName "Nil",
3879/// result = SApp (SName "Nil") A
3880fn apply_type_args_to_ctor(ctor: &Term, ind_type: &Term) -> Term {
3881    // Extract type arguments from ind_type
3882    let args = extract_type_args(ind_type);
3883
3884    if args.is_empty() {
3885        return ctor.clone();
3886    }
3887
3888    // Apply each arg: SApp (... (SApp ctor arg1) ...) argN
3889    args.iter().fold(ctor.clone(), |acc, arg| {
3890        Term::App(
3891            Box::new(Term::App(
3892                Box::new(Term::Global("SApp".to_string())),
3893                Box::new(acc),
3894            )),
3895            Box::new(arg.clone()),
3896        )
3897    })
3898}
3899
3900/// Extract type arguments from polymorphic Syntax.
3901///
3902/// SApp (SApp (SName "Either") A) B → [A, B]
3903/// SApp (SName "List") A → [A]
3904/// SName "Nat" → []
3905fn extract_type_args(term: &Term) -> Vec<Term> {
3906    let mut args = Vec::new();
3907    let mut current = term;
3908
3909    // Traverse SApp chain from outside in
3910    loop {
3911        if let Term::App(inner, arg) = current {
3912            if let Term::App(sapp, func) = inner.as_ref() {
3913                if let Term::Global(ctor) = sapp.as_ref() {
3914                    if ctor == "SApp" {
3915                        args.push(arg.as_ref().clone());
3916                        current = func.as_ref();
3917                        continue;
3918                    }
3919                }
3920            }
3921        }
3922        break;
3923    }
3924
3925    // Reverse because we collected outside-in but want inside-out
3926    args.reverse();
3927    args
3928}
3929
3930/// Build Forall Syntax for generic inductive type.
3931///
3932/// Forall ind_type motive = SApp (SApp (SName "Forall") ind_type) motive
3933fn make_forall_syntax_generic(ind_type: &Term, motive: &Term) -> Term {
3934    // SApp (SName "Forall") ind_type
3935    let forall_type = Term::App(
3936        Box::new(Term::App(
3937            Box::new(Term::Global("SApp".to_string())),
3938            Box::new(make_sname("Forall")),
3939        )),
3940        Box::new(ind_type.clone()),
3941    );
3942
3943    // SApp forall_type motive
3944    Term::App(
3945        Box::new(Term::App(
3946            Box::new(Term::Global("SApp".to_string())),
3947            Box::new(forall_type),
3948        )),
3949        Box::new(motive.clone()),
3950    )
3951}
3952
3953/// Check if a constructor is recursive (has arguments of the inductive type).
3954fn is_recursive_constructor(
3955    _ctx: &Context,
3956    ctor_ty: &Term,
3957    ind_name: &str,
3958    _ind_type: &Term,
3959) -> bool {
3960    // Traverse the constructor type looking for the inductive type in argument positions
3961    // For Cons : Π(A:Type). A -> List A -> List A
3962    // The "List A" argument makes it recursive
3963
3964    fn contains_inductive(term: &Term, ind_name: &str) -> bool {
3965        match term {
3966            Term::Global(name) => name == ind_name,
3967            Term::App(f, a) => {
3968                contains_inductive(f, ind_name) || contains_inductive(a, ind_name)
3969            }
3970            Term::Pi { param_type, body_type, .. } => {
3971                contains_inductive(param_type, ind_name) || contains_inductive(body_type, ind_name)
3972            }
3973            Term::Lambda { param_type, body, .. } => {
3974                contains_inductive(param_type, ind_name) || contains_inductive(body, ind_name)
3975            }
3976            _ => false,
3977        }
3978    }
3979
3980    // Check if any parameter type (not the final result) contains the inductive
3981    fn check_params(term: &Term, ind_name: &str) -> bool {
3982        match term {
3983            Term::Pi { param_type, body_type, .. } => {
3984                // Check if this parameter has the inductive type
3985                if contains_inductive(param_type, ind_name) {
3986                    return true;
3987                }
3988                // Check remaining parameters
3989                check_params(body_type, ind_name)
3990            }
3991            _ => false,
3992        }
3993    }
3994
3995    check_params(ctor_ty, ind_name)
3996}
3997
3998/// Build the case formula for a recursive constructor.
3999///
4000/// For Cons : Π(A:Type). A -> List A -> List A
4001/// with motive P : List A -> Prop
4002/// Expected case: ∀x:A. ∀xs:List A. P(xs) -> P(Cons A x xs)
4003fn build_recursive_case_formula(
4004    ctx: &Context,
4005    ctor_name: &str,
4006    ctor_ty: &Term,
4007    motive_body: &Term,
4008    ind_type: &Term,
4009    ind_name: &str,
4010) -> Option<Term> {
4011    // Extract type args from ind_type for matching
4012    let type_args = extract_type_args(ind_type);
4013
4014    // Collect constructor arguments (skipping type parameters)
4015    let args = collect_ctor_args(ctor_ty, ind_name, &type_args);
4016
4017    if args.is_empty() {
4018        // No non-type arguments, treat as base case
4019        let ctor_applied = apply_type_args_to_ctor(&make_sname(ctor_name), ind_type);
4020        return try_syn_subst_reduce(ctx, &ctor_applied, 0, motive_body);
4021    }
4022
4023    // Build from inside out:
4024    // 1. Build ctor application: Cons A x xs (with de Bruijn indices for args)
4025    // 2. Build P(ctor args): motive_body[ctor args/var]
4026    // 3. For each recursive arg, wrap with IH: P(xs) ->
4027    // 4. For each arg, wrap with forall: ∀xs:List A.
4028
4029    // Build constructor application with de Bruijn indices
4030    let mut ctor_app = apply_type_args_to_ctor(&make_sname(ctor_name), ind_type);
4031    for (i, _) in args.iter().enumerate() {
4032        // Index from end: last arg is index 0, second-to-last is 1, etc.
4033        let idx = (args.len() - 1 - i) as i64;
4034        let var = Term::App(
4035            Box::new(Term::Global("SVar".to_string())),
4036            Box::new(Term::Lit(Literal::Int(idx))),
4037        );
4038        ctor_app = Term::App(
4039            Box::new(Term::App(
4040                Box::new(Term::Global("SApp".to_string())),
4041                Box::new(ctor_app),
4042            )),
4043            Box::new(var),
4044        );
4045    }
4046
4047    // P(ctor args) - substitute ctor_app into motive
4048    let p_ctor = try_syn_subst_reduce(ctx, &ctor_app, 0, motive_body)?;
4049
4050    // Build implications from inside out (for recursive args)
4051    let mut body = p_ctor;
4052    for (i, (arg_ty, is_recursive)) in args.iter().enumerate().rev() {
4053        if *is_recursive {
4054            // Add IH: P(arg) -> body
4055            // arg is at index (args.len() - 1 - i)
4056            let idx = (args.len() - 1 - i) as i64;
4057            let var = Term::App(
4058                Box::new(Term::Global("SVar".to_string())),
4059                Box::new(Term::Lit(Literal::Int(idx))),
4060            );
4061            let p_arg = try_syn_subst_reduce(ctx, &var, 0, motive_body)?;
4062            body = make_implies_syntax(&p_arg, &body);
4063        }
4064        // Skip non-recursive args in the implication chain
4065        let _ = (i, arg_ty); // suppress unused warning
4066    }
4067
4068    // Wrap with foralls from inside out
4069    for (arg_ty, _) in args.iter().rev() {
4070        // SLam arg_ty body
4071        let slam = Term::App(
4072            Box::new(Term::App(
4073                Box::new(Term::Global("SLam".to_string())),
4074                Box::new(arg_ty.clone()),
4075            )),
4076            Box::new(body.clone()),
4077        );
4078        // Forall arg_ty slam
4079        body = make_forall_syntax_with_type(arg_ty, &slam);
4080    }
4081
4082    Some(body)
4083}
4084
4085/// Collect constructor arguments, skipping type parameters.
4086/// Returns (arg_type, is_recursive) pairs.
4087fn collect_ctor_args(ctor_ty: &Term, ind_name: &str, type_args: &[Term]) -> Vec<(Term, bool)> {
4088    let mut args = Vec::new();
4089    let mut current = ctor_ty;
4090    let mut skip_count = type_args.len();
4091
4092    loop {
4093        match current {
4094            Term::Pi { param_type, body_type, .. } => {
4095                if skip_count > 0 {
4096                    // Skip type parameter
4097                    skip_count -= 1;
4098                } else {
4099                    // Regular argument
4100                    let is_recursive = contains_inductive_term(param_type, ind_name);
4101                    // Convert kernel type to Syntax representation
4102                    let arg_ty_syntax = kernel_type_to_syntax(param_type);
4103                    args.push((arg_ty_syntax, is_recursive));
4104                }
4105                current = body_type;
4106            }
4107            _ => break,
4108        }
4109    }
4110
4111    args
4112}
4113
4114/// Check if a kernel Term contains the inductive type.
4115fn contains_inductive_term(term: &Term, ind_name: &str) -> bool {
4116    match term {
4117        Term::Global(name) => name == ind_name,
4118        Term::App(f, a) => {
4119            contains_inductive_term(f, ind_name) || contains_inductive_term(a, ind_name)
4120        }
4121        Term::Pi { param_type, body_type, .. } => {
4122            contains_inductive_term(param_type, ind_name) || contains_inductive_term(body_type, ind_name)
4123        }
4124        Term::Lambda { param_type, body, .. } => {
4125            contains_inductive_term(param_type, ind_name) || contains_inductive_term(body, ind_name)
4126        }
4127        _ => false,
4128    }
4129}
4130
4131/// Convert a kernel Term (type) to its Syntax representation.
4132fn kernel_type_to_syntax(term: &Term) -> Term {
4133    match term {
4134        Term::Global(name) => make_sname(name),
4135        Term::Var(name) => make_sname(name), // Named variable
4136        Term::App(f, a) => {
4137            let f_syn = kernel_type_to_syntax(f);
4138            let a_syn = kernel_type_to_syntax(a);
4139            // SApp f_syn a_syn
4140            Term::App(
4141                Box::new(Term::App(
4142                    Box::new(Term::Global("SApp".to_string())),
4143                    Box::new(f_syn),
4144                )),
4145                Box::new(a_syn),
4146            )
4147        }
4148        Term::Pi { param, param_type, body_type } => {
4149            let pt_syn = kernel_type_to_syntax(param_type);
4150            let bt_syn = kernel_type_to_syntax(body_type);
4151            // SPi pt_syn bt_syn
4152            Term::App(
4153                Box::new(Term::App(
4154                    Box::new(Term::Global("SPi".to_string())),
4155                    Box::new(pt_syn),
4156                )),
4157                Box::new(bt_syn),
4158            )
4159        }
4160        Term::Sort(univ) => {
4161            // SSort univ
4162            Term::App(
4163                Box::new(Term::Global("SSort".to_string())),
4164                Box::new(univ_to_syntax(univ)),
4165            )
4166        }
4167        Term::Lit(lit) => {
4168            // SLit lit
4169            Term::App(
4170                Box::new(Term::Global("SLit".to_string())),
4171                Box::new(Term::Lit(lit.clone())),
4172            )
4173        }
4174        _ => {
4175            // Fallback for complex terms
4176            make_sname("Unknown")
4177        }
4178    }
4179}
4180
4181/// Convert a Universe to Syntax.
4182fn univ_to_syntax(univ: &crate::term::Universe) -> Term {
4183    match univ {
4184        crate::term::Universe::Prop => Term::Global("UProp".to_string()),
4185        crate::term::Universe::Type(n) => Term::App(
4186            Box::new(Term::Global("UType".to_string())),
4187            Box::new(Term::Lit(Literal::Int(*n as i64))),
4188        ),
4189    }
4190}
4191
4192// -------------------------------------------------------------------------
4193// Inversion Tactic
4194// -------------------------------------------------------------------------
4195
4196/// Inversion tactic: analyze hypothesis to derive False if no constructor matches.
4197///
4198/// Given hypothesis H of form `SApp (SName "IndName") args`, check if any constructor
4199/// of IndName can produce those args. If no constructor can match, return DInversion H.
4200fn try_try_inversion_reduce(ctx: &Context, goal: &Term) -> Option<Term> {
4201    // Extract inductive name and arguments from the hypothesis type
4202    let (ind_name, hyp_args) = match extract_applied_inductive_from_syntax(goal) {
4203        Some((name, args)) => (name, args),
4204        None => return Some(make_error_derivation()),
4205    };
4206
4207    // Check if the inductive type actually exists
4208    if !ctx.is_inductive(&ind_name) {
4209        // Unknown inductive type - cannot derive anything
4210        return Some(make_error_derivation());
4211    }
4212
4213    // Get constructors for this inductive
4214    let constructors = ctx.get_constructors(&ind_name);
4215
4216    // Check each constructor to see if it can match
4217    let mut any_possible = false;
4218    for (_ctor_name, ctor_type) in constructors.iter() {
4219        if can_constructor_match_args(ctx, ctor_type, &hyp_args, &ind_name) {
4220            any_possible = true;
4221            break;
4222        }
4223    }
4224
4225    if any_possible {
4226        // Cannot derive False - some constructor could match
4227        return Some(make_error_derivation());
4228    }
4229
4230    // All constructors impossible → build DInversion
4231    Some(Term::App(
4232        Box::new(Term::Global("DInversion".to_string())),
4233        Box::new(goal.clone()),
4234    ))
4235}
4236
4237/// Verify DInversion proof: check that no constructor can match the hypothesis.
4238fn try_dinversion_conclude(ctx: &Context, hyp_type: &Term) -> Option<Term> {
4239    let norm_hyp = normalize(ctx, hyp_type);
4240
4241    let (ind_name, hyp_args) = match extract_applied_inductive_from_syntax(&norm_hyp) {
4242        Some((name, args)) => (name, args),
4243        None => return Some(make_sname_error()),
4244    };
4245
4246    // Check if the inductive type actually exists
4247    if !ctx.is_inductive(&ind_name) {
4248        return Some(make_sname_error());
4249    }
4250
4251    let constructors = ctx.get_constructors(&ind_name);
4252
4253    // Verify ALL constructors are impossible
4254    for (_ctor_name, ctor_type) in constructors.iter() {
4255        if can_constructor_match_args(ctx, ctor_type, &hyp_args, &ind_name) {
4256            return Some(make_sname_error());
4257        }
4258    }
4259
4260    // All impossible → concludes False
4261    Some(make_sname("False"))
4262}
4263
4264/// Extract inductive name and arguments from Syntax.
4265///
4266/// SApp (SApp (SName "Even") x) y → ("Even", [x, y])
4267/// SName "False" → ("False", [])
4268fn extract_applied_inductive_from_syntax(term: &Term) -> Option<(String, Vec<Term>)> {
4269    // Base case: SName "X"
4270    if let Term::App(ctor, text) = term {
4271        if let Term::Global(ctor_name) = ctor.as_ref() {
4272            if ctor_name == "SName" {
4273                if let Term::Lit(Literal::Text(name)) = text.as_ref() {
4274                    return Some((name.clone(), vec![]));
4275                }
4276            }
4277        }
4278    }
4279
4280    // Recursive case: SApp f x
4281    if let Term::App(inner, arg) = term {
4282        if let Term::App(sapp_ctor, func) = inner.as_ref() {
4283            if let Term::Global(ctor_name) = sapp_ctor.as_ref() {
4284                if ctor_name == "SApp" {
4285                    // Recursively extract from the function
4286                    let (name, mut args) = extract_applied_inductive_from_syntax(func)?;
4287                    args.push(arg.as_ref().clone());
4288                    return Some((name, args));
4289                }
4290            }
4291        }
4292    }
4293
4294    None
4295}
4296
4297/// Check if a constructor can possibly match the given arguments.
4298///
4299/// For constructor `even_succ : ∀n. Even n → Even (Succ (Succ n))`:
4300/// - The constructor's result pattern is `Even (Succ (Succ n))`
4301/// - If hyp_args is `[Succ (Succ (Succ Zero))]` (representing 3):
4302///   - Unify `Succ (Succ n)` with `Succ (Succ (Succ Zero))`
4303///   - This succeeds with n = Succ Zero = 1
4304///   - But then we need to check if `Even 1` is constructible (recursive)
4305fn can_constructor_match_args(
4306    ctx: &Context,
4307    ctor_type: &Term,
4308    hyp_args: &[Term],
4309    ind_name: &str,
4310) -> bool {
4311    // Decompose constructor type to get result pattern and bound variable names
4312    let (result, pattern_vars) = decompose_ctor_type_with_vars(ctor_type);
4313
4314    // Extract result's arguments (what the constructor produces)
4315    let result_args = match extract_applied_inductive_from_syntax(&kernel_type_to_syntax(&result)) {
4316        Some((name, args)) if name == *ind_name => args,
4317        _ => return false,
4318    };
4319
4320    // If argument counts don't match, can't unify
4321    if result_args.len() != hyp_args.len() {
4322        return false;
4323    }
4324
4325    // Try syntactic unification of all arguments together (tracking bindings across args)
4326    let mut bindings: std::collections::HashMap<String, Term> = std::collections::HashMap::new();
4327
4328    for (pattern, concrete) in result_args.iter().zip(hyp_args.iter()) {
4329        if !can_unify_syntax_terms_with_bindings(ctx, pattern, concrete, &pattern_vars, &mut bindings) {
4330            return false;
4331        }
4332    }
4333
4334    // If we get here, the constructor could match
4335    // (We don't check recursive hypotheses for simplicity - that would require
4336    // full inversion with backtracking)
4337    true
4338}
4339
4340/// Decompose a constructor type to get the result type and bound variable names.
4341///
4342/// `∀n:Nat. Even n → Even (Succ (Succ n))` → (`Even (Succ (Succ n))`, ["n"])
4343/// `∀A:Type. ∀x:A. Eq A x x` → (`Eq A x x`, ["A", "x"])
4344/// `Bool` → (`Bool`, [])
4345fn decompose_ctor_type_with_vars(ty: &Term) -> (Term, Vec<String>) {
4346    let mut vars = Vec::new();
4347    let mut current = ty;
4348    loop {
4349        match current {
4350            Term::Pi { param, body_type, .. } => {
4351                vars.push(param.clone());
4352                current = body_type;
4353            }
4354            _ => break,
4355        }
4356    }
4357    (current.clone(), vars)
4358}
4359
4360/// Check if two Syntax terms can unify, tracking variable bindings.
4361///
4362/// Pattern variables (names in `pattern_vars`) can bind to any concrete value,
4363/// but must bind consistently (same variable must bind to same value).
4364/// Other SNames must match exactly.
4365/// SApp recurses on function and argument.
4366fn can_unify_syntax_terms_with_bindings(
4367    ctx: &Context,
4368    pattern: &Term,
4369    concrete: &Term,
4370    pattern_vars: &[String],
4371    bindings: &mut std::collections::HashMap<String, Term>,
4372) -> bool {
4373    // SVar can match anything (explicit unification variable)
4374    if let Term::App(ctor, _idx) = pattern {
4375        if let Term::Global(name) = ctor.as_ref() {
4376            if name == "SVar" {
4377                return true;
4378            }
4379        }
4380    }
4381
4382    // SName: check if it's a pattern variable or a constant
4383    if let Term::App(ctor1, text1) = pattern {
4384        if let Term::Global(n1) = ctor1.as_ref() {
4385            if n1 == "SName" {
4386                if let Term::Lit(Literal::Text(var_name)) = text1.as_ref() {
4387                    // Check if this is a pattern variable
4388                    if pattern_vars.contains(var_name) {
4389                        // Pattern variable: check existing binding or create new one
4390                        if let Some(existing) = bindings.get(var_name) {
4391                            // Already bound: concrete must match existing binding
4392                            return syntax_terms_equal(existing, concrete);
4393                        } else {
4394                            // Not yet bound: bind to concrete value
4395                            bindings.insert(var_name.clone(), concrete.clone());
4396                            return true;
4397                        }
4398                    }
4399                }
4400                // Not a pattern variable: must match exactly
4401                if let Term::App(ctor2, text2) = concrete {
4402                    if let Term::Global(n2) = ctor2.as_ref() {
4403                        if n2 == "SName" {
4404                            return text1 == text2;
4405                        }
4406                    }
4407                }
4408                return false;
4409            }
4410        }
4411    }
4412
4413    // SApp: recurse on both function and argument
4414    if let (Term::App(inner1, arg1), Term::App(inner2, arg2)) = (pattern, concrete) {
4415        if let (Term::App(sapp1, func1), Term::App(sapp2, func2)) =
4416            (inner1.as_ref(), inner2.as_ref())
4417        {
4418            if let (Term::Global(n1), Term::Global(n2)) = (sapp1.as_ref(), sapp2.as_ref()) {
4419                if n1 == "SApp" && n2 == "SApp" {
4420                    return can_unify_syntax_terms_with_bindings(ctx, func1, func2, pattern_vars, bindings)
4421                        && can_unify_syntax_terms_with_bindings(ctx, arg1.as_ref(), arg2.as_ref(), pattern_vars, bindings);
4422                }
4423            }
4424        }
4425    }
4426
4427    // SLit: compare literal values
4428    if let (Term::App(ctor1, lit1), Term::App(ctor2, lit2)) = (pattern, concrete) {
4429        if let (Term::Global(n1), Term::Global(n2)) = (ctor1.as_ref(), ctor2.as_ref()) {
4430            if n1 == "SLit" && n2 == "SLit" {
4431                return lit1 == lit2;
4432            }
4433        }
4434    }
4435
4436    // Fall back to exact structural equality
4437    pattern == concrete
4438}
4439
4440/// Check if two Syntax terms are structurally equal.
4441fn syntax_terms_equal(a: &Term, b: &Term) -> bool {
4442    match (a, b) {
4443        (Term::App(f1, x1), Term::App(f2, x2)) => {
4444            syntax_terms_equal(f1, f2) && syntax_terms_equal(x1, x2)
4445        }
4446        (Term::Global(n1), Term::Global(n2)) => n1 == n2,
4447        (Term::Lit(l1), Term::Lit(l2)) => l1 == l2,
4448        _ => a == b,
4449    }
4450}
4451
4452// -------------------------------------------------------------------------
4453// Operator Tactics (rewrite, destruct, apply)
4454// -------------------------------------------------------------------------
4455
4456/// Extract Eq A x y components from a Syntax term.
4457///
4458/// SApp (SApp (SApp (SName "Eq") A) x) y → Some((A, x, y))
4459fn extract_eq_components_from_syntax(term: &Term) -> Option<(Term, Term, Term)> {
4460    // term = SApp (SApp (SApp (SName "Eq") A) x) y
4461    // In kernel representation: App(App(SApp, App(App(SApp, App(App(SApp, SName "Eq"), A)), x)), y)
4462
4463    // Peel off outermost SApp to get ((SApp (SApp (SName "Eq") A) x), y)
4464    let (eq_a_x, y) = extract_sapp(term)?;
4465
4466    // Peel off next SApp to get ((SApp (SName "Eq") A), x)
4467    let (eq_a, x) = extract_sapp(&eq_a_x)?;
4468
4469    // Peel off next SApp to get ((SName "Eq"), A)
4470    let (eq, a) = extract_sapp(&eq_a)?;
4471
4472    // Verify it's SName "Eq"
4473    let eq_name = extract_sname(&eq)?;
4474    if eq_name != "Eq" {
4475        return None;
4476    }
4477
4478    Some((a, x, y))
4479}
4480
4481/// Extract (f, x) from SApp f x (in kernel representation).
4482fn extract_sapp(term: &Term) -> Option<(Term, Term)> {
4483    // SApp f x = App(App(Global("SApp"), f), x)
4484    if let Term::App(inner, x) = term {
4485        if let Term::App(sapp_ctor, f) = inner.as_ref() {
4486            if let Term::Global(ctor_name) = sapp_ctor.as_ref() {
4487                if ctor_name == "SApp" {
4488                    return Some((f.as_ref().clone(), x.as_ref().clone()));
4489                }
4490            }
4491        }
4492    }
4493    None
4494}
4495
4496/// Extract name from SName "name".
4497fn extract_sname(term: &Term) -> Option<String> {
4498    if let Term::App(ctor, text) = term {
4499        if let Term::Global(ctor_name) = ctor.as_ref() {
4500            if ctor_name == "SName" {
4501                if let Term::Lit(Literal::Text(name)) = text.as_ref() {
4502                    return Some(name.clone());
4503                }
4504            }
4505        }
4506    }
4507    None
4508}
4509
4510/// Check if a Syntax term contains a specific subterm.
4511fn contains_subterm_syntax(term: &Term, target: &Term) -> bool {
4512    if syntax_equal(term, target) {
4513        return true;
4514    }
4515
4516    // Check SApp f x
4517    if let Some((f, x)) = extract_sapp(term) {
4518        if contains_subterm_syntax(&f, target) || contains_subterm_syntax(&x, target) {
4519            return true;
4520        }
4521    }
4522
4523    // Check SLam T body
4524    if let Some((t, body)) = extract_slam(term) {
4525        if contains_subterm_syntax(&t, target) || contains_subterm_syntax(&body, target) {
4526            return true;
4527        }
4528    }
4529
4530    // Check SPi T body
4531    if let Some((t, body)) = extract_spi(term) {
4532        if contains_subterm_syntax(&t, target) || contains_subterm_syntax(&body, target) {
4533            return true;
4534        }
4535    }
4536
4537    false
4538}
4539
4540/// Extract (T, body) from SLam T body.
4541fn extract_slam(term: &Term) -> Option<(Term, Term)> {
4542    if let Term::App(inner, body) = term {
4543        if let Term::App(slam_ctor, t) = inner.as_ref() {
4544            if let Term::Global(ctor_name) = slam_ctor.as_ref() {
4545                if ctor_name == "SLam" {
4546                    return Some((t.as_ref().clone(), body.as_ref().clone()));
4547                }
4548            }
4549        }
4550    }
4551    None
4552}
4553
4554/// Extract (T, body) from SPi T body.
4555fn extract_spi(term: &Term) -> Option<(Term, Term)> {
4556    if let Term::App(inner, body) = term {
4557        if let Term::App(spi_ctor, t) = inner.as_ref() {
4558            if let Term::Global(ctor_name) = spi_ctor.as_ref() {
4559                if ctor_name == "SPi" {
4560                    return Some((t.as_ref().clone(), body.as_ref().clone()));
4561                }
4562            }
4563        }
4564    }
4565    None
4566}
4567
4568/// Replace first occurrence of target with replacement in a Syntax term.
4569fn replace_first_subterm_syntax(term: &Term, target: &Term, replacement: &Term) -> Option<Term> {
4570    // If term equals target, return replacement
4571    if syntax_equal(term, target) {
4572        return Some(replacement.clone());
4573    }
4574
4575    // Try to replace in SApp f x
4576    if let Some((f, x)) = extract_sapp(term) {
4577        // First try to replace in f
4578        if let Some(new_f) = replace_first_subterm_syntax(&f, target, replacement) {
4579            return Some(make_sapp(new_f, x));
4580        }
4581        // Then try to replace in x
4582        if let Some(new_x) = replace_first_subterm_syntax(&x, target, replacement) {
4583            return Some(make_sapp(f, new_x));
4584        }
4585    }
4586
4587    // Try to replace in SLam T body
4588    if let Some((t, body)) = extract_slam(term) {
4589        if let Some(new_t) = replace_first_subterm_syntax(&t, target, replacement) {
4590            return Some(make_slam(new_t, body));
4591        }
4592        if let Some(new_body) = replace_first_subterm_syntax(&body, target, replacement) {
4593            return Some(make_slam(t, new_body));
4594        }
4595    }
4596
4597    // Try to replace in SPi T body
4598    if let Some((t, body)) = extract_spi(term) {
4599        if let Some(new_t) = replace_first_subterm_syntax(&t, target, replacement) {
4600            return Some(make_spi(new_t, body));
4601        }
4602        if let Some(new_body) = replace_first_subterm_syntax(&body, target, replacement) {
4603            return Some(make_spi(t, new_body));
4604        }
4605    }
4606
4607    // No replacement found
4608    None
4609}
4610
4611/// Rewrite tactic: given eq_proof (concluding Eq A x y) and goal,
4612/// replaces x with y (or y with x if reverse=true) in goal.
4613fn try_try_rewrite_reduce(
4614    ctx: &Context,
4615    eq_proof: &Term,
4616    goal: &Term,
4617    reverse: bool,
4618) -> Option<Term> {
4619    // Get the conclusion of eq_proof
4620    let eq_conclusion = try_concludes_reduce(ctx, eq_proof)?;
4621
4622    // Extract Eq A x y components
4623    let (ty, lhs, rhs) = match extract_eq_components_from_syntax(&eq_conclusion) {
4624        Some(components) => components,
4625        None => return Some(make_error_derivation()),
4626    };
4627
4628    // Determine what to replace based on direction
4629    let (target, replacement) = if reverse { (rhs, lhs) } else { (lhs, rhs) };
4630
4631    // Check if target exists in goal
4632    if !contains_subterm_syntax(goal, &target) {
4633        return Some(make_error_derivation());
4634    }
4635
4636    // Replace target with replacement in goal
4637    let new_goal = match replace_first_subterm_syntax(goal, &target, &replacement) {
4638        Some(ng) => ng,
4639        None => return Some(make_error_derivation()),
4640    };
4641
4642    // Build DRewrite eq_proof goal new_goal
4643    Some(Term::App(
4644        Box::new(Term::App(
4645            Box::new(Term::App(
4646                Box::new(Term::Global("DRewrite".to_string())),
4647                Box::new(eq_proof.clone()),
4648            )),
4649            Box::new(goal.clone()),
4650        )),
4651        Box::new(new_goal),
4652    ))
4653}
4654
4655/// Verify DRewrite derivation and return the new goal.
4656fn try_drewrite_conclude(
4657    ctx: &Context,
4658    eq_proof: &Term,
4659    old_goal: &Term,
4660    new_goal: &Term,
4661) -> Option<Term> {
4662    // Get the conclusion of eq_proof
4663    let eq_conclusion = try_concludes_reduce(ctx, eq_proof)?;
4664
4665    // Extract Eq A x y components
4666    let (_ty, lhs, rhs) = match extract_eq_components_from_syntax(&eq_conclusion) {
4667        Some(components) => components,
4668        None => return Some(make_sname_error()),
4669    };
4670
4671    // Verify: new_goal = old_goal[lhs := rhs] OR new_goal = old_goal[rhs := lhs]
4672    // Check forward direction first
4673    if let Some(computed_new) = replace_first_subterm_syntax(old_goal, &lhs, &rhs) {
4674        if syntax_equal(&computed_new, new_goal) {
4675            return Some(new_goal.clone());
4676        }
4677    }
4678
4679    // Check reverse direction
4680    if let Some(computed_new) = replace_first_subterm_syntax(old_goal, &rhs, &lhs) {
4681        if syntax_equal(&computed_new, new_goal) {
4682            return Some(new_goal.clone());
4683        }
4684    }
4685
4686    // Verification failed
4687    Some(make_sname_error())
4688}
4689
4690/// Destruct tactic: case analysis without induction hypotheses.
4691fn try_try_destruct_reduce(
4692    ctx: &Context,
4693    ind_type: &Term,
4694    motive: &Term,
4695    cases: &Term,
4696) -> Option<Term> {
4697    // For now, destruct is essentially the same as induction
4698    // The key difference is in what goals are expected for each case
4699    // (no IH for recursive constructors)
4700    //
4701    // We simply build a DDestruct and let verification check case proofs
4702
4703    Some(Term::App(
4704        Box::new(Term::App(
4705            Box::new(Term::App(
4706                Box::new(Term::Global("DDestruct".to_string())),
4707                Box::new(ind_type.clone()),
4708            )),
4709            Box::new(motive.clone()),
4710        )),
4711        Box::new(cases.clone()),
4712    ))
4713}
4714
4715/// Verify DDestruct derivation.
4716fn try_ddestruct_conclude(
4717    ctx: &Context,
4718    ind_type: &Term,
4719    motive: &Term,
4720    cases: &Term,
4721) -> Option<Term> {
4722    // Similar to DElim but without verifying IH in step cases
4723    // For now, we accept the derivation and return Forall ind_type motive
4724
4725    // Extract the inductive type name
4726    let ind_name = extract_inductive_name_from_syntax(ind_type)?;
4727
4728    // Verify it's actually an inductive type
4729    if !ctx.is_inductive(&ind_name) {
4730        return Some(make_sname_error());
4731    }
4732
4733    let constructors = ctx.get_constructors(&ind_name);
4734
4735    // Extract case proofs
4736    let case_proofs = match extract_case_proofs(cases) {
4737        Some(proofs) => proofs,
4738        None => return Some(make_sname_error()),
4739    };
4740
4741    // Verify case count matches
4742    if case_proofs.len() != constructors.len() {
4743        return Some(make_sname_error());
4744    }
4745
4746    // For each case, verify the conclusion matches the expected goal (without IH)
4747    // For simplicity, we just check case count matches for now
4748    // Full verification would check each case proves P(ctor args)
4749
4750    // Build Forall ind_type motive
4751    Some(make_forall_syntax_with_type(ind_type, motive))
4752}
4753
4754/// Apply tactic: manual backward chaining.
4755fn try_try_apply_reduce(
4756    ctx: &Context,
4757    hyp_name: &Term,
4758    hyp_proof: &Term,
4759    goal: &Term,
4760) -> Option<Term> {
4761    // Get the conclusion of hyp_proof
4762    let hyp_conclusion = try_concludes_reduce(ctx, hyp_proof)?;
4763
4764    // Check if it's an implication: SPi A B where B doesn't use the bound var
4765    if let Some((antecedent, consequent)) = extract_spi(&hyp_conclusion) {
4766        // Check if consequent matches goal
4767        if syntax_equal(&consequent, goal) {
4768            // Build DApply hyp_name hyp_proof goal antecedent
4769            return Some(Term::App(
4770                Box::new(Term::App(
4771                    Box::new(Term::App(
4772                        Box::new(Term::App(
4773                            Box::new(Term::Global("DApply".to_string())),
4774                            Box::new(hyp_name.clone()),
4775                        )),
4776                        Box::new(hyp_proof.clone()),
4777                    )),
4778                    Box::new(goal.clone()),
4779                )),
4780                Box::new(antecedent),
4781            ));
4782        }
4783    }
4784
4785    // Check if it's a forall that could match
4786    if let Some(forall_body) = extract_forall_body(&hyp_conclusion) {
4787        // Try to match goal with forall body (simple syntactic check)
4788        // For now, if goal appears to be an instance of the forall body, accept it
4789        // Full implementation would do proper unification
4790
4791        // Build DApply with new goal being True (trivially satisfied)
4792        return Some(Term::App(
4793            Box::new(Term::App(
4794                Box::new(Term::App(
4795                    Box::new(Term::App(
4796                        Box::new(Term::Global("DApply".to_string())),
4797                        Box::new(hyp_name.clone()),
4798                    )),
4799                    Box::new(hyp_proof.clone()),
4800                )),
4801                Box::new(goal.clone()),
4802            )),
4803            Box::new(make_sname("True")),
4804        ));
4805    }
4806
4807    // If hypothesis directly matches goal, we're done
4808    if syntax_equal(&hyp_conclusion, goal) {
4809        return Some(Term::App(
4810            Box::new(Term::App(
4811                Box::new(Term::App(
4812                    Box::new(Term::App(
4813                        Box::new(Term::Global("DApply".to_string())),
4814                        Box::new(hyp_name.clone()),
4815                    )),
4816                    Box::new(hyp_proof.clone()),
4817                )),
4818                Box::new(goal.clone()),
4819            )),
4820            Box::new(make_sname("True")),
4821        ));
4822    }
4823
4824    // Cannot apply this hypothesis to this goal
4825    Some(make_error_derivation())
4826}
4827
4828/// Verify DApply derivation.
4829fn try_dapply_conclude(
4830    ctx: &Context,
4831    hyp_name: &Term,
4832    hyp_proof: &Term,
4833    old_goal: &Term,
4834    new_goal: &Term,
4835) -> Option<Term> {
4836    // Get the conclusion of hyp_proof
4837    let hyp_conclusion = try_concludes_reduce(ctx, hyp_proof)?;
4838
4839    // If hypothesis is an implication A -> B and old_goal is B
4840    // then new_goal should be A
4841    if let Some((antecedent, consequent)) = extract_spi(&hyp_conclusion) {
4842        if syntax_equal(&consequent, old_goal) {
4843            if syntax_equal(&antecedent, new_goal) || extract_sname(new_goal) == Some("True".to_string()) {
4844                return Some(new_goal.clone());
4845            }
4846        }
4847    }
4848
4849    // If hypothesis is a forall and goal matches instantiation
4850    if let Some(_forall_body) = extract_forall_body(&hyp_conclusion) {
4851        // For forall application, the new goal is typically True or the instantiated body
4852        if extract_sname(new_goal) == Some("True".to_string()) {
4853            return Some(new_goal.clone());
4854        }
4855    }
4856
4857    // If hypothesis directly matches old_goal
4858    if syntax_equal(&hyp_conclusion, old_goal) {
4859        if extract_sname(new_goal) == Some("True".to_string()) {
4860            return Some(new_goal.clone());
4861        }
4862    }
4863
4864    // Verification failed
4865    Some(make_sname_error())
4866}
4867
logicaffeine_kernel/reduction.rs

logicaffeine_kernel/
reduction.rs
