[Merged by Bors] - feat(computability): strong reducibility and degrees #1203

minchaowu · 2019-07-10T04:48:09Z

TO CONTRIBUTORS:

Make sure you have:

reviewed and applied the coding style: coding, naming
for tactics:
- added or adapted documentation in tactics.md
- write an example of use of the new feature in tactics.lean
make sure definitions and lemmas are put in the right files
make sure definitions and lemmas are not redundant

If this PR is related to a discussion on Zulip, please include a link in the discussion.

minchaowu · 2019-07-18T16:37:33Z

I think this one is ready to merge in terms of content. @digama0 what do you think? (I'm sure you can squeeze these proofs!) More can be proved once we have the parameter theorem.

robertylewis · 2019-07-25T09:05:34Z

Could you update this to match the new doc requirements? (https://github.com/leanprover-community/mathlib/blob/master/docs/contribute/doc.md)

digama0 · 2019-09-19T08:56:19Z

src/computability/partrec_code.lean

@@ -506,6 +512,19 @@ theorem curry_prim : primrec₂ curry :=
 comp_prim.comp primrec.fst $
 pair_prim.comp (const_prim.comp primrec.snd) (primrec.const code.id)

+theorem one_one_curry {c₁ c₂ n₁ n₂} (h : curry c₁ n₁ = curry c₂ n₂) : c₁ = c₂ ∧ n₁ = n₂ :=


The name seems a bit nonconventional. I would actually be inclined to call this one injective_curry, and the other one injective_curry' or similar; we've never used one-one to refer to injectivity before in mathlib.

digama0 · 2019-09-19T08:57:29Z

src/computability/partrec_code.lean

+λ a b h, (@one_one_curry _ _ 0 0 $ by rw h).1
+
+theorem s_m_n (c n x) : ∃ f : code → ℕ → code, 
+  function.injective f ∧ computable₂ f ∧ eval (f c n) x = eval c (mkpair n x) := 


Is injectivity like this a part of S_m^n? It's a bit weird to have injectivity of a binary curried function relative to one of its arguments.

Also, n and x are quantified in the wrong place here. They should be in the third conjunct, since we want to say that f has a certain behavior on any input values n,x.

Ah, that's a shame. I copy-pasted eval_curry without thinking about it.

Recursion theorists usually want it to be injective for better reducibility purposes, but as you said it's unnatural to have it relative to one of its arguments. I have removed the condition, but left the injectivity as a separate theorem.

digama0 · 2019-09-19T08:59:06Z

src/computability/reduce.lean

+ λ x y h, ⟨h.2, h.1⟩, 
+ λ x y z h₁ h₂, ⟨transitive_one_one_reducible h₁.1 h₂.1, transitive_one_one_reducible h₂.2 h₁.2⟩⟩
+
+instance many_one_equiv_setoid {α} [primcodable α] : setoid (set α) := 


This shouldn't be an instance

If I don't make this an instance then I have to provide it to the quotient.lift proofs below, which is fine but looks a bit awkward. Is there any particular reason that you think this shouldn't be an instance?

You can make it a local instance, but the problem is that the typeclass problem is not domain specific but the solution is. This instance will equip any set anywhere with the many one equiv, which is unlikely to be the right one if you are doing ring theory, say.

digama0 · 2019-09-19T09:00:59Z

src/computability/reduce.lean

+
+def many_one_degree {α} [primcodable α] := quotient (@many_one_equiv_setoid α _)
+
+def disjoin (p q : set ℕ) : set ℕ  := (λ x, 2 * x) '' p ∪ (λ x, 2 * x + 1) '' q


I would like to see this generalized over other types. Rather than coding everything over nats, this would look much better if the domain is simply a sum type, and the primcodable instance will do all the odd/even interleaving work.

I would also like to make things as general as possible, but just like Rice's theorem, the classical results are almost always about nats. I feel that we can go with nats for now, and if the generalized version turns out to be useful for other theories, then we do the refactoring.

I actually am claiming that the work you are doing now can be done easier with sum types, even setting aside any possible future benefits of generalization. sum.inl is primrec, which replaces your theorems about 2x and 2x+1.

Also, many_one_equiv and friends can be stated with different types on the left and right, although of course the setoid instance can't.

I agree that sum type naturally interleaves things, but then we end up having something like set (ℕ ⊕ ℕ) when trying to instantiate them with nats. That looks a bit weird to me when I just want to reason about predicates on natural numbers. We could prove some translation theorems, though.

digama0 · 2019-09-19T09:02:37Z

src/computability/reduce.lean

+lemma add1 : primrec (nat.unpaired (λ x y, nat.succ y)) :=
+by simp [primrec₂.unpaired, primrec.comp₂ primrec.succ primrec₂.right]
+
+lemma double : primrec (λ n, 2 * n) :=


I am concerned that this theorem is not a trivial consequence of the primrec library. It should be the composition of primrec_mul and primrec_const

This one drives me crazy. I'm still not sure how to prove it elegantly. Apparently I haven't fully understood the primrec library :(

you should not be using nat.primrec, that is only for bootstrapping. primrec also works on functions from nat to nat and has a lot more theorems

digama0 · 2019-09-20T12:15:03Z

@minchaowu I pushed a bunch of changes regarding type generalization. The disjoin operator builds a bigger type, but for the join semilattice of degrees, we need to map it back into a single type, which only works if the type is nat (or more generally, denumerable). This is done via the comap function that transfers degrees across a computable equiv.

minchaowu · 2019-09-20T12:52:55Z

@digama0 This looks fancy. No objections from me. I like it.

robertylewis · 2019-09-25T11:30:17Z

I think this is still waiting for doc strings on all definitions. I'd love to see the header doc expanded also, at the very least to mention the main definitions and results in the file.

avigad · 2020-04-16T01:41:01Z

At a recent maintainers meeting, it was decided that aside from documentation, this PR could be merged. I rebased the PR and repaired it, and documented the main file, reduce.lean.

I could not get up the motivation to document Mario's whole computability development, but I added headers and a reference to his ITP paper to three of the main files, which should help.

gebner

I think this good enough to be merged. I'll leave the last word to @digama0 as boss of the computability theory.

Is there a reason to consider degrees on a given type α? This makes it awkward to use ≤ on degrees because you want to compare degrees on different types. I would have thought that many_one_degree α is isomorphic to many_one_degree ℕ and that the extra parameter is kind of pointless.

gebner · 2020-04-16T13:26:06Z

src/computability/reduce.lean

+-- local attribute [instance] many_one_equiv_setoid
+


Suggested change

-- local attribute [instance] many_one_equiv_setoid

src/computability/reduce.lean

gebner · 2020-04-16T13:40:04Z

src/computability/reduce.lean

+quotient.lift_on₂' d₁ d₂ (λ a b, a ≤₀ b)
+  (λ a b c d h₁ h₂, propext $ (h₁.le_congr_left).trans (h₂.le_congr_right))
+
+instance many_one_degree.has_le {α} [primcodable α] : has_le (many_one_degree α) := ⟨many_one_degree.le⟩


I'm not sure if it is a good idea to have two ways to compare degrees (i.e., .le and ≤). Unfortunately the .le is more general than ≤.

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

digama0 · 2020-04-16T14:03:29Z

I think this PR has already been reviewed, so I don't have much to add. We can revisit many_one_degree A if necessary in the future (I think I agree that it can skip the type argument in favor of a function that returns the degree of a problem on any primcodable set), but this PR has sat around long enough.

bors r+

Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Jeremy Avigad <avigad@cmu.edu>

bors · 2020-04-16T14:57:33Z

Pull request successfully merged into master.

Build succeeded:

Build mathlib

…unity#1203) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Jeremy Avigad <avigad@cmu.edu>

…eter (#2630) The file `reduce.lean` defines many-one degrees for computable reductions. At the moment every primcodable type `α` has a separate type of degrees `many_one_degree α`. This is completely antithetical to the notion of degrees, which are introduced to classify problems up to many-one equivalence. This PR defines a single `many_one_degree` type that lives in `Type 0`. We use the `ulower` infrastructure from #2574 which shows that every type is computably equivalent to a subset of natural numbers. The function `many_one_degree.of` which assigns to every set of a primcodable type a degree is still universe polymorphic. In particular, we show that `of p = of q ↔ many_one_equiv p q`, etc. in maximal generality, where `p` and `q` are subsets of different types in different universes. See previous discussion at #1203.

…unity#1203) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Jeremy Avigad <avigad@cmu.edu>

minchaowu requested a review from a team as a code owner July 10, 2019 04:48

minchaowu changed the title ~~feat(src/computability): strong reducibility and degrees~~ feat(computability): strong reducibility and degrees Jul 10, 2019

cipher1024 assigned digama0 Jul 13, 2019

robertylewis added the needs-documentation This PR is missing required documentation label Jul 25, 2019

digama0 reviewed Sep 19, 2019

View reviewed changes

semorrison added the please-adopt This PR/issue may have been abandoned by the original contributor. You are welcome to take it over. label Mar 28, 2020

minchaowu and others added 16 commits April 15, 2020 20:05

feat(src/computability): strong reducibility and degrees

77c5244

rename

f21050d

simplify proofs

0429b19

generalize two theorems

cfa1672

fix style

ccf10f0

Proving that many-one degree is a join-semilattice

8019218

simplify proofs

c7a715d

start docs

a4ecfe0

explicitly state s_m_n theorem

8fbd9e0

fix docs

0ef2acf

fix smn

98d6d1f

make it local for now

6b3e456

generalize reduction to multiple types

6545456

simplify definition of add

0575b60

simplify proofs

8831112

documentation

aebf0de

avigad force-pushed the more_comp branch from 4504518 to aebf0de Compare April 16, 2020 01:37

gebner removed the needs-documentation This PR is missing required documentation label Apr 16, 2020

gebner added awaiting-review The author would like community review of the PR and removed please-adopt This PR/issue may have been abandoned by the original contributor. You are welcome to take it over. labels Apr 16, 2020

gebner approved these changes Apr 16, 2020

View reviewed changes

digama0 and others added 8 commits April 16, 2020 06:58

Update src/computability/reduce.lean

59c8a20

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

Update src/computability/reduce.lean

27ba006

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

Update src/computability/reduce.lean

97af703

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

Update src/computability/reduce.lean

dbaa025

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

Update src/computability/reduce.lean

93532ac

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

Update src/computability/reduce.lean

29cf93c

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

Update src/computability/reduce.lean

5c716c8

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

Update src/computability/reduce.lean

3c96ba1

Co-Authored-By: Gabriel Ebner <gebner@gebner.org>

bors bot pushed a commit that referenced this pull request Apr 16, 2020

feat(computability): strong reducibility and degrees (#1203)

c3d943e

Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Jeremy Avigad <avigad@cmu.edu>

github-actions bot added ready-to-merge All that is left is for bors to build and merge this PR. (Remember you need to say `bors r+`.) and removed awaiting-review The author would like community review of the PR labels Apr 16, 2020

bors bot changed the title ~~feat(computability): strong reducibility and degrees~~ [Merged by Bors] - feat(computability): strong reducibility and degrees Apr 16, 2020

bors bot closed this Apr 16, 2020

bors bot deleted the more_comp branch April 16, 2020 14:57

gebner mentioned this pull request May 8, 2020

[Merged by Bors] - refactor(computability/reduce): define many-one degrees without parameter #2630

Closed

anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 15, 2020

feat(computability): strong reducibility and degrees (leanprover-comm…

6500b5c

…unity#1203) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Jeremy Avigad <avigad@cmu.edu>

anrddh pushed a commit to anrddh/mathlib that referenced this pull request May 16, 2020

feat(computability): strong reducibility and degrees (leanprover-comm…

c179b83

…unity#1203) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Jeremy Avigad <avigad@cmu.edu>

cipher1024 pushed a commit to cipher1024/mathlib that referenced this pull request Mar 15, 2022

feat(computability): strong reducibility and degrees (leanprover-comm…

9208e4e

…unity#1203) Co-authored-by: Mario Carneiro <di.gama@gmail.com> Co-authored-by: Jeremy Avigad <avigad@cmu.edu>

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[Merged by Bors] - feat(computability): strong reducibility and degrees #1203

[Merged by Bors] - feat(computability): strong reducibility and degrees #1203

minchaowu commented Jul 10, 2019 •

edited

minchaowu commented Jul 18, 2019

robertylewis commented Jul 25, 2019

digama0 Sep 19, 2019

minchaowu Sep 20, 2019

digama0 Sep 19, 2019

digama0 Sep 20, 2019

minchaowu Sep 20, 2019

minchaowu Sep 20, 2019

digama0 Sep 19, 2019

minchaowu Sep 20, 2019

digama0 Sep 20, 2019 •

edited

digama0 Sep 19, 2019

minchaowu Sep 20, 2019

digama0 Sep 20, 2019

minchaowu Sep 20, 2019

digama0 Sep 19, 2019

minchaowu Sep 20, 2019

digama0 Sep 20, 2019

digama0 commented Sep 20, 2019

minchaowu commented Sep 20, 2019 •

edited

robertylewis commented Sep 25, 2019

avigad commented Apr 16, 2020

gebner left a comment

gebner Apr 16, 2020

gebner Apr 16, 2020

digama0 commented Apr 16, 2020

bors bot commented Apr 16, 2020


		def many_one_degree {α} [primcodable α] := quotient (@many_one_equiv_setoid α _)

		def disjoin (p q : set ℕ) : set ℕ := (λ x, 2 * x) '' p ∪ (λ x, 2 * x + 1) '' q

[Merged by Bors] - feat(computability): strong reducibility and degrees #1203

[Merged by Bors] - feat(computability): strong reducibility and degrees #1203

Conversation

minchaowu commented Jul 10, 2019 • edited

minchaowu commented Jul 18, 2019

robertylewis commented Jul 25, 2019

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 Sep 20, 2019 • edited

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 commented Sep 20, 2019

minchaowu commented Sep 20, 2019 • edited

robertylewis commented Sep 25, 2019

avigad commented Apr 16, 2020

gebner left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

digama0 commented Apr 16, 2020

bors bot commented Apr 16, 2020

minchaowu commented Jul 10, 2019 •

edited

digama0 Sep 20, 2019 •

edited

minchaowu commented Sep 20, 2019 •

edited