group2/
group2.rs

1use vampire_prover::{Function, Options, Predicate, Problem, ProofRes, Term, exists, forall};
2
3fn main() {
4    // Prove that every subgroup of index 2 is normal.
5    let mult = Function::new("mult", 2);
6    let inv = Function::new("inv", 1);
7    let one = Function::constant("1");
8
9    // Helper to make multiplication more readable
10    let mul = |x: Term, y: Term| -> Term { mult.with([x, y]) };
11
12    // Group Axiom 1: Right identity - ∀x. x * 1 = x
13    let right_identity = forall(|x| mul(x, one).eq(x));
14
15    // Group Axiom 2: Right inverse - ∀x. x * inv(x) = 1
16    let right_inverse = forall(|x| {
17        let inv_x = inv.with(x);
18        mul(x, inv_x).eq(one)
19    });
20
21    // Group Axiom 3: Associativity - ∀x,y,z. (x * y) * z = x * (y * z)
22    let associativity = forall(|x| forall(|y| forall(|z| mul(mul(x, y), z).eq(mul(x, mul(y, z))))));
23
24    // Describe the subgroup
25    let h = Predicate::new("h", 1);
26
27    // Any subgroup contains the identity
28    let h_ident = h.with(one);
29
30    // And is closed under multiplication
31    let h_mul_closed = forall(|x| forall(|y| (h.with(x) & h.with(y)) >> h.with(mul(x, y))));
32
33    // And is closed under inverse
34    let h_inv_closed = forall(|x| h.with(x) >> h.with(inv.with(x)));
35
36    // H specifically is of order 2
37    let h_index_2 = exists(|x| {
38        // an element not in H
39        let not_in_h = !h.with(x);
40        // but everything is in H or x H
41        let class = forall(|y| h.with(y) | h.with(mul(inv.with(x), y)));
42
43        not_in_h & class
44    });
45
46    // Conjecture: H is normal
47    let h_normal = forall(|x| {
48        let h_x = h.with(x);
49        let conj_x = forall(|y| {
50            let y_inv = inv.with(y);
51            h.with(mul(mul(y, x), y_inv))
52        });
53        h_x.iff(conj_x)
54    });
55
56    let (solution, proof) = Problem::new(Options::new())
57        .with_axiom(right_identity)
58        .with_axiom(right_inverse)
59        .with_axiom(associativity)
60        .with_axiom(h_ident)
61        .with_axiom(h_mul_closed)
62        .with_axiom(h_inv_closed)
63        .with_axiom(h_index_2)
64        .conjecture(h_normal)
65        .solve_and_prove();
66
67    if let Some(proof) = proof {
68        println!("{}", proof);
69    }
70
71    assert_eq!(solution, ProofRes::Proved);
72}
group2/group2.rs

group2/
group2.rs
