logicaffeine_kernel/dag/
primitive_wf.rs

1//! Validating the well-founded `Nat` primitives: `Nat.div`, `Nat.mod`, `Nat.gcd`, `Nat.bitwise`.
2//!
3//! These are defined by fuel or by `WellFounded.fix`, so their defining equations are not
4//! definitional for a symbolic argument the way `Nat.add`'s are. Following `lean4lean`'s
5//! `Primitive.lean`, the kernel instead checks, over free variables:
6//!
7//! * the decision procedures they branch on (`Nat.decLe`, `Nat.decEq`, `Bool.decEq`) reflect their
8//!   Boolean counterparts (`Nat.ble`, `Nat.beq`), so `if`/`dite` on them compute like the
9//!   corresponding literal comparison;
10//! * `Nat.div`/`Nat.mod` unfold, one fuel step at a time, to exactly the recursion of division;
11//! * `Nat.gcd`/`Nat.bitwise` unfold through `WellFounded.Nat.fix` to the right-hand sides of their
12//!   `eq_def` equations, whose fuel is always sufficient.
13//!
14//! The reference terms these checks are stated with were elaborated by the pinned Lean toolchain
15//! (`primitive_refs/PrimitiveRefs.lean`), so no elaborated shape is reconstructed by hand.
16
17use super::check::DefnDecl;
18use super::error::{KResult, KernelFailure};
19use super::expr::{ExprId, Node};
20use super::level::LevelsId;
21use super::tc::Kernel;
22use rustc_hash::FxHashMap as FxMap;
23
24const REFS: &[u8] = include_bytes!("primitive_refs/lean-4.29.1.ndjson");
25
26struct Refs(FxMap<String, ExprId>);
27
28impl Refs {
29    fn get(&self, k: &str) -> KResult<ExprId> {
30        self.0.get(k).copied().ok_or_else(|| {
31            KernelFailure::resource(format!("missing primitive reference term '{k}'"))
32        })
33    }
34}
35
36#[derive(Clone, Copy)]
37struct Reflection {
38    ty: ExprId,
39    of_true: ExprId,
40    of_false: ExprId,
41    to_dec: ExprId,
42}
43
44#[derive(Clone, Copy)]
45enum Impl {
46    Bool,
47    ReflectNatNat {
48        as_bool: ExprId,
49        reflect: Reflection,
50        proof: ExprId,
51    },
52}
53
54#[derive(Clone, Copy)]
55struct Condition {
56    prop: ExprId,
57    dec: ExprId,
58    imp: Impl,
59}
60
61/// The constants the checks are written with, interned once.
62struct C {
63    prop: ExprId,
64    ty1: ExprId,
65    nat: ExprId,
66    bool_: ExprId,
67    tru: ExprId,
68    fal: ExprId,
69    zero: ExprId,
70    succ: ExprId,
71    not: ExprId,
72    ite1: ExprId,
73    dite_nat: ExprId,
74    ite_nat: ExprId,
75}
76
77struct Fail;
78
79type V<T> = Result<T, Fail>;
80
81impl Kernel {
82    /// `Ok(true)` when the definition passes, `Ok(false)` when it does not have the canonical
83    /// form (the primitive is then admitted by its type but never accelerated).
84    pub(crate) fn check_wf_primitive(&mut self, d: &DefnDecl) -> KResult<bool> {
85        let refs = Refs(super::export::load_refs(self, REFS)?);
86        match self.check_wf_primitive_inner(d, &refs) {
87            Ok(r) => Ok(r),
88            Err(e) if e.is_reject() => Ok(false),
89            Err(e) => Err(e),
90        }
91    }
92
93    fn check_wf_primitive_inner(&mut self, d: &DefnDecl, refs: &Refs) -> KResult<bool> {
94        let c = self.prim_consts();
95        let n = d.header.name;
96        let w = (
97            self.wk.nat_mod,
98            self.wk.nat_div,
99            self.wk.nat_gcd,
100            self.wk.nat_bitwise,
101        );
102        let r = if n == w.0 {
103            self.check_mod(d, refs, &c)?
104        } else if n == w.1 {
105            self.check_div(d, refs, &c)?
106        } else if n == w.2 {
107            self.check_gcd(d, refs, &c)?
108        } else if n == w.3 {
109            self.check_bitwise(d, refs, &c)?
110        } else {
111            return Ok(false);
112        };
113        Ok(r.is_ok())
114    }
115
116    fn prim_consts(&mut self) -> C {
117        let one = self.s.levels.of_nat(1);
118        let l1 = self.s.levels.list(&[one]);
119        let e = LevelsId::EMPTY;
120        let nat = self.s.cnst(self.wk.nat, e);
121        let dite = self.s.names.dotted("dite");
122        let ite = self.s.names.dotted("ite");
123        let not = self.s.names.dotted("Not");
124        let dite1 = self.s.cnst(dite, l1);
125        let ite1 = self.s.cnst(ite, l1);
126        C {
127            prop: self.s.prop(),
128            ty1: self.s.sort(one),
129            nat,
130            bool_: self.s.cnst(self.wk.bool_, e),
131            tru: self.s.cnst(self.wk.bool_true, e),
132            fal: self.s.cnst(self.wk.bool_false, e),
133            zero: self.s.cnst(self.wk.nat_zero, e),
134            succ: self.s.cnst(self.wk.nat_succ, e),
135            not: self.s.cnst(not, e),
136            ite1,
137            dite_nat: self.s.app(dite1, nat),
138            ite_nat: self.s.app(ite1, nat),
139        }
140    }
141
142    fn c0n(&mut self, dotted: &str) -> ExprId {
143        let n = self.s.names.dotted(dotted);
144        self.s.cnst(n, LevelsId::EMPTY)
145    }
146
147    fn apps(&mut self, f: ExprId, args: &[ExprId]) -> ExprId {
148        self.s.mk_app_n(f, args)
149    }
150
151    fn lam0(&mut self, t: ExprId, b: ExprId) -> ExprId {
152        self.s.lam(t, b)
153    }
154
155    fn raw_arrow(&mut self, d: ExprId, b: ExprId) -> ExprId {
156        self.s.pi(d, b)
157    }
158
159    fn reflection(&self, refs: &Refs, which: &str) -> KResult<Reflection> {
160        Ok(Reflection {
161            ty: refs.get(&format!("{which}.type"))?,
162            of_true: refs.get(&format!("{which}.ofTrue"))?,
163            of_false: refs.get(&format!("{which}.ofFalse"))?,
164            to_dec: refs.get(&format!("{which}.toDec"))?,
165        })
166    }
167
168    fn cond_nat_le(&mut self, refs: &Refs) -> KResult<Condition> {
169        let as_bool = self.s.cnst(self.wk.nat_ble, LevelsId::EMPTY);
170        Ok(Condition {
171            prop: refs.get("natLE.prop")?,
172            dec: refs.get("natLE.dec")?,
173            imp: Impl::ReflectNatNat {
174                as_bool,
175                reflect: self.reflection(refs, "refl1")?,
176                proof: refs.get("natLE.proof")?,
177            },
178        })
179    }
180
181    fn cond_nat_eq(&mut self, refs: &Refs) -> KResult<Condition> {
182        let as_bool = self.s.cnst(self.wk.nat_beq, LevelsId::EMPTY);
183        Ok(Condition {
184            prop: refs.get("natEq.prop")?,
185            dec: refs.get("natEq.dec")?,
186            imp: Impl::ReflectNatNat {
187                as_bool,
188                reflect: self.reflection(refs, "refl2")?,
189                proof: refs.get("natEq.proof")?,
190            },
191        })
192    }
193
194    fn cond_bool(&self, refs: &Refs) -> KResult<Condition> {
195        Ok(Condition {
196            prop: refs.get("bool.prop")?,
197            dec: refs.get("bool.dec")?,
198            imp: Impl::Bool,
199        })
200    }
201
202    fn defeq(&mut self, a: ExprId, b: ExprId) -> KResult<V<()>> {
203        Ok(if self.is_def_eq(a, b)? {
204            Ok(())
205        } else {
206            Err(Fail)
207        })
208    }
209
210    fn nat_nat_prop(&mut self, c: &C) -> ExprId {
211        let np = self.raw_arrow(c.nat, c.prop);
212        self.raw_arrow(c.nat, np)
213    }
214
215    fn reflection_check(&mut self, r: &Reflection, c: &C) -> KResult<V<()>> {
216        let t = self.check(r.ty)?;
217        let bp = self.raw_arrow(c.bool_, c.prop);
218        let pbp = self.raw_arrow(c.prop, bp);
219        self.defeq(t, pbp)
220    }
221
222    fn reflection_ite(&mut self, r: &Reflection, c: &C) -> ExprId {
223        let (b0, b1, b2, b3) = (
224            self.s.bvar(0),
225            self.s.bvar(1),
226            self.s.bvar(2),
227            self.s.bvar(3),
228        );
229        let dec = self.apps(r.to_dec, &[b3, b2, b1]);
230        let body = self.apps(c.ite1, &[b0, b3, dec]);
231        let l4 = self.lam0(c.ty1, body);
232        let h_ty = self.apps(r.ty, &[b1, b0]);
233        let l3 = self.lam0(h_ty, l4);
234        let l2 = self.lam0(c.bool_, l3);
235        self.lam0(c.prop, l2)
236    }
237
238    fn reflection_nat_dite(&mut self, r: &Reflection, c: &C) -> ExprId {
239        let (b0, b1, b2) = (self.s.bvar(0), self.s.bvar(1), self.s.bvar(2));
240        let dec = self.apps(r.to_dec, &[b2, b1, b0]);
241        let body = self.apps(c.dite_nat, &[b2, dec]);
242        let h_ty = self.apps(r.ty, &[b1, b0]);
243        let l3 = self.lam0(h_ty, body);
244        let l2 = self.lam0(c.bool_, l3);
245        self.lam0(c.prop, l2)
246    }
247
248    /// The body of `fun α a _ => a` (`first`) or `fun α _ a => a` under the binder `α`.
249    fn select(&mut self, first: bool) -> ExprId {
250        let (b0, b1) = (self.s.bvar(0), self.s.bvar(1));
251        let pick = if first { b1 } else { b0 };
252        let inner = self.lam0(b1, pick);
253        self.lam0(b0, inner)
254    }
255
256    fn check_ite(&mut self, r: &Reflection, c: &C) -> KResult<V<()>> {
257        let ite = self.reflection_ite(r, c);
258        let t = self.check(ite)?;
259        let (b0, b1, b2) = (self.s.bvar(0), self.s.bvar(1), self.s.bvar(2));
260        let aaa = {
261            let a_a = self.raw_arrow(b1, b2);
262            let a_aa = self.raw_arrow(b0, a_a);
263            self.s.pi(c.ty1, a_aa)
264        };
265        let h_ty = self.apps(r.ty, &[b1, b0]);
266        let x3 = self.raw_arrow(h_ty, aaa);
267        let x2 = self.raw_arrow(c.bool_, x3);
268        let expect = self.raw_arrow(c.prop, x2);
269        if self.defeq(t, expect)?.is_err() {
270            return Ok(Err(Fail));
271        }
272        let p = self.push_local(c.prop, None);
273        for (b, first) in [(c.tru, true), (c.fal, false)] {
274            let hty = self.apps(r.ty, &[p, b]);
275            let h = self.push_local(hty, None);
276            let lhs = self.apps(ite, &[p, b, h]);
277            let sel = self.select(first);
278            let rhs = self.lam0(c.ty1, sel);
279            if self.defeq(lhs, rhs)?.is_err() {
280                return Ok(Err(Fail));
281            }
282        }
283        Ok(Ok(()))
284    }
285
286    fn check_nat_dite(&mut self, r: &Reflection, c: &C) -> KResult<V<()>> {
287        let not_t = self.check(c.not)?;
288        let pp = self.raw_arrow(c.prop, c.prop);
289        if self.defeq(not_t, pp)?.is_err() {
290            return Ok(Err(Fail));
291        }
292        let nd = self.reflection_nat_dite(r, c);
293        let t = self.check(nd)?;
294        let (b0, b1, b2, b3) = (
295            self.s.bvar(0),
296            self.s.bvar(1),
297            self.s.bvar(2),
298            self.s.bvar(3),
299        );
300        let not_b3 = self.s.app(c.not, b3);
301        let a5 = self.raw_arrow(not_b3, c.nat);
302        let x5 = self.raw_arrow(a5, c.nat);
303        let a4 = self.raw_arrow(b2, c.nat);
304        let x4 = self.raw_arrow(a4, x5);
305        let h_ty = self.apps(r.ty, &[b1, b0]);
306        let x3 = self.raw_arrow(h_ty, x4);
307        let x2 = self.raw_arrow(c.bool_, x3);
308        let expect = self.raw_arrow(c.prop, x2);
309        if self.defeq(t, expect)?.is_err() {
310            return Ok(Err(Fail));
311        }
312        for (term, b, negate) in [(r.of_true, c.tru, false), (r.of_false, c.fal, true)] {
313            let t = self.check(term)?;
314            let rt = self.apps(r.ty, &[b0, b]);
315            let concl = if negate { self.s.app(c.not, b1) } else { b1 };
316            let x = self.raw_arrow(rt, concl);
317            let expect = self.raw_arrow(c.prop, x);
318            if self.defeq(t, expect)?.is_err() {
319                return Ok(Err(Fail));
320            }
321        }
322        let p = self.push_local(c.prop, None);
323        let pn = self.raw_arrow(p, c.nat);
324        let a = self.push_local(pn, None);
325        let not_p = self.s.app(c.not, p);
326        let npn = self.raw_arrow(not_p, c.nat);
327        let bb = self.push_local(npn, None);
328        for (bv, of, branch) in [(c.tru, r.of_true, a), (c.fal, r.of_false, bb)] {
329            let hty = self.apps(r.ty, &[p, bv]);
330            let h = self.push_local(hty, None);
331            let lhs = self.apps(nd, &[p, bv, h, a, bb]);
332            let proof = self.apps(of, &[p, h]);
333            let rhs = self.s.app(branch, proof);
334            if self.defeq(lhs, rhs)?.is_err() {
335                return Ok(Err(Fail));
336            }
337        }
338        Ok(Ok(()))
339    }
340
341    fn condition_check(
342        &mut self,
343        cond: &Condition,
344        c: &C,
345        ite: bool,
346        dite: bool,
347    ) -> KResult<V<()>> {
348        self.check(cond.dec)?;
349        match cond.imp {
350            Impl::ReflectNatNat {
351                as_bool,
352                reflect,
353                proof,
354            } => {
355                let pt = self.infer(cond.prop, true)?;
356                let nnp = self.nat_nat_prop(c);
357                if self.defeq(pt, nnp)?.is_err() || self.reflection_check(&reflect, c)?.is_err() {
358                    return Ok(Err(Fail));
359                }
360                if ite && self.check_ite(&reflect, c)?.is_err() {
361                    return Ok(Err(Fail));
362                }
363                if dite && self.check_nat_dite(&reflect, c)?.is_err() {
364                    return Ok(Err(Fail));
365                }
366                let (y, x) = (self.s.bvar(0), self.s.bvar(1));
367                let p = self.apps(cond.prop, &[x, y]);
368                let b = self.apps(as_bool, &[x, y]);
369                let pr = self.apps(proof, &[x, y]);
370                let body = self.apps(reflect.to_dec, &[p, b, pr]);
371                let l = self.lam0(c.nat, body);
372                let e = self.lam0(c.nat, l);
373                self.check(e)?;
374                let bt = self.infer(as_bool, true)?;
375                let nb = self.raw_arrow(c.nat, c.bool_);
376                let nnb = self.raw_arrow(c.nat, nb);
377                if self.defeq(bt, nnb)?.is_err() {
378                    return Ok(Err(Fail));
379                }
380                let prt = self.infer(proof, true)?;
381                if !self.is_prop(prt)? {
382                    return Ok(Err(Fail));
383                }
384                self.defeq(e, cond.dec)
385            }
386            Impl::Bool => {
387                let pt = self.infer(cond.prop, true)?;
388                let bp = self.raw_arrow(c.bool_, c.prop);
389                if self.defeq(pt, bp)?.is_err() {
390                    return Ok(Err(Fail));
391                }
392                if dite {
393                    return Ok(Err(Fail));
394                }
395                if ite {
396                    let b = self.s.bvar(0);
397                    let pb = self.s.app(cond.prop, b);
398                    let db = self.s.app(cond.dec, b);
399                    let body = self.apps(c.ite_nat, &[pb, db]);
400                    let nat_ite = self.lam0(c.bool_, body);
401                    let t = self.check(nat_ite)?;
402                    let nn = self.raw_arrow(c.nat, c.nat);
403                    let nnn = self.raw_arrow(c.nat, nn);
404                    let expect = self.raw_arrow(c.bool_, nnn);
405                    if self.defeq(t, expect)?.is_err() {
406                        return Ok(Err(Fail));
407                    }
408                    for (bv, first) in [(c.tru, true), (c.fal, false)] {
409                        let lhs = self.s.app(nat_ite, bv);
410                        let (b0, b1) = (self.s.bvar(0), self.s.bvar(1));
411                        let pick = if first { b1 } else { b0 };
412                        let inner = self.lam0(c.nat, pick);
413                        let rhs = self.lam0(c.nat, inner);
414                        if self.defeq(lhs, rhs)?.is_err() {
415                            return Ok(Err(Fail));
416                        }
417                    }
418                }
419                Ok(Ok(()))
420            }
421        }
422    }
423
424    fn cond_ite(
425        &mut self,
426        cond: &Condition,
427        c: &C,
428        alpha: ExprId,
429        args: &[ExprId],
430        t: ExprId,
431        e: ExprId,
432    ) -> ExprId {
433        let p = self.apps(cond.prop, args);
434        let d = self.apps(cond.dec, args);
435        self.apps(c.ite1, &[alpha, p, d, t, e])
436    }
437
438    fn cond_dite(
439        &mut self,
440        cond: &Condition,
441        c: &C,
442        args: &[ExprId],
443        t: ExprId,
444        e: ExprId,
445    ) -> ExprId {
446        let p = self.apps(cond.prop, args);
447        let d = self.apps(cond.dec, args);
448        let tl = self.lam0(p, t);
449        let np = self.s.app(c.not, p);
450        let el = self.lam0(np, e);
451        self.apps(c.dite_nat, &[p, d, tl, el])
452    }
453
454    fn cond_decide(&mut self, cond: &Condition, c: &C, args: &[ExprId]) -> ExprId {
455        self.cond_ite(cond, c, c.bool_, args, c.tru, c.fal)
456    }
457
458    fn nat3(&mut self, c: &C) -> ExprId {
459        let nn = self.raw_arrow(c.nat, c.nat);
460        self.raw_arrow(c.nat, nn)
461    }
462
463    fn defeq1n(&mut self, c: &C, a: ExprId, b: ExprId) -> KResult<bool> {
464        let pa = self.raw_arrow(c.nat, a);
465        let pb = self.raw_arrow(c.nat, b);
466        self.is_def_eq(pa, pb)
467    }
468
469    fn check_div_mod_common(
470        &mut self,
471        d: &DefnDecl,
472        refs: &Refs,
473        c: &C,
474        go_name: &str,
475    ) -> KResult<V<(ExprId, Condition)>> {
476        let sub = self.wk.nat_sub;
477        if !self.env.contains(sub) || !self.env.contains(self.wk.bool_) {
478            return Ok(Err(Fail));
479        }
480        let n3 = self.nat3(c);
481        if self.defeq(d.header.ty, n3)?.is_err() {
482            return Ok(Err(Fail));
483        }
484        let le = refs.get("natLE.prop")?;
485        let le_t = self.check(le)?;
486        let nnp = refs.get("natLE.type")?;
487        if self.defeq(le_t, nnp)?.is_err() {
488            return Ok(Err(Fail));
489        }
490        let go = self.c0n(go_name);
491        if self.env.get(self.s.const_head(go).unwrap().0).is_none() {
492            return Ok(Err(Fail));
493        }
494        let go_t = self.check(go)?;
495        let go_ty = refs.get("goType")?;
496        if self.defeq(go_t, go_ty)?.is_err() {
497            return Ok(Err(Fail));
498        }
499        let cond = self.cond_nat_le(refs)?;
500        Ok(Ok((go, cond)))
501    }
502
503    fn check_mod(&mut self, d: &DefnDecl, refs: &Refs, c: &C) -> KResult<V<()>> {
504        let (go, cond) = match self.check_div_mod_common(d, refs, c, "Nat.modCore.go")? {
505            Ok(x) => x,
506            Err(f) => return Ok(Err(f)),
507        };
508        let v = d.value;
509        let x = self.s.bvar(0);
510        let m0 = self.apps(v, &[c.zero, x]);
511        if !self.defeq1n(c, m0, c.zero)? {
512            return Ok(Err(Fail));
513        }
514        if self.condition_check(&cond, c, true, true)?.is_err() {
515            return Ok(Err(Fail));
516        }
517        let lt_succ_self = self.c0n("Nat.lt_succ_self");
518        let fuel_lemma = self.c0n("Nat.div_rec_fuel_lemma");
519        let sub = self.s.cnst(self.wk.nat_sub, LevelsId::EMPTY);
520        let le = refs.get("natLE.prop")?;
521        let one = self.s.app(c.succ, c.zero);
522        let x = self.push_local(c.nat, None);
523        let y = self.push_local(c.nat, None);
524        let sx = self.s.app(c.succ, x);
525        let ssx = self.s.app(c.succ, sx);
526        let lt = self.s.app(lt_succ_self, sx);
527        let h0 = self.s.bvar(0);
528        let go_app = self.apps(go, &[y, h0, ssx, sx, lt]);
529        let inner = self.cond_dite(&cond, c, &[one, y], go_app, sx);
530        let e = self.cond_ite(&cond, c, c.nat, &[y, sx], inner, sx);
531        self.check(e)?;
532        let lhs = self.apps(v, &[sx, y]);
533        if self.defeq(lhs, e)?.is_err() {
534            return Ok(Err(Fail));
535        }
536        let hy_ty = self.apps(le, &[one, y]);
537        let hy = self.push_local(hy_ty, None);
538        let fuel = self.push_local(c.nat, None);
539        let sfuel = self.s.app(c.succ, fuel);
540        let h_ty = self.apps(le, &[sx, sfuel]);
541        let h = self.push_local(h_ty, None);
542        let xy = self.apps(sub, &[x, y]);
543        let lem = self.apps(fuel_lemma, &[x, y, fuel, hy, h0, h]);
544        let rec = self.apps(go, &[y, hy, fuel, xy, lem]);
545        let e = self.cond_dite(&cond, c, &[y, x], rec, x);
546        self.check(e)?;
547        let lhs = self.apps(go, &[y, hy, sfuel, x, h]);
548        self.defeq(lhs, e)
549    }
550
551    fn check_div(&mut self, d: &DefnDecl, refs: &Refs, c: &C) -> KResult<V<()>> {
552        let sub_ok = self.env.contains(self.wk.nat_sub) && self.env.contains(self.wk.bool_);
553        if !sub_ok {
554            return Ok(Err(Fail));
555        }
556        let n3 = self.nat3(c);
557        if self.defeq(d.header.ty, n3)?.is_err() {
558            return Ok(Err(Fail));
559        }
560        let cond = self.cond_nat_le(refs)?;
561        if self.condition_check(&cond, c, false, true)?.is_err() {
562            return Ok(Err(Fail));
563        }
564        let (go, _) = match self.check_div_mod_common(d, refs, c, "Nat.div.go")? {
565            Ok(x) => x,
566            Err(f) => return Ok(Err(f)),
567        };
568        let v = d.value;
569        let lt_succ_self = self.c0n("Nat.lt_succ_self");
570        let fuel_lemma = self.c0n("Nat.div_rec_fuel_lemma");
571        let sub = self.s.cnst(self.wk.nat_sub, LevelsId::EMPTY);
572        let le = refs.get("natLE.prop")?;
573        let one = self.s.app(c.succ, c.zero);
574        let h0 = self.s.bvar(0);
575        let x = self.push_local(c.nat, None);
576        let y = self.push_local(c.nat, None);
577        let sx = self.s.app(c.succ, x);
578        let lt = self.s.app(lt_succ_self, x);
579        let go_app = self.apps(go, &[y, h0, sx, x, lt]);
580        let e = self.cond_dite(&cond, c, &[one, y], go_app, c.zero);
581        self.check(e)?;
582        let lhs = self.apps(v, &[x, y]);
583        if self.defeq(lhs, e)?.is_err() {
584            return Ok(Err(Fail));
585        }
586        let hy_ty = self.apps(le, &[one, y]);
587        let hy = self.push_local(hy_ty, None);
588        let fuel = self.push_local(c.nat, None);
589        let sfuel = self.s.app(c.succ, fuel);
590        let h_ty = self.apps(le, &[sx, sfuel]);
591        let h = self.push_local(h_ty, None);
592        let xy = self.apps(sub, &[x, y]);
593        let lem = self.apps(fuel_lemma, &[x, y, fuel, hy, h0, h]);
594        let rec = self.apps(go, &[y, hy, fuel, xy, lem]);
595        let srec = self.s.app(c.succ, rec);
596        let e = self.cond_dite(&cond, c, &[y, x], srec, c.zero);
597        self.check(e)?;
598        let lhs = self.apps(go, &[y, hy, sfuel, x, h]);
599        self.defeq(lhs, e)
600    }
601
602    fn check_gcd(&mut self, d: &DefnDecl, refs: &Refs, c: &C) -> KResult<V<()>> {
603        if !self.env.contains(self.wk.nat_mod) {
604            return Ok(Err(Fail));
605        }
606        let n3 = self.nat3(c);
607        if self.defeq(d.header.ty, n3)?.is_err() {
608            return Ok(Err(Fail));
609        }
610        let m = self.push_local(c.nat, None);
611        let n = self.push_local(c.nat, None);
612        let eq_def = refs.get("gcd.eq_def")?;
613        let gcd2 = match self.unfold_nat_well_founded(d.value, &[m, n], eq_def, refs, c)? {
614            Ok(g) => g,
615            Err(f) => return Ok(Err(f)),
616        };
617        let lhs = self.apps(gcd2, &[c.zero, m]);
618        if self.defeq(lhs, m)?.is_err() {
619            return Ok(Err(Fail));
620        }
621        let modc = self.s.cnst(self.wk.nat_mod, LevelsId::EMPTY);
622        let sn = self.s.app(c.succ, n);
623        let lhs = self.apps(gcd2, &[sn, m]);
624        let mm = self.apps(modc, &[m, sn]);
625        let rhs = self.apps(d.value, &[mm, sn]);
626        self.defeq(lhs, rhs)
627    }
628
629    fn check_bitwise(&mut self, d: &DefnDecl, refs: &Refs, c: &C) -> KResult<V<()>> {
630        if !self.env.contains(self.wk.nat) || !self.env.contains(self.wk.bool_) {
631            return Ok(Err(Fail));
632        }
633        let bb = self.raw_arrow(c.bool_, c.bool_);
634        let bbb = self.raw_arrow(c.bool_, bb);
635        let n3 = self.nat3(c);
636        let expect = self.raw_arrow(bbb, n3);
637        if self.defeq(d.header.ty, expect)?.is_err() {
638            return Ok(Err(Fail));
639        }
640        let f = self.push_local(bbb, None);
641        let n = self.push_local(c.nat, None);
642        let m = self.push_local(c.nat, None);
643        let eq_def = refs.get("bitwise.eq_def")?;
644        let bw2 = match self.unfold_nat_well_founded(d.value, &[f, n, m], eq_def, refs, c)? {
645            Ok(g) => g,
646            Err(fl) => return Ok(Err(fl)),
647        };
648        let ce = self.cond_nat_eq(refs)?;
649        if self.condition_check(&ce, c, true, false)?.is_err() {
650            return Ok(Err(Fail));
651        }
652        let bc = self.cond_bool(refs)?;
653        if self.condition_check(&bc, c, true, false)?.is_err() {
654            return Ok(Err(Fail));
655        }
656        let div = self.s.cnst(self.wk.nat_div, LevelsId::EMPTY);
657        let modc = self.s.cnst(self.wk.nat_mod, LevelsId::EMPTY);
658        let add = self.s.cnst(self.wk.nat_add, LevelsId::EMPTY);
659        let one = self.s.app(c.succ, c.zero);
660        let two = self.s.app(c.succ, one);
661        let f_ft = self.apps(f, &[c.fal, c.tru]);
662        let t1 = self.cond_ite(&bc, c, c.nat, &[f_ft], m, c.zero);
663        let f_tf = self.apps(f, &[c.tru, c.fal]);
664        let t2 = self.cond_ite(&bc, c, c.nat, &[f_tf], n, c.zero);
665        let n2 = self.apps(div, &[n, two]);
666        let m2 = self.apps(div, &[m, two]);
667        let nmod = self.apps(modc, &[n, two]);
668        let mmod = self.apps(modc, &[m, two]);
669        let b1 = self.cond_decide(&ce, c, &[nmod, one]);
670        let b2 = self.cond_decide(&ce, c, &[mmod, one]);
671        let r = self.apps(d.value, &[f, n2, m2]);
672        let rr = self.apps(add, &[r, r]);
673        let rr1 = self.apps(add, &[rr, one]);
674        let fb = self.apps(f, &[b1, b2]);
675        let last = self.cond_ite(&bc, c, c.nat, &[fb], rr1, rr);
676        let inner = self.cond_ite(&ce, c, c.nat, &[m, c.zero], t2, last);
677        let e = self.cond_ite(&ce, c, c.nat, &[n, c.zero], t1, inner);
678        self.check(e)?;
679        let lhs = self.apps(bw2, &[f, n, m]);
680        self.defeq(lhs, e)
681    }
682
683    fn lambda_telescope(&mut self, mut e: ExprId) -> (Vec<ExprId>, ExprId) {
684        let mut fvs = Vec::new();
685        while let Node::Lam(d, b) = self.s.node(e) {
686            let dt = self.s.instantiate_rev(d, &fvs);
687            fvs.push(self.push_local(dt, None));
688            e = b;
689        }
690        let body = self.s.instantiate_rev(e, &fvs);
691        (fvs, body)
692    }
693
694    fn forall_telescope(&mut self, mut e: ExprId) -> (Vec<ExprId>, ExprId) {
695        let mut fvs = Vec::new();
696        while let Node::Pi(d, b) = self.s.node(e) {
697            let dt = self.s.instantiate_rev(d, &fvs);
698            fvs.push(self.push_local(dt, None));
699            e = b;
700        }
701        let body = self.s.instantiate_rev(e, &fvs);
702        (fvs, body)
703    }
704
705    fn replace_expr(
706        &mut self,
707        e: ExprId,
708        from: ExprId,
709        to: ExprId,
710        memo: &mut FxMap<ExprId, ExprId>,
711    ) -> ExprId {
712        if e == from {
713            return to;
714        }
715        if let Some(r) = memo.get(&e) {
716            return *r;
717        }
718        let r = match self.s.node(e) {
719            Node::App(f, a) => {
720                let (f2, a2) = (
721                    self.replace_expr(f, from, to, memo),
722                    self.replace_expr(a, from, to, memo),
723                );
724                self.s.app(f2, a2)
725            }
726            Node::Lam(t, b) => {
727                let (t2, b2) = (
728                    self.replace_expr(t, from, to, memo),
729                    self.replace_expr(b, from, to, memo),
730                );
731                self.s.lam(t2, b2)
732            }
733            Node::Pi(t, b) => {
734                let (t2, b2) = (
735                    self.replace_expr(t, from, to, memo),
736                    self.replace_expr(b, from, to, memo),
737                );
738                self.s.pi(t2, b2)
739            }
740            Node::Let(t, v, b) => {
741                let t2 = self.replace_expr(t, from, to, memo);
742                let v2 = self.replace_expr(v, from, to, memo);
743                let b2 = self.replace_expr(b, from, to, memo);
744                self.s.let_(t2, v2, b2)
745            }
746            Node::Proj(n, i, x) => {
747                let x2 = self.replace_expr(x, from, to, memo);
748                self.s.proj(n, i, x2)
749            }
750            _ => e,
751        };
752        memo.insert(e, r);
753        r
754    }
755
756    /// lean4lean's `unfoldNatWellFounded`: shows the definition `e`, applied to `fvs`, unfolds
757    /// through `WellFounded.Nat.fix` to the right-hand side of its `eq_def`, and returns that
758    /// right-hand side abstracted over `fvs` (with the recursive constant replaced by `e`).
759    fn unfold_nat_well_founded(
760        &mut self,
761        e: ExprId,
762        fvs: &[ExprId],
763        eq_def: ExprId,
764        _refs: &Refs,
765        c: &C,
766    ) -> KResult<V<ExprId>> {
767        let mut body = eq_def;
768        while let Node::Pi(_, b) = self.s.node(body) {
769            body = b;
770        }
771        let body = self.s.instantiate_rev(body, fvs);
772        let Node::App(eq_l, rhs) = self.s.node(body) else {
773            return Ok(Err(Fail));
774        };
775        let Node::App(_, lhs) = self.s.node(eq_l) else {
776            return Ok(Err(Fail));
777        };
778        let orig = self.s.app_fn(lhs);
779        let rhs = self.replace_expr(rhs, orig, e, &mut FxMap::default());
780        let applied = self.apps(e, fvs);
781        let e1 = self.whnf_core(applied, false)?;
782        let Some(e1) = self.unfold_definition(e1) else {
783            return Ok(Err(Fail));
784        };
785        let e1w = self.whnf_core(e1, false)?;
786        let (fix, args) = self.s.app_args(e1w);
787        let fix_name = self.s.names.dotted("WellFounded.Nat.fix");
788        let Node::Const(fixn, fix_ls) = self.s.node(fix) else {
789            return Ok(Err(Fail));
790        };
791        if fixn != fix_name || self.s.levels.get_list(fix_ls).len() != 2 || args.len() != 5 {
792            return Ok(Err(Fail));
793        }
794        let (alpha, motive, f, big_f, a0) = (args[0], args[1], args[2], args[3], args[4]);
795        let fix_fn = self.apps(fix, &[alpha, motive, f, big_f]);
796        {
797            let a0t = self.infer(a0, true)?;
798            let a = self.push_local(a0t, None);
799            let fa = self.s.app(fix_fn, a);
800            let Some(u) = self.unfold_definition(fa) else {
801                return Ok(Err(Fail));
802            };
803            let e1 = self.whnf_core(u, false)?;
804            let (fix_go, gargs) = self.s.app_args(e1);
805            if gargs.len() != 7
806                || (gargs[0], gargs[1], gargs[2], gargs[3], gargs[5])
807                    != (alpha, motive, f, big_f, a)
808            {
809                return Ok(Err(Fail));
810            }
811            let fuel = gargs[4];
812            let Node::App(eager, nn) = self.s.node(fuel) else {
813                return Ok(Err(Fail));
814            };
815            let fa2 = self.s.app(f, a);
816            let sfa = self.s.app(c.succ, fa2);
817            if !self.is_def_eq(nn, sfa)? {
818                return Ok(Err(Fail));
819            }
820            if !self.env.contains(self.wk.nat_beq) {
821                return Ok(Err(Fail));
822            }
823            let bc = self.cond_bool(_refs)?;
824            if self.condition_check(&bc, c, true, false)?.is_err() {
825                return Ok(Err(Fail));
826            }
827            let x = self.s.bvar(0);
828            let beq = self.s.cnst(self.wk.nat_beq, LevelsId::EMPTY);
829            let lhs = self.s.app(eager, x);
830            let bxx = self.apps(beq, &[x, x]);
831            let rhs_e = self.cond_ite(&bc, c, c.nat, &[bxx], x, x);
832            if !self.defeq1n(c, lhs, rhs_e)? {
833                return Ok(Err(Fail));
834            }
835            let go2 = self.unfold_definition(fix_go).unwrap_or(fix_go);
836            let (gfvs, go_body) = self.lambda_telescope(go2);
837            if gfvs.len() != 5 {
838                return Ok(Err(Fail));
839            }
840            let (gf, t) = (gfvs[3], gfvs[4]);
841            let Node::App(nat_rec, t2) = self.s.node(go_body) else {
842                return Ok(Err(Fail));
843            };
844            let t_idx = self.fvar_index(t);
845            let mentions_t = self.s.any_node(
846                nat_rec,
847                &mut |s, n| matches!(s.node(n), Node::FVar(i) if i == t_idx),
848            );
849            if mentions_t || t != t2 {
850                return Ok(Err(Fail));
851            }
852            let st = self.s.app(c.succ, t);
853            self.check(st)?;
854            let nr_st = self.s.app(nat_rec, st);
855            let gor = self.whnf_core(nr_st, false)?;
856            let (xfvs, gor_body) = self.lambda_telescope(gor);
857            if xfvs.len() != 2 {
858                return Ok(Err(Fail));
859            }
860            let Node::App(fx, ih) = self.s.node(gor_body) else {
861                return Ok(Err(Fail));
862            };
863            let expect_fx = self.s.app(gf, xfvs[0]);
864            if fx != expect_fx {
865                return Ok(Err(Fail));
866            }
867            let (yfvs, ih_body) = self.lambda_telescope(ih);
868            if yfvs.len() != 2 {
869                return Ok(Err(Fail));
870            }
871            let Node::App(ih_head, _) = self.s.node(ih_body) else {
872                return Ok(Err(Fail));
873            };
874            let nrt = self.s.app(nat_rec, t);
875            let expect = self.s.app(nrt, yfvs[0]);
876            if ih_head != expect {
877                return Ok(Err(Fail));
878            }
879        }
880        let fa0 = self.s.app(big_f, a0);
881        let ft = self.infer(fa0, true)?;
882        let Node::Pi(dom, _) = self.s.node(ft) else {
883            return Ok(Err(Fail));
884        };
885        let (dfvs, _) = self.forall_telescope(dom);
886        if dfvs.len() != 2 {
887            return Ok(Err(Fail));
888        }
889        let fy = self.s.app(fix_fn, dfvs[0]);
890        let ih2 = self.mk_lambda(&dfvs, fy);
891        let rhs2 = self.apps(big_f, &[a0, ih2]);
892        self.check(rhs2)?;
893        if !self.is_def_eq(rhs, rhs2)? {
894            return Ok(Err(Fail));
895        }
896        Ok(Ok(self.mk_lambda(fvs, rhs)))
897    }
898}
logicaffeine_kernel/dag/primitive_wf.rs

logicaffeine_kernel/dag/
primitive_wf.rs
