logicaffeine_kernel/prelude.rs
1//! Standard Library for the Kernel.
2//!
3//! Defines fundamental types and logical connectives:
4//! - Entity: domain of individuals (for FOL)
5//! - Nat: natural numbers
6//! - True, False: propositional constants
7//! - Eq: propositional equality
8//! - And, Or: logical connectives
9
10use crate::context::Context;
11use crate::term::{Term, Universe};
12
13/// Standard library definitions.
14pub struct StandardLibrary;
15
16impl StandardLibrary {
17 /// Register all standard library definitions in the context.
18 pub fn register(ctx: &mut Context) {
19 Self::register_entity(ctx);
20 Self::register_nat(ctx);
21 Self::register_bool(ctx);
22 Self::register_tlist(ctx);
23 Self::register_true(ctx);
24 Self::register_false(ctx);
25 Self::register_not(ctx);
26 Self::register_eq(ctx);
27 Self::register_and(ctx);
28 Self::register_or(ctx);
29 Self::register_ex(ctx);
30 Self::register_primitives(ctx);
31 Self::register_reflection(ctx);
32 }
33
34 /// Primitive types and operations.
35 ///
36 /// Int : Type 0 (64-bit signed integer)
37 /// Float : Type 0 (64-bit floating point)
38 /// Text : Type 0 (UTF-8 string)
39 ///
40 /// add, sub, mul, div, mod : Int -> Int -> Int
41 fn register_primitives(ctx: &mut Context) {
42 // Opaque types (no constructors, cannot be pattern-matched)
43 ctx.add_inductive("Int", Term::Sort(Universe::Type(0)));
44 ctx.add_inductive("Float", Term::Sort(Universe::Type(0)));
45 ctx.add_inductive("Text", Term::Sort(Universe::Type(0)));
46
47 let int = Term::Global("Int".to_string());
48
49 // Binary Int -> Int -> Int type
50 let bin_int_type = Term::Pi {
51 param: "_".to_string(),
52 param_type: Box::new(int.clone()),
53 body_type: Box::new(Term::Pi {
54 param: "_".to_string(),
55 param_type: Box::new(int.clone()),
56 body_type: Box::new(int.clone()),
57 }),
58 };
59
60 // Register arithmetic builtins as declarations (axioms with computational behavior)
61 ctx.add_declaration("add", bin_int_type.clone());
62 ctx.add_declaration("sub", bin_int_type.clone());
63 ctx.add_declaration("mul", bin_int_type.clone());
64 ctx.add_declaration("div", bin_int_type.clone());
65 ctx.add_declaration("mod", bin_int_type);
66 }
67
68 /// Entity : Type 0
69 ///
70 /// The domain of individuals for first-order logic.
71 /// Proper names like "Socrates" are declared as Entity.
72 /// Predicates like "Man" are declared as Entity → Prop.
73 fn register_entity(ctx: &mut Context) {
74 ctx.add_inductive("Entity", Term::Sort(Universe::Type(0)));
75 }
76
77 /// Nat : Type 0
78 /// Zero : Nat
79 /// Succ : Nat → Nat
80 fn register_nat(ctx: &mut Context) {
81 let nat = Term::Global("Nat".to_string());
82
83 // Nat : Type 0
84 ctx.add_inductive("Nat", Term::Sort(Universe::Type(0)));
85
86 // Zero : Nat
87 ctx.add_constructor("Zero", "Nat", nat.clone());
88
89 // Succ : Nat → Nat
90 ctx.add_constructor(
91 "Succ",
92 "Nat",
93 Term::Pi {
94 param: "_".to_string(),
95 param_type: Box::new(nat.clone()),
96 body_type: Box::new(nat),
97 },
98 );
99 }
100
101 /// Bool : Type 0
102 /// true : Bool
103 /// false : Bool
104 fn register_bool(ctx: &mut Context) {
105 let bool_type = Term::Global("Bool".to_string());
106
107 // Bool : Type 0
108 ctx.add_inductive("Bool", Term::Sort(Universe::Type(0)));
109
110 // true : Bool
111 ctx.add_constructor("true", "Bool", bool_type.clone());
112
113 // false : Bool
114 ctx.add_constructor("false", "Bool", bool_type);
115 }
116
117 /// TList : Type 0 -> Type 0
118 /// TNil : Π(A : Type 0). TList A
119 /// TCons : Π(A : Type 0). A -> TList A -> TList A
120 fn register_tlist(ctx: &mut Context) {
121 let type0 = Term::Sort(Universe::Type(0));
122 let a = Term::Var("A".to_string());
123
124 // TList : Type 0 -> Type 0
125 let tlist_type = Term::Pi {
126 param: "A".to_string(),
127 param_type: Box::new(type0.clone()),
128 body_type: Box::new(type0.clone()),
129 };
130 ctx.add_inductive("TList", tlist_type);
131
132 // TList A
133 let tlist_a = Term::App(
134 Box::new(Term::Global("TList".to_string())),
135 Box::new(a.clone()),
136 );
137
138 // TNil : Π(A : Type 0). TList A
139 let tnil_type = Term::Pi {
140 param: "A".to_string(),
141 param_type: Box::new(type0.clone()),
142 body_type: Box::new(tlist_a.clone()),
143 };
144 ctx.add_constructor("TNil", "TList", tnil_type);
145
146 // TCons : Π(A : Type 0). A -> TList A -> TList A
147 let tcons_type = Term::Pi {
148 param: "A".to_string(),
149 param_type: Box::new(type0),
150 body_type: Box::new(Term::Pi {
151 param: "_".to_string(),
152 param_type: Box::new(a.clone()),
153 body_type: Box::new(Term::Pi {
154 param: "_".to_string(),
155 param_type: Box::new(tlist_a.clone()),
156 body_type: Box::new(tlist_a),
157 }),
158 }),
159 };
160 ctx.add_constructor("TCons", "TList", tcons_type);
161
162 // Convenience aliases for tactic lists (Syntax -> Derivation)
163 Self::register_tactic_list_helpers(ctx);
164 }
165
166 /// TTactics : Type 0 = TList (Syntax -> Derivation)
167 /// TacNil : TTactics
168 /// TacCons : (Syntax -> Derivation) -> TTactics -> TTactics
169 ///
170 /// Convenience wrappers to avoid explicit type arguments for tactic lists.
171 fn register_tactic_list_helpers(ctx: &mut Context) {
172 let syntax = Term::Global("Syntax".to_string());
173 let derivation = Term::Global("Derivation".to_string());
174
175 // Tactic type: Syntax -> Derivation
176 let tactic_type = Term::Pi {
177 param: "_".to_string(),
178 param_type: Box::new(syntax.clone()),
179 body_type: Box::new(derivation.clone()),
180 };
181
182 // TTactics = TList (Syntax -> Derivation)
183 let ttactics = Term::App(
184 Box::new(Term::Global("TList".to_string())),
185 Box::new(tactic_type.clone()),
186 );
187
188 // TTactics : Type 0
189 ctx.add_definition("TTactics".to_string(), Term::Sort(Universe::Type(0)), ttactics.clone());
190
191 // TacNil : TTactics = TNil (Syntax -> Derivation)
192 let tac_nil_body = Term::App(
193 Box::new(Term::Global("TNil".to_string())),
194 Box::new(tactic_type.clone()),
195 );
196 ctx.add_definition("TacNil".to_string(), ttactics.clone(), tac_nil_body);
197
198 // TacCons : (Syntax -> Derivation) -> TTactics -> TTactics
199 let tac_cons_type = Term::Pi {
200 param: "t".to_string(),
201 param_type: Box::new(tactic_type.clone()),
202 body_type: Box::new(Term::Pi {
203 param: "ts".to_string(),
204 param_type: Box::new(ttactics.clone()),
205 body_type: Box::new(ttactics.clone()),
206 }),
207 };
208
209 // TacCons t ts = TCons (Syntax -> Derivation) t ts
210 let tac_cons_body = Term::Lambda {
211 param: "t".to_string(),
212 param_type: Box::new(tactic_type.clone()),
213 body: Box::new(Term::Lambda {
214 param: "ts".to_string(),
215 param_type: Box::new(ttactics.clone()),
216 body: Box::new(Term::App(
217 Box::new(Term::App(
218 Box::new(Term::App(
219 Box::new(Term::Global("TCons".to_string())),
220 Box::new(tactic_type),
221 )),
222 Box::new(Term::Var("t".to_string())),
223 )),
224 Box::new(Term::Var("ts".to_string())),
225 )),
226 }),
227 };
228 ctx.add_definition("TacCons".to_string(), tac_cons_type, tac_cons_body);
229 }
230
231 /// True : Prop
232 /// I : True
233 fn register_true(ctx: &mut Context) {
234 ctx.add_inductive("True", Term::Sort(Universe::Prop));
235 ctx.add_constructor("I", "True", Term::Global("True".to_string()));
236 }
237
238 /// False : Prop
239 /// (no constructors)
240 fn register_false(ctx: &mut Context) {
241 ctx.add_inductive("False", Term::Sort(Universe::Prop));
242 }
243
244 /// Not : Prop -> Prop
245 /// Not P := P -> False
246 fn register_not(ctx: &mut Context) {
247 // Type: Π(P : Prop). Prop
248 let not_type = Term::Pi {
249 param: "P".to_string(),
250 param_type: Box::new(Term::Sort(Universe::Prop)),
251 body_type: Box::new(Term::Sort(Universe::Prop)),
252 };
253
254 // Body: λ(P : Prop). Π(_ : P). False
255 let not_body = Term::Lambda {
256 param: "P".to_string(),
257 param_type: Box::new(Term::Sort(Universe::Prop)),
258 body: Box::new(Term::Pi {
259 param: "_".to_string(),
260 param_type: Box::new(Term::Var("P".to_string())),
261 body_type: Box::new(Term::Global("False".to_string())),
262 }),
263 };
264
265 ctx.add_definition("Not".to_string(), not_type, not_body);
266 }
267
268 /// Eq : Π(A : Type 0). A → A → Prop
269 /// refl : Π(A : Type 0). Π(x : A). Eq A x x
270 fn register_eq(ctx: &mut Context) {
271 // Eq : Π(A : Type 0). A → A → Prop
272 let eq_type = Term::Pi {
273 param: "A".to_string(),
274 param_type: Box::new(Term::Sort(Universe::Type(0))),
275 body_type: Box::new(Term::Pi {
276 param: "x".to_string(),
277 param_type: Box::new(Term::Var("A".to_string())),
278 body_type: Box::new(Term::Pi {
279 param: "y".to_string(),
280 param_type: Box::new(Term::Var("A".to_string())),
281 body_type: Box::new(Term::Sort(Universe::Prop)),
282 }),
283 }),
284 };
285 ctx.add_inductive("Eq", eq_type);
286
287 // refl : Π(A : Type 0). Π(x : A). Eq A x x
288 let refl_type = Term::Pi {
289 param: "A".to_string(),
290 param_type: Box::new(Term::Sort(Universe::Type(0))),
291 body_type: Box::new(Term::Pi {
292 param: "x".to_string(),
293 param_type: Box::new(Term::Var("A".to_string())),
294 body_type: Box::new(Term::App(
295 Box::new(Term::App(
296 Box::new(Term::App(
297 Box::new(Term::Global("Eq".to_string())),
298 Box::new(Term::Var("A".to_string())),
299 )),
300 Box::new(Term::Var("x".to_string())),
301 )),
302 Box::new(Term::Var("x".to_string())),
303 )),
304 }),
305 };
306 ctx.add_constructor("refl", "Eq", refl_type);
307
308 // Eq_rec : Π(A:Type). Π(x:A). Π(P:A→Prop). P x → Π(y:A). Eq A x y → P y
309 // The eliminator for equality - Leibniz's Law
310 Self::register_eq_rec(ctx);
311
312 // Eq_sym : Π(A:Type). Π(x:A). Π(y:A). Eq A x y → Eq A y x
313 Self::register_eq_sym(ctx);
314
315 // Eq_trans : Π(A:Type). Π(x:A). Π(y:A). Π(z:A). Eq A x y → Eq A y z → Eq A x z
316 Self::register_eq_trans(ctx);
317 }
318
319 /// Eq_rec : Π(A:Type). Π(x:A). Π(P:A→Prop). P x → Π(y:A). Eq A x y → P y
320 /// The eliminator for equality - Leibniz's Law / Substitution of Equals
321 fn register_eq_rec(ctx: &mut Context) {
322 let a = Term::Var("A".to_string());
323 let x = Term::Var("x".to_string());
324 let y = Term::Var("y".to_string());
325 let p = Term::Var("P".to_string());
326
327 // P x = P applied to x
328 let p_x = Term::App(Box::new(p.clone()), Box::new(x.clone()));
329
330 // P y = P applied to y
331 let p_y = Term::App(Box::new(p.clone()), Box::new(y.clone()));
332
333 // Eq A x y
334 let eq_a_x_y = Term::App(
335 Box::new(Term::App(
336 Box::new(Term::App(
337 Box::new(Term::Global("Eq".to_string())),
338 Box::new(a.clone()),
339 )),
340 Box::new(x.clone()),
341 )),
342 Box::new(y.clone()),
343 );
344
345 // P : A → Prop
346 let p_type = Term::Pi {
347 param: "_".to_string(),
348 param_type: Box::new(a.clone()),
349 body_type: Box::new(Term::Sort(Universe::Prop)),
350 };
351
352 // Full type: Π(A:Type). Π(x:A). Π(P:A→Prop). P x → Π(y:A). Eq A x y → P y
353 let eq_rec_type = Term::Pi {
354 param: "A".to_string(),
355 param_type: Box::new(Term::Sort(Universe::Type(0))),
356 body_type: Box::new(Term::Pi {
357 param: "x".to_string(),
358 param_type: Box::new(a.clone()),
359 body_type: Box::new(Term::Pi {
360 param: "P".to_string(),
361 param_type: Box::new(p_type),
362 body_type: Box::new(Term::Pi {
363 param: "_".to_string(),
364 param_type: Box::new(p_x),
365 body_type: Box::new(Term::Pi {
366 param: "y".to_string(),
367 param_type: Box::new(a),
368 body_type: Box::new(Term::Pi {
369 param: "_".to_string(),
370 param_type: Box::new(eq_a_x_y),
371 body_type: Box::new(p_y),
372 }),
373 }),
374 }),
375 }),
376 }),
377 };
378
379 ctx.add_declaration("Eq_rec", eq_rec_type);
380 }
381
382 /// Eq_sym : Π(A:Type). Π(x:A). Π(y:A). Eq A x y → Eq A y x
383 /// Symmetry of equality
384 fn register_eq_sym(ctx: &mut Context) {
385 let a = Term::Var("A".to_string());
386 let x = Term::Var("x".to_string());
387 let y = Term::Var("y".to_string());
388
389 // Eq A x y
390 let eq_a_x_y = Term::App(
391 Box::new(Term::App(
392 Box::new(Term::App(
393 Box::new(Term::Global("Eq".to_string())),
394 Box::new(a.clone()),
395 )),
396 Box::new(x.clone()),
397 )),
398 Box::new(y.clone()),
399 );
400
401 // Eq A y x
402 let eq_a_y_x = Term::App(
403 Box::new(Term::App(
404 Box::new(Term::App(
405 Box::new(Term::Global("Eq".to_string())),
406 Box::new(a.clone()),
407 )),
408 Box::new(y.clone()),
409 )),
410 Box::new(x.clone()),
411 );
412
413 // Π(A:Type). Π(x:A). Π(y:A). Eq A x y → Eq A y x
414 let eq_sym_type = Term::Pi {
415 param: "A".to_string(),
416 param_type: Box::new(Term::Sort(Universe::Type(0))),
417 body_type: Box::new(Term::Pi {
418 param: "x".to_string(),
419 param_type: Box::new(a.clone()),
420 body_type: Box::new(Term::Pi {
421 param: "y".to_string(),
422 param_type: Box::new(a),
423 body_type: Box::new(Term::Pi {
424 param: "_".to_string(),
425 param_type: Box::new(eq_a_x_y),
426 body_type: Box::new(eq_a_y_x),
427 }),
428 }),
429 }),
430 };
431
432 ctx.add_declaration("Eq_sym", eq_sym_type);
433 }
434
435 /// Eq_trans : Π(A:Type). Π(x:A). Π(y:A). Π(z:A). Eq A x y → Eq A y z → Eq A x z
436 /// Transitivity of equality
437 fn register_eq_trans(ctx: &mut Context) {
438 let a = Term::Var("A".to_string());
439 let x = Term::Var("x".to_string());
440 let y = Term::Var("y".to_string());
441 let z = Term::Var("z".to_string());
442
443 // Eq A x y
444 let eq_a_x_y = Term::App(
445 Box::new(Term::App(
446 Box::new(Term::App(
447 Box::new(Term::Global("Eq".to_string())),
448 Box::new(a.clone()),
449 )),
450 Box::new(x.clone()),
451 )),
452 Box::new(y.clone()),
453 );
454
455 // Eq A y z
456 let eq_a_y_z = Term::App(
457 Box::new(Term::App(
458 Box::new(Term::App(
459 Box::new(Term::Global("Eq".to_string())),
460 Box::new(a.clone()),
461 )),
462 Box::new(y.clone()),
463 )),
464 Box::new(z.clone()),
465 );
466
467 // Eq A x z
468 let eq_a_x_z = Term::App(
469 Box::new(Term::App(
470 Box::new(Term::App(
471 Box::new(Term::Global("Eq".to_string())),
472 Box::new(a.clone()),
473 )),
474 Box::new(x.clone()),
475 )),
476 Box::new(z.clone()),
477 );
478
479 // Π(A:Type). Π(x:A). Π(y:A). Π(z:A). Eq A x y → Eq A y z → Eq A x z
480 let eq_trans_type = Term::Pi {
481 param: "A".to_string(),
482 param_type: Box::new(Term::Sort(Universe::Type(0))),
483 body_type: Box::new(Term::Pi {
484 param: "x".to_string(),
485 param_type: Box::new(a.clone()),
486 body_type: Box::new(Term::Pi {
487 param: "y".to_string(),
488 param_type: Box::new(a.clone()),
489 body_type: Box::new(Term::Pi {
490 param: "z".to_string(),
491 param_type: Box::new(a),
492 body_type: Box::new(Term::Pi {
493 param: "_".to_string(),
494 param_type: Box::new(eq_a_x_y),
495 body_type: Box::new(Term::Pi {
496 param: "_".to_string(),
497 param_type: Box::new(eq_a_y_z),
498 body_type: Box::new(eq_a_x_z),
499 }),
500 }),
501 }),
502 }),
503 }),
504 };
505
506 ctx.add_declaration("Eq_trans", eq_trans_type);
507 }
508
509 /// And : Prop → Prop → Prop
510 /// conj : Π(P : Prop). Π(Q : Prop). P → Q → And P Q
511 fn register_and(ctx: &mut Context) {
512 // And : Prop → Prop → Prop
513 let and_type = Term::Pi {
514 param: "P".to_string(),
515 param_type: Box::new(Term::Sort(Universe::Prop)),
516 body_type: Box::new(Term::Pi {
517 param: "Q".to_string(),
518 param_type: Box::new(Term::Sort(Universe::Prop)),
519 body_type: Box::new(Term::Sort(Universe::Prop)),
520 }),
521 };
522 ctx.add_inductive("And", and_type);
523
524 // conj : Π(P : Prop). Π(Q : Prop). P → Q → And P Q
525 let conj_type = Term::Pi {
526 param: "P".to_string(),
527 param_type: Box::new(Term::Sort(Universe::Prop)),
528 body_type: Box::new(Term::Pi {
529 param: "Q".to_string(),
530 param_type: Box::new(Term::Sort(Universe::Prop)),
531 body_type: Box::new(Term::Pi {
532 param: "p".to_string(),
533 param_type: Box::new(Term::Var("P".to_string())),
534 body_type: Box::new(Term::Pi {
535 param: "q".to_string(),
536 param_type: Box::new(Term::Var("Q".to_string())),
537 body_type: Box::new(Term::App(
538 Box::new(Term::App(
539 Box::new(Term::Global("And".to_string())),
540 Box::new(Term::Var("P".to_string())),
541 )),
542 Box::new(Term::Var("Q".to_string())),
543 )),
544 }),
545 }),
546 }),
547 };
548 ctx.add_constructor("conj", "And", conj_type);
549 }
550
551 /// Or : Prop → Prop → Prop
552 /// left : Π(P : Prop). Π(Q : Prop). P → Or P Q
553 /// right : Π(P : Prop). Π(Q : Prop). Q → Or P Q
554 fn register_or(ctx: &mut Context) {
555 // Or : Prop → Prop → Prop
556 let or_type = Term::Pi {
557 param: "P".to_string(),
558 param_type: Box::new(Term::Sort(Universe::Prop)),
559 body_type: Box::new(Term::Pi {
560 param: "Q".to_string(),
561 param_type: Box::new(Term::Sort(Universe::Prop)),
562 body_type: Box::new(Term::Sort(Universe::Prop)),
563 }),
564 };
565 ctx.add_inductive("Or", or_type);
566
567 // left : Π(P : Prop). Π(Q : Prop). P → Or P Q
568 let left_type = Term::Pi {
569 param: "P".to_string(),
570 param_type: Box::new(Term::Sort(Universe::Prop)),
571 body_type: Box::new(Term::Pi {
572 param: "Q".to_string(),
573 param_type: Box::new(Term::Sort(Universe::Prop)),
574 body_type: Box::new(Term::Pi {
575 param: "p".to_string(),
576 param_type: Box::new(Term::Var("P".to_string())),
577 body_type: Box::new(Term::App(
578 Box::new(Term::App(
579 Box::new(Term::Global("Or".to_string())),
580 Box::new(Term::Var("P".to_string())),
581 )),
582 Box::new(Term::Var("Q".to_string())),
583 )),
584 }),
585 }),
586 };
587 ctx.add_constructor("left", "Or", left_type);
588
589 // right : Π(P : Prop). Π(Q : Prop). Q → Or P Q
590 let right_type = Term::Pi {
591 param: "P".to_string(),
592 param_type: Box::new(Term::Sort(Universe::Prop)),
593 body_type: Box::new(Term::Pi {
594 param: "Q".to_string(),
595 param_type: Box::new(Term::Sort(Universe::Prop)),
596 body_type: Box::new(Term::Pi {
597 param: "q".to_string(),
598 param_type: Box::new(Term::Var("Q".to_string())),
599 body_type: Box::new(Term::App(
600 Box::new(Term::App(
601 Box::new(Term::Global("Or".to_string())),
602 Box::new(Term::Var("P".to_string())),
603 )),
604 Box::new(Term::Var("Q".to_string())),
605 )),
606 }),
607 }),
608 };
609 ctx.add_constructor("right", "Or", right_type);
610 }
611
612 /// Ex : Π(A : Type 0). (A → Prop) → Prop
613 /// witness : Π(A : Type 0). Π(P : A → Prop). Π(x : A). P x → Ex A P
614 ///
615 /// Ex is the existential type for propositions.
616 /// Ex A P means "there exists an x:A such that P(x)"
617 fn register_ex(ctx: &mut Context) {
618 // Ex : Π(A : Type 0). (A → Prop) → Prop
619 let ex_type = Term::Pi {
620 param: "A".to_string(),
621 param_type: Box::new(Term::Sort(Universe::Type(0))),
622 body_type: Box::new(Term::Pi {
623 param: "P".to_string(),
624 param_type: Box::new(Term::Pi {
625 param: "_".to_string(),
626 param_type: Box::new(Term::Var("A".to_string())),
627 body_type: Box::new(Term::Sort(Universe::Prop)),
628 }),
629 body_type: Box::new(Term::Sort(Universe::Prop)),
630 }),
631 };
632 ctx.add_inductive("Ex", ex_type);
633
634 // witness : Π(A : Type 0). Π(P : A → Prop). Π(x : A). P x → Ex A P
635 //
636 // To construct an existential proof, provide:
637 // - A: the type being quantified over
638 // - P: the predicate
639 // - x: the witness (an element of A)
640 // - proof: evidence that P(x) holds
641 let a = Term::Var("A".to_string());
642 let p = Term::Var("P".to_string());
643 let x = Term::Var("x".to_string());
644
645 // P x = P applied to x
646 let p_x = Term::App(Box::new(p.clone()), Box::new(x.clone()));
647
648 // Ex A P = Ex applied to A, then to P
649 let ex_a_p = Term::App(
650 Box::new(Term::App(
651 Box::new(Term::Global("Ex".to_string())),
652 Box::new(a.clone()),
653 )),
654 Box::new(p.clone()),
655 );
656
657 let witness_type = Term::Pi {
658 param: "A".to_string(),
659 param_type: Box::new(Term::Sort(Universe::Type(0))),
660 body_type: Box::new(Term::Pi {
661 param: "P".to_string(),
662 param_type: Box::new(Term::Pi {
663 param: "_".to_string(),
664 param_type: Box::new(a.clone()),
665 body_type: Box::new(Term::Sort(Universe::Prop)),
666 }),
667 body_type: Box::new(Term::Pi {
668 param: "x".to_string(),
669 param_type: Box::new(a),
670 body_type: Box::new(Term::Pi {
671 param: "_".to_string(),
672 param_type: Box::new(p_x),
673 body_type: Box::new(ex_a_p),
674 }),
675 }),
676 }),
677 };
678 ctx.add_constructor("witness", "Ex", witness_type);
679 }
680
681 // -------------------------------------------------------------------------
682 // Reflection System (Deep Embedding)
683 // -------------------------------------------------------------------------
684
685 /// Reflection types for deep embedding.
686 ///
687 /// Univ : Type 0 (representation of universes)
688 /// Syntax : Type 0 (representation of terms with De Bruijn indices)
689 /// syn_size : Syntax -> Int (compute size of syntax tree)
690 /// syn_max_var : Syntax -> Int (compute max free variable index)
691 fn register_reflection(ctx: &mut Context) {
692 Self::register_univ(ctx);
693 Self::register_syntax(ctx);
694 Self::register_syn_size(ctx);
695 Self::register_syn_max_var(ctx);
696 Self::register_syn_lift(ctx);
697 Self::register_syn_subst(ctx);
698 Self::register_syn_beta(ctx);
699 Self::register_syn_step(ctx);
700 Self::register_syn_eval(ctx);
701 Self::register_syn_quote(ctx);
702 Self::register_syn_diag(ctx);
703 Self::register_derivation(ctx);
704 Self::register_concludes(ctx);
705 Self::register_try_refl(ctx);
706 Self::register_try_compute(ctx);
707 Self::register_try_cong(ctx);
708 Self::register_tact_fail(ctx);
709 Self::register_tact_orelse(ctx);
710 Self::register_tact_try(ctx);
711 Self::register_tact_repeat(ctx);
712 Self::register_tact_then(ctx);
713 Self::register_tact_first(ctx);
714 Self::register_tact_solve(ctx);
715 Self::register_try_ring(ctx);
716 Self::register_try_lia(ctx);
717 Self::register_try_cc(ctx);
718 Self::register_try_simp(ctx);
719 Self::register_try_omega(ctx);
720 Self::register_try_auto(ctx);
721 Self::register_try_induction(ctx);
722 Self::register_induction_helpers(ctx);
723 Self::register_try_inversion_tactic(ctx);
724 Self::register_operator_tactics(ctx);
725 }
726
727 /// Univ : Type 0 (representation of universes)
728 /// UProp : Univ
729 /// UType : Int -> Univ
730 fn register_univ(ctx: &mut Context) {
731 let univ = Term::Global("Univ".to_string());
732 let int = Term::Global("Int".to_string());
733
734 // Univ : Type 0
735 ctx.add_inductive("Univ", Term::Sort(Universe::Type(0)));
736
737 // UProp : Univ
738 ctx.add_constructor("UProp", "Univ", univ.clone());
739
740 // UType : Int -> Univ
741 ctx.add_constructor(
742 "UType",
743 "Univ",
744 Term::Pi {
745 param: "_".to_string(),
746 param_type: Box::new(int),
747 body_type: Box::new(univ),
748 },
749 );
750 }
751
752 /// Syntax : Type 0 (representation of terms with De Bruijn indices)
753 ///
754 /// SVar : Int -> Syntax (De Bruijn variable index)
755 /// SGlobal : Int -> Syntax (global reference by ID)
756 /// SSort : Univ -> Syntax (universe)
757 /// SApp : Syntax -> Syntax -> Syntax (application)
758 /// SLam : Syntax -> Syntax -> Syntax (lambda: param_type, body)
759 /// SPi : Syntax -> Syntax -> Syntax (pi: param_type, body_type)
760 fn register_syntax(ctx: &mut Context) {
761 let syntax = Term::Global("Syntax".to_string());
762 let int = Term::Global("Int".to_string());
763 let univ = Term::Global("Univ".to_string());
764
765 // Syntax : Type 0
766 ctx.add_inductive("Syntax", Term::Sort(Universe::Type(0)));
767
768 // SVar : Int -> Syntax (De Bruijn index)
769 ctx.add_constructor(
770 "SVar",
771 "Syntax",
772 Term::Pi {
773 param: "_".to_string(),
774 param_type: Box::new(int.clone()),
775 body_type: Box::new(syntax.clone()),
776 },
777 );
778
779 // SGlobal : Int -> Syntax (global reference by ID)
780 ctx.add_constructor(
781 "SGlobal",
782 "Syntax",
783 Term::Pi {
784 param: "_".to_string(),
785 param_type: Box::new(int.clone()),
786 body_type: Box::new(syntax.clone()),
787 },
788 );
789
790 // SSort : Univ -> Syntax
791 ctx.add_constructor(
792 "SSort",
793 "Syntax",
794 Term::Pi {
795 param: "_".to_string(),
796 param_type: Box::new(univ),
797 body_type: Box::new(syntax.clone()),
798 },
799 );
800
801 // SApp : Syntax -> Syntax -> Syntax
802 ctx.add_constructor(
803 "SApp",
804 "Syntax",
805 Term::Pi {
806 param: "_".to_string(),
807 param_type: Box::new(syntax.clone()),
808 body_type: Box::new(Term::Pi {
809 param: "_".to_string(),
810 param_type: Box::new(syntax.clone()),
811 body_type: Box::new(syntax.clone()),
812 }),
813 },
814 );
815
816 // SLam : Syntax -> Syntax -> Syntax (param_type, body)
817 ctx.add_constructor(
818 "SLam",
819 "Syntax",
820 Term::Pi {
821 param: "_".to_string(),
822 param_type: Box::new(syntax.clone()),
823 body_type: Box::new(Term::Pi {
824 param: "_".to_string(),
825 param_type: Box::new(syntax.clone()),
826 body_type: Box::new(syntax.clone()),
827 }),
828 },
829 );
830
831 // SPi : Syntax -> Syntax -> Syntax (param_type, body_type)
832 ctx.add_constructor(
833 "SPi",
834 "Syntax",
835 Term::Pi {
836 param: "_".to_string(),
837 param_type: Box::new(syntax.clone()),
838 body_type: Box::new(Term::Pi {
839 param: "_".to_string(),
840 param_type: Box::new(syntax.clone()),
841 body_type: Box::new(syntax.clone()),
842 }),
843 },
844 );
845
846 // SLit : Int -> Syntax (integer literal in quoted syntax)
847 ctx.add_constructor(
848 "SLit",
849 "Syntax",
850 Term::Pi {
851 param: "_".to_string(),
852 param_type: Box::new(int),
853 body_type: Box::new(syntax.clone()),
854 },
855 );
856
857 // SName : Text -> Syntax (named global reference)
858 let text = Term::Global("Text".to_string());
859 ctx.add_constructor(
860 "SName",
861 "Syntax",
862 Term::Pi {
863 param: "_".to_string(),
864 param_type: Box::new(text),
865 body_type: Box::new(syntax),
866 },
867 );
868 }
869
870 /// syn_size : Syntax -> Int
871 ///
872 /// Computes the number of nodes in a syntax tree.
873 /// Computational behavior defined in reduction.rs.
874 fn register_syn_size(ctx: &mut Context) {
875 let syntax = Term::Global("Syntax".to_string());
876 let int = Term::Global("Int".to_string());
877
878 // syn_size : Syntax -> Int
879 let syn_size_type = Term::Pi {
880 param: "_".to_string(),
881 param_type: Box::new(syntax),
882 body_type: Box::new(int),
883 };
884
885 ctx.add_declaration("syn_size", syn_size_type);
886 }
887
888 /// syn_max_var : Syntax -> Int
889 ///
890 /// Returns the maximum free variable index in a syntax term.
891 /// Returns -1 if the term is closed (all variables bound).
892 /// Computational behavior defined in reduction.rs.
893 fn register_syn_max_var(ctx: &mut Context) {
894 let syntax = Term::Global("Syntax".to_string());
895 let int = Term::Global("Int".to_string());
896
897 let syn_max_var_type = Term::Pi {
898 param: "_".to_string(),
899 param_type: Box::new(syntax),
900 body_type: Box::new(int),
901 };
902
903 ctx.add_declaration("syn_max_var", syn_max_var_type);
904 }
905
906 // -------------------------------------------------------------------------
907 // De Bruijn Operations (Substitution)
908 // -------------------------------------------------------------------------
909
910 /// syn_lift : Int -> Int -> Syntax -> Syntax
911 ///
912 /// Shifts free variables (index >= cutoff) by amount.
913 /// - syn_lift amount cutoff term
914 /// - Variables with index < cutoff are bound -> unchanged
915 /// - Variables with index >= cutoff are free -> add amount
916 /// Computational behavior defined in reduction.rs.
917 fn register_syn_lift(ctx: &mut Context) {
918 let syntax = Term::Global("Syntax".to_string());
919 let int = Term::Global("Int".to_string());
920
921 // syn_lift : Int -> Int -> Syntax -> Syntax
922 let syn_lift_type = Term::Pi {
923 param: "_".to_string(),
924 param_type: Box::new(int.clone()),
925 body_type: Box::new(Term::Pi {
926 param: "_".to_string(),
927 param_type: Box::new(int),
928 body_type: Box::new(Term::Pi {
929 param: "_".to_string(),
930 param_type: Box::new(syntax.clone()),
931 body_type: Box::new(syntax),
932 }),
933 }),
934 };
935
936 ctx.add_declaration("syn_lift", syn_lift_type);
937 }
938
939 /// syn_subst : Syntax -> Int -> Syntax -> Syntax
940 ///
941 /// Substitutes replacement for variable at index in term.
942 /// - syn_subst replacement index term
943 /// - If term is SVar k and k == index, return replacement
944 /// - If term is SVar k and k != index, return term unchanged
945 /// - For binders, increment index and lift replacement
946 /// Computational behavior defined in reduction.rs.
947 fn register_syn_subst(ctx: &mut Context) {
948 let syntax = Term::Global("Syntax".to_string());
949 let int = Term::Global("Int".to_string());
950
951 // syn_subst : Syntax -> Int -> Syntax -> Syntax
952 let syn_subst_type = Term::Pi {
953 param: "_".to_string(),
954 param_type: Box::new(syntax.clone()),
955 body_type: Box::new(Term::Pi {
956 param: "_".to_string(),
957 param_type: Box::new(int),
958 body_type: Box::new(Term::Pi {
959 param: "_".to_string(),
960 param_type: Box::new(syntax.clone()),
961 body_type: Box::new(syntax),
962 }),
963 }),
964 };
965
966 ctx.add_declaration("syn_subst", syn_subst_type);
967 }
968
969 // -------------------------------------------------------------------------
970 // Beta Reduction (Computation)
971 // -------------------------------------------------------------------------
972
973 /// syn_beta : Syntax -> Syntax -> Syntax
974 ///
975 /// Beta reduction: substitute arg for variable 0 in body.
976 /// - syn_beta body arg = syn_subst arg 0 body
977 /// Computational behavior defined in reduction.rs.
978 fn register_syn_beta(ctx: &mut Context) {
979 let syntax = Term::Global("Syntax".to_string());
980
981 // syn_beta : Syntax -> Syntax -> Syntax
982 let syn_beta_type = Term::Pi {
983 param: "_".to_string(),
984 param_type: Box::new(syntax.clone()),
985 body_type: Box::new(Term::Pi {
986 param: "_".to_string(),
987 param_type: Box::new(syntax.clone()),
988 body_type: Box::new(syntax),
989 }),
990 };
991
992 ctx.add_declaration("syn_beta", syn_beta_type);
993 }
994
995 /// syn_step : Syntax -> Syntax
996 ///
997 /// Single-step head reduction. Finds first beta redex and reduces.
998 /// - If SApp (SLam T body) arg: perform beta reduction
999 /// - If SApp f x where f is reducible: reduce f
1000 /// - Otherwise: return unchanged (stuck or value)
1001 /// Computational behavior defined in reduction.rs.
1002 fn register_syn_step(ctx: &mut Context) {
1003 let syntax = Term::Global("Syntax".to_string());
1004
1005 // syn_step : Syntax -> Syntax
1006 let syn_step_type = Term::Pi {
1007 param: "_".to_string(),
1008 param_type: Box::new(syntax.clone()),
1009 body_type: Box::new(syntax),
1010 };
1011
1012 ctx.add_declaration("syn_step", syn_step_type);
1013 }
1014
1015 // -------------------------------------------------------------------------
1016 // Bounded Evaluation
1017 // -------------------------------------------------------------------------
1018
1019 /// syn_eval : Int -> Syntax -> Syntax
1020 ///
1021 /// Bounded evaluation: reduce for up to N steps.
1022 /// - syn_eval fuel term
1023 /// - If fuel <= 0: return term unchanged
1024 /// - Otherwise: step and repeat until normal form or fuel exhausted
1025 /// Computational behavior defined in reduction.rs.
1026 fn register_syn_eval(ctx: &mut Context) {
1027 let syntax = Term::Global("Syntax".to_string());
1028 let int = Term::Global("Int".to_string());
1029
1030 // syn_eval : Int -> Syntax -> Syntax
1031 let syn_eval_type = Term::Pi {
1032 param: "_".to_string(),
1033 param_type: Box::new(int),
1034 body_type: Box::new(Term::Pi {
1035 param: "_".to_string(),
1036 param_type: Box::new(syntax.clone()),
1037 body_type: Box::new(syntax),
1038 }),
1039 };
1040
1041 ctx.add_declaration("syn_eval", syn_eval_type);
1042 }
1043
1044 // -------------------------------------------------------------------------
1045 // Reification (Quote)
1046 // -------------------------------------------------------------------------
1047
1048 /// syn_quote : Syntax -> Syntax
1049 ///
1050 /// Converts a Syntax value to Syntax code that constructs it.
1051 /// Computational behavior defined in reduction.rs.
1052 fn register_syn_quote(ctx: &mut Context) {
1053 let syntax = Term::Global("Syntax".to_string());
1054
1055 // syn_quote : Syntax -> Syntax
1056 let syn_quote_type = Term::Pi {
1057 param: "_".to_string(),
1058 param_type: Box::new(syntax.clone()),
1059 body_type: Box::new(syntax),
1060 };
1061
1062 ctx.add_declaration("syn_quote", syn_quote_type);
1063 }
1064
1065 // -------------------------------------------------------------------------
1066 // Diagonalization (Self-Reference)
1067 // -------------------------------------------------------------------------
1068
1069 /// syn_diag : Syntax -> Syntax
1070 ///
1071 /// The diagonal function: syn_diag x = syn_subst (syn_quote x) 0 x
1072 /// This is the key construction for self-reference and the diagonal lemma.
1073 fn register_syn_diag(ctx: &mut Context) {
1074 let syntax = Term::Global("Syntax".to_string());
1075
1076 let syn_diag_type = Term::Pi {
1077 param: "_".to_string(),
1078 param_type: Box::new(syntax.clone()),
1079 body_type: Box::new(syntax),
1080 };
1081
1082 ctx.add_declaration("syn_diag", syn_diag_type);
1083 }
1084
1085 // -------------------------------------------------------------------------
1086 // Inference Rules (Proof Trees)
1087 // -------------------------------------------------------------------------
1088
1089 /// Derivation : Type 0 (deep embedding of proof trees)
1090 ///
1091 /// DAxiom : Syntax -> Derivation (introduce an axiom)
1092 /// DModusPonens : Derivation -> Derivation -> Derivation (A->B, A |- B)
1093 /// DUnivIntro : Derivation -> Derivation (P(x) |- forall x. P(x))
1094 /// DUnivElim : Derivation -> Syntax -> Derivation (forall x. P(x), t |- P(t))
1095 fn register_derivation(ctx: &mut Context) {
1096 let syntax = Term::Global("Syntax".to_string());
1097 let derivation = Term::Global("Derivation".to_string());
1098
1099 // Derivation : Type 0
1100 ctx.add_inductive("Derivation", Term::Sort(Universe::Type(0)));
1101
1102 // DAxiom : Syntax -> Derivation
1103 ctx.add_constructor(
1104 "DAxiom",
1105 "Derivation",
1106 Term::Pi {
1107 param: "_".to_string(),
1108 param_type: Box::new(syntax.clone()),
1109 body_type: Box::new(derivation.clone()),
1110 },
1111 );
1112
1113 // DModusPonens : Derivation -> Derivation -> Derivation
1114 ctx.add_constructor(
1115 "DModusPonens",
1116 "Derivation",
1117 Term::Pi {
1118 param: "_".to_string(),
1119 param_type: Box::new(derivation.clone()),
1120 body_type: Box::new(Term::Pi {
1121 param: "_".to_string(),
1122 param_type: Box::new(derivation.clone()),
1123 body_type: Box::new(derivation.clone()),
1124 }),
1125 },
1126 );
1127
1128 // DUnivIntro : Derivation -> Derivation
1129 ctx.add_constructor(
1130 "DUnivIntro",
1131 "Derivation",
1132 Term::Pi {
1133 param: "_".to_string(),
1134 param_type: Box::new(derivation.clone()),
1135 body_type: Box::new(derivation.clone()),
1136 },
1137 );
1138
1139 // DUnivElim : Derivation -> Syntax -> Derivation
1140 ctx.add_constructor(
1141 "DUnivElim",
1142 "Derivation",
1143 Term::Pi {
1144 param: "_".to_string(),
1145 param_type: Box::new(derivation.clone()),
1146 body_type: Box::new(Term::Pi {
1147 param: "_".to_string(),
1148 param_type: Box::new(syntax.clone()),
1149 body_type: Box::new(derivation.clone()),
1150 }),
1151 },
1152 );
1153
1154 // DRefl : Syntax -> Syntax -> Derivation
1155 // DRefl T a proves (Eq T a a)
1156 ctx.add_constructor(
1157 "DRefl",
1158 "Derivation",
1159 Term::Pi {
1160 param: "_".to_string(),
1161 param_type: Box::new(syntax.clone()),
1162 body_type: Box::new(Term::Pi {
1163 param: "_".to_string(),
1164 param_type: Box::new(syntax.clone()),
1165 body_type: Box::new(derivation.clone()),
1166 }),
1167 },
1168 );
1169
1170 // DInduction : Syntax -> Derivation -> Derivation -> Derivation
1171 // DInduction motive base step proves (∀n:Nat. motive n) via induction
1172 // - motive: λn:Nat. P(n) as Syntax
1173 // - base: proof of P(Zero)
1174 // - step: proof of ∀k:Nat. P(k) → P(Succ k)
1175 ctx.add_constructor(
1176 "DInduction",
1177 "Derivation",
1178 Term::Pi {
1179 param: "_".to_string(),
1180 param_type: Box::new(syntax.clone()), // motive
1181 body_type: Box::new(Term::Pi {
1182 param: "_".to_string(),
1183 param_type: Box::new(derivation.clone()), // base proof
1184 body_type: Box::new(Term::Pi {
1185 param: "_".to_string(),
1186 param_type: Box::new(derivation.clone()), // step proof
1187 body_type: Box::new(derivation.clone()),
1188 }),
1189 }),
1190 },
1191 );
1192
1193 // DCompute : Syntax -> Derivation
1194 // DCompute goal proves goal by computation
1195 // - Validates that goal is (Eq T A B) and eval(A) == eval(B)
1196 ctx.add_constructor(
1197 "DCompute",
1198 "Derivation",
1199 Term::Pi {
1200 param: "_".to_string(),
1201 param_type: Box::new(syntax.clone()),
1202 body_type: Box::new(derivation.clone()),
1203 },
1204 );
1205
1206 // DCong : Syntax -> Derivation -> Derivation
1207 // DCong context eq_proof proves congruence
1208 // - context: SLam T body (function with hole at SVar 0)
1209 // - eq_proof: proof of (Eq T a b)
1210 // - Result: proof of (Eq T (body[0:=a]) (body[0:=b]))
1211 ctx.add_constructor(
1212 "DCong",
1213 "Derivation",
1214 Term::Pi {
1215 param: "_".to_string(),
1216 param_type: Box::new(syntax.clone()), // context
1217 body_type: Box::new(Term::Pi {
1218 param: "_".to_string(),
1219 param_type: Box::new(derivation.clone()), // eq_proof
1220 body_type: Box::new(derivation.clone()),
1221 }),
1222 },
1223 );
1224
1225 // DCase : Derivation -> Derivation -> Derivation
1226 // Cons cell for case proofs in DElim
1227 ctx.add_constructor(
1228 "DCase",
1229 "Derivation",
1230 Term::Pi {
1231 param: "_".to_string(),
1232 param_type: Box::new(derivation.clone()), // head (case proof)
1233 body_type: Box::new(Term::Pi {
1234 param: "_".to_string(),
1235 param_type: Box::new(derivation.clone()), // tail (rest of cases)
1236 body_type: Box::new(derivation.clone()),
1237 }),
1238 },
1239 );
1240
1241 // DCaseEnd : Derivation
1242 // Nil for case proofs in DElim
1243 ctx.add_constructor("DCaseEnd", "Derivation", derivation.clone());
1244
1245 // DElim : Syntax -> Syntax -> Derivation -> Derivation
1246 // Generic elimination for any inductive type
1247 // - ind_type: the inductive type (e.g., SName "Nat" or SApp (SName "List") A)
1248 // - motive: SLam param_type body (the property to prove)
1249 // - cases: DCase chain with one proof per constructor
1250 ctx.add_constructor(
1251 "DElim",
1252 "Derivation",
1253 Term::Pi {
1254 param: "_".to_string(),
1255 param_type: Box::new(syntax.clone()), // ind_type
1256 body_type: Box::new(Term::Pi {
1257 param: "_".to_string(),
1258 param_type: Box::new(syntax.clone()), // motive
1259 body_type: Box::new(Term::Pi {
1260 param: "_".to_string(),
1261 param_type: Box::new(derivation.clone()), // cases
1262 body_type: Box::new(derivation.clone()),
1263 }),
1264 }),
1265 },
1266 );
1267
1268 // DInversion : Syntax -> Derivation
1269 // Proves False when no constructor can build the given hypothesis.
1270 // - hyp_type: the Syntax representation of the hypothesis (e.g., SApp (SName "Even") three)
1271 // - Returns proof of False if verified that all constructors are impossible
1272 ctx.add_constructor(
1273 "DInversion",
1274 "Derivation",
1275 Term::Pi {
1276 param: "_".to_string(),
1277 param_type: Box::new(syntax.clone()),
1278 body_type: Box::new(derivation.clone()),
1279 },
1280 );
1281
1282 // DRewrite : Derivation -> Syntax -> Syntax -> Derivation
1283 // Stores: eq_proof, original_goal, new_goal
1284 // Given eq_proof : Eq A x y, rewrites goal by replacing x with y
1285 ctx.add_constructor(
1286 "DRewrite",
1287 "Derivation",
1288 Term::Pi {
1289 param: "_".to_string(),
1290 param_type: Box::new(derivation.clone()), // eq_proof
1291 body_type: Box::new(Term::Pi {
1292 param: "_".to_string(),
1293 param_type: Box::new(syntax.clone()), // original_goal
1294 body_type: Box::new(Term::Pi {
1295 param: "_".to_string(),
1296 param_type: Box::new(syntax.clone()), // new_goal
1297 body_type: Box::new(derivation.clone()),
1298 }),
1299 }),
1300 },
1301 );
1302
1303 // DDestruct : Syntax -> Syntax -> Derivation -> Derivation
1304 // Case analysis without induction hypotheses
1305 // - ind_type: the inductive type
1306 // - motive: the property to prove
1307 // - cases: DCase chain with proofs for each constructor
1308 ctx.add_constructor(
1309 "DDestruct",
1310 "Derivation",
1311 Term::Pi {
1312 param: "_".to_string(),
1313 param_type: Box::new(syntax.clone()), // ind_type
1314 body_type: Box::new(Term::Pi {
1315 param: "_".to_string(),
1316 param_type: Box::new(syntax.clone()), // motive
1317 body_type: Box::new(Term::Pi {
1318 param: "_".to_string(),
1319 param_type: Box::new(derivation.clone()), // cases
1320 body_type: Box::new(derivation.clone()),
1321 }),
1322 }),
1323 },
1324 );
1325
1326 // DApply : Syntax -> Derivation -> Syntax -> Syntax -> Derivation
1327 // Manual backward chaining
1328 // - hyp_name: name of hypothesis
1329 // - hyp_proof: proof of the hypothesis
1330 // - original_goal: the goal we started with
1331 // - new_goal: the antecedent we need to prove
1332 ctx.add_constructor(
1333 "DApply",
1334 "Derivation",
1335 Term::Pi {
1336 param: "_".to_string(),
1337 param_type: Box::new(syntax.clone()), // hyp_name
1338 body_type: Box::new(Term::Pi {
1339 param: "_".to_string(),
1340 param_type: Box::new(derivation.clone()), // hyp_proof
1341 body_type: Box::new(Term::Pi {
1342 param: "_".to_string(),
1343 param_type: Box::new(syntax.clone()), // original_goal
1344 body_type: Box::new(Term::Pi {
1345 param: "_".to_string(),
1346 param_type: Box::new(syntax), // new_goal
1347 body_type: Box::new(derivation),
1348 }),
1349 }),
1350 }),
1351 },
1352 );
1353 }
1354
1355 /// concludes : Derivation -> Syntax
1356 ///
1357 /// Extracts the conclusion from a derivation.
1358 /// Computational behavior defined in reduction.rs.
1359 fn register_concludes(ctx: &mut Context) {
1360 let derivation = Term::Global("Derivation".to_string());
1361 let syntax = Term::Global("Syntax".to_string());
1362
1363 // concludes : Derivation -> Syntax
1364 let concludes_type = Term::Pi {
1365 param: "_".to_string(),
1366 param_type: Box::new(derivation),
1367 body_type: Box::new(syntax),
1368 };
1369
1370 ctx.add_declaration("concludes", concludes_type);
1371 }
1372
1373 // -------------------------------------------------------------------------
1374 // Core Tactics
1375 // -------------------------------------------------------------------------
1376
1377 /// try_refl : Syntax -> Derivation
1378 ///
1379 /// Reflexivity tactic: given a goal, try to prove it by reflexivity.
1380 /// - If goal matches (Eq T a b) and a == b, returns DRefl T a
1381 /// - Otherwise returns DAxiom (SName "Error")
1382 /// Computational behavior defined in reduction.rs.
1383 fn register_try_refl(ctx: &mut Context) {
1384 let syntax = Term::Global("Syntax".to_string());
1385 let derivation = Term::Global("Derivation".to_string());
1386
1387 // try_refl : Syntax -> Derivation
1388 let try_refl_type = Term::Pi {
1389 param: "_".to_string(),
1390 param_type: Box::new(syntax),
1391 body_type: Box::new(derivation),
1392 };
1393
1394 ctx.add_declaration("try_refl", try_refl_type);
1395 }
1396
1397 /// try_compute : Syntax -> Derivation
1398 ///
1399 /// Computation tactic: given a goal (Eq T A B), proves it by evaluating
1400 /// both sides and checking equality.
1401 /// Returns DCompute goal.
1402 /// Computational behavior defined in reduction.rs.
1403 fn register_try_compute(ctx: &mut Context) {
1404 let syntax = Term::Global("Syntax".to_string());
1405 let derivation = Term::Global("Derivation".to_string());
1406
1407 // try_compute : Syntax -> Derivation
1408 let try_compute_type = Term::Pi {
1409 param: "_".to_string(),
1410 param_type: Box::new(syntax),
1411 body_type: Box::new(derivation),
1412 };
1413
1414 ctx.add_declaration("try_compute", try_compute_type);
1415 }
1416
1417 /// try_cong : Syntax -> Derivation -> Derivation
1418 ///
1419 /// Congruence tactic: given a context (SLam T body) and proof of (Eq T a b),
1420 /// produces proof of (Eq T (body[0:=a]) (body[0:=b])).
1421 /// Returns DCong context eq_proof.
1422 /// Computational behavior defined in reduction.rs.
1423 fn register_try_cong(ctx: &mut Context) {
1424 let syntax = Term::Global("Syntax".to_string());
1425 let derivation = Term::Global("Derivation".to_string());
1426
1427 // try_cong : Syntax -> Derivation -> Derivation
1428 let try_cong_type = Term::Pi {
1429 param: "_".to_string(),
1430 param_type: Box::new(syntax), // context
1431 body_type: Box::new(Term::Pi {
1432 param: "_".to_string(),
1433 param_type: Box::new(derivation.clone()), // eq_proof
1434 body_type: Box::new(derivation),
1435 }),
1436 };
1437
1438 ctx.add_declaration("try_cong", try_cong_type);
1439 }
1440
1441 // -------------------------------------------------------------------------
1442 // Tactic Combinators
1443 // -------------------------------------------------------------------------
1444
1445 /// tact_fail : Syntax -> Derivation
1446 ///
1447 /// A tactic that always fails by returning DAxiom (SName "Error").
1448 /// Useful for testing combinators and as a base case.
1449 /// Computational behavior defined in reduction.rs.
1450 fn register_tact_fail(ctx: &mut Context) {
1451 let syntax = Term::Global("Syntax".to_string());
1452 let derivation = Term::Global("Derivation".to_string());
1453
1454 // tact_fail : Syntax -> Derivation
1455 let tact_fail_type = Term::Pi {
1456 param: "_".to_string(),
1457 param_type: Box::new(syntax),
1458 body_type: Box::new(derivation),
1459 };
1460
1461 ctx.add_declaration("tact_fail", tact_fail_type);
1462 }
1463
1464 /// tact_orelse : (Syntax -> Derivation) -> (Syntax -> Derivation) -> Syntax -> Derivation
1465 ///
1466 /// Tactic combinator: try first tactic, if it fails (concludes to Error) try second.
1467 /// Enables composition of tactics with fallback behavior.
1468 /// Computational behavior defined in reduction.rs.
1469 fn register_tact_orelse(ctx: &mut Context) {
1470 let syntax = Term::Global("Syntax".to_string());
1471 let derivation = Term::Global("Derivation".to_string());
1472
1473 // Tactic type: Syntax -> Derivation
1474 let tactic_type = Term::Pi {
1475 param: "_".to_string(),
1476 param_type: Box::new(syntax.clone()),
1477 body_type: Box::new(derivation.clone()),
1478 };
1479
1480 // tact_orelse : (Syntax -> Derivation) -> (Syntax -> Derivation) -> Syntax -> Derivation
1481 let tact_orelse_type = Term::Pi {
1482 param: "_".to_string(),
1483 param_type: Box::new(tactic_type.clone()), // t1
1484 body_type: Box::new(Term::Pi {
1485 param: "_".to_string(),
1486 param_type: Box::new(tactic_type), // t2
1487 body_type: Box::new(Term::Pi {
1488 param: "_".to_string(),
1489 param_type: Box::new(syntax), // goal
1490 body_type: Box::new(derivation),
1491 }),
1492 }),
1493 };
1494
1495 ctx.add_declaration("tact_orelse", tact_orelse_type);
1496 }
1497
1498 /// tact_try : (Syntax -> Derivation) -> Syntax -> Derivation
1499 ///
1500 /// Tactic combinator: try the tactic, but never fail.
1501 /// If the tactic fails (concludes to Error), return identity (DAxiom goal).
1502 /// Computational behavior defined in reduction.rs.
1503 fn register_tact_try(ctx: &mut Context) {
1504 let syntax = Term::Global("Syntax".to_string());
1505 let derivation = Term::Global("Derivation".to_string());
1506
1507 // Tactic type: Syntax -> Derivation
1508 let tactic_type = Term::Pi {
1509 param: "_".to_string(),
1510 param_type: Box::new(syntax.clone()),
1511 body_type: Box::new(derivation.clone()),
1512 };
1513
1514 // tact_try : (Syntax -> Derivation) -> Syntax -> Derivation
1515 let tact_try_type = Term::Pi {
1516 param: "_".to_string(),
1517 param_type: Box::new(tactic_type), // t
1518 body_type: Box::new(Term::Pi {
1519 param: "_".to_string(),
1520 param_type: Box::new(syntax),
1521 body_type: Box::new(derivation),
1522 }),
1523 };
1524
1525 ctx.add_declaration("tact_try", tact_try_type);
1526 }
1527
1528 /// tact_repeat : (Syntax -> Derivation) -> Syntax -> Derivation
1529 ///
1530 /// Tactic combinator: apply tactic repeatedly until it fails or makes no progress.
1531 /// Returns identity if tactic fails immediately.
1532 /// Computational behavior defined in reduction.rs.
1533 fn register_tact_repeat(ctx: &mut Context) {
1534 let syntax = Term::Global("Syntax".to_string());
1535 let derivation = Term::Global("Derivation".to_string());
1536
1537 // Tactic type: Syntax -> Derivation
1538 let tactic_type = Term::Pi {
1539 param: "_".to_string(),
1540 param_type: Box::new(syntax.clone()),
1541 body_type: Box::new(derivation.clone()),
1542 };
1543
1544 // tact_repeat : (Syntax -> Derivation) -> Syntax -> Derivation
1545 let tact_repeat_type = Term::Pi {
1546 param: "_".to_string(),
1547 param_type: Box::new(tactic_type), // t
1548 body_type: Box::new(Term::Pi {
1549 param: "_".to_string(),
1550 param_type: Box::new(syntax),
1551 body_type: Box::new(derivation),
1552 }),
1553 };
1554
1555 ctx.add_declaration("tact_repeat", tact_repeat_type);
1556 }
1557
1558 /// tact_then : (Syntax -> Derivation) -> (Syntax -> Derivation) -> Syntax -> Derivation
1559 ///
1560 /// Tactic combinator: sequence two tactics (the ";" operator).
1561 /// Apply t1 to goal, then apply t2 to the result.
1562 /// Fails if either tactic fails.
1563 /// Computational behavior defined in reduction.rs.
1564 fn register_tact_then(ctx: &mut Context) {
1565 let syntax = Term::Global("Syntax".to_string());
1566 let derivation = Term::Global("Derivation".to_string());
1567
1568 // Tactic type: Syntax -> Derivation
1569 let tactic_type = Term::Pi {
1570 param: "_".to_string(),
1571 param_type: Box::new(syntax.clone()),
1572 body_type: Box::new(derivation.clone()),
1573 };
1574
1575 // tact_then : (Syntax -> Derivation) -> (Syntax -> Derivation) -> Syntax -> Derivation
1576 let tact_then_type = Term::Pi {
1577 param: "_".to_string(),
1578 param_type: Box::new(tactic_type.clone()), // t1
1579 body_type: Box::new(Term::Pi {
1580 param: "_".to_string(),
1581 param_type: Box::new(tactic_type), // t2
1582 body_type: Box::new(Term::Pi {
1583 param: "_".to_string(),
1584 param_type: Box::new(syntax),
1585 body_type: Box::new(derivation),
1586 }),
1587 }),
1588 };
1589
1590 ctx.add_declaration("tact_then", tact_then_type);
1591 }
1592
1593 /// tact_first : TList (Syntax -> Derivation) -> Syntax -> Derivation
1594 ///
1595 /// Tactic combinator: try tactics from a list until one succeeds.
1596 /// Returns Error if all tactics fail or list is empty.
1597 /// Computational behavior defined in reduction.rs.
1598 fn register_tact_first(ctx: &mut Context) {
1599 let syntax = Term::Global("Syntax".to_string());
1600 let derivation = Term::Global("Derivation".to_string());
1601
1602 // Tactic type: Syntax -> Derivation
1603 let tactic_type = Term::Pi {
1604 param: "_".to_string(),
1605 param_type: Box::new(syntax.clone()),
1606 body_type: Box::new(derivation.clone()),
1607 };
1608
1609 // TList (Syntax -> Derivation)
1610 let tactic_list_type = Term::App(
1611 Box::new(Term::Global("TList".to_string())),
1612 Box::new(tactic_type),
1613 );
1614
1615 // tact_first : TList (Syntax -> Derivation) -> Syntax -> Derivation
1616 let tact_first_type = Term::Pi {
1617 param: "_".to_string(),
1618 param_type: Box::new(tactic_list_type), // tactics
1619 body_type: Box::new(Term::Pi {
1620 param: "_".to_string(),
1621 param_type: Box::new(syntax),
1622 body_type: Box::new(derivation),
1623 }),
1624 };
1625
1626 ctx.add_declaration("tact_first", tact_first_type);
1627 }
1628
1629 /// tact_solve : (Syntax -> Derivation) -> Syntax -> Derivation
1630 ///
1631 /// Tactic combinator: tactic MUST completely solve the goal.
1632 /// If tactic returns Error, returns Error.
1633 /// If tactic returns a proof, returns that proof.
1634 /// Computational behavior defined in reduction.rs.
1635 fn register_tact_solve(ctx: &mut Context) {
1636 let syntax = Term::Global("Syntax".to_string());
1637 let derivation = Term::Global("Derivation".to_string());
1638
1639 // Tactic type: Syntax -> Derivation
1640 let tactic_type = Term::Pi {
1641 param: "_".to_string(),
1642 param_type: Box::new(syntax.clone()),
1643 body_type: Box::new(derivation.clone()),
1644 };
1645
1646 // tact_solve : (Syntax -> Derivation) -> Syntax -> Derivation
1647 let tact_solve_type = Term::Pi {
1648 param: "_".to_string(),
1649 param_type: Box::new(tactic_type), // t
1650 body_type: Box::new(Term::Pi {
1651 param: "_".to_string(),
1652 param_type: Box::new(syntax),
1653 body_type: Box::new(derivation),
1654 }),
1655 };
1656
1657 ctx.add_declaration("tact_solve", tact_solve_type);
1658 }
1659
1660 // -------------------------------------------------------------------------
1661 // Ring Tactic (Polynomial Equality)
1662 // -------------------------------------------------------------------------
1663
1664 /// DRingSolve : Syntax -> Derivation
1665 /// try_ring : Syntax -> Derivation
1666 ///
1667 /// Ring tactic: proves polynomial equalities by normalization.
1668 /// Computational behavior defined in reduction.rs.
1669 fn register_try_ring(ctx: &mut Context) {
1670 let syntax = Term::Global("Syntax".to_string());
1671 let derivation = Term::Global("Derivation".to_string());
1672
1673 // DRingSolve : Syntax -> Derivation
1674 // Proof constructor for ring-solved equalities
1675 ctx.add_constructor(
1676 "DRingSolve",
1677 "Derivation",
1678 Term::Pi {
1679 param: "_".to_string(),
1680 param_type: Box::new(syntax.clone()),
1681 body_type: Box::new(derivation.clone()),
1682 },
1683 );
1684
1685 // try_ring : Syntax -> Derivation
1686 // Ring tactic: given a goal, try to prove it by polynomial normalization
1687 let try_ring_type = Term::Pi {
1688 param: "_".to_string(),
1689 param_type: Box::new(syntax),
1690 body_type: Box::new(derivation),
1691 };
1692
1693 ctx.add_declaration("try_ring", try_ring_type);
1694 }
1695
1696 // -------------------------------------------------------------------------
1697 // LIA Tactic (Linear Integer Arithmetic)
1698 // -------------------------------------------------------------------------
1699
1700 /// DLiaSolve : Syntax -> Derivation
1701 /// try_lia : Syntax -> Derivation
1702 ///
1703 /// LIA tactic: proves linear inequalities by Fourier-Motzkin elimination.
1704 /// Computational behavior defined in reduction.rs.
1705 fn register_try_lia(ctx: &mut Context) {
1706 let syntax = Term::Global("Syntax".to_string());
1707 let derivation = Term::Global("Derivation".to_string());
1708
1709 // DLiaSolve : Syntax -> Derivation
1710 // Proof constructor for LIA-solved inequalities
1711 ctx.add_constructor(
1712 "DLiaSolve",
1713 "Derivation",
1714 Term::Pi {
1715 param: "_".to_string(),
1716 param_type: Box::new(syntax.clone()),
1717 body_type: Box::new(derivation.clone()),
1718 },
1719 );
1720
1721 // try_lia : Syntax -> Derivation
1722 // LIA tactic: given a goal, try to prove it by linear arithmetic
1723 let try_lia_type = Term::Pi {
1724 param: "_".to_string(),
1725 param_type: Box::new(syntax),
1726 body_type: Box::new(derivation),
1727 };
1728
1729 ctx.add_declaration("try_lia", try_lia_type);
1730 }
1731
1732 /// DccSolve : Syntax -> Derivation
1733 /// try_cc : Syntax -> Derivation
1734 ///
1735 /// Congruence Closure tactic: proves equalities over uninterpreted functions.
1736 /// Handles hypotheses via implications: (implies (Eq x y) (Eq (f x) (f y)))
1737 /// Computational behavior defined in reduction.rs.
1738 fn register_try_cc(ctx: &mut Context) {
1739 let syntax = Term::Global("Syntax".to_string());
1740 let derivation = Term::Global("Derivation".to_string());
1741
1742 // DccSolve : Syntax -> Derivation
1743 // Proof constructor for congruence closure proofs
1744 ctx.add_constructor(
1745 "DccSolve",
1746 "Derivation",
1747 Term::Pi {
1748 param: "_".to_string(),
1749 param_type: Box::new(syntax.clone()),
1750 body_type: Box::new(derivation.clone()),
1751 },
1752 );
1753
1754 // try_cc : Syntax -> Derivation
1755 // CC tactic: given a goal, try to prove it by congruence closure
1756 let try_cc_type = Term::Pi {
1757 param: "_".to_string(),
1758 param_type: Box::new(syntax),
1759 body_type: Box::new(derivation),
1760 };
1761
1762 ctx.add_declaration("try_cc", try_cc_type);
1763 }
1764
1765 /// DSimpSolve : Syntax -> Derivation
1766 /// try_simp : Syntax -> Derivation
1767 ///
1768 /// Simplifier tactic: proves equalities by term rewriting.
1769 /// Uses bottom-up rewriting with arithmetic evaluation and hypothesis substitution.
1770 /// Handles: reflexivity, constant folding (2+3=5), and hypothesis-based substitution.
1771 /// Computational behavior defined in reduction.rs.
1772 fn register_try_simp(ctx: &mut Context) {
1773 let syntax = Term::Global("Syntax".to_string());
1774 let derivation = Term::Global("Derivation".to_string());
1775
1776 // DSimpSolve : Syntax -> Derivation
1777 // Proof constructor for simplifier proofs
1778 ctx.add_constructor(
1779 "DSimpSolve",
1780 "Derivation",
1781 Term::Pi {
1782 param: "_".to_string(),
1783 param_type: Box::new(syntax.clone()),
1784 body_type: Box::new(derivation.clone()),
1785 },
1786 );
1787
1788 // try_simp : Syntax -> Derivation
1789 // Simp tactic: given a goal, try to prove it by simplification
1790 let try_simp_type = Term::Pi {
1791 param: "_".to_string(),
1792 param_type: Box::new(syntax),
1793 body_type: Box::new(derivation),
1794 };
1795
1796 ctx.add_declaration("try_simp", try_simp_type);
1797 }
1798
1799 /// DOmegaSolve : Syntax -> Derivation
1800 /// try_omega : Syntax -> Derivation
1801 ///
1802 /// Omega tactic: proves linear integer arithmetic with proper floor/ceil rounding.
1803 /// Unlike lia (which uses rationals), omega handles integers correctly:
1804 /// - x > 1 means x >= 2 (strict-to-nonstrict conversion)
1805 /// - 3x <= 10 means x <= 3 (floor division)
1806 /// Computational behavior defined in reduction.rs.
1807 fn register_try_omega(ctx: &mut Context) {
1808 let syntax = Term::Global("Syntax".to_string());
1809 let derivation = Term::Global("Derivation".to_string());
1810
1811 // DOmegaSolve : Syntax -> Derivation
1812 // Proof constructor for omega-solved inequalities
1813 ctx.add_constructor(
1814 "DOmegaSolve",
1815 "Derivation",
1816 Term::Pi {
1817 param: "_".to_string(),
1818 param_type: Box::new(syntax.clone()),
1819 body_type: Box::new(derivation.clone()),
1820 },
1821 );
1822
1823 // try_omega : Syntax -> Derivation
1824 // Omega tactic: given a goal, try to prove it by integer arithmetic
1825 let try_omega_type = Term::Pi {
1826 param: "_".to_string(),
1827 param_type: Box::new(syntax),
1828 body_type: Box::new(derivation),
1829 };
1830
1831 ctx.add_declaration("try_omega", try_omega_type);
1832 }
1833
1834 /// DAutoSolve : Syntax -> Derivation
1835 /// try_auto : Syntax -> Derivation
1836 ///
1837 /// Auto tactic: tries all decision procedures in sequence.
1838 /// Order: simp → ring → cc → omega → lia
1839 /// Returns the first successful derivation, or error if all fail.
1840 /// Computational behavior defined in reduction.rs.
1841 fn register_try_auto(ctx: &mut Context) {
1842 let syntax = Term::Global("Syntax".to_string());
1843 let derivation = Term::Global("Derivation".to_string());
1844
1845 // DAutoSolve : Syntax -> Derivation
1846 // Proof constructor for auto-solved goals
1847 ctx.add_constructor(
1848 "DAutoSolve",
1849 "Derivation",
1850 Term::Pi {
1851 param: "_".to_string(),
1852 param_type: Box::new(syntax.clone()),
1853 body_type: Box::new(derivation.clone()),
1854 },
1855 );
1856
1857 // try_auto : Syntax -> Derivation
1858 // Auto tactic: given a goal, try all tactics in sequence
1859 let try_auto_type = Term::Pi {
1860 param: "_".to_string(),
1861 param_type: Box::new(syntax),
1862 body_type: Box::new(derivation),
1863 };
1864
1865 ctx.add_declaration("try_auto", try_auto_type);
1866 }
1867
1868 /// try_induction : Syntax -> Syntax -> Derivation -> Derivation
1869 ///
1870 /// Generic induction tactic for any inductive type.
1871 /// Arguments:
1872 /// - ind_type: The inductive type (SName "Nat" or SApp (SName "List") A)
1873 /// - motive: The property to prove (SLam param_type body)
1874 /// - cases: DCase chain with one derivation per constructor
1875 ///
1876 /// Returns a DElim derivation if verification passes.
1877 fn register_try_induction(ctx: &mut Context) {
1878 let syntax = Term::Global("Syntax".to_string());
1879 let derivation = Term::Global("Derivation".to_string());
1880
1881 // try_induction : Syntax -> Syntax -> Derivation -> Derivation
1882 let try_induction_type = Term::Pi {
1883 param: "_".to_string(),
1884 param_type: Box::new(syntax.clone()), // ind_type
1885 body_type: Box::new(Term::Pi {
1886 param: "_".to_string(),
1887 param_type: Box::new(syntax.clone()), // motive
1888 body_type: Box::new(Term::Pi {
1889 param: "_".to_string(),
1890 param_type: Box::new(derivation.clone()), // cases
1891 body_type: Box::new(derivation),
1892 }),
1893 }),
1894 };
1895
1896 ctx.add_declaration("try_induction", try_induction_type);
1897 }
1898
1899 /// Helper functions for building induction goals.
1900 ///
1901 /// These functions help construct the subgoals for induction:
1902 /// - induction_base_goal: Computes the base case goal
1903 /// - induction_step_goal: Computes the step case goal for a constructor
1904 /// - induction_num_cases: Returns number of constructors for an inductive
1905 fn register_induction_helpers(ctx: &mut Context) {
1906 let syntax = Term::Global("Syntax".to_string());
1907 let nat = Term::Global("Nat".to_string());
1908
1909 // induction_base_goal : Syntax -> Syntax -> Syntax
1910 // Given ind_type and motive, returns the base case goal (first constructor)
1911 ctx.add_declaration(
1912 "induction_base_goal",
1913 Term::Pi {
1914 param: "_".to_string(),
1915 param_type: Box::new(syntax.clone()),
1916 body_type: Box::new(Term::Pi {
1917 param: "_".to_string(),
1918 param_type: Box::new(syntax.clone()),
1919 body_type: Box::new(syntax.clone()),
1920 }),
1921 },
1922 );
1923
1924 // induction_step_goal : Syntax -> Syntax -> Nat -> Syntax
1925 // Given ind_type, motive, constructor index, returns the case goal
1926 ctx.add_declaration(
1927 "induction_step_goal",
1928 Term::Pi {
1929 param: "_".to_string(),
1930 param_type: Box::new(syntax.clone()),
1931 body_type: Box::new(Term::Pi {
1932 param: "_".to_string(),
1933 param_type: Box::new(syntax.clone()),
1934 body_type: Box::new(Term::Pi {
1935 param: "_".to_string(),
1936 param_type: Box::new(nat),
1937 body_type: Box::new(syntax.clone()),
1938 }),
1939 }),
1940 },
1941 );
1942
1943 // induction_num_cases : Syntax -> Nat
1944 // Returns number of constructors for an inductive type
1945 ctx.add_declaration(
1946 "induction_num_cases",
1947 Term::Pi {
1948 param: "_".to_string(),
1949 param_type: Box::new(syntax),
1950 body_type: Box::new(Term::Global("Nat".to_string())),
1951 },
1952 );
1953 }
1954
1955 // -------------------------------------------------------------------------
1956 // Inversion Tactic
1957 // -------------------------------------------------------------------------
1958
1959 /// try_inversion : Syntax -> Derivation
1960 ///
1961 /// Inversion tactic: given a hypothesis type, derives False if no constructor
1962 /// can possibly build that type.
1963 ///
1964 /// Example: try_inversion (SApp (SName "Even") three) proves False because
1965 /// neither even_zero (requires 0) nor even_succ (requires Even 1) can build Even 3.
1966 ///
1967 /// Computational behavior defined in reduction.rs.
1968 fn register_try_inversion_tactic(ctx: &mut Context) {
1969 let syntax = Term::Global("Syntax".to_string());
1970 let derivation = Term::Global("Derivation".to_string());
1971
1972 // try_inversion : Syntax -> Derivation
1973 ctx.add_declaration(
1974 "try_inversion",
1975 Term::Pi {
1976 param: "_".to_string(),
1977 param_type: Box::new(syntax),
1978 body_type: Box::new(derivation),
1979 },
1980 );
1981 }
1982
1983 // -------------------------------------------------------------------------
1984 // Operator Tactics (rewrite, destruct, apply)
1985 // -------------------------------------------------------------------------
1986
1987 /// Operator tactics for manual proof control.
1988 ///
1989 /// try_rewrite : Derivation -> Syntax -> Derivation
1990 /// try_rewrite_rev : Derivation -> Syntax -> Derivation
1991 /// try_destruct : Syntax -> Syntax -> Derivation -> Derivation
1992 /// try_apply : Syntax -> Derivation -> Syntax -> Derivation
1993 fn register_operator_tactics(ctx: &mut Context) {
1994 let syntax = Term::Global("Syntax".to_string());
1995 let derivation = Term::Global("Derivation".to_string());
1996
1997 // try_rewrite : Derivation -> Syntax -> Derivation
1998 // Given eq_proof (concluding Eq A x y) and goal, replaces x with y in goal
1999 ctx.add_declaration(
2000 "try_rewrite",
2001 Term::Pi {
2002 param: "_".to_string(),
2003 param_type: Box::new(derivation.clone()), // eq_proof
2004 body_type: Box::new(Term::Pi {
2005 param: "_".to_string(),
2006 param_type: Box::new(syntax.clone()), // goal
2007 body_type: Box::new(derivation.clone()),
2008 }),
2009 },
2010 );
2011
2012 // try_rewrite_rev : Derivation -> Syntax -> Derivation
2013 // Given eq_proof (concluding Eq A x y) and goal, replaces y with x in goal (reverse direction)
2014 ctx.add_declaration(
2015 "try_rewrite_rev",
2016 Term::Pi {
2017 param: "_".to_string(),
2018 param_type: Box::new(derivation.clone()), // eq_proof
2019 body_type: Box::new(Term::Pi {
2020 param: "_".to_string(),
2021 param_type: Box::new(syntax.clone()), // goal
2022 body_type: Box::new(derivation.clone()),
2023 }),
2024 },
2025 );
2026
2027 // try_destruct : Syntax -> Syntax -> Derivation -> Derivation
2028 // Case analysis without induction hypotheses
2029 ctx.add_declaration(
2030 "try_destruct",
2031 Term::Pi {
2032 param: "_".to_string(),
2033 param_type: Box::new(syntax.clone()), // ind_type
2034 body_type: Box::new(Term::Pi {
2035 param: "_".to_string(),
2036 param_type: Box::new(syntax.clone()), // motive
2037 body_type: Box::new(Term::Pi {
2038 param: "_".to_string(),
2039 param_type: Box::new(derivation.clone()), // cases
2040 body_type: Box::new(derivation.clone()),
2041 }),
2042 }),
2043 },
2044 );
2045
2046 // try_apply : Syntax -> Derivation -> Syntax -> Derivation
2047 // Manual backward chaining - applies hypothesis to transform goal
2048 ctx.add_declaration(
2049 "try_apply",
2050 Term::Pi {
2051 param: "_".to_string(),
2052 param_type: Box::new(syntax.clone()), // hyp_name
2053 body_type: Box::new(Term::Pi {
2054 param: "_".to_string(),
2055 param_type: Box::new(derivation.clone()), // hyp_proof
2056 body_type: Box::new(Term::Pi {
2057 param: "_".to_string(),
2058 param_type: Box::new(syntax), // goal
2059 body_type: Box::new(derivation),
2060 }),
2061 }),
2062 },
2063 );
2064 }
2065}