Code

Post's problem#4

Code

Merged

yforster merged 56 commits intouds-psl:mainuds-psl/coq-synthetic-computability:mainfrom HaoyiZeng:mainHaoyiZeng/coq-synthetic-computability:mainCopy head branch name to clipboardJan 27, 2025

Commits

Commits on Oct 3, 2023

• Adds proof of Limit lemma 1

  HaoyiZeng

  committed
  069b6ff

  Copy full SHA for 069b6ff

• Add lowsimple.v

  HaoyiZeng

  committed
  4458ab8

  Copy full SHA for 4458ab8

• delete dup comments

  HaoyiZeng

  committed
  7164566

  Copy full SHA for 7164566

Commits on Oct 29, 2023

• Ongoing Limit Lemma2

  HaoyiZeng

  committed
  5b36e60

  Copy full SHA for 5b36e60

Commits on Oct 31, 2023

• Finshed proof outline

  HaoyiZeng

  committed
  83e54b1

  Copy full SHA for 83e54b1

• Proof mono_m

  HaoyiZeng

  committed
  4e3f02a

  Copy full SHA for 4e3f02a

Commits on Nov 5, 2023

• Proof monotonic of m

  HaoyiZeng

  committed
  e8551f6

  Copy full SHA for e8551f6

Commits on Nov 7, 2023

• Done Limit Lemma

  HaoyiZeng

  committed
  cac6b7e

  Copy full SHA for cac6b7e

Commits on Feb 1, 2024

• Try SS

  HaoyiZeng

  committed
  4a1eb99

  Copy full SHA for 4a1eb99

Commits on Feb 6, 2024

• Add F_

  HaoyiZeng

  committed
  08bde05

  Copy full SHA for 08bde05

• typo

  HaoyiZeng

  committed
  12e8cfc

  Copy full SHA for 12e8cfc

Commits on Mar 15, 2024

• update

  HaoyiZeng

  committed
  ac9a327

  Copy full SHA for ac9a327

Commits on Mar 17, 2024

• refactor

  HaoyiZeng

  committed
  6399aa4

  Copy full SHA for 6399aa4

• decidability of extension

  HaoyiZeng

  committed
  bfa7cf6

  Copy full SHA for bfa7cf6

Commits on Mar 18, 2024

• dn of requirements

  HaoyiZeng

  committed
  f5c5513

  Copy full SHA for f5c5513

Commits on Mar 19, 2024

• P is simple

  HaoyiZeng

  committed
  65c55d8

  Copy full SHA for 65c55d8

• refactor

  HaoyiZeng

  committed
  161b808

  Copy full SHA for 161b808

• adds detail

  HaoyiZeng

  committed
  e790d58

  Copy full SHA for e790d58

Commits on Mar 24, 2024

• wall function

  HaoyiZeng

  committed
  22242ac

  Copy full SHA for 22242ac

Commits on Mar 25, 2024

• refactor

  HaoyiZeng

  committed
  a04cc7e

  Copy full SHA for a04cc7e

Commits on Apr 1, 2024

• step-indexed Oracle

  HaoyiZeng

  committed
  078f19c

  Copy full SHA for 078f19c

• done Phi

  HaoyiZeng

  committed
  5d84cf5

  Copy full SHA for 5d84cf5

Commits on Apr 12, 2024

• final fact

  HaoyiZeng

  committed
  df53dde

  Copy full SHA for df53dde

• fix error

  HaoyiZeng

  committed
  6b826b4

  Copy full SHA for 6b826b4

Commits on Apr 20, 2024

• final fact gen

  HaoyiZeng

  committed
  a8f78d5

  Copy full SHA for a8f78d5

Commits on May 6, 2024

• state the lemma

  HaoyiZeng

  committed
  7ffa62c

  Copy full SHA for 7ffa62c

Commits on Aug 11, 2024

• LPO -> exists p, p is low simple

  HaoyiZeng

  committed
  0eafc42

  Copy full SHA for 0eafc42

Commits on Aug 12, 2024

• error

  HaoyiZeng

  committed
  4945062

  Copy full SHA for 4945062

• finish proof

  HaoyiZeng

  committed
  54a37e7

  Copy full SHA for 54a37e7

Commits on Aug 17, 2024

• PostsProblem

  HaoyiZeng

  committed
  9d1f69c

  Copy full SHA for 9d1f69c

Commits on Aug 18, 2024

• Delete theories/PostsProblem/.DS_Store

  HaoyiZeng

  authored
  3ed8a4f

  Copy full SHA for 3ed8a4f

• Rename Limit.v to limit_computability.v

  HaoyiZeng

  authored
  7e9a5d0

  Copy full SHA for 7e9a5d0

• Rename StepIndex.v to step_indexing.v

  HaoyiZeng

  authored
  ec490eb

  Copy full SHA for ec490eb

• Rename low_wall.v to the_low_wall_function.v

  HaoyiZeng

  authored
  493e4b4

  Copy full SHA for 493e4b4

• Rename lowsimple.v to low_simple_predicates.v

  HaoyiZeng

  authored
  9f3e663

  Copy full SHA for 9f3e663

• Rename priority_method.v to the_priority_method.v

  HaoyiZeng

  authored
  aa1d305

  Copy full SHA for aa1d305

• Rename the_low_wall_function.v to lowness.v

  HaoyiZeng

  authored
  5fb992a

  Copy full SHA for 5fb992a

• Rename simple_extension.v to simpleness.v

  HaoyiZeng

  authored
  e69fa22

  Copy full SHA for e69fa22

• index

  HaoyiZeng

  committed
  fac238d

  Copy full SHA for fac238d

• Merge branch 'main' of github.com:HaoyiZeng/coq-synthetic-computability

  HaoyiZeng

  committed
  3fb6f31

  Copy full SHA for 3fb6f31

Commits on Dec 10, 2024

• refactor to prove Post's problem from ~~ LPO

  yforster

  committed
  4bcc0b3

  Copy full SHA for 4bcc0b3

Commits on Dec 11, 2024

• ¬¬(¬¬Σ⁰₁)-LEM suffices

  yforster

  committed
  885692c

  Copy full SHA for 885692c

• fix proof

  HaoyiZeng

  committed
  87a3fcf

  Copy full SHA for 87a3fcf

• remove one double negation

  yforster

  committed
  597fdbb

  Copy full SHA for 597fdbb

Commits on Jan 21, 2025

• generalise attend_at_most_once_bound

  yforster

  committed
  e9817a0

  Copy full SHA for e9817a0

• polish

  HaoyiZeng

  committed
  89b0641

  Copy full SHA for 89b0641

• Merge branch 'main' of github.com:HaoyiZeng/coq-synthetic-computability

  HaoyiZeng

  committed
  aa7e172

  Copy full SHA for aa7e172

• fix lowness

  HaoyiZeng

  committed
  11b57b2

  Copy full SHA for 11b57b2

• refactoring

  HaoyiZeng

  committed
  b6c341b

  Copy full SHA for b6c341b

• polisj

  HaoyiZeng

  committed
  affbbf7

  Copy full SHA for affbbf7

Commits on Jan 22, 2025

• typo

  HaoyiZeng

  committed
  b3b0c1c

  Copy full SHA for b3b0c1c

• using unicode

  HaoyiZeng

  committed
  d67c467

  Copy full SHA for d67c467

• unicode

  HaoyiZeng

  committed
  11614ee

  Copy full SHA for 11614ee

Commits on Jan 23, 2025

• fixed code

  HaoyiZeng

  committed
  3d9ff2d

  Copy full SHA for 3d9ff2d

• updated

  HaoyiZeng

  committed
  e79e182

  Copy full SHA for e79e182

• fix error

  HaoyiZeng

  committed
  2dd4e44

  Copy full SHA for 2dd4e44