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 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    pub fn eq(lhs: Prop, other: Prop) -> Prop {
25        Prop(lhs.0 == other.0)
26    }
27    pub fn ne(lhs: Prop, other: Prop) -> Prop {
28        Prop(lhs.0 != other.0)
29    }
30    pub fn implies(lhs: Prop, other: Prop) -> Prop {
31        Prop(lhs.0 || !other.0)
32    }
33    pub fn forall<A, F: Fn(A) -> Prop>(_pred: F) -> Prop {
34        Prop(true)
35    }
36    pub fn exists<A, F: Fn(A) -> Prop>(_pred: F) -> Prop {
37        Prop(true)
38    }
39}
40
41impl Prop {
42    /// Lifts a boolean to a logical proposition.
43    pub fn from_bool(b: bool) -> Self {
44        constructors::from_bool(b)
45    }
46    /// Conjuction of two propositions.
47    pub fn and(self, other: impl Into<Self>) -> Self {
48        constructors::and(self, other.into())
49    }
50    /// Disjunction of two propositions.
51    pub fn or(self, other: impl Into<Self>) -> Self {
52        constructors::or(self, other.into())
53    }
54    /// Negation of a proposition.
55    pub fn not(self) -> Self {
56        constructors::not(self)
57    }
58    /// Equality between two propositions.
59    pub fn eq(self, other: impl Into<Self>) -> Self {
60        constructors::eq(self, other.into())
61    }
62    /// Equality between two propositions.
63    pub fn ne(self, other: impl Into<Self>) -> Self {
64        constructors::ne(self, other.into())
65    }
66    /// Logical implication.
67    pub fn implies(self, other: impl Into<Self>) -> Self {
68        constructors::implies(self, other.into())
69    }
70}
71
72impl Abstraction for bool {
73    type AbstractType = Prop;
74    fn lift(self) -> Self::AbstractType {
75        Prop(self)
76    }
77}
78
79pub trait ToProp {
80    fn to_prop(self) -> Prop;
81}
82impl ToProp for bool {
83    fn to_prop(self) -> Prop {
84        self.lift()
85    }
86}
87
88impl From<bool> for Prop {
89    fn from(value: bool) -> Self {
90        Prop(value)
91    }
92}
93
94impl<T: Into<Prop>> BitAnd<T> for Prop {
95    type Output = Prop;
96    fn bitand(self, rhs: T) -> Self::Output {
97        Prop(self.0 & rhs.into().0)
98    }
99}
100
101impl<T: Into<Prop>> BitOr<T> for Prop {
102    type Output = Prop;
103    fn bitor(self, rhs: T) -> Self::Output {
104        Prop(self.0 | rhs.into().0)
105    }
106}
107
108impl Not for Prop {
109    type Output = Prop;
110    fn not(self) -> Self::Output {
111        Prop(!self.0)
112    }
113}
114
115/// The universal quantifier. This should be used only for Hax code: in
116/// Rust, this is always true.
117///
118/// # Example:
119///
120/// The Rust expression `forall(|x: T| phi(x))` corresponds to `∀ (x: T), phi(x)`.
121pub fn forall<T, U: Into<Prop>>(f: impl Fn(T) -> U) -> Prop {
122    constructors::forall(|x| f(x).into())
123}
124
125/// The existential quantifier. This should be used only for Hax code: in
126/// Rust, this is always true.
127///
128/// # Example:
129///
130/// The Rust expression `exists(|x: T| phi(x))` corresponds to `∃ (x: T), phi(x)`.
131pub fn exists<T, U: Into<Prop>>(f: impl Fn(T) -> U) -> Prop {
132    constructors::exists(|x| f(x).into())
133}
134
135/// The logical implication `a ==> b`.
136pub fn implies(lhs: impl Into<Prop>, rhs: impl Into<Prop>) -> Prop {
137    constructors::implies(lhs.into(), rhs.into())
138}
hax_lib/prop.rs

hax_lib/
prop.rs
