logicaffeine_kernel/
quotient.rs

1//! Certified universe-polymorphic quotient primitives for kernel importers.
2use crate::{Context, KernelError, Term, Universe};
3
4mod prelude;
5pub(crate) use prelude::{kind as prelude_kind, same_base as same_prelude_base};
6pub(crate) use prelude::{PreludeCertificate, PreludeKind};
7pub(crate) fn register_prelude(ctx: &mut Context) -> Result<(), KernelError> {
8    prelude::register(ctx)
9}
10
11#[derive(Debug, Clone, Copy, PartialEq, Eq)]
12pub enum Kind {
13    Type,
14    Constructor,
15    Lift,
16    Induction,
17}
18impl Kind {
19    pub fn name(self) -> &'static str {
20        match self {
21            Self::Type => "kernel.quot.type",
22            Self::Constructor => "kernel.quot.mk",
23            Self::Lift => "kernel.quot.lift",
24            Self::Induction => "kernel.quot.ind",
25        }
26    }
27    pub fn arity(self) -> usize {
28        if self == Self::Lift {
29            2
30        } else {
31            1
32        }
33    }
34}
35#[derive(Debug, Clone)]
36pub(crate) struct Certificate {
37    pub kind: Kind,
38    pub dependencies: Vec<String>,
39    /// The lift's: the equality its respect hypothesis is stated with.
40    pub equality: Option<String>,
41}
42fn v(n: &str) -> Term {
43    Term::Var(format!("quot.{n}"))
44}
45fn pi(n: &str, ty: Term, body: Term) -> Term {
46    Term::Pi {
47        param: format!("quot.{n}"),
48        param_type: Box::new(ty),
49        body_type: Box::new(body),
50    }
51}
52fn app(f: Term, args: impl IntoIterator<Item = Term>) -> Term {
53    args.into_iter()
54        .fold(f, |f, a| Term::App(Box::new(f), Box::new(a)))
55}
56fn constant(name: &str, levels: Vec<Universe>) -> Term {
57    Term::Const {
58        name: name.into(),
59        levels,
60    }
61}
62fn prop() -> Term {
63    Term::Sort(Universe::Prop)
64}
65fn error(message: &str) -> KernelError {
66    KernelError::CertificationError(message.into())
67}
68
69/// The canonical Lean signature, with explicit universe instances throughout.
70pub fn signature(kind: Kind, levels: &[Universe], equality: &str) -> Result<Term, KernelError> {
71    if levels.len() != kind.arity() {
72        return Err(error("quotient universe arity mismatch"));
73    }
74    let u = levels[0].clone();
75    let carrier = || Term::Sort(u.clone());
76    let relation = || pi("x", v("A"), pi("y", v("A"), prop()));
77    let quotient = || {
78        app(
79            constant(Kind::Type.name(), vec![u.clone()]),
80            [v("A"), v("r")],
81        )
82    };
83    let mk = |x| {
84        app(
85            constant(Kind::Constructor.name(), vec![u.clone()]),
86            [v("A"), v("r"), x],
87        )
88    };
89    let body = match kind {
90        Kind::Type => carrier(),
91        Kind::Constructor => pi("a", v("A"), quotient()),
92        Kind::Induction => pi(
93            "P",
94            pi("q", quotient(), prop()),
95            pi(
96                "f",
97                pi("a", v("A"), app(v("P"), [mk(v("a"))])),
98                pi("q", quotient(), app(v("P"), [v("q")])),
99            ),
100        ),
101        Kind::Lift => {
102            let level_v = levels[1].clone();
103            let respect = pi(
104                "a",
105                v("A"),
106                pi(
107                    "b",
108                    v("A"),
109                    pi(
110                        "h",
111                        app(v("r"), [v("a"), v("b")]),
112                        app(
113                            constant(equality, vec![level_v.clone()]),
114                            [v("B"), app(v("f"), [v("a")]), app(v("f"), [v("b")])],
115                        ),
116                    ),
117                ),
118            );
119            pi(
120                "B",
121                Term::Sort(level_v),
122                pi(
123                    "f",
124                    pi("a", v("A"), v("B")),
125                    pi("respect", respect, pi("q", quotient(), v("B"))),
126                ),
127            )
128        }
129    };
130    Ok(pi("A", carrier(), pi("r", relation(), body)))
131}
132
133fn canonical_signature(actual: &Term, expected: &Term) -> bool {
134    let mut store = crate::term_store::TermStore::new();
135    let actual = store.intern(actual);
136    let expected = store.intern(expected);
137    store.alpha_same(actual, expected)
138}
139
140fn equality_dependencies(ctx: &Context, name: &str) -> Result<Vec<String>, KernelError> {
141    let Some((params, ty)) = ctx.poly_declaration(name) else {
142        return Err(error(
143            "quotient lift requires a polymorphic equality inductive",
144        ));
145    };
146    let constructors = ctx.get_constructors(name);
147    if params.len() != 1
148        || !ctx.is_inductive(name)
149        || ctx.inductive_num_params(name) != 2
150        || ctx.inductive_num_indices(name) != 1
151        || constructors.len() != 1
152    {
153        return Err(error("quotient lift requires canonical equality"));
154    }
155    let u = Universe::Var(params[0].clone());
156    let expected = pi(
157        "A",
158        Term::Sort(u.clone()),
159        pi("a", v("A"), pi("b", v("A"), prop())),
160    );
161    if !canonical_signature(ty, &expected) {
162        return Err(error(
163            "quotient equality type differs from canonical equality",
164        ));
165    }
166    let (ctor, _) = constructors[0];
167    let Some((cp, ct)) = ctx.poly_declaration(ctor) else {
168        return Err(error(
169            "quotient equality constructor lacks universe telescope",
170        ));
171    };
172    if cp.len() != 1 {
173        return Err(error("quotient equality constructor universe arity"));
174    }
175    let cu = Universe::Var(cp[0].clone());
176    let expected_ctor = pi(
177        "A",
178        Term::Sort(cu.clone()),
179        pi(
180            "a",
181            v("A"),
182            app(constant(name, vec![cu]), [v("A"), v("a"), v("a")]),
183        ),
184    );
185    if !canonical_signature(ct, &expected_ctor) {
186        return Err(error(
187            "quotient equality constructor differs from reflexivity",
188        ));
189    }
190    Ok(vec![name.into(), ctor.into()])
191}
192
193/// Install only a canonical primitive, never an arbitrary trusted input type.
194/// The importer separately compares its serialized signature with this one.
195pub fn install(
196    ctx: &mut Context,
197    kind: Kind,
198    params: Vec<String>,
199    equality: &str,
200) -> Result<(), KernelError> {
201    let levels = params
202        .iter()
203        .cloned()
204        .map(Universe::Var)
205        .collect::<Vec<_>>();
206    let ty = signature(kind, &levels, equality)?;
207    let mut dependencies = vec![kind.name().into()];
208    if kind != Kind::Type {
209        if ctx
210            .quotient_primitives
211            .get(Kind::Type.name())
212            .map(|c| c.kind)
213            != Some(Kind::Type)
214        {
215            return Err(error(
216                "quotient type must be installed before its primitives",
217            ));
218        }
219        dependencies.push(Kind::Type.name().into());
220    }
221    if kind == Kind::Induction {
222        if ctx
223            .quotient_primitives
224            .get(Kind::Constructor.name())
225            .map(|c| c.kind)
226            != Some(Kind::Constructor)
227        {
228            return Err(error("quotient constructor must precede induction"));
229        }
230        dependencies.push(Kind::Constructor.name().into());
231    }
232    if kind == Kind::Lift {
233        dependencies.extend(equality_dependencies(ctx, equality)?);
234    }
235    ctx.add_universe_poly_declaration(kind.name(), params, ty)?;
236    let equality = (kind == Kind::Lift).then(|| equality.to_string());
237    ctx.record(
238        |c| &mut c.quotient_primitives,
239        kind.name().into(),
240        Certificate {
241            kind,
242            dependencies,
243            equality,
244        },
245    );
246    Ok(())
247}
248
249/// Resolve a certified identity only at a well-formed universe instance.
250pub(crate) fn kind(ctx: &Context, name: &str, levels: &[Universe]) -> Option<Kind> {
251    let certificate = ctx.quotient_primitives.get(name)?;
252    let (params, ty) = ctx.poly_declaration(name)?;
253    crate::term::resolve_const_levels(name, Some(params), ty, levels).ok()?;
254    Some(certificate.kind)
255}
256
257#[cfg(test)]
258#[path = "../../logicaffeine_tests/unit/logicaffeine_kernel/quotient/tests.rs"]
259mod tests;
260
261#[cfg(test)]
262#[path = "../../logicaffeine_tests/unit/logicaffeine_kernel/quotient/prelude_identity_controls.rs"]
263mod prelude_identity_controls;
264
265#[cfg(test)]
266#[path = "../../logicaffeine_tests/unit/logicaffeine_kernel/quotient/recursor_definition_controls.rs"]
267mod recursor_definition_controls;
logicaffeine_kernel/quotient.rs

logicaffeine_kernel/
quotient.rs
