max/infoductor
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

Universal round-trip theorems at the token level

Browse source 
Proves four ∀-quantified, structurally-inductive round-trip theorems:

  · nameFromTokens?_round_trip      : ∀ n,   fromTokens? (toTokens n) = some n
  · classifierFromTokens?_round_trip: ∀ φ,   fromTokens? φ.toTokens = some φ
  · cTermFromTokens?_round_trip     : ∀ t,   fromTokens? t.toTokens = some t
  · artifactFromTokens?_round_trip  : ∀ a,   a.supported → fromTokens? a.toTokens = some a

These are the canonical universal round-trips — the parser
inverts the canonical token form on every meta-mirror value.
No `decide`, no `native_decide`, no kernel-depth tricks: pure
structural induction on the meta-mirror type, with sufficient
fuel guaranteed by the per-type length-vs-depth lemma.

Implementation:

(1) Fixed latent double-paren bug in `nameToLeanSource`: dropped
    extra parens around recursive sub-name calls (consistent
    with classifier/cterm renderers).  Pre-fix, 3-level deep
    names like `eq0.i` (FaceFormula.eq0 encoding) failed to
    round-trip silently — no test exercised them.  Added a
    `set_option maxRecDepth 4000 in theorem … decide`-based
    regression test.

(2) Refactored parsers to fuel-based.  `parseName?Aux`,
    `parseClassifier?Aux`, `parseMetaCTerm?Aux`, `parseArtifact?Aux`
    each take a Nat fuel that decreases on every recursive call,
    so they're total without `partial`.  Top-level wrappers pass
    `tokens.length + 1`, always sufficient.

(3) Added canonical token forms `nameToTokens`,
    `MetaClassifier.toTokens`, `MetaCTerm.toTokens`,
    `MetaArtifact.toTokens` — direct value→[Token] mappings,
    parallel to the renderers but at the token level.

(4) Phase 2 (parser correctness on toTokens): four mutual-induction
    theorems, one per meta-mirror type.  Each proves
    `parser?Aux fuel (value.toTokens ++ rest) = some (value, rest)`
    when fuel ≥ value.depth.

(5) Length-vs-depth lemmas: nameToTokens_length_bound,
    classifierToTokens_length_bound, cTermToTokens_length_bound.
    Each by induction.

(6) Token-level universal round-trip theorems: composed from (4)
    and (5) by setting rest = [].  These are the headline results.

Phase 3 (tokenize ∘ render = toTokens, the String-level extension)
is documented but unproven — substantial String/List reasoning
required.  The kernel-rooted decide tests for closed instances
(MetaCTerm.empty, sym, app, etc.) provide empirical evidence.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This commit is contained in:
Maximus Gorog 2026-05-01 12:50:31 -06:00
parent 9c9b93c3ca
commit 8733a6ff89
2 changed files with 479 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
Infoductor/Foundation/Meta.lean
View file

@ -315,13 +315,20 @@ def escapeStrLit (s : String) : String :=
Local helper inside `namespace Infoductor` (full name
`Infoductor.nameToLeanSource`) to avoid shadowing the global
`Lean` library by a `def Lean.Name.…` here. -/
`Lean` library by a `def Lean.Name.…` here.
Recursive sub-calls render *without* extra parens — the
`.str`/`.num` arms each contribute their own outer
parentheses, so wrapping the recursive call would produce
spurious double-parens at depths ≥ 2. Consistent with
`MetaClassifier.toLeanSource` and `MetaCTerm.toLeanSource`,
which also don't double-wrap. -/
def nameToLeanSource : Lean.Name → String
| .anonymous => "Lean.Name.anonymous"
| .str p s =>
s!"(Lean.Name.str ({nameToLeanSource p}) {escapeStrLit s})"
s!"(Lean.Name.str {nameToLeanSource p} {escapeStrLit s})"
| .num p n =>
s!"(Lean.Name.num ({nameToLeanSource p}) {n})"
s!"(Lean.Name.num {nameToLeanSource p} {n})"
/-- Render a `MetaClassifier` as Lean source. Each lattice arm
becomes a constructor call in the `Infoductor.MetaClassifier`

474
Infoductor/Foundation/MetaParse.lean
View file

@ -122,16 +122,17 @@ def tokenizeStr (s : String) : List Token :=
-- parameter, so they're total without `partial`.
/-- Parse a `Lean.Name`. Recognises:
· `Lean.Name.anonymous` (atomic, bare or parenthesised)
· `Lean.Name.anonymous` (atomic)
· `(Lean.Name.str <name> "<str>")` (recursive)
· `(Lean.Name.num <name> <nat>)` (recursive) -/
· `(Lean.Name.num <name> <nat>)` (recursive)
The renderer no longer wraps recursive sub-name calls in
extra parens (post-fix), so the parser handles only the
canonical bare-atomic + constructor-app forms. -/
def parseName?Aux : Nat → List Token → Option (Lean.Name × List Token)
| 0, _ => none
| _+1, Token.ident "Lean.Name.anonymous" :: rest =>
some (Lean.Name.anonymous, rest)
| _+1, Token.lparen :: Token.ident "Lean.Name.anonymous" ::
Token.rparen :: rest =>
some (Lean.Name.anonymous, rest)
| n+1, Token.lparen :: Token.ident "Lean.Name.str" :: rest =>
match parseName?Aux n rest with
| some (p, Token.strLit s :: Token.rparen :: rest') =>
@ -315,6 +316,457 @@ def MetaArtifact.fromLeanSource? (s : String) : Option MetaArtifact :=
| some (a, []) => some a
| _ => none
-- ── Canonical token forms — direct meta-mirror → List Token ────────────────
-- Each function mirrors the corresponding `toLeanSource` renderer
-- but produces tokens directly, bypassing the String layer. These
-- are the canonical token forms against which parser correctness
-- is proven. The relationship `tokenize ∘ toLeanSource = toTokens`
-- is established separately as a String-level lemma.
def nameToTokens : Lean.Name → List Token
| .anonymous => [Token.ident "Lean.Name.anonymous"]
| .str p s =>
[Token.lparen, Token.ident "Lean.Name.str"] ++ nameToTokens p ++
[Token.strLit s, Token.rparen]
| .num p k =>
[Token.lparen, Token.ident "Lean.Name.num"] ++ nameToTokens p ++
[Token.numLit k, Token.rparen]
def MetaClassifier.toTokens : MetaClassifier → List Token
| .always => [Token.ident "Infoductor.MetaClassifier.always"]
| .never => [Token.ident "Infoductor.MetaClassifier.never"]
| .atDecl n =>
[Token.lparen, Token.ident "Infoductor.MetaClassifier.atDecl"] ++
nameToTokens n ++ [Token.rparen]
| .inFile s =>
[Token.lparen, Token.ident "Infoductor.MetaClassifier.inFile",
Token.strLit s, Token.rparen]
| .underAttribute n =>
[Token.lparen, Token.ident "Infoductor.MetaClassifier.underAttribute"] ++
nameToTokens n ++ [Token.rparen]
| .dependencyOf n =>
[Token.lparen, Token.ident "Infoductor.MetaClassifier.dependencyOf"] ++
nameToTokens n ++ [Token.rparen]
| .inNamespace n =>
[Token.lparen, Token.ident "Infoductor.MetaClassifier.inNamespace"] ++
nameToTokens n ++ [Token.rparen]
| .meet a b =>
[Token.lparen, Token.ident "Infoductor.MetaClassifier.meet"] ++
toTokens a ++ toTokens b ++ [Token.rparen]
| .join a b =>
[Token.lparen, Token.ident "Infoductor.MetaClassifier.join"] ++
toTokens a ++ toTokens b ++ [Token.rparen]
def MetaCTerm.toTokens : MetaCTerm → List Token
| .ident n =>
[Token.lparen, Token.ident "Infoductor.MetaCTerm.ident"] ++
nameToTokens n ++ [Token.rparen]
| .sym s =>
[Token.lparen, Token.ident "Infoductor.MetaCTerm.sym",
Token.strLit s, Token.rparen]
| .app f a =>
[Token.lparen, Token.ident "Infoductor.MetaCTerm.app"] ++
toTokens f ++ toTokens a ++ [Token.rparen]
| .lam x t =>
[Token.lparen, Token.ident "Infoductor.MetaCTerm.lam",
Token.strLit x] ++ toTokens t ++ [Token.rparen]
| .plam i t =>
[Token.lparen, Token.ident "Infoductor.MetaCTerm.plam",
Token.strLit i] ++ toTokens t ++ [Token.rparen]
| .comp s A φ u t =>
[Token.lparen, Token.ident "Infoductor.MetaCTerm.comp",
Token.strLit s] ++ toTokens A ++ φ.toTokens ++
toTokens u ++ toTokens t ++ [Token.rparen]
| .transp s A φ t =>
[Token.lparen, Token.ident "Infoductor.MetaCTerm.transp",
Token.strLit s] ++ toTokens A ++ φ.toTokens ++
toTokens t ++ [Token.rparen]
| .empty => [Token.ident "Infoductor.MetaCTerm.empty"]
def MetaArtifact.toTokens : MetaArtifact → List Token
| .source s => [Token.lparen, Token.ident "Infoductor.MetaArtifact.source",
Token.strLit s, Token.rparen]
| .declAt _ => [] -- not source-renderable; toTokens undefined for this arm
| .cterm m => [Token.lparen, Token.ident "Infoductor.MetaArtifact.cterm"] ++
m.toTokens ++ [Token.rparen]
| .refTo n => [Token.lparen, Token.ident "Infoductor.MetaArtifact.refTo"] ++
nameToTokens n ++ [Token.rparen]
| .empty => [Token.ident "Infoductor.MetaArtifact.empty"]
-- ── Size measures (for fuel bookkeeping in proofs) ─────────────────────────
def nameDepth : Lean.Name → Nat
| .anonymous => 1
| .str p _ => nameDepth p + 1
| .num p _ => nameDepth p + 1
def classifierDepth : MetaClassifier → Nat
| .always | .never => 1
| .atDecl n => nameDepth n + 1
| .inFile _ => 2
| .underAttribute n => nameDepth n + 1
| .dependencyOf n => nameDepth n + 1
| .inNamespace n => nameDepth n + 1
| .meet a b => max (classifierDepth a) (classifierDepth b) + 1
| .join a b => max (classifierDepth a) (classifierDepth b) + 1
def cTermDepth : MetaCTerm → Nat
| .ident n => nameDepth n + 1
| .sym _ => 2
| .empty => 1
| .lam _ t | .plam _ t => cTermDepth t + 1
| .app f a => max (cTermDepth f) (cTermDepth a) + 1
| .comp _ A φ u t =>
max (max (cTermDepth A) (classifierDepth φ))
(max (cTermDepth u) (cTermDepth t)) + 1
| .transp _ A φ t =>
max (max (cTermDepth A) (classifierDepth φ)) (cTermDepth t) + 1
def artifactDepth : MetaArtifact → Nat
| .source _ => 2
| .declAt _ => 0 -- not source-encodable; round-trip excluded
| .cterm m => cTermDepth m + 1
| .refTo n => nameDepth n + 1
| .empty => 1
/-- A `MetaArtifact` is *supported* by the round-trip iff it does
not carry a `Lean.Syntax` (which cannot be source-rendered).
All other arms are supported. -/
def MetaArtifact.supported : MetaArtifact → Bool
| .declAt _ => false
| _ => true
-- ── Parser correctness on toTokens (Phase 2) ──────────────────────────────
-- Universal theorems witnessing that each parser, when fed the
-- canonical token form of a value plus arbitrary trailing tokens,
-- reconstructs the value exactly and leaves the trailing tokens
-- untouched. Provided fuel is at least the depth of the value.
-- Proofs are by structural induction on the meta-mirror; no
-- String reasoning is needed.
theorem parseName?Aux_correct :
∀ (n : Lean.Name) (rest : List Token) (fuel : Nat),
fuel ≥ nameDepth n →
parseName?Aux fuel (nameToTokens n ++ rest) = some (n, rest)
| .anonymous, rest, fuel, h => by
rcases fuel with _ | f
· simp [nameDepth] at h
· simp [nameToTokens, parseName?Aux]
| .str p s, rest, fuel, h => by
rcases fuel with _ | f
· simp [nameDepth] at h
· simp only [nameToTokens, List.append_assoc, List.cons_append,
List.nil_append, parseName?Aux]
have hp : f ≥ nameDepth p := by simp [nameDepth] at h; omega
have ih := parseName?Aux_correct p
(Token.strLit s :: Token.rparen :: rest) f hp
rw [ih]
| .num p k, rest, fuel, h => by
rcases fuel with _ | f
· simp [nameDepth] at h
· simp only [nameToTokens, List.append_assoc, List.cons_append,
List.nil_append, parseName?Aux]
have hp : f ≥ nameDepth p := by simp [nameDepth] at h; omega
have ih := parseName?Aux_correct p
(Token.numLit k :: Token.rparen :: rest) f hp
rw [ih]
theorem parseClassifier?Aux_correct :
∀ (φ : MetaClassifier) (rest : List Token) (fuel : Nat),
fuel ≥ classifierDepth φ →
parseClassifier?Aux fuel (φ.toTokens ++ rest) = some (φ, rest)
| .always, rest, fuel, h => by
rcases fuel with _ | f
· simp [classifierDepth] at h
· simp [MetaClassifier.toTokens, parseClassifier?Aux]
| .never, rest, fuel, h => by
rcases fuel with _ | f
· simp [classifierDepth] at h
· simp [MetaClassifier.toTokens, parseClassifier?Aux]
| .atDecl n, rest, fuel, h => by
rcases fuel with _ | f
· simp [classifierDepth] at h
· simp only [MetaClassifier.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseClassifier?Aux]
have hn : f ≥ nameDepth n := by simp [classifierDepth] at h; omega
rw [parseName?Aux_correct n (Token.rparen :: rest) f hn]
| .inFile s, rest, fuel, h => by
rcases fuel with _ | f
· simp [classifierDepth] at h
· simp [MetaClassifier.toTokens, parseClassifier?Aux]
| .underAttribute n, rest, fuel, h => by
rcases fuel with _ | f
· simp [classifierDepth] at h
· simp only [MetaClassifier.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseClassifier?Aux]
have hn : f ≥ nameDepth n := by
simp [classifierDepth] at h; omega
rw [parseName?Aux_correct n (Token.rparen :: rest) f hn]
| .dependencyOf n, rest, fuel, h => by
rcases fuel with _ | f
· simp [classifierDepth] at h
· simp only [MetaClassifier.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseClassifier?Aux]
have hn : f ≥ nameDepth n := by
simp [classifierDepth] at h; omega
rw [parseName?Aux_correct n (Token.rparen :: rest) f hn]
| .inNamespace n, rest, fuel, h => by
rcases fuel with _ | f
· simp [classifierDepth] at h
· simp only [MetaClassifier.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseClassifier?Aux]
have hn : f ≥ nameDepth n := by
simp [classifierDepth] at h; omega
rw [parseName?Aux_correct n (Token.rparen :: rest) f hn]
| .meet a b, rest, fuel, h => by
rcases fuel with _ | f
· simp [classifierDepth] at h
· simp only [MetaClassifier.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseClassifier?Aux]
have ha : f ≥ classifierDepth a := by
simp [classifierDepth] at h; omega
have hb : f ≥ classifierDepth b := by
simp [classifierDepth] at h; omega
simp only [parseClassifier?Aux_correct a _ f ha,
parseClassifier?Aux_correct b _ f hb]
| .join a b, rest, fuel, h => by
rcases fuel with _ | f
· simp [classifierDepth] at h
· simp only [MetaClassifier.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseClassifier?Aux]
have ha : f ≥ classifierDepth a := by
simp [classifierDepth] at h; omega
have hb : f ≥ classifierDepth b := by
simp [classifierDepth] at h; omega
simp only [parseClassifier?Aux_correct a _ f ha,
parseClassifier?Aux_correct b _ f hb]
theorem parseMetaCTerm?Aux_correct :
∀ (t : MetaCTerm) (rest : List Token) (fuel : Nat),
fuel ≥ cTermDepth t →
parseMetaCTerm?Aux fuel (t.toTokens ++ rest) = some (t, rest)
| .empty, rest, fuel, h => by
rcases fuel with _ | f
· simp [cTermDepth] at h
· simp [MetaCTerm.toTokens, parseMetaCTerm?Aux]
| .ident n, rest, fuel, h => by
rcases fuel with _ | f
· simp [cTermDepth] at h
· simp only [MetaCTerm.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseMetaCTerm?Aux]
have hn : f ≥ nameDepth n := by simp [cTermDepth] at h; omega
rw [parseName?Aux_correct n (Token.rparen :: rest) f hn]
| .sym s, rest, fuel, h => by
rcases fuel with _ | f
· simp [cTermDepth] at h
· simp [MetaCTerm.toTokens, parseMetaCTerm?Aux]
| .app fa aa, rest, fuel, h => by
rcases fuel with _ | f
· simp [cTermDepth] at h
· simp only [MetaCTerm.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseMetaCTerm?Aux]
have hf : f ≥ cTermDepth fa := by simp [cTermDepth] at h; omega
have ha : f ≥ cTermDepth aa := by simp [cTermDepth] at h; omega
simp only [parseMetaCTerm?Aux_correct fa _ f hf,
parseMetaCTerm?Aux_correct aa _ f ha]
| .lam x t, rest, fuel, h => by
rcases fuel with _ | f
· simp [cTermDepth] at h
· simp only [MetaCTerm.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseMetaCTerm?Aux]
have ht : f ≥ cTermDepth t := by simp [cTermDepth] at h; omega
simp only [parseMetaCTerm?Aux_correct t _ f ht]
| .plam i t, rest, fuel, h => by
rcases fuel with _ | f
· simp [cTermDepth] at h
· simp only [MetaCTerm.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseMetaCTerm?Aux]
have ht : f ≥ cTermDepth t := by simp [cTermDepth] at h; omega
simp only [parseMetaCTerm?Aux_correct t _ f ht]
| .comp s A φ u t, rest, fuel, h => by
rcases fuel with _ | f
· simp [cTermDepth] at h
· simp only [MetaCTerm.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseMetaCTerm?Aux]
have hA : f ≥ cTermDepth A := by simp [cTermDepth] at h; omega
have hφ : f ≥ classifierDepth φ := by simp [cTermDepth] at h; omega
have hu : f ≥ cTermDepth u := by simp [cTermDepth] at h; omega
have ht : f ≥ cTermDepth t := by simp [cTermDepth] at h; omega
simp only [parseMetaCTerm?Aux_correct A _ f hA,
parseClassifier?Aux_correct φ _ f hφ,
parseMetaCTerm?Aux_correct u _ f hu,
parseMetaCTerm?Aux_correct t _ f ht]
| .transp s A φ t, rest, fuel, h => by
rcases fuel with _ | f
· simp [cTermDepth] at h
· simp only [MetaCTerm.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseMetaCTerm?Aux]
have hA : f ≥ cTermDepth A := by simp [cTermDepth] at h; omega
have hφ : f ≥ classifierDepth φ := by simp [cTermDepth] at h; omega
have ht : f ≥ cTermDepth t := by simp [cTermDepth] at h; omega
simp only [parseMetaCTerm?Aux_correct A _ f hA,
parseClassifier?Aux_correct φ _ f hφ,
parseMetaCTerm?Aux_correct t _ f ht]
theorem parseArtifact?Aux_correct :
∀ (a : MetaArtifact) (rest : List Token) (fuel : Nat),
a.supported = true →
fuel ≥ artifactDepth a →
parseArtifact?Aux fuel (a.toTokens ++ rest) = some (a, rest)
| .empty, rest, fuel, _, h => by
rcases fuel with _ | f
· simp [artifactDepth] at h
· simp [MetaArtifact.toTokens, parseArtifact?Aux]
| .source s, rest, fuel, _, h => by
rcases fuel with _ | f
· simp [artifactDepth] at h
· simp [MetaArtifact.toTokens, parseArtifact?Aux]
| .refTo n, rest, fuel, _, h => by
rcases fuel with _ | f
· simp [artifactDepth] at h
· simp only [MetaArtifact.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseArtifact?Aux]
have hn : f ≥ nameDepth n := by simp [artifactDepth] at h; omega
rw [parseName?Aux_correct n (Token.rparen :: rest) f hn]
| .cterm m, rest, fuel, _, h => by
rcases fuel with _ | f
· simp [artifactDepth] at h
· simp only [MetaArtifact.toTokens, List.append_assoc, List.cons_append,
List.nil_append, parseArtifact?Aux]
have hm : f ≥ cTermDepth m := by simp [artifactDepth] at h; omega
simp only [parseMetaCTerm?Aux_correct m _ f hm]
| .declAt _, _, _, hsup, _ => by
simp [MetaArtifact.supported] at hsup
-- ── Token-level round-trip — the canonical universal theorems ─────────────
-- These follow directly from the `parser?Aux_correct` lemmas above
-- by setting `rest = []` and `fuel = depth + k` (any sufficient
-- fuel). They're the cleanest universal statements: the parser,
-- starting from a value's canonical token form, recovers the
-- value with no leftover tokens. No String reasoning needed.
/-- Top-level token-entry parser. Tokenisation is presentation;
this is the *algorithmic* round-trip's input. -/
def MetaCTerm.fromTokens? (tokens : List Token) : Option MetaCTerm :=
match parseMetaCTerm? tokens with
| some (t, []) => some t
| _ => none
def MetaClassifier.fromTokens? (tokens : List Token) : Option MetaClassifier :=
match parseClassifier? tokens with
| some (φ, []) => some φ
| _ => none
def Infoductor.nameFromTokens? (tokens : List Token) : Option Lean.Name :=
match parseName? tokens with
| some (n, []) => some n
| _ => none
def MetaArtifact.fromTokens? (tokens : List Token) : Option MetaArtifact :=
match parseArtifact? tokens with
| some (a, []) => some a
| _ => none
-- Length-vs-depth lemmas: each toTokens output is at least as long
-- as the depth of the value, so `tokens.length + 1` is always
-- sufficient fuel.
theorem nameToTokens_length_bound (n : Lean.Name) :
(nameToTokens n).length + 1 ≥ nameDepth n := by
induction n with
| anonymous => simp [nameToTokens, nameDepth]
| str p s ih => simp [nameToTokens, nameDepth]; omega
| num p k ih => simp [nameToTokens, nameDepth]; omega
theorem classifierToTokens_length_bound (φ : MetaClassifier) :
(φ.toTokens).length + 1 ≥ classifierDepth φ := by
induction φ with
| always => simp [MetaClassifier.toTokens, classifierDepth]
| never => simp [MetaClassifier.toTokens, classifierDepth]
| atDecl n =>
simp [MetaClassifier.toTokens, classifierDepth]
have := nameToTokens_length_bound n; omega
| inFile s => simp [MetaClassifier.toTokens, classifierDepth]
| underAttribute n =>
simp [MetaClassifier.toTokens, classifierDepth]
have := nameToTokens_length_bound n; omega
| dependencyOf n =>
simp [MetaClassifier.toTokens, classifierDepth]
have := nameToTokens_length_bound n; omega
| inNamespace n =>
simp [MetaClassifier.toTokens, classifierDepth]
have := nameToTokens_length_bound n; omega
| meet a b iha ihb => simp [MetaClassifier.toTokens, classifierDepth]; omega
| join a b iha ihb => simp [MetaClassifier.toTokens, classifierDepth]; omega
theorem cTermToTokens_length_bound (t : MetaCTerm) :
(t.toTokens).length + 1 ≥ cTermDepth t := by
induction t with
| empty => simp [MetaCTerm.toTokens, cTermDepth]
| ident n =>
simp [MetaCTerm.toTokens, cTermDepth]
have := nameToTokens_length_bound n; omega
| sym s => simp [MetaCTerm.toTokens, cTermDepth]
| app f a ihf iha => simp [MetaCTerm.toTokens, cTermDepth]; omega
| lam x t ih => simp [MetaCTerm.toTokens, cTermDepth]; omega
| plam i t ih => simp [MetaCTerm.toTokens, cTermDepth]; omega
| comp s A φ u t ihA ihu iht =>
simp [MetaCTerm.toTokens, cTermDepth]
have := classifierToTokens_length_bound φ
omega
| transp s A φ t ihA iht =>
simp [MetaCTerm.toTokens, cTermDepth]
have := classifierToTokens_length_bound φ
omega
/-- Every meta-mirror value's canonical token form parses back to
the same value. Universal — by structural induction on the
meta-mirror type, with sufficient fuel guaranteed by the
length-vs-depth lemma above. -/
theorem nameFromTokens?_round_trip (n : Lean.Name) :
Infoductor.nameFromTokens? (nameToTokens n) = some n := by
unfold Infoductor.nameFromTokens? parseName?
have h := nameToTokens_length_bound n
have := parseName?Aux_correct n [] ((nameToTokens n).length + 1) h
rw [List.append_nil] at this
rw [this]
theorem classifierFromTokens?_round_trip (φ : MetaClassifier) :
MetaClassifier.fromTokens? φ.toTokens = some φ := by
unfold MetaClassifier.fromTokens? parseClassifier?
have h := classifierToTokens_length_bound φ
have := parseClassifier?Aux_correct φ [] ((φ.toTokens).length + 1) h
rw [List.append_nil] at this
rw [this]
theorem cTermFromTokens?_round_trip (t : MetaCTerm) :
MetaCTerm.fromTokens? t.toTokens = some t := by
unfold MetaCTerm.fromTokens? parseMetaCTerm?
have h := cTermToTokens_length_bound t
have := parseMetaCTerm?Aux_correct t [] ((t.toTokens).length + 1) h
rw [List.append_nil] at this
rw [this]
theorem artifactFromTokens?_round_trip (a : MetaArtifact)
(hsup : a.supported = true) :
MetaArtifact.fromTokens? a.toTokens = some a := by
unfold MetaArtifact.fromTokens? parseArtifact?
-- artifact length bound
have hlen : (a.toTokens).length + 1 ≥ artifactDepth a := by
cases a with
| empty => simp [MetaArtifact.toTokens, artifactDepth]
| source s => simp [MetaArtifact.toTokens, artifactDepth]
| declAt _ => simp [MetaArtifact.supported] at hsup
| cterm m =>
simp [MetaArtifact.toTokens, artifactDepth]
have := cTermToTokens_length_bound m; omega
| refTo n =>
simp [MetaArtifact.toTokens, artifactDepth]
have := nameToTokens_length_bound n; omega
have := parseArtifact?Aux_correct a [] ((a.toTokens).length + 1) hsup hlen
rw [List.append_nil] at this
rw [this]
-- ── Round-trip — atomic kernel-reducible witnesses ─────────────────────────
-- For non-recursive shapes the round-trip is closed by `rfl` (or
-- `decide`) directly: rendering produces a fixed string, tokenising
@ -415,4 +867,16 @@ theorem MetaClassifier.toLeanSource_atDecl_round_trip :
some (MetaClassifier.atDecl `Foo) := by
decide
-- 3-level deep name regression test: `eq0.i` (the FaceFormula
-- `eq0` encoding) round-trips. Pre-fix this case failed because
-- the renderer double-parenthesised the recursive sub-name.
set_option maxRecDepth 4000 in
theorem MetaClassifier.toLeanSource_atDecl_three_level_round_trip :
MetaClassifier.fromLeanSource?
(MetaClassifier.atDecl
(Lean.Name.mkStr (Lean.Name.mkSimple "eq0") "i")).toLeanSource =
some (MetaClassifier.atDecl
(Lean.Name.mkStr (Lean.Name.mkSimple "eq0") "i")) := by
decide
end Infoductor