From 8733a6ff89682dc64fb7f6b2aff65fac9b9c9963 Mon Sep 17 00:00:00 2001 From: Maximus Gorog Date: Fri, 1 May 2026 12:50:31 -0600 Subject: [PATCH] Universal round-trip theorems at the token level MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit 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) --- Infoductor/Foundation/Meta.lean | 13 +- Infoductor/Foundation/MetaParse.lean | 474 ++++++++++++++++++++++++++- 2 files changed, 479 insertions(+), 8 deletions(-) diff --git a/Infoductor/Foundation/Meta.lean b/Infoductor/Foundation/Meta.lean index 22abb51..7db043c 100644 --- a/Infoductor/Foundation/Meta.lean +++ b/Infoductor/Foundation/Meta.lean @@ -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` diff --git a/Infoductor/Foundation/MetaParse.lean b/Infoductor/Foundation/MetaParse.lean index 7d17f27..00f3828 100644 --- a/Infoductor/Foundation/MetaParse.lean +++ b/Infoductor/Foundation/MetaParse.lean @@ -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 "")` (recursive) - · `(Lean.Name.num )` (recursive) -/ + · `(Lean.Name.num )` (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