Build a Church-numeral Peano env: PN := ∀ α, (α → α) → α → α PN.zero : PN := fun α s z => z PN.succ : PN → PN := fun n α s z => s (n α s z)
()
| 19 | /// PN.zero : PN := fun α s z => z |
| 20 | /// PN.succ : PN → PN := fun n α s z => s (n α s z) |
| 21 | fn peano_env() -> KEnv<Meta> { |
| 22 | let mut env = KEnv::<Meta>::new(); |
| 23 | // PN := ∀ α, (α → α) → α → α |
| 24 | // = ∀ (α : Type), (α → α) → α → α |
| 25 | // depth 0: α=var(0). (α → α) = pi(var(0), var(1)). α → α at depth 1. |
| 26 | // Full: npi("α", sort1(), pi(pi(var(0), var(1)), pi(var(1), var(2)))) |
| 27 | let pn_ty = sort1(); // PN : Type |
| 28 | let _pn_val = npi( |
| 29 | "α", |
| 30 | sort1(), |
| 31 | pi( |
| 32 | pi(var(0), var(1)), // (α → α) at depth 1: α shifted to var(1) |
| 33 | pi( |
| 34 | var(1), // α at depth 2: α = var(2)... wait |
| 35 | var(2), |
| 36 | ), |
| 37 | ), |
| 38 | ); // α at depth 3 |
| 39 | // Actually: ∀ (α : Type), (α → α) → α → α |
| 40 | // = npi("α", Sort 1, npi("s", pi(var(0), var(1)), npi("z", var(1), var(2)))) |
| 41 | // depth 0 (outside): nothing |
| 42 | // depth 1 (inside α): α = var(0) |
| 43 | // s_ty = α → α = pi(var(0), var(1)) — inside pi: α shifts to var(1) |
| 44 | // depth 2 (inside s): s = var(0), α = var(1) |
| 45 | // z_ty = α = var(1) |
| 46 | // depth 3 (inside z): z = var(0), s = var(1), α = var(2) |
| 47 | // result = α = var(2) |
| 48 | let pn_val2 = |
| 49 | npi("α", sort1(), npi("s", pi(var(0), var(1)), npi("z", var(1), var(2)))); |
| 50 | let (pn_id, pn_c) = |
| 51 | mk_defn("PN", 0, vec![], pn_ty, pn_val2, ReducibilityHints::Abbrev); |
| 52 | env.insert(pn_id, pn_c); |
| 53 | |
| 54 | // PN.zero : PN := fun α s z => z |
| 55 | let (z_id, z_c) = mk_defn( |
| 56 | "PN.zero", |
| 57 | 0, |
| 58 | vec![], |
| 59 | cnst("PN", &[]), |
| 60 | nlam( |
| 61 | "α", |
| 62 | sort1(), |
| 63 | nlam("s", pi(var(0), var(1)), nlam("z", var(1), var(0))), |
| 64 | ), |
| 65 | ReducibilityHints::Abbrev, |
| 66 | ); |
| 67 | env.insert(z_id, z_c); |
| 68 | |
| 69 | // PN.succ : PN → PN := fun n α s z => s (n α s z) |
| 70 | // depth 4: z=var(0), s=var(1), α=var(2), n=var(3) |
| 71 | // n α s z = app(app(app(var(3), var(2)), var(1)), var(0)) |
| 72 | // s (n α s z) = app(var(1), app(app(app(var(3), var(2)), var(1)), var(0))) |
| 73 | let succ_body = app(var(1), apps(var(3), &[var(2), var(1), var(0)])); |
| 74 | let (s_id, s_c) = mk_defn( |
| 75 | "PN.succ", |
| 76 | 0, |
| 77 | vec![], |
| 78 | pi(cnst("PN", &[]), cnst("PN", &[])), |