hax_lib/
prop.rs

1use crate::abstraction::*;
2use core::ops::*;
3
4/// Represent a logical proposition, that may be not computable.
5#[derive(Clone, Copy, Debug)]
6pub struct Prop(bool);
7
8/// This module provides monomorphic constructors for `Prop`.
9/// Hax rewrite more elaborated versions (see `forall` or `AndBit` below) to those monomorphic constructors.
10pub mod constructors {
11    use super::Prop;
12    pub const fn from_bool(b: bool) -> Prop {
13        Prop(b)
14    }
15    pub fn and(lhs: Prop, other: Prop) -> Prop {
16        Prop(lhs.0 && other.0)
17    }
18    pub fn or(lhs: Prop, other: Prop) -> Prop {
19        Prop(lhs.0 || other.0)
20    }
21    pub fn not(lhs: Prop) -> Prop {
22        Prop(!lhs.0)
23    }
24
25    /// Logical equality between two value of *any* type
26    pub fn eq<T>(_lhs: T, _rhs: T) -> Prop {
27        Prop(true)
28    }
29
30    pub fn ne<T>(_lhs: T, _rhs: T) -> Prop {
31        Prop(true)
32    }
33
34    pub fn implies(lhs: Prop, other: Prop) -> Prop {
35        Prop(lhs.0 || !other.0)
36    }
37
38    pub fn forall<A, F: Fn(A) -> Prop>(_pred: F) -> Prop {
39        Prop(true)
40    }
41
42    pub fn exists<A, F: Fn(A) -> Prop>(_pred: F) -> Prop {
43        Prop(true)
44    }
45}
46
47impl Prop {
48    /// Lifts a boolean to a logical proposition.
49    pub const fn from_bool(b: bool) -> Self {
50        constructors::from_bool(b)
51    }
52    /// Conjuction of two propositions.
53    pub fn and(self, other: impl Into<Self>) -> Self {
54        constructors::and(self, other.into())
55    }
56    /// Disjunction of two propositions.
57    pub fn or(self, other: impl Into<Self>) -> Self {
58        constructors::or(self, other.into())
59    }
60    /// Negation of a proposition.
61    pub fn not(self) -> Self {
62        constructors::not(self)
63    }
64    /// Equality between two propositions.
65    pub fn eq(self, other: impl Into<Self>) -> Self {
66        constructors::eq(self, other.into())
67    }
68    /// Equality between two propositions.
69    pub fn ne(self, other: impl Into<Self>) -> Self {
70        constructors::ne(self, other.into())
71    }
72    /// Logical implication.
73    pub fn implies(self, other: impl Into<Self>) -> Self {
74        constructors::implies(self, other.into())
75    }
76}
77
78impl Abstraction for bool {
79    type AbstractType = Prop;
80    fn lift(self) -> Self::AbstractType {
81        Prop(self)
82    }
83}
84
85pub trait ToProp {
86    fn to_prop(self) -> Prop;
87}
88impl ToProp for bool {
89    fn to_prop(self) -> Prop {
90        self.lift()
91    }
92}
93
94impl From<bool> for Prop {
95    fn from(value: bool) -> Self {
96        Prop(value)
97    }
98}
99
100impl<T: Into<Prop>> BitAnd<T> for Prop {
101    type Output = Prop;
102    fn bitand(self, rhs: T) -> Self::Output {
103        Prop(self.0 & rhs.into().0)
104    }
105}
106
107impl<T: Into<Prop>> BitOr<T> for Prop {
108    type Output = Prop;
109    fn bitor(self, rhs: T) -> Self::Output {
110        Prop(self.0 | rhs.into().0)
111    }
112}
113
114impl Not for Prop {
115    type Output = Prop;
116    fn not(self) -> Self::Output {
117        Prop(!self.0)
118    }
119}
120
121/// The universal quantifier. This should be used only for Hax code: in
122/// Rust, this is always true.
123///
124/// # Example:
125///
126/// The Rust expression `forall(|x: T| phi(x))` corresponds to `∀ (x: T), phi(x)`.
127pub fn forall<T, U: Into<Prop>>(f: impl Fn(T) -> U) -> Prop {
128    constructors::forall(|x| f(x).into())
129}
130
131/// The existential quantifier. This should be used only for Hax code: in
132/// Rust, this is always true.
133///
134/// # Example:
135///
136/// The Rust expression `exists(|x: T| phi(x))` corresponds to `∃ (x: T), phi(x)`.
137pub fn exists<T, U: Into<Prop>>(f: impl Fn(T) -> U) -> Prop {
138    constructors::exists(|x| f(x).into())
139}
140
141/// The logical implication `a ==> b`.
142pub fn implies(lhs: impl Into<Prop>, rhs: impl Into<Prop>) -> Prop {
143    constructors::implies(lhs.into(), rhs.into())
144}
145
146pub use constructors::eq;
hax_lib/prop.rs

hax_lib/
prop.rs
