Skip to main content

group/
group.rs

1use vampire_prover::{Function, Options, Problem, ProofRes, Term, forall};
2
3fn main() {
4    // Prove that the identity element works on the left using group axioms
5    // In group theory, if we define a group with:
6    //   - Right identity: x * 1 = x
7    //   - Right inverse: x * inv(x) = 1
8    //   - Associativity: (x * y) * z = x * (y * z)
9    // Then we can prove the left identity: 1 * x = x
10
11    let mult = Function::new("mult", 2);
12    let inv = Function::new("inv", 1);
13    let one = Function::constant("1");
14
15    // Helper to make multiplication more readable
16    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };
17
18    // Axiom 1: Right identity - ∀x. x * 1 = x
19    let right_identity = forall(|x| mul(x, one).eq(x));
20
21    // Axiom 2: Right inverse - ∀x. x * inv(x) = 1
22    let right_inverse = forall(|x| {
23        let inv_x = inv.with(x);
24        mul(x, inv_x).eq(one)
25    });
26
27    // Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
28    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));
29
30    // Conjecture: Left identity - ∀x. 1 * x = x
31    let left_identity = forall(|x| mul(one, x).eq(x));
32
33    let (solution, proof) = Problem::new(Options::new())
34        .with_axiom(right_identity)
35        .with_axiom(right_inverse)
36        .with_axiom(associativity)
37        .conjecture(left_identity)
38        .solve_and_prove();
39
40    if let Some(proof) = proof {
41        println!("{}", proof);
42    }
43
44    assert_eq!(solution, ProofRes::Proved);
45}