prop/fun/
is_const.rs

1use super::*;
2
3/// Whether some symbol is a constant.
4///
5/// When a symbol `x` is a constant, `x[a := b] == x` (invariant under substitution).
6#[derive(Copy, Clone)]
7pub struct IsConst<A>(A);
8
9/// A proof that some symbol is not a constant.
10///
11/// This is used to prevent collapse of propositions into constants,
12/// e.g. when doing a proof by induction.
13pub type IsVar<A> = Not<IsConst<A>>;
14
15/// Implemented by variable propositions.
16pub trait VProp: Prop {
17    /// Constructs a proof that the proposition is variable.
18    fn is_var() -> IsVar<Self>;
19}
20
21/// `is_const(a) ⋀ is_const(b)  =>  is_const((a, b))`.
22pub fn const_tup<A: Prop, B: Prop>(a: IsConst<A>, b: IsConst<B>) -> IsConst<Tup<A, B>> {
23    tup_is_const(a, b)
24}
25/// `is_const((a, b))  =>  is_const(a) ⋀ is_const(b)`.
26pub fn tup_const<A: Prop, B: Prop>(_x: IsConst<Tup<A, B>>) -> And<IsConst<A>, IsConst<B>> {
27    unimplemented!()
28}
29/// `(a == b)  =>  (is_const(a) == is_const(b))`.
30///
31/// This is an axiom since it accesses the inner value, which is not sound as a theorem.
32pub fn const_eq<A: Prop, B: Prop>((ab, ba): Eq<A, B>) -> Eq<IsConst<A>, IsConst<B>> {
33    (Rc::new(move |a| IsConst(ab(a.0))), Rc::new(move |b| IsConst(ba(b.0))))
34}
35/// `is_const(a) ⋀ is_const(b)  =>  is_const(a ⋀ b)`.
36pub fn and_is_const<A: Prop, B: Prop>(_a: IsConst<A>, _b: IsConst<B>) -> IsConst<And<A, B>> {
37    unimplemented!()
38}
39/// `is_const(a) ⋀ is_const(b)  =>  is_const(a ⋁ b)`.
40pub fn or_is_const<A: Prop, B: Prop>(_a: IsConst<A>, _b: IsConst<B>) -> IsConst<Or<A, B>> {
41    unimplemented!()
42}
43/// `is_const(a) ⋀ is_const(b)  =>  is_const(a => b)`.
44pub fn imply_is_const<A: Prop, B: Prop>(_a: IsConst<A>, _b: IsConst<B>) -> IsConst<Imply<A, B>> {
45    unimplemented!()
46}
47/// `is_const(a) ⋀ is_const(b)  =>  is_const(pord(a, b))`.
48pub fn pord_is_const<A: Prop, B: Prop>(
49    _a: IsConst<A>,
50    _b: IsConst<B>
51) -> IsConst<POrdProof<A, B>> {
52    unimplemented!()
53}
54
55/// `is_const(a) ⋀ is_const(b)  =>  is_const(a : b)`.
56pub fn ty_is_const<A: Prop, B: Prop>(a: IsConst<A>, b: IsConst<B>) -> IsConst<Ty<A, B>> {
57    and_is_const(imply_is_const(a.clone(), b.clone()), pord_is_const(a, b))
58}
59
60/// `is_const(a) ⋀ (a == b)  =>  is_const(b)`.
61pub fn const_in_arg<A: Prop, B: Prop>(a: IsConst<A>, x: Eq<A, B>) -> IsConst<B> {
62    const_eq(x).0(a)
63}
prop/fun/is_const.rs

prop/fun/
is_const.rs
