refactor(computability/reduce): define many-one degrees without param…

…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.

src/computability/partrec.lean

@@ -564,6 +564,17 @@ theorem option_map {f : α → option β} {g : α → β → σ}
   (hf : computable f) (hg : computable₂ g) : computable (λ a, (f a).map (g a)) :=
 option_bind hf (option_some.comp₂ hg)
 
+theorem option_get_or_else {f : α → option β} {g : α → β}
+  (hf : computable f) (hg : computable g) :
+  computable (λ a, (f a).get_or_else (g a)) :=
+(computable.option_cases hf hg (show computable₂ (λ a b, b), from computable.snd)).of_eq $
+λ a, by cases f a; refl
+
+theorem subtype_mk {f : α → β} {p : β → Prop} [decidable_pred p] {h : ∀ a, p (f a)}
+    (hp : primrec_pred p) (hf : computable f) :
+  @computable _ _ _ (primcodable.subtype hp) (λ a, (⟨f a, h a⟩ : subtype p)) :=
+nat.partrec.of_eq hf $ λ n, by cases decode α n; simp [subtype.encode_eq]
+
 theorem sum_cases
   {f : α → β ⊕ γ} {g : α → β → σ} {h : α → γ → σ}
   (hf : computable f) (hg : computable₂ g) (hh : computable₂ h) :