Repository navigation

Utm - #159

Open

crei wants to merge 270 commits into

mainfrom

utm

Open

Utm#159
crei wants to merge 270 commits into
mainfrom
utm

This pull request is big! We're only showing the most recent 250 commits

Commits on Jan 23, 2026
- clean up bitape file
  BoltonBailey
  committed
  7092768
- use relatesInSteps API
  BoltonBailey
  committed
  0711013
- revert ReductionSystem/Basic
  BoltonBailey
  committed
  a6a1c23
- refactor computer
  BoltonBailey
  committed
  7d8557b
- improve variable names
  BoltonBailey
  committed
  b1384f7
- claude refactor out time from composition functionality
  BoltonBailey
  committed
  faca3ff
- add private to lemmas
  BoltonBailey
  committed
  435971c
- rename helper lemmas
  BoltonBailey
  committed
  6426bc5
- Merge branch 'main' into single-tape-turing-machines
  BoltonBailey
  authored
  50b6131
- claude: uniformize the helper lemmas
  BoltonBailey
  committed
  bacefc5
- Merge branch 'single-tape-turing-machines' of github.com:BoltonBailey/cslib into single-tape-turing-machines
  BoltonBailey
  committed
  664f62c
- clean up helpers
  BoltonBailey
  committed
  1576498
- further trim helpers
  BoltonBailey
  committed
  e348d76
- remove vanilla computable
  BoltonBailey
  committed
  c5231d9
- rename fields
  BoltonBailey
  committed
  b191ee9
- public import Cslib.Init
  BoltonBailey
  committed
  c9ac367
- add note
  BoltonBailey
  committed
  9286128
Commits on Jan 25, 2026
- correct cons and provide API
  BoltonBailey
  committed
  2ab4751
- clean up tape apis
  BoltonBailey
  committed
  ccd4034
- add docstrings
  BoltonBailey
  committed
  ba47f4f
- more doc linter
  BoltonBailey
  committed
  a387696
- imrove docs
  BoltonBailey
  committed
  1a77e7c
- revert whitespace
  BoltonBailey
  committed
  3d639c2
- clean up lines
  BoltonBailey
  committed
  d14d5ee
- use variables
  BoltonBailey
  committed
  8b06d4a
- golfs
  BoltonBailey
  committed
  f7b6bbb
Commits on Jan 26, 2026
- more golfs
  BoltonBailey
  committed
  19ebc8c
- add movement lemmas
  BoltonBailey
  committed
  1361553
- golf
  BoltonBailey
  committed
  4335852
- more line golfing
  BoltonBailey
  committed
  4da0154
- clean up docstring
  BoltonBailey
  committed
  f220ae0
- namespaces
  BoltonBailey
  committed
  aad3692
Commits on Jan 30, 2026
- Update Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
  
  BoltonBailey
  and
  chenson2018
  authored
  36615f3
- fix typeclass arg names
  BoltonBailey
  committed
  90e6ac4
- remove unneeded parens
  BoltonBailey
  committed
  f5b92e7
- use notation
  BoltonBailey
  committed
  78733a8
- more bundled instances
  BoltonBailey
  committed
  d7f384c
- Update Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
  
  BoltonBailey
  and
  chenson2018
  authored
  f5d0cfe
- golf
  BoltonBailey
  committed
  b5e035f
- reorder args
  BoltonBailey
  committed
  c3858fe
- move args before :=
  BoltonBailey
  committed
  e6a2746
- Update Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
  
  BoltonBailey
  and
  chenson2018
  authored
  0746a77
- reorder proof
  BoltonBailey
  committed
  e356245
- Update Cslib/Computability/Machines/SingleTapeTuring/Basic.lean
  
  BoltonBailey
  and
  chenson2018
  authored
  9a08b4e
- Merge branch 'single-tape-turing-machines' of github.com:BoltonBailey/cslib into single-tape-turing-machines
  BoltonBailey
  committed
  9a2190e
- Stmt becomes structure
  BoltonBailey
  committed
  3329685
- clean up docs
  BoltonBailey
  committed
  76e7c6e
- add doc
  BoltonBailey
  committed
  f45d40e
- add comment
  BoltonBailey
  committed
  1c251fb
- add documentation on design
  BoltonBailey
  committed
  82ed427
- Merge branch 'main' of github.com:leanprover/cslib into single-tape-turing-machines
  BoltonBailey
  committed
  a03c551
- ipossilbe instances removed
  BoltonBailey
  committed
  5516a25
- lake exe mk_all
  BoltonBailey
  committed
  4944e7a
- lake exe mk_all --module
  BoltonBailey
  committed
  97308fa
- grind annotations
  BoltonBailey
  committed
  7c097a6
- some more grind lemmas
  BoltonBailey
  committed
  600e016
Commits on Jan 31, 2026
- more grind annotations
  BoltonBailey
  committed
  b4704d1
- scoped grind
  BoltonBailey
  committed
  ee79f80
Commits on Feb 2, 2026
- Multi-tape Turing machine.
  crei
  committed
  de5ca7d
- define eval
  crei
  committed
  f07cb72
- relates_eq_some
  crei
  committed
  27dd827
- simplify
  crei
  committed
  4fc2c1c
- Merge remote-tracking branch 'origin/main' into multi-tape-turing-machine
  crei
  committed
  363a31c
- Finish eval proof
  crei
  committed
  9782a33
- move_right_nth
  crei
  committed
  c3226c0
- move_int
  crei
  committed
  9840eb6
- move until
  crei
  committed
  be76f0f
- progress
  crei
  committed
  e0b12b6
- stacktape_ext
  crei
  committed
  65c4a32
Commits on Feb 3, 2026
- move_int_move_int
  crei
  committed
  df08110
- sorry proof
  crei
  committed
  a59a09c
Commits on Feb 20, 2026
- Merge remote-tracking branch 'origin/main' into multi-tape-turing-machine
  crei
  committed
  dacb2eb
- Allow warnings.
  crei
  committed
  0d0d604
- Fix imports.
  crei
  committed
  89fc03e
Commits on Feb 21, 2026
- Addition and multiplication routines
  crei
  authored
  269ed49
- feat: add background and orientation information on how to contribute to CSLib (#358)
  
  fmontesi
  authored and
  crei
  committed
  949a0ef
- feat: generalize `TimeM` to arbitrary cost types providing `AddZero` (#357)
  
  eric-wieser
  authored and
  crei
  committed
  6fc3949
Commits on Feb 24, 2026
- Simplify semantics of succ.
  crei
  authored
  e4c2347
- Always-halting Turing machines.
  crei
  authored
  d693e99
Commits on Mar 2, 2026
- Multi-tape Turing machine.
  crei
  committed
  dce94e8
Commits on Mar 4, 2026
- Merge branch 'multi-tape-tm' into multi-tape-turing-machine
  crei
  committed
  f5da60a
- Fix some files post-merge.
  crei
  committed
  11fcde8
- Merge branch 'main' into multi-tape-turing-machine
  crei
  committed
  bf81e99
- Update files.
  crei
  committed
  3728302
- lint
  crei
  committed
  19e8c12
Commits on Mar 5, 2026
- Add decrement and duplication routine.
  crei
  committed
  3be8999
Commits on Mar 6, 2026
- Structural encoding.
  crei
  committed
  e37b53d
- satisfiability
  crei
  committed
  597b6ec
- feat(StrEnc): prove more eval lemmas for structural machines
  
  crei
  and
  Copilot
  committed
  7d3a5fe
Commits on Mar 7, 2026
- feat(SAT): state main satisfiability theorem
  
  crei
  and
  Copilot
  committed
  c5d62bb
- refactor(StrEnc): split any_list/all_list eval into unconditional simp + result spec
  
  crei
  and
  Copilot
  committed
  d6ec2d2
- feat(SAT): structure sat_eval proof with unconditional simp lemmas
  
  crei
  and
  Copilot
  committed
  3098e3b
- refactor(StrEnc): make *_result take individual tapes for simp chains
  
  crei
  and
  Copilot
  committed
  729b8d8
Commits on Mar 9, 2026
- refactor(StructuralMachines): split routines into separate files
  
  crei
  and
  Copilot
  committed
  40d2395
- feat(Encoding): add TapeView.pushList for prepending to list tapes
  
  crei
  and
  Copilot
  committed
  02225a9
- refactor(Navigation): split outOfArg_eval_struct into valid/empty/none cases
  
  crei
  and
  Copilot
  committed
  8df9713
- refactor(Navigation): combine toArg_eval_struct into single conditional lemma
  
  crei
  and
  Copilot
  committed
  a218555
- style(Navigation): pull Function.update outside match in toArg_eval_struct
  
  crei
  and
  Copilot
  committed
  5cd73eb
- fix(ListOps): rename duplicate pushList_eval_struct to pushList_eval
  
  crei
  and
  Copilot
  committed
  bd48d34
- feat(CaseDispatch): add case_popList_num_eval_struct lemma
  
  crei
  and
  Copilot
  committed
  258afde
- feat(CaseDispatch): implement case_popList_num using right and case_num
  
  crei
  and
  Copilot
  committed
  5a0df8c
- refactor(Routines): remove _tape and _eval lemmas, keep only eval_struct
  
  crei
  and
  Copilot
  committed
  0254beb
- feat(Boolean): implement negateBool using case_popList_num and pushList
  
  crei
  and
  Copilot
  committed
  fe57d70
- refactor(Encoding): change TapeView.data from Option Data to Data
  
  crei
  and
  Copilot
  committed
  2794dd7
Commits on Mar 10, 2026
- More structural code.
  crei
  committed
  6fc3a31
- list ops
  crei
  committed
  715018c
Commits on Mar 11, 2026
- list iteration.
  crei
  committed
  cc7e898
- Typed computations.
  crei
  committed
  9c4e281
- cleanup
  crei
  committed
  4419258
- list iteration
  crei
  committed
  1408fbd
Commits on Mar 13, 2026
- Using the old method again.
  crei
  committed
  ed63c3a
Commits on Mar 15, 2026
- prove semantics of all list from any list.
  crei
  committed
  bb44cc1
- progress
  crei
  committed
  440639e
- Try to introduce types.
  crei
  committed
  2db3bfb
Commits on Mar 16, 2026
- progress on satisfiability.
  crei
  committed
  c56252a
- simplify proofs
  crei
  committed
  17d1ce2
- eval_literal
  crei
  committed
  e6583fc
- core semantics.
  crei
  committed
  1de0452
- state semantics of sat
  crei
  committed
  20928d2
- start of semantics
  crei
  committed
  95fc761
- progress
  crei
  committed
  86960bb
- simplify
  crei
  committed
  e9d8468
Commits on Mar 17, 2026
- progress
  crei
  committed
  307abc5
- lint
  crei
  committed
  8ba1641
- some simp lemmas.
  crei
  committed
  e0b45b4
- working proof
  crei
  committed
  8f42ef8
- simplify proof
  crei
  committed
  dc4116b
Commits on Mar 18, 2026
- case_literal
  crei
  committed
  1c97af3
- more proofs
  crei
  committed
  bc39bf9
- cleanup
  crei
  committed
  6c69428
Commits on Mar 19, 2026
- Try to prove toElem.
  crei
  committed
  ed26fe1
- Merge remote-tracking branch 'origin/main' into encoding
  crei
  committed
  63a295f
Commits on Mar 20, 2026
- prove toElem.
  crei
  committed
  9fcbe1c
- proofs and simplification.
  crei
  committed
  42743de
- Require TapeView to always be valid.
  crei
  committed
  7544172
- fix encoding lemmas
  crei
  committed
  e026424
- fix proof
  crei
  committed
  b389a83
- correct proofs.
  crei
  committed
  39b7578
- encoded pos
  crei
  committed
  8822f65
Commits on Mar 22, 2026
- lemma
  crei
  committed
  fe00d7d
- partial work
  crei
  committed
  c9e4419
- prove right_on_nonempty_list.
  crei
  committed
  85f55cd
- clear and while loops.
  crei
  committed
  305d8dd
- fix sat
  crei
  committed
  39b7ec0
Commits on Mar 23, 2026
- prove some lemmas
  crei
  committed
  00a0ee4
- partial progress
  crei
  committed
  4dadc2f
- complete proofs in Put.lean
  crei
  committed
  06875b4
- progress
  crei
  committed
  4451250
- outOfList inner
  crei
  committed
  196e240
- split files.
  crei
  committed
  85b360e
- Remove encoding
  crei
  committed
  47ec267
- ite_enc
  crei
  committed
  f06593c
Commits on Mar 24, 2026
- some work
  crei
  committed
  e5f13f3
- Beginning of universal tm.
  crei
  committed
  4aae857
Commits on Mar 25, 2026
- feat(Data): prove enc_injective and enc_prefix_free
  
  crei
  and
  Copilot
  committed
  baefd9d
- fix(Data): restore StrEnc instances and imports
  
  crei
  and
  Copilot
  committed
  aa03b39
- refactor(Data): simplify balance and injectivity proofs
  
  crei
  and
  Copilot
  committed
  3206807
- refactor(Data): further simplify balance proofs
  
  crei
  and
  Copilot
  committed
  10013f9
- refactor(Data): simplify StrEnc proofs and remove TODO comments
  
  crei
  and
  Copilot
  committed
  62adaf5
- refactor(Data): use simp only for balance-is-zero proofs
  
  crei
  and
  Copilot
  committed
  8e36d9f
- refactor(Data): use le_or_gt and shorter membership patterns
  
  crei
  and
  Copilot
  committed
  4ca6e6c
- refactor(Dyadic): simplify dyadic_mem_chars to grind [dyadic]
  
  crei
  and
  Copilot
  committed
  489c137
Commits on Mar 26, 2026
- cleanup
  crei
  committed
  22e2ca0
- Try out more flexible update functions.
  crei
  committed
  7e9eb8d
- try out more flexible update function
  crei
  committed
  e6ade40
- proof for any_list complete
  crei
  committed
  6881b4c
- feat(ListIteration): scaffold run_list_fold proof with helpers
  
  crei
  and
  Copilot
  committed
  150095d
- try to prove run_list_fold.
  crei
  committed
  ae5a09d
- relax ci
  crei
  committed
  3b4d710
- cleanup
  crei
  committed
  6ec3a46
- cleanup
  crei
  committed
  dbc0f49
- doc: add TODO document stubs for all docBlame lint errors
  
  crei
  and
  Copilot
  committed
  57bbcd3
- remove spaces
  crei
  committed
  b3ba7f4
Commits on Mar 27, 2026
- fix
  crei
  committed
  3dfadf2
- Merge branch 'main' into encoding
  crei
  committed
  a905f5c
- Multi-tape TMs and computations on structured data
  crei
  authored
  918de0b
Commits on Mar 29, 2026
- Initial definitions for universal tm.
  crei
  committed
  56b3d2c
Commits on Mar 30, 2026
- refactor(MultiTape): split into Copy.lean and Eq.lean
  
  crei
  and
  Copilot
  committed
  b39f836
- fix: add missing doWhileEq definition and remove stale While import
  
  crei
  and
  Copilot
  committed
  67fea0b
- Merge pull request #136 from crei/cleanup
  crei
  authored
  58e3f40
- Merge remote-tracking branch 'self/main' into utm
  crei
  committed
  cf074f1
- Merge pull request #135 from crei/utm
  crei
  authored
  5c7488c
- Simplify encoding.
  crei
  committed
  a0a9626
- fix(TapeView): adapt to Data without .num and 4-field TapeView with HeadPos
  
  crei
  and
  Copilot
  committed
  5547224
- fix(TapeView): fix enc_drop_prefix for HeadPos
  
  crei
  and
  Copilot
  committed
  aae83b1
- feat(Data): prove StrEnc ℕ fromData_toData roundtrip
  
  crei
  and
  Copilot
  committed
  4842ed8
- feat(Data): prove all remaining atPath lemmas, eliminating all sorry's
  
  crei
  and
  Copilot
  committed
  e8d1de6
- refactor(Skip): update skipLeft_eval_struct as inverse of skipRight
  
  crei
  and
  Copilot
  committed
  65fae57
- refactor(Skip): combine skipLeft lemmas into single skipLeft_eval_struct
  
  crei
  and
  Copilot
  committed
  aa3997a
- skip
  crei
  committed
  db286e8
- feat(Data): add atPath_dropLast_bind_getLast simp lemma
  
  crei
  and
  Copilot
  committed
  a67874e
- fix(Navigation): add h_left hypotheses and fix compilation errors
  
  crei
  and
  Copilot
  committed
  54eee7f
- feat(Data): prove atPath_zero_isSome_of_nonempty
  
  crei
  and
  Copilot
  committed
  a9934a4
- more work to simplify Data.
  crei
  committed
  f45704a
- fix build
  crei
  committed
  a76a532
- fix simp lint.
  crei
  committed
  f8dd6b7
Commits on Mar 31, 2026
- doc: add missing documentation strings for Data.toList, toLeftEnd, toRightEnd
  
  crei
  and
  Copilot
  committed
  7fdd8f3
- split out ite.
  crei
  committed
  6e165be
- feat(Ite): prove ite.eval_struct with h_left hypothesis
  
  crei
  and
  Copilot
  committed
  60fe84b
- refactor(Ite): support both left-end and right-end head positions
  
  crei
  and
  Copilot
  committed
  c616e91
- feat(Ite): prove left_n.eval, right_n.eval, ite_enc_from_right.eval
  
  crei
  and
  Copilot
  committed
  acaa8b4
- feat(Iterate): add iterate_n utility for repeating TM operations
  
  crei
  and
  Copilot
  committed
  625d9d3
- feat(Iterate): add iterate_n_eval_of_total lemma
  
  crei
  and
  Copilot
  committed
  fb5ba30
- feat(Iterate): add iterate_n_eval_bind and simplify iterate_n_eval_of_total
  
  crei
  and
  Copilot
  committed
  df10a84
- refactor(Ite): simplify left_n.eval and right_n.eval using iterate_n_eval_of_total
  
  crei
  and
  Copilot
  committed
  f3e2072
- feat(Iterate): add Function.iterate_update simp lemma
  
  crei
  and
  Copilot
  committed
  4f75d9e
- feat(Navigation): prove skipRight_n.eval_struct
  
  crei
  and
  Copilot
  committed
  069ca59
- feat(Ite): prove ite.eval_struct
  
  crei
  and
  Copilot
  committed
  d98c089
- refactor(Ite): simplify proofs
  
  crei
  and
  Copilot
  committed
  03fc32c
- feat(TapeView): prove ite_enc_condition_right_iff and enc_suffix_free
  
  crei
  and
  Copilot
  committed
  fbd2faa
Commits on Apr 1, 2026
- simplify
  crei
  committed
  bc139e8
- fix: resolve build errors in Navigation, ListIteration, and ListEncoding
  
  crei
  and
  Copilot
  committed
  2a175c7
- style: fix all non-sorry build warnings
  
  crei
  and
  Copilot
  committed
  e7854ac
- feat(Navigation): prove right_on_nonempty_list sorry-free
  
  crei
  and
  Copilot
  committed
  3c00305
- refactor(Navigation): simplify skipRight_n.eval_struct proof
  
  crei
  and
  Copilot
  committed
  2cbd220
- document
  crei
  committed
  58e1625
- rename, simplify
  crei
  committed
  a08d1c1
- fix(Navigation): prove right_of_leftEnd sorry-free
  
  crei
  and
  Copilot
  committed
  d45f861
Commits on Apr 2, 2026
- fix algorithms by using atElement
  crei
  committed
  0de7273
- fix(Navigation): prove toElem_eval_struct sorry-free
  
  crei
  and
  Copilot
  committed
  e0ca2c5
- style(Navigation): shorten toElem_eval_struct, fix lint errors
  
  crei
  and
  Copilot
  committed
  080c41c
- right_eval_struct
  crei
  committed
  1d1c8a7
- Simplify encoding
  crei
  authored
  5fd3221
- feat(Navigation): prove last-child branch of right_eval_struct
  
  crei
  and
  Copilot
  committed
  d40a44d
- feat(Navigation): prove next-sibling branch of right_eval_struct
  
  crei
  and
  Copilot
  committed
  34b72ef
- refactor: simplify encodedPos and right_eval_struct proofs
  
  crei
  and
  Copilot
  committed
  3a9080d
- refactor: add simp lemmas, remove redundant right_of_leftEnd
  
  crei
  and
  Copilot
  committed
  9a47c43
Commits on Apr 5, 2026
- move lemma
  crei
  committed
  c48ed98
Commits on Apr 17, 2026
- lint
  crei
  committed
  722a98d
- General lemma for single right movement
  crei
  authored
  53ce134
Commits on Apr 29, 2026
- Merge remote-tracking branch 'origin/main'
  crei
  committed
  c1f2e8e
- Fix build..
  crei
  committed
  693971a
- Merge pull request #165 from crei/fix_build
  crei
  authored
  ce302dd
- Semantics of atPath
  crei
  authored
  4e9da07
Commits on Apr 30, 2026
- Head position over time
  crei
  authored
  c87ed82
- Lemmas about atPath.
  crei
  authored
  284e1b2
- Progress on utm.
  crei
  committed
  5ebcb37
- Semantics of copying out the symbols under the head.
  crei
  committed
  0d05f71
Commits on May 4, 2026
- Merge remote-tracking branch 'origin/main'
  crei
  committed
  62f5a7c
- Merge remote-tracking branch 'self/main' into utm
  crei
  committed
  d3fd75c
- Introduce encoding type.
  crei
  committed
  9a4fa29
Commits on May 5, 2026
- Remove StrEnc.fromData.
  crei
  authored
  ff7f42f
- Merge remote-tracking branch 'self/main' into utm
  crei
  committed
  6b64b45
- Function view for tapes. (#160)
  crei
  authored
  02c9109
- Merge remote-tracking branch 'self/main' into utm
  crei
  committed
  7d78344
- fix merge.
  crei
  committed
  17fcdb9
- Simplify proof.
  crei
  committed
  c7394a1
- Semantics of getHeadSymbols.
  crei
  committed
  c2c1101
Commits on May 7, 2026
- Semantics of provideTransitionInput
  crei
  committed
  ecf5daa
Commits on May 11, 2026
- eval fun
  crei
  committed
  e24da87

Commits

Commits on Jan 23, 2026

Commits on Jan 25, 2026

Commits on Jan 26, 2026

Commits on Jan 30, 2026

Commits on Jan 31, 2026

Commits on Feb 2, 2026

Commits on Feb 3, 2026

Commits on Feb 20, 2026

Commits on Feb 21, 2026

Commits on Feb 24, 2026

Commits on Mar 2, 2026

Commits on Mar 4, 2026

Commits on Mar 5, 2026

Commits on Mar 6, 2026

Commits on Mar 7, 2026

Commits on Mar 9, 2026

Commits on Mar 10, 2026

Commits on Mar 11, 2026

Commits on Mar 13, 2026

Commits on Mar 15, 2026

Commits on Mar 16, 2026

Commits on Mar 17, 2026