OAI/Computability/FiniteCompiler/Rewriting.lean

GitHub source file

89 declarations, 0 contain sorry, 0 declared as axioms

Newman normalization, block coding, canonical representatives, and static tests.

  1. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Irreducible line 19
  2. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.exists_irreducible line 21
  3. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.irreducible_reaches line 33
  4. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.normal_unique line 40

    Source documentation

    Newman's induction, with the terminal-descendant existence made explicit.

    theorem normal_unique (wf : WellFounded (flip R))
    (localJoin : ∀ a b c, R a b → R a c → Join (ReflTransGen R) b c)
    (a : α) : ∀ b c, ReflTransGen R a b → ReflTransGen R a c →
      Irreducible R b → Irreducible R c → b = c := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Irreducible

  5. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.newman line 56
  6. inductive OAI.FiniteAlgebraicEnvelopes.Bootstrap.Step line 69

    Source documentation

    One directed rule in an arbitrary two-sided context.

    inductive Step (rules : List (List S × List S)) : List S → List S → Prop
  | apply {u v} (h : (u,v) ∈ rules) (x y) : Step rules (x++u++y) (x++v++y)
  7. abbrev OAI.FiniteAlgebraicEnvelopes.Bootstrap.Steps line 72
  8. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.step_context line 74
  9. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.steps_context line 79
  10. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.lex_append_suffix line 83
  11. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.shortlex_context line 91
  12. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.step_shortlex line 101
  13. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.steps_length line 107
  14. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.steps_wellFounded line 116
  15. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.step_stable line 122

    Source documentation

    A bounded table sees precisely those rules whose left sides fit the bound.

    theorem step_stable {rs rt : List (List S × List S)} {k : ℕ}
    (stable : ∀ p, p.1.length ≤ k → (p ∈ rs ↔ p ∈ rt)) {w v : List S}
    (hw : w.length ≤ k) : Step rs w v ↔ Step rt w v := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Step

  16. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.rootNext line 138

    Source documentation

    The fixed choice of rule at the leftmost position, then table order.

    def rootNext (w : List S) : List (List S × List S) → Option (List S)
  | [] => none
  | (u,v)::rs => if w.take u.length = u then some (v ++ w.drop u.length) else rootNext w rs
  17. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.next line 142
  18. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.rootNext_sound line 146
  19. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.rootNext_none line 163
  20. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.next_sound line 179
  21. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.next_none_root line 204
  22. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.next_none_tail line 210
  23. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.next_none line 214
  24. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.iteration line 225

    Source documentation

    Fully specified finite-table reduction; divergence is retained for arbitrary (possibly nonterminating) tables.

    def iteration (s : List (List S × List S) × List S) :
    List S ⊕ (List (List S × List S) × List S) :=
…
  25. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.evaluate line 231
  26. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.evaluate_sound line 234
  27. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.evaluate_total line 255
  28. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.evaluate_unique_on line 271

    Source documentation

    Bounded local confluence is enough: every intervening reduction has nonincreasing length, so no confluence outside the source budget is used.

    theorem evaluate_unique_on {r : S → S → Prop} {rules : List (List S × List S)}
    (wf : WellFounded r) (dec : ∀ p ∈ rules, List.Shortlex r p.2 p.1) (n : ℕ)
    (localJoin : ∀ a b c, a.length ≤ n → Step rules a b → Step rules a c →
      Join (Steps rules) b c) {a b c : List S} (ha : a.length ≤ n)
    (hab : Steps rules a b) (hac : Steps rules a c)
    (hb : Irreducible (Step rules) b) (hc : Irreducible (Step rules) c) : b = c := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Step, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Steps, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Irreducible

  29. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.evaluate_context_on line 290
  30. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.primrec_rootNext line 307
  31. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.primrec_next line 327
  32. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.primrec_iteration line 347
  33. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.partrec_evaluate line 353
  34. structure OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode line 361
  35. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.block line 372
  36. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.encode line 374
  37. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.block_length line 376
  38. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.encode_nil line 379
  39. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.encode_cons line 380
  40. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.encode_append line 381
  41. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.encode_length line 383
  42. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.block_injective line 388
  43. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.prefix_decode line 392
  44. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.encode_injective line 407
  45. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.split_past_avoiding line 414
  46. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.marker_alignment line 429

    Source documentation

    Every marker inside an encoded word starts a complete generator block.

     theorem marker_alignment {v : List A} {x y : List S}
    (h : C.encode v = x ++ C.marker :: y) :
    ∃ u a w, v=u++a::w ∧ x=C.encode u ∧ y=C.tail a ++ C.encode w := by
…
  47. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.occurrence_decode line 447

    Source documentation

    A nonempty code occurrence in a code sequence has both boundaries aligned.

     theorem occurrence_decode {v u : List A} (hu : u≠[]) {x y : List S}
    (h : C.encode v = x++C.encode u++y) :
    ∃ p q, v=p++u++q ∧ x=C.encode p ∧ y=C.encode q := by
…
  48. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.overlap_decode line 465

    Source documentation

    Overlapping code left sides have a union which is itself a full code; the common part is an entire (nonempty) code suffix/prefix.

     theorem overlap_decode {u v : List A} {p middle q : List S}
    (hm : middle≠[]) (h₁ : C.encode u = p++middle)
    (h₂ : C.encode v = middle++q) :
    ∃ a b c, u=a++b ∧ v=b++c ∧ p=C.encode a ∧
      middle=C.encode b ∧ q=C.encode c := by
…
  49. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.encode_avoids line 484
  50. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.lex_append_two line 491
  51. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.encode_lex line 500

    Source documentation

    The chosen generator order is transported from the equal-width blocks.

    theorem encode_lex {r : A → A → Prop} {s : S → S → Prop}
    (hblock : ∀ a b, r a b → List.Lex s (C.block a) (C.block b))
    {u v : List A} (h : List.Lex r u v) : List.Lex s (C.encode u) (C.encode v) := by
…
  52. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.BlockCode.encode_shortlex line 508
  53. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.binaryTail line 520

    Source documentation

    An explicit computable constant-width binary tail family. Choosing the generator order by its lexicographic order implements the source convention. The generous width still obeys D₀>M=2, with no machine-size restriction.

    def binaryTail {S : Type*} (a c : S) (m : ℕ) (i : Fin m) : List S :=
…
  54. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.binaryTail_length line 523
  55. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.binaryTail_injective line 529
  56. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.binaryCode line 538
  57. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.candidates line 552

    Source documentation

    Exactly the bounded tested-class candidate set in the self-reference construction.

    def candidates (w : List A) : Set (List A) := {v | v.length ≤ w.length ∧ q v=q w}
  58. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least line 554
  59. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least_mem line 557
  60. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least_length line 560
  61. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least_class line 563
  62. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least_min line 565
  63. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least_lt_or_eq line 569
  64. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least_global_min line 576
  65. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least_congr line 586

    Source documentation

    Changing the finite search bound to that of another same-class candidate cannot change the result, including when the result is empty.

    theorem least_congr [Std.Trichotomous r] {u v : List A} (hq : q u=q v) :
    least wf q u=least wf q v := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least

  66. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least_idem line 592
  67. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least_nil line 596
  68. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.eq_least_iff line 601

    Source documentation

    Literal characterization which requires no class tests longer than w.

    theorem eq_least_iff [Std.Trichotomous r] {w v : List A} : v=least wf q w ↔
    v.length≤w.length ∧ q v=q w ∧
      ∀ t, t.length≤w.length → q t=q w → ¬ List.Shortlex r t v := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Canonical.least

  69. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.step_mono line 616
  70. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.steps_mono line 621
  71. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Absorbs line 629

    Source documentation

    The absorbing equations, stated as finite-table membership, not as an additional computation oracle.

    def Absorbs (rs : List (List S × List S)) (z : S) : Prop :=
…
  72. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.absorbs_context line 632
  73. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.absorbs_mem line 650
  74. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.step_preserves_letter line 661
  75. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.letters line 676
  76. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.words line 677
  77. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.mem_words line 681
  78. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.output line 690
  79. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table line 693
  80. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.mem_table line 697
  81. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.output_congr line 704
  82. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.output_nil line 709
  83. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.whole_steps line 712
  84. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.Contextual line 722

    Source documentation

    Precisely the bounded contextual tests used at source bootstrap:273–297.

    def Contextual (n : ℕ) : Prop :=
…
  85. def OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.ZeroIdeal line 726
  86. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.branch_normalizes line 733

    Source documentation

    A single contextual static replacement inside a full code reduces to the same literal whole-code output. Both endpoint bounds are proved separately.

    theorem branch_normalizes {n : ℕ} {rs : List (List S × List S)}
    (hzero : q []≠none) (hz : Absorbs rs z)
    (ht : ∀ p∈table C wf q z n, p∈rs)
    (hc : Contextual q n) (hi : ZeroIdeal q n)
    {v : List A} {a b : List A} (hlen : (a++v++b).length≤n) :
    Steps rs (C.encode a++output C wf q z v++C.encode b) (output C wf q z (a++v++b)) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Absorbs, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.Contextual, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.ZeroIdeal, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Steps, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.output

  87. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.occurrence_normalizes line 757

    Source documentation

    Contained code occurrences are aligned, so the preceding branch analysis applies at exactly the source code boundaries.

    theorem occurrence_normalizes {n : ℕ} {rs : List (List S × List S)}
    (hzero : q []≠none) (hz : Absorbs rs z)
    (ht : ∀ p∈table C wf q z n, p∈rs)
    (hc : Contextual q n) (hi : ZeroIdeal q n)
    {w v : List A} {x y : List S} (hw : w.length≤n) (hv : v≠[])
    (he : C.encode w=x++C.encode v++y) :
    Steps rs (x++output C wf q z v++y) (output C wf q z w) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Absorbs, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.Contextual, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.ZeroIdeal, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Steps, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.output

  88. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.critical_containment line 768

    Source documentation

    Static containment criticals join at the canonical output of the union.

    theorem critical_containment {n k l : ℕ} {rs : List (List S × List S)}
    (hzero : q []≠none) (hz : Absorbs rs z)
    (ht : ∀ p∈table C wf q z n, p∈rs)
    (hc : Contextual q n) (hi : ZeroIdeal q n)
    {u u' v v' x y : List S}
    (hu : (u,u')∈table C wf q z k) (hv : (v,v')∈table C wf q z l)
    (he : u=x++v++y) (hlen : u.length≤(C.width+1)*n) :
    Join (Steps rs) u' (x++v'++y) := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Absorbs, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.Contextual, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.ZeroIdeal, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Steps

  89. theorem OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.critical_overlap line 786

    Source documentation

    Static boundary criticals have a full, aligned code union, and both contextual branches reach its same literal output.

    theorem critical_overlap {n k l : ℕ} {rs : List (List S × List S)}
    (hzero : q []≠none) (hz : Absorbs rs z)
    (ht : ∀ p∈table C wf q z n, p∈rs)
    (hc : Contextual q n) (hi : ZeroIdeal q n)
    {u u' v v' x middle y : List S}
    (hu : (u,u')∈table C wf q z k) (hv : (v,v')∈table C wf q z l)
    (hm : middle≠[]) (he : u=x++middle) (hf : v=middle++y)
    (hlen : (x++middle++y).length≤(C.width+1)*n) :
    Join (Steps rs) (u'++y) (x++v') := by
…

    Mentions: OAI.FiniteAlgebraicEnvelopes.Bootstrap.Absorbs, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.table, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.Contextual, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Static.ZeroIdeal, OAI.FiniteAlgebraicEnvelopes.Bootstrap.Steps