diff --git a/Cargo.toml b/Cargo.toml index 2b5276c..998e190 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -5,6 +5,7 @@ members = [ "crates/my-cli", # Command-line interface (my binary) "crates/my-hir", "crates/my-mir", + "crates/my-qtt", # QTT verified-core checker (faithful port of Coq R5 check / R5b aff_type_dec) "crates/my-llvm", # LLVM code generation "crates/my-lsp", "crates/my-pkg", @@ -33,6 +34,7 @@ repository = "https://github.com/hyperpolymath/my-lang" my-lang = { path = "crates/my-lang" } my-hir = { path = "crates/my-hir" } my-mir = { path = "crates/my-mir" } +my-qtt = { path = "crates/my-qtt" } my-llvm = { path = "crates/my-llvm" } my-ai = { path = "crates/my-ai" } diff --git a/crates/my-qtt/Cargo.toml b/crates/my-qtt/Cargo.toml new file mode 100644 index 0000000..0aec9a6 --- /dev/null +++ b/crates/my-qtt/Cargo.toml @@ -0,0 +1,12 @@ +# SPDX-License-Identifier: MPL-2.0 +# SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell +[package] +name = "my-qtt" +version.workspace = true +edition.workspace = true +license.workspace = true +authors.workspace = true +repository.workspace = true +description = "QTT verified-core checker for my-lang: a faithful Rust port of the machine-checked Coq usage-walk synthesiser (SoloCore.v R5 `check` / R5b `aff_type_dec`)." + +[dependencies] diff --git a/crates/my-qtt/src/lib.rs b/crates/my-qtt/src/lib.rs new file mode 100644 index 0000000..90d680a --- /dev/null +++ b/crates/my-qtt/src/lib.rs @@ -0,0 +1,419 @@ +// SPDX-License-Identifier: MPL-2.0 +// SPDX-FileCopyrightText: 2026 Jonathan D.A. Jewell + +//! # `my-qtt` — the QTT verified-core checker +//! +//! A **faithful Rust port** of the machine-checked Coq usage-walk synthesiser +//! `check` (rung **R5**) and the affine-budget decision `aff_type_dec` (**R5b**) +//! from `proofs/verification/coq/solo-core/SoloCore.v`. This is the first +//! concrete step of the *fundamentals ⇄ implementation coupling*: the QTT +//! resource discipline the proofs establish, executed by the compiler rather +//! than re-implemented ad hoc. (Today the conventional `crates/my-lang` +//! checker has no usage axis — see `proofs/STATUS.md` §"Implementation ⇄ spec +//! coupling".) +//! +//! [`check`] : `Tctx -> Tm -> Option<(Ty, Uvec)>` is a one-pass synthesiser +//! that returns BOTH the type and the EXACT usage vector a term realises. The +//! Coq `check_correct` theorem proves `has_type G D t a <-> check G t = +//! Some (a, D)` (axiom-free, CI-gated). The four `reflexivity` examples in +//! `SoloCore.v` (`check_id_unit` / `check_drop_linear` / `check_dup_linear` / +//! `check_dup_omega`) are reproduced below as `#[test]`s, so this port is +//! checked against the verified algorithm's own closed computations. +//! +//! ## Representation note (de Bruijn ⇄ `Vec`) +//! The Coq context is a snoc-list `TSnoc G a` where de Bruijn index `0` is the +//! most-recently-bound (innermost) variable. Here [`Tctx`]` = Vec` with the +//! **last** element innermost: entering a binder is `push`, index `n` reads +//! `g[g.len()-1-n]`, and a body's synthesised usage carries the binder's +//! quantity as its **last** element (the Coq `USnoc D qb` shape, recovered by +//! `pop`). +//! +//! ## Scope +//! Exactly the mechanised QTT solo core (`tm`). Wiring the full my-lang surface +//! AST onto this core (so the running compiler enforces the resource axis) is +//! the next coupling step; this crate is the verified engine it will call. + +#![forbid(unsafe_code)] + +/// Quantities: the three-point affine semiring `{0, 1, ω}` (Coq `Quantity.Q`). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Q { + Zero, + One, + Omega, +} + +/// Echo linearity mode — the thin poset `linear ⊑ affine` (Coq `Mode`). +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum Mode { + Linear, + Affine, +} + +/// QTT core types (Coq `ty`). +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Ty { + Unit, + /// additive product `a & b` (shared usage, projected by `Fst`/`Snd`) + With(Box, Box), + /// multiplicative product `a ⊗ b` (split usage, eliminated by `LetPair`) + Tensor(Box, Box), + Sum(Box, Box), + /// `(q x : a) -> b` + Arr(Q, Box, Box), + /// echo residue `[m] Echo b>` + Echo(Mode, Box, Box), +} + +/// QTT core terms, de Bruijn (Coq `tm`). +#[derive(Debug, Clone, PartialEq, Eq)] +pub enum Tm { + Var(usize), + UnitT, + Lam(Q, Ty, Box), + App(Box, Box), + With(Box, Box), + Fst(Box), + Snd(Box), + Tensor(Box, Box), + /// `let (x, y) = e1 in e2` — `e2` binds two vars (index 1 = `x`, 0 = `y`) + LetPair(Box, Box), + /// annotation = the OTHER summand + Inl(Ty, Box), + Inr(Ty, Box), + /// scrutinee, left arm (binds 1), right arm (binds 1) + Case(Box, Box, Box), + /// `let (q x) = e1 in e2` + Let(Q, Box, Box), + MkEcho(Mode, Ty, Ty, Box), + Weaken(Box), +} + +/// Type context; last element = innermost binder (de Bruijn `0`). +pub type Tctx = Vec; +/// Usage vector, aligned slot-for-slot with a [`Tctx`]. +pub type Uvec = Vec; + +// ----- the Q semiring (Coq `Quantity.v` qadd/qmul/qle) ----- + +/// Additive accounting: `0` identity, `1+1 = ω`, anything with `ω` is `ω`. +pub fn qadd(a: Q, b: Q) -> Q { + use Q::*; + match (a, b) { + (Zero, q) => q, + (One, Zero) => One, + (One, One) => Omega, + (One, Omega) => Omega, + (Omega, _) => Omega, + } +} + +/// Multiplicative scaling: `0` absorbing, `1` identity, `ω·ω = ω`. +pub fn qmul(a: Q, b: Q) -> Q { + use Q::*; + match (a, b) { + (Zero, _) => Zero, + (One, q) => q, + (Omega, Zero) => Zero, + (Omega, One) => Omega, + (Omega, Omega) => Omega, + } +} + +/// Subquantity order: a value of quantity `a` may be used where `b` is +/// expected. The affine weakening `qle Zero One = true` is the discard. +pub fn qle(a: Q, b: Q) -> bool { + use Q::*; + match (a, b) { + (Zero, _) => true, + (_, Omega) => true, + (One, One) => true, + (One, Zero) => false, + (Omega, Zero) => false, + (Omega, One) => false, + } +} + +// ----- usage vectors (Coq uzero/onehot/uadd/uscale/ule) ----- + +/// All-`Zero` usage of length `n` (Coq `uzero`). +pub fn uzero(n: usize) -> Uvec { + vec![Q::Zero; n] +} + +/// `One` at the de Bruijn-`n` slot (`len-1-n`), `Zero` elsewhere (Coq `onehot`). +pub fn onehot(len: usize, n: usize) -> Uvec { + let mut d = vec![Q::Zero; len]; + if n < len { + d[len - 1 - n] = Q::One; + } + d +} + +/// Pointwise add; `None` on length mismatch (Coq `uadd` is partial on shape). +pub fn uadd(d1: &[Q], d2: &[Q]) -> Option { + if d1.len() != d2.len() { + return None; + } + Some(d1.iter().zip(d2).map(|(&x, &y)| qadd(x, y)).collect()) +} + +/// Scale every slot by `q` (Coq `uscale`). +pub fn uscale(q: Q, d: &[Q]) -> Uvec { + d.iter().map(|&x| qmul(q, x)).collect() +} + +/// Pointwise order: equal length and `qle` at every slot (Coq `ule`). +pub fn ule(d: &[Q], d2: &[Q]) -> bool { + d.len() == d2.len() && d.iter().zip(d2).all(|(&x, &y)| qle(x, y)) +} + +/// `n`-th type from the innermost end (Coq `tnth`). +fn tnth(g: &[Ty], n: usize) -> Option<&Ty> { + if n < g.len() { + Some(&g[g.len() - 1 - n]) + } else { + None + } +} + +// ----- the usage-walk synthesiser (Coq `check`, SoloCore.v:2128) ----- + +/// One-pass synthesiser: returns the type and the EXACT realised usage, or +/// `None` if the term is ill-typed or mis-used (a linear binder dropped or +/// duplicated). Faithful to the Coq `check`; `check_correct` proves it agrees +/// with the declarative `has_type` judgement. +pub fn check(g: &[Ty], t: &Tm) -> Option<(Ty, Uvec)> { + match t { + Tm::Var(n) => tnth(g, *n).map(|a| (a.clone(), onehot(g.len(), *n))), + + Tm::UnitT => Some((Ty::Unit, uzero(g.len()))), + + Tm::Lam(q, a, body) => { + let mut g2 = g.to_vec(); + g2.push(a.clone()); + let (b, mut d) = check(&g2, body)?; + let qb = d.pop()?; // innermost binder's usage (the `USnoc _ qb` top) + if qb == *q { + Some((Ty::Arr(*q, Box::new(a.clone()), Box::new(b)), d)) + } else { + None + } + } + + Tm::App(t1, t2) => { + let (f, d1) = check(g, t1)?; + let (a2, d2) = check(g, t2)?; + match f { + Ty::Arr(q, a, b) if a2 == *a => uadd(&d1, &uscale(q, &d2)).map(|d| (*b, d)), + _ => None, + } + } + + Tm::With(t1, t2) => { + let (a, d1) = check(g, t1)?; + let (b, d2) = check(g, t2)?; + // additive product: both components SHARE the same usage. + if d1 == d2 { + Some((Ty::With(Box::new(a), Box::new(b)), d1)) + } else { + None + } + } + + Tm::Fst(t1) => match check(g, t1)? { + (Ty::With(a, _), d) => Some((*a, d)), + _ => None, + }, + + Tm::Snd(t1) => match check(g, t1)? { + (Ty::With(_, b), d) => Some((*b, d)), + _ => None, + }, + + Tm::Tensor(t1, t2) => { + let (a, d1) = check(g, t1)?; + let (b, d2) = check(g, t2)?; + // multiplicative product: usage is SPLIT (added). + uadd(&d1, &d2).map(|d| (Ty::Tensor(Box::new(a), Box::new(b)), d)) + } + + Tm::LetPair(t1, t2) => { + let (ta, d1) = check(g, t1)?; + if let Ty::Tensor(a, b) = ta { + let mut g2 = g.to_vec(); + g2.push(*a); // x : a (index 1 in body) + g2.push(*b); // y : b (index 0 in body, innermost) + let (c, mut d) = check(&g2, t2)?; + let q1 = d.pop()?; // innermost (y) usage — must be linear + let q2 = d.pop()?; // next (x) usage — must be linear + if q1 == Q::One && q2 == Q::One { + uadd(&d1, &d).map(|dd| (c, dd)) + } else { + None + } + } else { + None + } + } + + Tm::Inl(b, t1) => check(g, t1).map(|(a, d)| (Ty::Sum(Box::new(a), Box::new(b.clone())), d)), + + Tm::Inr(a, t1) => check(g, t1).map(|(b, d)| (Ty::Sum(Box::new(a.clone()), Box::new(b)), d)), + + Tm::Case(t1, tl, tr) => { + let (ts, d1) = check(g, t1)?; + if let Ty::Sum(a, b) = ts { + let mut gl = g.to_vec(); + gl.push(*a); + let mut gr = g.to_vec(); + gr.push(*b); + let (cl, mut dl) = check(&gl, tl)?; + let (cr, mut dr) = check(&gr, tr)?; + let ql = dl.pop()?; // left arm binder usage — linear + let qr = dr.pop()?; // right arm binder usage — linear + // both arms: bind linearly, agree on result type AND residual usage. + if ql == Q::One && qr == Q::One && cl == cr && dl == dr { + uadd(&d1, &dl).map(|d| (cl, d)) + } else { + None + } + } else { + None + } + } + + Tm::Let(q, t1, t2) => { + let (a, d1) = check(g, t1)?; + let mut g2 = g.to_vec(); + g2.push(a); + let (b, mut d2) = check(&g2, t2)?; + let qb = d2.pop()?; + if qb == *q { + uadd(&uscale(*q, &d1), &d2).map(|d| (b, d)) + } else { + None + } + } + + Tm::MkEcho(m, a, b, t1) => { + let (a2, d) = check(g, t1)?; + if a2 == *a { + Some((Ty::Echo(*m, Box::new(a.clone()), Box::new(b.clone())), d)) + } else { + None + } + } + + Tm::Weaken(t1) => match check(g, t1)? { + // a Linear echo weakens to an Affine one (one-way; no section). + (Ty::Echo(Mode::Linear, a, b), d) => Some((Ty::Echo(Mode::Affine, a, b), d)), + _ => None, + }, + } +} + +/// Affine-budget decision (Coq `aff_type_dec`, via `aff_type_iff`): the term +/// has type `expected` within usage `budget` iff the UNIQUE synthesised usage +/// fits (`ule realised budget`). The affine **discard** lives here — a +/// `One`-budget resource may be left unused (`Zero <= One`), which strict +/// linear [`check`] rejects. +pub fn aff_check(g: &[Ty], t: &Tm, expected: &Ty, budget: &[Q]) -> bool { + match check(g, t) { + Some((a0, d0)) => &a0 == expected && ule(&d0, budget), + None => false, + } +} + +#[cfg(test)] +mod tests { + //! Oracle tests: each mirrors a `reflexivity` `Example` in `SoloCore.v`, so + //! a green run means this port computes what the machine-checked algorithm + //! computes on the same closed terms. + use super::*; + use Q::*; + + fn b(x: T) -> Box { + Box::new(x) + } + fn arr(q: Q, a: Ty, r: Ty) -> Ty { + Ty::Arr(q, b(a), b(r)) + } + fn lam(q: Q, a: Ty, body: Tm) -> Tm { + Tm::Lam(q, a, b(body)) + } + fn tensor(x: Tm, y: Tm) -> Tm { + Tm::Tensor(b(x), b(y)) + } + + /// Coq `check_id_unit`: the `One`-binder is used exactly once -> accepted, + /// synthesising the type AND the (empty, closed) usage. + #[test] + fn check_id_unit() { + let t = lam(One, Ty::Unit, Tm::Var(0)); + assert_eq!( + check(&[], &t), + Some((arr(One, Ty::Unit, Ty::Unit), vec![])) + ); + } + + /// Coq `check_drop_linear`: a `One`-binder left UNUSED -> rejected. + #[test] + fn check_drop_linear() { + let t = lam(One, Ty::Unit, Tm::UnitT); + assert_eq!(check(&[], &t), None); + } + + /// Coq `check_dup_linear`: a `One`-binder used TWICE (usage `ω`) -> rejected. + #[test] + fn check_dup_linear() { + let t = lam(One, Ty::Unit, tensor(Tm::Var(0), Tm::Var(0))); + assert_eq!(check(&[], &t), None); + } + + /// Coq `check_dup_omega`: the SAME body under an `ω`-binder -> accepted, so + /// the rejection above is exactly the linearity check. + #[test] + fn check_dup_omega() { + let t = lam(Omega, Ty::Unit, tensor(Tm::Var(0), Tm::Var(0))); + assert_eq!( + check(&[], &t), + Some((arr(Omega, Ty::Unit, Ty::Tensor(b(Ty::Unit), b(Ty::Unit))), vec![])) + ); + } + + /// Coq `aff_discard_ok` (R5b): with one `Unit` in scope at budget `One`, + /// the affine judgement ACCEPTS dropping it (realises `Zero <= One`); the + /// strict linear walk realises usage `[Zero]`, not `[One]`. + #[test] + fn aff_discard_ok() { + let g = vec![Ty::Unit]; + assert_eq!(check(&g, &Tm::UnitT), Some((Ty::Unit, vec![Zero]))); + assert!(aff_check(&g, &Tm::UnitT, &Ty::Unit, &[One])); + } + + /// The echo weakening rung: `Weaken (echo_L a b v) : echo_A a b`. + #[test] + fn weaken_linear_to_affine() { + let inner = Tm::MkEcho(Mode::Linear, Ty::Unit, Ty::Unit, b(Tm::UnitT)); + let t = Tm::Weaken(b(inner)); + assert_eq!( + check(&[], &t), + Some((Ty::Echo(Mode::Affine, b(Ty::Unit), b(Ty::Unit)), vec![])) + ); + // and the reverse weakening (affine -> ... ) has no source: an Affine + // echo is not a `Weaken` redex, so `check` rejects weakening it again. + let aff = Tm::MkEcho(Mode::Affine, Ty::Unit, Ty::Unit, b(Tm::UnitT)); + assert_eq!(check(&[], &Tm::Weaken(b(aff))), None); + } + + /// Semiring spot-checks against the Coq tables. + #[test] + fn semiring_tables() { + assert_eq!(qadd(One, One), Omega); + assert_eq!(qmul(Omega, Zero), Zero); + assert!(qle(Zero, One)); + assert!(!qle(One, Zero)); + assert!(qle(Omega, Omega)); + } +} diff --git a/proofs/verification/idris/solo-core/Substitution.idr b/proofs/verification/idris/solo-core/Substitution.idr index 787aea4..944239c 100644 --- a/proofs/verification/idris/solo-core/Substitution.idr +++ b/proofs/verification/idris/solo-core/Substitution.idr @@ -487,3 +487,259 @@ htShift i g c dg di (Let q t1 t2) hlen (THLet d1 d2 _ a' h1 h2 prf) = uaddUshift (uscale q d1g) (uscale q d1i) d2g d2i dg di hg hi) htShift i g c dg di (MkEcho m aE bE t) hlen (THEcho h) = THEcho (htShift i g c dg di t hlen h) htShift i g c dg di (Weaken t) hlen (THWeaken h) = THWeaken (htShift i g c dg di t hlen h) + +------------------------------------------------------------ +-- 4c. Substitution core — accounting algebra +------------------------------------------------------------ + +||| Iterated weakening shift: `shiftn k = (shift 0)` iterated `k` times. +||| The cumulative shift the substituted term carries after descending `k` +||| binders (mirrors Coq `shiftn`). +public export +shiftn : Nat -> Tm -> Tm +shiftn Z u = u +shiftn (S k) u = shift 0 (shiftn k u) + +||| `ht_shift0`: weaken a derivation by one fresh `Zero`-usage binder — the +||| `htShift` instance at `i = TEmpty`. +public export +htShift0 : (g : Tctx) -> (c : Ty) -> (dg : Uvec) -> (t : Tm) + -> Has g dg t a -> Has (TSnoc g c) (USnoc dg Zero) (shift 0 t) a +htShift0 g c dg t h = htShift TEmpty g c dg UEmpty t Refl h + +||| Middle-four exchange for `qAdd` (pure semiring rearrangement): groups the +||| inner pair so the additive accounting can be re-associated. +qAddRearrange : (w, x, y, z : Q) + -> qAdd (qAdd w x) (qAdd y z) = qAdd (qAdd w y) (qAdd x z) +qAddRearrange w x y z = + trans (qAddAssoc w x (qAdd y z)) + (trans (cong (qAdd w) midSwap) (sym (qAddAssoc w y (qAdd x z)))) + where + midSwap : qAdd x (qAdd y z) = qAdd y (qAdd x z) + midSwap = trans (sym (qAddAssoc x y z)) + (trans (cong (\u => qAdd u z) (qAddComm x y)) (qAddAssoc y x z)) + +||| The Q-semiring identity behind substituting through an additive split +||| (mirrors Coq `q_reassoc`; derived from the named semiring laws, no +||| 3^6-case enumeration). +qReassoc : (dg1, dg2, du, q', q1, q2 : Q) + -> qAdd (qAdd dg1 (qMul q' dg2)) (qMul (qAdd q1 (qMul q' q2)) du) + = qAdd (qAdd dg1 (qMul q1 du)) (qMul q' (qAdd dg2 (qMul q2 du))) +qReassoc dg1 dg2 du q' q1 q2 = + trans (cong (qAdd (qAdd dg1 (qMul q' dg2))) + (trans (qMulDistribR q1 (qMul q' q2) du) + (cong (qAdd (qMul q1 du)) (qMulAssoc q' q2 du)))) + (trans (qAddRearrange dg1 (qMul q' dg2) (qMul q1 du) (qMul q' (qMul q2 du))) + (cong (qAdd (qAdd dg1 (qMul q1 du))) + (sym (qMulDistribL q' dg2 (qMul q2 du))))) + +||| `uadd D (Zero · E) = D` (lengths matched): the zero-scaled right summand +||| is the additive identity. (Mirrors Coq `uadd_uscaleZero_r`.) +public export +uaddUscaleZeroR : (d, e : Uvec) -> ulen d = ulen e -> uadd d (uscale Zero e) = Just d +uaddUscaleZeroR UEmpty UEmpty _ = Refl +uaddUscaleZeroR UEmpty (USnoc _ _) prf = void (zNotS' prf) +uaddUscaleZeroR (USnoc _ _) UEmpty prf = void (sNotZ' prf) +uaddUscaleZeroR (USnoc d qd) (USnoc e qe) prf = + rewrite uaddUscaleZeroR d e (predEq' prf) in + rewrite qMulZeroL qe in + rewrite qAddZeroR qd in Refl + +||| The `Just`-headed tail-combinator `uadd` uses on a USnoc/USnoc pair: +||| `uadd (USnoc a p) (USnoc b s) = combMaybe (qAdd p s) (uadd a b)`. +combMaybe : Q -> Maybe Uvec -> Maybe Uvec +combMaybe p Nothing = Nothing +combMaybe p (Just d) = Just (USnoc d p) + +||| `uadd` on a USnoc pair reduces to `combMaybe` of the tail sum (definitional +||| once the tail sum is scrutinised). +uaddUSnocReduce : (a, b : Uvec) -> (p, s : Q) + -> uadd (USnoc a p) (USnoc b s) = combMaybe (qAdd p s) (uadd a b) +uaddUSnocReduce a b p s with (uadd a b) + _ | Nothing = Refl + _ | Just d = Refl + +||| Invert a successful USnoc/USnoc sum: recover the tail sum and the head. +uaddSnocSplit : (a, b : Uvec) -> (p, s : Q) -> (z : Uvec) + -> uadd (USnoc a p) (USnoc b s) = Just z + -> (c : Uvec ** (uadd a b = Just c, z = USnoc c (qAdd p s))) +uaddSnocSplit a b p s z prf with (uadd a b) + _ | Nothing = void (nothingNotJust' prf) + _ | Just cc = (cc ** (Refl, sym (justInj' prf))) + +||| Lift `qReassoc` to usage vectors: the two reassociations of the additive +||| substitution accounting agree as `Maybe Uvec` (mirrors Coq `vec_reassoc`). +vecReassoc : (du, dg1, dg2 : Uvec) -> (q', q1, q2 : Q) -> (dgr1, dgr2, dg : Uvec) + -> uadd dg1 (uscale q1 du) = Just dgr1 + -> uadd dg2 (uscale q2 du) = Just dgr2 + -> uadd dg1 (uscale q' dg2) = Just dg + -> uadd dgr1 (uscale q' dgr2) = uadd dg (uscale (qAdd q1 (qMul q' q2)) du) +vecReassoc UEmpty UEmpty UEmpty q' q1 q2 dgr1 dgr2 dg h1 h2 h3 = + rewrite sym (justInj' h1) in rewrite sym (justInj' h2) in rewrite sym (justInj' h3) in Refl +vecReassoc UEmpty (USnoc _ _) _ q' q1 q2 dgr1 dgr2 dg h1 h2 h3 = void (nothingNotJust' h1) +vecReassoc UEmpty UEmpty (USnoc _ _) q' q1 q2 dgr1 dgr2 dg h1 h2 h3 = void (nothingNotJust' h2) +vecReassoc (USnoc du0 qd) UEmpty _ q' q1 q2 dgr1 dgr2 dg h1 h2 h3 = void (nothingNotJust' h1) +vecReassoc (USnoc du0 qd) (USnoc _ _) UEmpty q' q1 q2 dgr1 dgr2 dg h1 h2 h3 = void (nothingNotJust' h2) +vecReassoc (USnoc du0 qd) (USnoc dg1' dgq1) (USnoc dg2' dgq2) q' q1 q2 dgr1 dgr2 dg h1 h2 h3 = + let (r1 ** (e1, hr1)) = uaddSnocSplit dg1' (uscale q1 du0) dgq1 (qMul q1 qd) dgr1 h1 + (r2 ** (e2, hr2)) = uaddSnocSplit dg2' (uscale q2 du0) dgq2 (qMul q2 qd) dgr2 h2 + (dm ** (e3, hdg)) = uaddSnocSplit dg1' (uscale q' dg2') dgq1 (qMul q' dgq2) dg h3 + ih = vecReassoc du0 dg1' dg2' q' q1 q2 r1 r2 dm e1 e2 e3 + in rewrite hr1 in rewrite hr2 in rewrite hdg in + trans (uaddUSnocReduce r1 (uscale q' r2) (qAdd dgq1 (qMul q1 qd)) + (qMul q' (qAdd dgq2 (qMul q2 qd)))) + (trans (cong2 combMaybe (sym (qReassoc dgq1 dgq2 qd q' q1 q2)) ih) + (sym (uaddUSnocReduce dm (uscale (qAdd q1 (qMul q' q2)) du0) + (qAdd dgq1 (qMul q' dgq2)) (qMul (qAdd q1 (qMul q' q2)) qd)))) + +||| The additive-split substitution accounting: combine the two recursive +||| residuals (mirrors Coq `subst_reassoc_add`). +public export +substReassocAdd : (dg1, dgr1, dg2, dgr2, dg, du : Uvec) -> (q', q1, q2 : Q) + -> uadd dg1 (uscale q1 du) = Just dgr1 + -> uadd dg2 (uscale q2 du) = Just dgr2 + -> uadd dg1 (uscale q' dg2) = Just dg + -> (dgr : Uvec ** (uadd dg (uscale (qAdd q1 (qMul q' q2)) du) = Just dgr, + uadd dgr1 (uscale q' dgr2) = Just dgr)) +substReassocAdd dg1 dgr1 dg2 dgr2 dg du q' q1 q2 h1 h2 h3 = + let hlen = trans (uaddLen dg1 (uscale q' dg2) dg h3) + (trans (uaddLenEq dg1 (uscale q1 du) dgr1 h1) + (trans (uscaleLen q1 du) (sym (uscaleLen (qAdd q1 (qMul q' q2)) du)))) + (dgr ** hdgr) = uaddTotal dg (uscale (qAdd q1 (qMul q' q2)) du) hlen + in (dgr ** (hdgr, trans (vecReassoc du dg1 dg2 q' q1 q2 dgr1 dgr2 dg h1 h2 h3) hdgr)) + +||| Multiplicative-split variant (`q' = One`) — mirrors Coq `subst_reassoc_mult`. +public export +substReassocMult : (dg1, dgr1, dg2, dgr2, dg, du : Uvec) -> (q1, q2 : Q) + -> uadd dg1 (uscale q1 du) = Just dgr1 + -> uadd dg2 (uscale q2 du) = Just dgr2 + -> uadd dg1 dg2 = Just dg + -> (dgr : Uvec ** (uadd dg (uscale (qAdd q1 q2) du) = Just dgr, + uadd dgr1 dgr2 = Just dgr)) +substReassocMult dg1 dgr1 dg2 dgr2 dg du q1 q2 h1 h2 h3 = + let (dgr ** (ha, hb)) = substReassocAdd dg1 dgr1 dg2 dgr2 dg du One q1 q2 h1 h2 + (rewrite uscaleOne dg2 in h3) + in (dgr ** (rewrite sym (qMulOneL q2) in ha, rewrite sym (uscaleOne dgr2) in hb)) + +------------------------------------------------------------ +-- 4c (cont). USnoc-headed boundary splitters + var arithmetic +------------------------------------------------------------ + +eqNotGT : (Prelude.EQ = Prelude.GT) -> Void +eqNotGT Refl impossible + +ltNotGT : (Prelude.LT = Prelude.GT) -> Void +ltNotGT Refl impossible + +lteFromEq : (d : Uvec) -> (k, m : Nat) -> ulen d = S k + m -> LTE m (ulen d) +lteFromEq d k m hl = + rewrite hl in lteSuccRight (rewrite plusCommutative k m in lteAddRight m) + +||| Split a usage whose length puts the substituted variable at the `USnoc` +||| boundary: `ulen d = S k + m` factors `d = uappend (USnoc dg q) di` with the +||| top `m` entries in `di`. (Mirrors Coq `usplit3`; the `ulen dg = k` conjunct +||| is unused downstream and dropped.) +public export +usplit3 : (d : Uvec) -> (k, m : Nat) -> ulen d = S k + m + -> (dg : Uvec ** q : Q ** di : Uvec ** (d = uappend (USnoc dg q) di, ulen di = m)) +usplit3 d k m hl with (uappendSplit m d (lteFromEq d k m hl)) + _ | (UEmpty ** di ** (heq, hldi)) = + void (sNotZ' (plusRightCancel (S k) Z m + (trans (sym hl) + (trans (cong ulen heq) (trans (uappendLen UEmpty di) hldi))))) + _ | (USnoc dg q ** di ** (heq, hldi)) = (dg ** q ** di ** (heq, hldi)) + +||| USnoc-headed boundary split of a sum: the heads add (`q = q1 + q2`), the +||| G-parts add, the I-parts add. (Mirrors Coq `uadd_split_boundary2`.) +public export +uaddSplitBoundary2 : (dg1 : Uvec) -> (q1 : Q) -> (di1 : Uvec) + -> (dg2 : Uvec) -> (q2 : Q) -> (di2 : Uvec) + -> (dg : Uvec) -> (q : Q) -> (di : Uvec) + -> ulen di1 = ulen di2 -> ulen di = ulen di1 + -> uadd (uappend (USnoc dg1 q1) di1) (uappend (USnoc dg2 q2) di2) + = Just (uappend (USnoc dg q) di) + -> (uadd dg1 dg2 = Just dg, q = qAdd q1 q2, uadd di1 di2 = Just di) +uaddSplitBoundary2 dg1 q1 di1 dg2 q2 di2 dg q di h12 hd heq = + let (hhead, htail) = uaddSplitBoundary (USnoc dg1 q1) di1 (USnoc dg2 q2) di2 (USnoc dg q) di + h12 hd heq + (dd ** (hadd, heqd)) = uaddSnocSplit dg1 dg2 q1 q2 (USnoc dg q) hhead + (hdg, hq) = usnocInj heqd + in (rewrite hdg in hadd, hq, htail) + +||| Substituting at a deeper index commutes with one extra weakening shift +||| (mirrors Coq `subst_var_succ`); the engine behind `hvSubst`'s `HVThere` step. +public export +substVarSucc : (k : Nat) -> (u : Tm) -> (n : Nat) + -> substAt (S k) (shiftn (S k) u) (Var (S n)) + = shift 0 (substAt k (shiftn k u) (Var n)) +substVarSucc k u n with (compare n k) proof eq + substVarSucc k u n | LT = sym (shiftVarLemma 0 n) + substVarSucc k u n | EQ = Refl + substVarSucc Z u Z | GT = void (eqNotGT eq) + substVarSucc (S j) u Z | GT = void (ltNotGT eq) + substVarSucc k u (S n0) | GT = rewrite minusZeroRight n0 in sym (shiftVarLemma 0 n0) + +------------------------------------------------------------ +-- 4c (cont). Variable substitution +------------------------------------------------------------ + +||| Substituting `u` for the boundary variable in a `HasVar`: either the +||| substituted variable itself (returns `u`, usage scaled by `q`), or a +||| different variable (unchanged, `Zero`-scaled). The general prefix-`I` form +||| (mirrors Coq `hv_subst`); `htSubst`'s `Var` case is this lemma. +public export +hvSubst : (i, g : Tctx) -> (a : Ty) -> (dg : Uvec) -> (q : Q) -> (di : Uvec) + -> (n : Nat) -> (b : Ty) -> (du : Uvec) -> (u : Tm) + -> ulen di = tlen i + -> HasVar (tappend (TSnoc g a) i) (uappend (USnoc dg q) di) n b + -> Has g du u a + -> (dgr : Uvec ** (uadd dg (uscale q du) = Just dgr, + Has (tappend g i) (uappend dgr di) + (substAt (tlen i) (shiftn (tlen i) u) (Var n)) b)) +hvSubst TEmpty g a dg q (USnoc _ _) n b du u hlen hv hu = void (sNotZ' hlen) +hvSubst TEmpty g a dg q UEmpty Z b du u hlen hv hu = + case varInv hv of + VIT hdq hn hv' => void (zNotS' hn) + VIH hdq hn hb => + let (hdg, hq) = usnocInj hdq + in (du ** (rewrite hdg in rewrite hq in rewrite uscaleOne du in + uaddZeroL g du (shapeType g u hu), + rewrite hb in hu)) +hvSubst TEmpty g a dg q UEmpty (S n0) b du u hlen hv hu = + case varInv hv of + VIH hdq hn hb => void (sNotZ' hn) + VIT hdq hn hv' => + let (hdg, hq) = usnocInj hdq + hv'' : HasVar g dg n0 b + hv'' = rewrite hdg in rewrite predEq' hn in hv' + in (dg ** (rewrite hq in + uaddUscaleZeroR dg du (trans (shapeVar g hv'') (sym (shapeType g u hu))), + rewrite minusZeroRight n0 in THVar hv'')) +hvSubst (TSnoc i' c) g a dg q UEmpty n b du u hlen hv hu = void (zNotS' hlen) +hvSubst (TSnoc i' c) g a dg q (USnoc di' qd) Z b du u hlen hv hu = + case varInv hv of + VIT hdq hn hv' => void (zNotS' hn) + VIH hdq hn hb => + let (hdgdi, hqd) = usnocInj hdq + (hdg, hdi) = uappendInj di' (uzero i') (USnoc dg q) (USnoc (uzero g) Zero) + (trans (predEq' hlen) (sym (uzeroLen i'))) + (trans hdgdi (uzeroTappend (TSnoc g a) i')) + (hdgg, hqq) = usnocInj hdg + in (uzero g ** + (rewrite hdgg in rewrite hqq in + uaddUscaleZeroR (uzero g) du (trans (uzeroLen g) (sym (shapeType g u hu))), + rewrite hb in rewrite hqd in rewrite hdi in + rewrite sym (uzeroTappend g i') in THVar HVHere)) +hvSubst (TSnoc i' c) g a dg q (USnoc di' qd) (S n0) b du u hlen hv hu = + case varInv hv of + VIH hdq hn hb => void (sNotZ' hn) + VIT hdq hn hv' => + let (hd0, hqd) = usnocInj hdq + (dgr ** (hadd, hht)) = hvSubst i' g a dg q di' n0 b du u (predEq' hlen) + (rewrite hd0 in rewrite predEq' hn in hv') hu + in (dgr ** + (hadd, + rewrite hqd in + rewrite substVarSucc (tlen i') u n0 in + htShift0 (tappend g i') c (uappend dgr di') + (substAt (tlen i') (shiftn (tlen i') u) (Var n0)) hht))