Documentation

Mathlib.Computability.Reduce

Strong reducibility and degrees. #

This file defines the notions of computable many-one reduction and one-one reduction between sets, and shows that the corresponding degrees form a semilattice.

Notations #

This file uses the local notation ⊕' for Sum.elim to denote the disjoint union of two degrees.

References #

Tags #

computability, reducibility, reduction

def ManyOneReducible {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (p : αProp) (q : βProp) :

p is many-one reducible to q if there is a computable function translating questions about p to questions about q.

Equations
Instances For

    p is many-one reducible to q if there is a computable function translating questions about p to questions about q.

    Equations
    Instances For
      theorem ManyOneReducible.mk {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : αβ} (q : βProp) (h : Computable f) :
      (fun (a : α) => q (f a)) ≤₀ q
      theorem manyOneReducible_refl {α : Type u_1} [Primcodable α] (p : αProp) :
      p ≤₀ p
      theorem ManyOneReducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} :
      p ≤₀ qq ≤₀ rp ≤₀ r
      theorem reflexive_manyOneReducible {α : Type u_1} [Primcodable α] :
      Reflexive ManyOneReducible
      theorem transitive_manyOneReducible {α : Type u_1} [Primcodable α] :
      Transitive ManyOneReducible
      def OneOneReducible {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (p : αProp) (q : βProp) :

      p is one-one reducible to q if there is an injective computable function translating questions about p to questions about q.

      Equations
      Instances For

        p is one-one reducible to q if there is an injective computable function translating questions about p to questions about q.

        Equations
        Instances For
          theorem OneOneReducible.mk {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {f : αβ} (q : βProp) (h : Computable f) (i : Function.Injective f) :
          (fun (a : α) => q (f a)) ≤₁ q
          theorem oneOneReducible_refl {α : Type u_1} [Primcodable α] (p : αProp) :
          p ≤₁ p
          theorem OneOneReducible.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} :
          p ≤₁ qq ≤₁ rp ≤₁ r
          theorem OneOneReducible.to_many_one {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : αProp} {q : βProp} :
          p ≤₁ qp ≤₀ q
          theorem OneOneReducible.of_equiv {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {e : α β} (q : βProp) (h : Computable e) :
          (q e) ≤₁ q
          theorem OneOneReducible.of_equiv_symm {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {e : α β} (q : βProp) (h : Computable e.symm) :
          q ≤₁ (q e)
          theorem reflexive_oneOneReducible {α : Type u_1} [Primcodable α] :
          Reflexive OneOneReducible
          theorem transitive_oneOneReducible {α : Type u_1} [Primcodable α] :
          Transitive OneOneReducible
          theorem ComputablePred.computable_of_manyOneReducible {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : αProp} {q : βProp} (h₁ : p ≤₀ q) (h₂ : ComputablePred q) :
          theorem ComputablePred.computable_of_oneOneReducible {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : αProp} {q : βProp} (h : p ≤₁ q) :
          def ManyOneEquiv {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (p : αProp) (q : βProp) :

          p and q are many-one equivalent if each one is many-one reducible to the other.

          Equations
          Instances For
            def OneOneEquiv {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (p : αProp) (q : βProp) :

            p and q are one-one equivalent if each one is one-one reducible to the other.

            Equations
            Instances For
              theorem manyOneEquiv_refl {α : Type u_1} [Primcodable α] (p : αProp) :
              theorem ManyOneEquiv.symm {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : αProp} {q : βProp} :
              theorem ManyOneEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} :
              theorem equivalence_of_manyOneEquiv {α : Type u_1} [Primcodable α] :
              Equivalence ManyOneEquiv
              theorem oneOneEquiv_refl {α : Type u_1} [Primcodable α] (p : αProp) :
              theorem OneOneEquiv.symm {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : αProp} {q : βProp} :
              theorem OneOneEquiv.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} :
              OneOneEquiv p qOneOneEquiv q rOneOneEquiv p r
              theorem equivalence_of_oneOneEquiv {α : Type u_1} [Primcodable α] :
              Equivalence OneOneEquiv
              theorem OneOneEquiv.to_many_one {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : αProp} {q : βProp} :
              def Equiv.Computable {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] (e : α β) :

              a computable bijection

              Equations
              Instances For
                theorem Equiv.Computable.symm {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {e : α β} :
                e.Computablee.symm.Computable
                theorem Equiv.Computable.trans {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {e₁ : α β} {e₂ : β γ} :
                e₁.Computablee₂.Computable(e₁.trans e₂).Computable
                theorem Computable.eqv (α : Type u_1) [Denumerable α] :
                (Denumerable.eqv α).Computable
                theorem Computable.equiv₂ (α : Type u_1) (β : Type u_2) [Denumerable α] [Denumerable β] :
                (Denumerable.equiv₂ α β).Computable
                theorem OneOneEquiv.of_equiv {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {e : α β} (h : e.Computable) {p : βProp} :
                OneOneEquiv (p e) p
                theorem ManyOneEquiv.of_equiv {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {e : α β} (h : e.Computable) {p : βProp} :
                ManyOneEquiv (p e) p
                theorem ManyOneEquiv.le_congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} (h : ManyOneEquiv p q) :
                p ≤₀ r q ≤₀ r
                theorem ManyOneEquiv.le_congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} (h : ManyOneEquiv q r) :
                p ≤₀ q p ≤₀ r
                theorem OneOneEquiv.le_congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} (h : OneOneEquiv p q) :
                p ≤₁ r q ≤₁ r
                theorem OneOneEquiv.le_congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} (h : OneOneEquiv q r) :
                p ≤₁ q p ≤₁ r
                theorem ManyOneEquiv.congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} (h : ManyOneEquiv p q) :
                theorem ManyOneEquiv.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} (h : ManyOneEquiv q r) :
                theorem OneOneEquiv.congr_left {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} (h : OneOneEquiv p q) :
                theorem OneOneEquiv.congr_right {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} (h : OneOneEquiv q r) :
                @[simp]
                theorem ULower.down_computable {α : Type u_1} [Primcodable α] :
                (ULower.equiv α).Computable
                theorem manyOneEquiv_up {α : Type u_1} [Primcodable α] {p : αProp} :
                ManyOneEquiv (p ULower.up) p
                theorem OneOneReducible.disjoin_left {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : αProp} {q : βProp} :
                theorem OneOneReducible.disjoin_right {α : Type u_1} {β : Type u_2} [Primcodable α] [Primcodable β] {p : αProp} {q : βProp} :
                theorem disjoin_manyOneReducible {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} :
                p ≤₀ rq ≤₀ rSum.elim p q ≤₀ r
                theorem disjoin_le {α : Type u_1} {β : Type u_2} {γ : Type u_3} [Primcodable α] [Primcodable β] [Primcodable γ] {p : αProp} {q : βProp} {r : γProp} :
                def toNat {α : Type u} [Primcodable α] [Inhabited α] (p : Set α) :

                Computable and injective mapping of predicates to sets of natural numbers.

                Equations
                Instances For
                  @[simp]
                  theorem toNat_manyOneReducible {α : Type u} [Primcodable α] [Inhabited α] {p : Set α} :
                  @[simp]
                  theorem manyOneReducible_toNat {α : Type u} [Primcodable α] [Inhabited α] {p : Set α} :
                  @[simp]
                  theorem manyOneReducible_toNat_toNat {α : Type u} [Primcodable α] [Inhabited α] {β : Type v} [Primcodable β] [Inhabited β] {p : Set α} {q : Set β} :
                  @[simp]
                  theorem toNat_manyOneEquiv {α : Type u} [Primcodable α] [Inhabited α] {p : Set α} :
                  @[simp]
                  theorem manyOneEquiv_toNat {α : Type u} [Primcodable α] [Inhabited α] {β : Type v} [Primcodable β] [Inhabited β] (p : Set α) (q : Set β) :

                  A many-one degree is an equivalence class of sets up to many-one equivalence.

                  Equations
                  Instances For
                    def ManyOneDegree.of {α : Type u} [Primcodable α] [Inhabited α] (p : αProp) :

                    The many-one degree of a set on a primcodable type.

                    Equations
                    Instances For
                      theorem ManyOneDegree.ind_on {C : ManyOneDegreeProp} (d : ManyOneDegree) (h : ∀ (p : Set ), C (ManyOneDegree.of p)) :
                      C d
                      @[reducible, inline]
                      abbrev ManyOneDegree.liftOn {φ : Sort u_1} (d : ManyOneDegree) (f : Set φ) (h : ∀ (p q : Prop), ManyOneEquiv p qf p = f q) :
                      φ

                      Lifts a function on sets of natural numbers to many-one degrees.

                      Equations
                      Instances For
                        @[simp]
                        theorem ManyOneDegree.liftOn_eq {φ : Sort u_1} (p : Set ) (f : Set φ) (h : ∀ (p q : Prop), ManyOneEquiv p qf p = f q) :
                        (ManyOneDegree.of p).liftOn f h = f p
                        @[reducible]
                        def ManyOneDegree.liftOn₂ {φ : Sort u_1} (d₁ : ManyOneDegree) (d₂ : ManyOneDegree) (f : Set Set φ) (h : ∀ (p₁ p₂ q₁ q₂ : Prop), ManyOneEquiv p₁ p₂ManyOneEquiv q₁ q₂f p₁ q₁ = f p₂ q₂) :
                        φ

                        Lifts a binary function on sets of natural numbers to many-one degrees.

                        Equations
                        • d₁.liftOn₂ d₂ f h = d₁.liftOn (fun (p : Set ) => d₂.liftOn (f p) )
                        Instances For
                          @[simp]
                          theorem ManyOneDegree.liftOn₂_eq {φ : Sort u_1} (p : Set ) (q : Set ) (f : Set Set φ) (h : ∀ (p₁ p₂ q₁ q₂ : Prop), ManyOneEquiv p₁ p₂ManyOneEquiv q₁ q₂f p₁ q₁ = f p₂ q₂) :
                          (ManyOneDegree.of p).liftOn₂ (ManyOneDegree.of q) f h = f p q
                          @[simp]
                          theorem ManyOneDegree.of_eq_of {α : Type u} [Primcodable α] [Inhabited α] {β : Type v} [Primcodable β] [Inhabited β] {p : αProp} {q : βProp} :

                          For many-one degrees d₁ and d₂, d₁ ≤ d₂ if the sets in d₁ are many-one reducible to the sets in d₂.

                          Equations
                          @[simp]
                          theorem ManyOneDegree.of_le_of {α : Type u} [Primcodable α] [Inhabited α] {β : Type v} [Primcodable β] [Inhabited β] {p : αProp} {q : βProp} :

                          The join of two degrees, induced by the disjoint union of two underlying sets.

                          Equations
                          @[simp]
                          theorem ManyOneDegree.add_of {α : Type u} [Primcodable α] [Inhabited α] {β : Type v} [Primcodable β] [Inhabited β] (p : Set α) (q : Set β) :
                          @[simp]
                          theorem ManyOneDegree.add_le {d₁ : ManyOneDegree} {d₂ : ManyOneDegree} {d₃ : ManyOneDegree} :
                          d₁ + d₂ d₃ d₁ d₃ d₂ d₃
                          @[simp]
                          theorem ManyOneDegree.le_add_left (d₁ : ManyOneDegree) (d₂ : ManyOneDegree) :
                          d₁ d₁ + d₂
                          @[simp]
                          theorem ManyOneDegree.le_add_right (d₁ : ManyOneDegree) (d₂ : ManyOneDegree) :
                          d₂ d₁ + d₂