prop/path_semantics/
ty.rs

1#![deny(unsafe_op_in_unsafe_fn)]
2
3//! # Model of Types in Path Semantics
4
5use super::*;
6
7/// Models a type relation `a : t`.
8pub type Ty<A, T> = And<Imply<A, T>, POrdProof<A, T>>;
9
10/// `x_{n} : ltrue{n+1}`.
11pub fn ltrue<X: LProp>() -> Ty<X, LTrue<S<X::N>>>
12    where X::N: Lt<S<X::N>> + Default
13{
14    (LTrue(Default::default()).map_any(), POrdProof::default())
15}
16
17/// `(a : b) ⋀ (a == c)  =>  (c : b)`.
18pub fn in_left_arg<A: Prop, B: Prop, C: Prop>((ab, pord): Ty<A, B>, eq: Eq<A, C>) -> Ty<C, B> {
19    (imply::in_left_arg(ab, eq.clone()), pord.by_eq_left(eq))
20}
21
22/// `(a : b) ⋀ (b == c)  =>  (a : c)`.
23///
24/// # Safety
25///
26/// This theorem is unsafe due to use of [POrdProof::by_eq_right].
27pub unsafe fn in_right_arg<A: Prop, B: Prop, C: Prop>(
28    (ab, pord): Ty<A, B>, eq: Eq<B, C>
29) -> Ty<A, C> {
30    (imply::in_right_arg(ab, eq.clone()), unsafe {pord.by_eq_right(eq)})
31}
32
33/// `(a == b)  =>  (a : c) == (b : c)`.
34pub fn eq_left<A: Prop, B: Prop, C: Prop>(x: Eq<A, B>) -> Eq<Ty<A, C>, Ty<B, C>> {
35    let x2 = eq::symmetry(x.clone());
36    (Rc::new(move |ty_a| in_left_arg(ty_a, x.clone())),
37     Rc::new(move |ty_b| in_left_arg(ty_b, x2.clone())))
38}
39/// `(b == c)  =>  (a : b) == (a : c)`.
40///
41/// # Safety
42///
43/// This theorem is unsafe due to use oof [in_right_arg].
44pub unsafe fn eq_right<A: Prop, B: Prop, C: Prop>(x: Eq<B, C>) -> Eq<Ty<A, B>, Ty<A, C>> {
45    let x2 = eq::symmetry(x.clone());
46    (Rc::new(move |ty_a| unsafe {in_right_arg(ty_a, x.clone())}),
47     Rc::new(move |ty_a| unsafe {in_right_arg(ty_a, x2.clone())}))
48}
49
50/// `(a : b) ⋀ (b => c)  =>  (a : c)`.
51///
52/// # Safety
53///
54/// This theorem is unsafe due to use of [POrdProof::by_imply_right].
55pub unsafe fn imply_right<A: Prop, B: Prop, C: Prop>(x: Ty<A, B>, y: Imply<B, C>) -> Ty<A, C> {
56    (imply::transitivity(x.0, y.clone()), unsafe {x.1.by_imply_right(y)})
57}
58
59/// `(x : false) => ¬x`.
60pub fn ty_false<X: Prop>(ty_x_false: Ty<X, False>) -> Not<X> {ty_x_false.0}
61
62/// `(true : x) => x`.
63pub fn ty_true<X: Prop>(ty_true_x: Ty<True, X>) -> X {ty_true_x.0(True)}
64
65/// `a => (true : a)`.
66///
67/// # Safety
68///
69/// This theorem is unsafe due to use of [in_right_arg].
70pub unsafe fn ty_rev_true<A: Prop>(a: A) -> Ty<True, A> {
71    unsafe {in_right_arg(true_true(), (a.map_any(), True.map_any()))}
72}
73
74/// `(a : x) ⋀ a => (true : x)`.
75pub fn triv<A: Prop, X: Prop>(ty_a_x: Ty<A, X>, a: A) -> Ty<True, X> {
76    in_left_arg(ty_a_x, (True.map_any(), a.map_any()))
77}
78
79/// `(x : a) ⋀ ¬a => (x : false)`.
80///
81/// # Safety
82///
83/// This theorem is unsafe due to use of [in_right_arg].
84pub unsafe fn non_triv<X: Prop, A: Prop>(
85    ty_x_a: Ty<X, A>,
86    na: Not<A>,
87) -> Ty<X, False> {
88    let eq_a_false: Eq<A, False> =
89        (Rc::new(move |a| na(a)), Rc::new(move |fa| imply::absurd()(fa)));
90    unsafe {in_right_arg(ty_x_a, eq_a_false)}
91}
92
93/// `true == ltrue{n}`.
94pub fn eq_true_ltrue<N: Nat>() -> Eq<True, LTrue<N>> {
95    (LTrue(Default::default()).map_any(), True.map_any())
96}
97
98/// `true : ltrue{n+1}`.
99pub fn true_ltrue<N: Nat>() -> Ty<True, LTrue<S<N>>> {
100    in_left_arg(ltrue(), eq::symmetry(eq_true_ltrue()))
101}
102
103/// `true : true`.
104///
105/// # Safety
106///
107/// This theorem is unsafe due to use of [in_right_arg].
108pub unsafe fn true_true() -> Ty<True, True> {
109    let x = in_left_arg(ltrue(), eq::symmetry(eq_true_ltrue::<Z>()));
110    unsafe {in_right_arg(x, eq::symmetry(eq_true_ltrue::<S<Z>>()))}
111}
112
113/// `(x : a) ⋀ (y : b)  =>  ((x ⋀ y) : (a ⋀ b))`.
114pub fn and<X: Prop, Y: Prop, A: Prop, B: Prop>(
115    (xa, pord_xa): Ty<X, A>,
116    (yb, pord_yb): Ty<Y, B>,
117) -> Ty<And<X, Y>, And<A, B>> {
118    let imply_and_xy_and_ab: Imply<And<X, Y>, And<A, B>> = Rc::new(move |(x, y)| (xa(x), yb(y)));
119    (imply_and_xy_and_ab, pord_xa.and(pord_yb))
120}
121
122/// `(x : a) ⋀ (y : b)  =>  ((x ⋁ y) : (a ⋁ b))`.
123pub fn or<X: Prop, Y: Prop, A: Prop, B: Prop>(
124    (xa, pord_xa): Ty<X, A>,
125    (yb, pord_yb): Ty<Y, B>,
126) -> Ty<Or<X, Y>, Or<A, B>> {
127    let or_xy_or_ab: Imply<Or<X, Y>, Or<A, B>> = Rc::new(move |or_xy| {
128        match or_xy {
129            Left(x) => Left(xa(x)),
130            Right(y) => Right(yb(y)),
131        }
132    });
133    (or_xy_or_ab, pord_xa.or(pord_yb))
134}
135
136/// `(x : a) ⋀ (y : b) ⋀ hom(x, y)  =>  ((x => y) : (a => b))`.
137pub fn hom_imply<X: Prop, Y: Prop, A: Prop, B: Prop>(
138    (xa, pord_xa): Ty<X, A>,
139    (yb, pord_yb): Ty<Y, B>,
140    hom: Hom<X, Y>,
141) -> Ty<Imply<X, Y>, Imply<A, B>> {
142    let pord = pord_xa.clone().imply(pord_yb.clone());
143    let xy_ab = Rc::new(move |xy| {
144        let q_xy = hom(xy);
145        let psem = assume();
146        let q_ab = psem(((q_xy, (pord_xa.clone(), pord_yb.clone())), (xa.clone(), yb.clone())));
147        quality::to_eq(q_ab).0
148    });
149    (xy_ab, pord)
150}
151
152/// `(x : a) ⋀ (y : b) ⋀ eqq(x, y)  =>  ((x => y) : (a => b))`.
153pub fn eqq_imply<X: DProp, Y: DProp, A: Prop, B: Prop>(
154    (xa, pord_xa): Ty<X, A>,
155    (yb, pord_yb): Ty<Y, B>,
156    eqq_xy: EqQ<X, Y>,
157) -> Ty<Imply<X, Y>, Imply<A, B>> {
158    let pord = pord_xa.clone().imply(pord_yb.clone());
159    let xy_ab: Imply<Imply<X, Y>, Imply<A, B>> = match (X::decide(), Y::decide()) {
160        (Left(x), _) => Rc::new(move |xy| yb(xy(x.clone())).map_any()),
161        (_, Left(y)) => {
162            let ab: Imply<A, B> = yb(y).map_any();
163            ab.map_any()
164        }
165        (Right(nx), Right(ny)) => {
166            let eq_xy: Eq<X, Y> = eq::rev_modus_tollens(and::to_eq_pos((ny, nx)));
167            let q_xy = eqq_xy(eq_xy);
168            let q_ab = assume()(((q_xy, (pord_xa, pord_yb)), (xa, yb)));
169            let ab = quality::to_eq(q_ab).0;
170            ab.map_any()
171        }
172    };
173    (xy_ab, pord)
174}
175
176/// `(a : (b ⋁ c)) ⋀ a  =>  (a : b) ⋁ (a : c)`.
177pub fn or_split<A: Prop, B: Prop, C: Prop>(
178    (ty_a, pord): Ty<A, Or<B, C>>,
179    a: A
180) -> Or<Ty<A, B>, Ty<A, C>> {
181    match ty_a(a) {
182        Left(b) => Left((b.map_any(), pord.or_left())),
183        Right(c) => Right((c.map_any(), pord.or_right()))
184    }
185}
186
187/// `(a : (b ⋁ c))  =>  (a : b) ⋁ (a : c)`.
188pub fn or_split_da<A: DProp, B: Prop, C: Prop>(
189    (ty_a_or_b_c, pord): Ty<A, Or<B, C>>
190) -> Or<Ty<A, B>, Ty<A, C>> {
191    match imply::or_split_da(ty_a_or_b_c) {
192        Left(ty_a_b) => Left((ty_a_b, pord.or_left())),
193        Right(ty_a_c) => Right((ty_a_c, pord.or_right()))
194    }
195}
196
197/// `(a : (b ⋁ c))  =>  (a : b) ⋁ (a : c)`.
198pub fn or_split_db<A: Prop, B: DProp, C: Prop>(
199    (ty_a_or_b_c, pord): Ty<A, Or<B, C>>
200) -> Or<Ty<A, B>, Ty<A, C>> {
201    match imply::or_split_db(ty_a_or_b_c) {
202        Left(ty_a_b) => Left((ty_a_b, pord.or_left())),
203        Right(ty_a_c) => Right((ty_a_c, pord.or_right()))
204    }
205}
206
207/// `(a : (b ⋁ c))  =>  (a : b) ⋁ (a : c)`.
208pub fn or_split_dc<A: Prop, B: Prop, C: DProp>(
209    (ty_a_or_b_c, pord): Ty<A, Or<B, C>>
210) -> Or<Ty<A, B>, Ty<A, C>> {
211    match imply::or_split_dc(ty_a_or_b_c) {
212        Left(ty_a_b) => Left((ty_a_b, pord.or_left())),
213        Right(ty_a_c) => Right((ty_a_c, pord.or_right()))
214    }
215}
216
217/// `(a : T) ⋀ (b : U)  =>  ((a ~~ b) : (T ~~ U))`.
218pub fn q_formation<A: Prop, B: Prop, T: Prop, U: Prop>(
219    (a_t, pord_a_t): Ty<A, T>,
220    (b_u, pord_b_u): Ty<B, U>,
221) -> Ty<Q<A, B>, Q<T, U>> {
222    let pord_a_t_2 = pord_a_t.clone();
223    let pord_b_u_2 = pord_b_u.clone();
224    (Rc::new(move |q_ab| {
225        let p = assume();
226        p(((q_ab, (pord_a_t_2.clone(), pord_b_u_2.clone())), (a_t.clone(), b_u.clone())))
227    }), {
228        pord_a_t.q(pord_b_u)
229    })
230}
231
232/// `(a : T)  =>  (~a : ~T)`.
233pub fn qu_formation<A: Prop, T: Prop>((a_t, pord_a_t): Ty<A, T>) -> Ty<Qu<A>, Qu<T>> {
234    let pord_a_t_2 = pord_a_t.clone();
235    (Rc::new(move |qu_ab| {
236        Qu::from_q(assume()(((Qu::to_q(qu_ab), (pord_a_t_2.clone(), pord_a_t_2.clone())),
237            (a_t.clone(), a_t.clone()))))
238    }), {
239        pord_a_t.qu()
240    })
241}
242
243/// `(a : T) ⋀ (b : U) ⋀ ¬(T == U)  =>  ¬(a ~~ b)`.
244pub fn neq_to_sesh<A: Prop, B: Prop, T: Prop, U: Prop>(
245    ty_a: Ty<A, T>,
246    ty_b: Ty<B, U>,
247    neq_tu: Not<Eq<T, U>>,
248) -> Not<Q<A, B>> {
249    imply::modus_tollens(q_formation(ty_a, ty_b).0)(quality::neq_to_sesh(neq_tu))
250}
251
252/// `(a : T) ⋀ (a : U) ⋀ ¬(T == U)  =>  ¬~a`.
253pub fn neq_to_not_qu<A: Prop, T: Prop, U: Prop>(
254    ty_a_t: Ty<A, T>,
255    ty_a_u: Ty<A, U>,
256    neq_t_u: Not<Eq<T, U>>
257) -> Not<Qu<A>> {imply::in_left(neq_to_sesh(ty_a_t, ty_a_u, neq_t_u), Qu::to_q)}
258
259/// `(a : b) ⋀ (b : c) => (a : c)`.
260pub fn transitivity<A: Prop, B: Prop, C: Prop>(
261    (ab, pord_ab): Ty<A, B>,
262    (bc, pord_bc): Ty<B, C>
263) -> Ty<A, C> {
264    (imply::transitivity(ab, bc), pord_ab.transitivity(pord_bc))
265}
266
267/// `(a : x) => (a : (a : x))`.
268///
269/// # Safety
270///
271/// This theorem is unsafe due to use of [POrdProof::by_imply_right].
272pub unsafe fn lift<A: Prop, X: Prop>(ty_a: Ty<A, X>) -> Ty<A, Ty<A, X>> {
273    let pord1 = unsafe {ty_a.1.clone().by_imply_right(Rc::new(|x| x.map_any()))};
274    let pord2 = unsafe {ty_a.1.clone().by_imply_right(ty_a.1.clone().map_any())};
275    (ty_a.map_any(), pord1.merge_right(pord2))
276}
277
278/// `(a : (a : x)) => (a : x)`.
279///
280/// # Safety
281///
282/// This theorem is unsafe due to use of [POrdProof::by_imply_right].
283pub unsafe fn lower<A: Prop, X: Prop>((a_ty_a, pord_a_ty_a): Ty<A, Ty<A, X>>) -> Ty<A, X> {
284    let ax = imply::reduce(Rc::new(move |a| a_ty_a(a).0));
285    let x: POrdProof<A, Imply<A, X>> = unsafe {pord_a_ty_a.by_imply_right(ax.clone().map_any())};
286    (ax, x.imply_reduce())
287}
prop/path_semantics/ty.rs

prop/path_semantics/
ty.rs
