Lax58.RamComplexityElab
Automatic RAM encoding selection (elaboration infrastructure)
concepts/Lax58/RamComplexityElab.lean · lax-58
No public endorsements yet.
Loading review…
Sign in with ORCIDConcept map
Elaboration infrastructure
This thin frontend expands a mathematical function and two resource bounds into the encoding-explicit RAM predicate. It reuses the closed constructor registry, adding only the fixed list and product presentation combinators. Subtypes erase proofs and finite families keep their intrinsic order. No presentation instances, arbitrary field encoders, or caller-supplied agreement witnesses participate in resolution.
Natural and Boolean outputs have fixed one-word conventions. All other supported outputs use the selected structural arena. uses exactly the same input resolver as .
Lean source view on GitHub
| 1 | import Lax58.CertifiedDerivationElab |
| 2 | import Lax58.RamComplexity |
| 3 | |
| 4 | /-! |
| 5 | --- |
| 6 | title: Automatic RAM encoding selection (elaboration infrastructure) |
| 7 | type: elaboration infrastructure |
| 8 | --- |
| 9 | |
| 10 | This thin frontend expands a mathematical function and two resource bounds |
| 11 | into the encoding-explicit RAM predicate. It reuses the closed constructor |
| 12 | registry, adding only the fixed list and product presentation combinators. |
| 13 | Subtypes erase proofs and finite families keep their intrinsic order. |
| 14 | No presentation instances, arbitrary field encoders, or caller-supplied |
| 15 | agreement witnesses participate in resolution. |
| 16 | |
| 17 | Natural and Boolean outputs have fixed one-word conventions. All other |
| 18 | supported outputs use the selected structural arena. `inputMagnitude x` |
| 19 | uses exactly the same input resolver as `RamComputableWithin`. |
| 20 | -/ |
| 21 | |
| 22 | namespace Lax58.RamComplexityElab |
| 23 | |
| 24 | open Lean Meta Elab Term |
| 25 | open Lax58.StructuralPresentation Lax58.StructuralCombinators |
| 26 | open Lax58.CertifiedDerivation Lax58.CertifiedDerivationElab |
| 27 | open Lax58.RamComplexity |
| 28 | |
| 29 | universe u |
| 30 | |
| 31 | private def subtypeRaw {α : Type u} (raw : α → Raw) (p : α → Prop) |
| 32 | (x : Subtype p) : Raw := raw x.val |
| 33 | |
| 34 | private def familyRaw {n : Nat} {α : Fin n → Type u} |
| 35 | (raw : (i : Fin n) → α i → Raw) (x : (i : Fin n) → α i) : Raw := |
| 36 | Raw.fields (List.ofFn fun i => raw i (x i)) |
| 37 | |
| 38 | /-- Resolve expressions, never pretty-printed syntax or typeclass instances. -/ |
| 39 | private partial def resolveInput (type : Expr) : TermElabM Expr := do |
| 40 | let type ← instantiateMVars type |
| 41 | let type ← instantiateMVars (← whnf type) |
| 42 | if type.hasExprMVar then |
| 43 | -- Binder-local numeral/typeclass constraints may be solved only after |
| 44 | -- the surrounding declaration has finished elaborating its signature. |
| 45 | tryPostpone |
| 46 | throwError "RAM encoding selection needs a fully determined input/output type, got {type}" |
| 47 | if type.isConstOf ``Nat then |
| 48 | return mkConst ``StructuralCombinators.nat |
| 49 | if type.isAppOfArity ``List 1 then |
| 50 | return ← mkAppM ``StructuralCombinators.list #[← resolveInput type.appArg!] |
| 51 | if type.isAppOfArity ``Prod 2 then |
| 52 | let args := type.getAppArgs |
| 53 | let left ← resolveInput args[0]! |
| 54 | let right ← resolveInput args[1]! |
| 55 | return ← mkAppM ``StructuralCombinators.prod #[left, right] |
| 56 | if type.isAppOfArity ``Subtype 2 then |
| 57 | let args := type.getAppArgs |
| 58 | let base ← mkAppM ``Presentation.toRaw #[← resolveInput args[0]!] |
| 59 | let raw ← mkAppM ``subtypeRaw #[base, args[1]!] |
| 60 | return ← mkAppM ``presentationOf #[raw] |
| 61 | if let .forallE name domain body bi := type then |
| 62 | let domain ← whnf domain |
| 63 | if domain.isAppOfArity ``Fin 1 then |
| 64 | return ← withLocalDecl name bi domain fun i => do |
| 65 | let raw ← mkAppM ``Presentation.toRaw #[← resolveInput (body.instantiate1 i)] |
| 66 | let family ← mkAppM ``familyRaw #[← mkLambdaFVars #[i] raw] |
| 67 | mkAppM ``presentationOf #[family] |
| 68 | let witness ← resolveCertifiedField type |
| 69 | let raw ← mkAppM ``CertifiedFieldEncoding.toRaw #[witness] |
| 70 | mkAppM ``presentationOf #[raw] |
| 71 | |
| 72 | private def resolveOutput (type : Expr) : TermElabM Expr := do |
| 73 | let type ← whnf type |
| 74 | if type.isConstOf ``Nat then return mkConst ``natOutput |
| 75 | if type.isConstOf ``Bool then return mkConst ``boolOutput |
| 76 | let raw ← mkAppM ``Presentation.toRaw #[← resolveInput type] |
| 77 | mkAppM ``arenaOutput #[raw] |
| 78 | |
| 79 | elab "RamComputableWithin " f:term:max time:term:max words:term:max : term => do |
| 80 | let f ← elabTerm f none |
| 81 | synthesizeSyntheticMVarsNoPostponing |
| 82 | let type ← whnf (← inferType f) |
| 83 | let .forallE _ domain body _ := type |
| 84 | | throwError "RamComputableWithin expects a function" |
| 85 | if body.hasLooseBVars then |
| 86 | throwError "RamComputableWithin expects a nondependent result type; bundle dependent data into an input datatype" |
| 87 | let input ← resolveInput domain |
| 88 | let output ← resolveOutput body |
| 89 | let boundType ← mkArrow domain (mkConst ``Nat) |
| 90 | let time ← elabTermEnsuringType time (some boundType) |
| 91 | let words ← elabTermEnsuringType words (some boundType) |
| 92 | mkAppM ``RamComputableWithinUsing #[input, output, f, time, words] |
| 93 | |
| 94 | elab "inputMagnitude " x:term:max : term => do |
| 95 | let x ← elabTerm x none |
| 96 | synthesizeSyntheticMVarsNoPostponing |
| 97 | let input ← resolveInput (← inferType x) |
| 98 | mkAppM ``inputMagnitudeUsing #[input, x] |
| 99 | |
| 100 | end Lax58.RamComplexityElab |
| 101 |
Used by
From Mathlib
none
Community review
Discussion
Ask a question or add context. Endorsements and structured flags are kept in the review panel above; your ORCID profile must share a public name.
0 comments