ComputablePred from Nat to α

Stream: mathlib4

[SnO2WMaN]

Recently I formalized the mathematical logic fact stated that "if there is a set s.t. recursive enumerable but not recursive (computable), then implies Gödel's first incompleteness theorem." (https://github.com/FormalizedFormalLogic/Foundation/blob/master/Foundation/FirstOrder/Incompleteness/Halting.lean)

We can take a set like that as halting_problem in mathlib4, but some issue about type.
I proved the fact on predicate on Nat. but halting_problem on Code, so cannot use directly.
I need these lemma (or similar else), but I don't these are correct and how to prove.

lemma REPred.iff_decoded_pred {A : α → Prop} [Primcodable α] : REPred A ↔ REPred λ n : ℕ ↦ match Encodable.decode n with | some a => A a | none => False := by
  sorry;

lemma ComputablePred.iff_decoded_pred {A : α → Prop} [h : Primcodable α] : ComputablePred A ↔ ComputablePred λ n : ℕ ↦ match Encodable.decode n with | some a => A a | none => False := by
  sorry;

[Robin Arnez]

The first one is true:

import Mathlib

@[congr]
lemma Part.assert_congr {p₁ p₂ : Prop} {f₁ : p₁ → Part α} {f₂ : p₂ → Part α}
    (hp : p₁ = p₂) (hf : ∀ h, f₁ (hp.mpr_prop h) = f₂ h) :
    Part.assert p₁ f₁ = Part.assert p₂ f₂ := by
  cases hp
  cases funext hf
  rfl

@[simp]
lemma Part.assert_false (f : False → Part α) : Part.assert False f = Part.none := by
  simp only [assert_neg, not_false_eq_true]

@[simp]
lemma Part.assert_true (f : True → Part α) : Part.assert True f = f trivial := by
  simp only [assert_pos]

lemma REPred.iff_decoded_pred {A : α → Prop} [Primcodable α] :
    REPred A ↔ REPred fun n : ℕ ↦ ∃ a, Encodable.decode n = some a ∧ A a := by
  simp only [REPred, Partrec, Encodable.decode_nat, Part.coe_some, Part.bind_some]
  apply propext_iff.mp
  congr 1
  funext n
  cases (Encodable.decode n : Option α) <;> simp

(the first three lemmas should probably be in mathlib somewhere)

[Robin Arnez]

I am inclined to believe the second one is too but I'm unsure

[SnO2WMaN]

It's nice! Thanks

[SnO2WMaN]

I tracked this issue: https://github.com/FormalizedFormalLogic/Foundation/pull/508

[Wuyang]

Great to see the REPred.iff_decoded_pred proof clarified. Curious to see if the ComputablePred case works out similarly. You can find related Lean formalizations with LeanFinder (www.leanfinder.org).

[Wuyang]

@leanfinder REPred and ComputablePred equivalence with decoded predicates in Lean mathlib4

[leanfinder]

Here’s what I found:

• definition ComputablePred {α} [Primcodable α] (p : α → Prop) := ∃ _ : DecidablePred p, Computable fun a => decide (p a) "A predicate \( p \colon \alpha \to \text{Prop} \) on a type \( \alpha \) with a primitive encoding is called computable if there exists a decidable version of \( p \) (i.e., a function \( \text{decide} \) that determines whether \( p(a) \) holds for any \( a \)) and this decision function is computable. In other words, the indicator function of \( p \) is computable." (score: 0.793)

• theorem ComputablePred.computable_iff_re_compl_re {p : α → Prop} [DecidablePred p] : ComputablePred p ↔ RePred p ∧ RePred fun a => ¬p a := ⟨fun h => ⟨h.to_re, h.not.to_re⟩, fun ⟨h₁, h₂⟩ => ⟨‹_›, by obtain ⟨k, pk, hk⟩ := Partrec.merge (h₁.map (Computable.const true).to₂) (h₂.map (Computable.const false).to₂) (by intro a x hx y hy simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true, exists_const] at hx hy cases hy.1 hx.1) refine Partrec.of_eq pk fun n => Part.eq_some_iff.2 ?_ rw [hk] simp only [Part.mem_map_iff, Part.mem_assert_iff, Part.mem_some_iff, exists_prop, and_true, true_eq_decide_iff, and_self, exists_const, false_eq_decide_iff] apply Decidable.em⟩⟩ "Let $\alpha$ be a primitively encodable type and $p \colon \alpha \to \text{Prop}$ a decidable predicate. Then $p$ is computable if and only if both $p$ and its complement $\neg p$ are recursively enumerable." (score: 0.789)

• theorem ComputablePred.computable_iff_re_compl_re' {p : α → Prop} : ComputablePred p ↔ RePred p ∧ RePred fun a => ¬p a := by classical exact computable_iff_re_compl_re "Let $\alpha$ be a primitively encodable type and $p \colon \alpha \to \text{Prop}$ a predicate. Then $p$ is computable if and only if both $p$ and its complement $\neg p$ are recursively enumerable." (score: 0.783)

• theorem ComputablePred.to_re {p : α → Prop} (hp : ComputablePred p) : RePred p := by obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp unfold RePred dsimp only [] refine (Partrec.cond hf (Decidable.Partrec.const' (Part.some ())) Partrec.none).of_eq fun n => Part.ext fun a => ?_ cases a; cases f n <;> simp "Let $\alpha$ be a primitively encodable type and $p \colon \alpha \to \text{Prop}$ a computable predicate. Then $p$ is recursively enumerable." (score: 0.776)

• theorem ComputablePred.computable_iff {p : α → Prop} : ComputablePred p ↔ ∃ f : α → Bool, Computable f ∧ p = fun a => (f a : Prop) := ⟨fun ⟨_, h⟩ => ⟨_, h, funext fun _ => propext (Bool.decide_iff _).symm⟩, by rintro ⟨f, h, rfl⟩; exact ⟨by infer_instance, by simpa using h⟩⟩ "A predicate \( p \colon \alpha \to \text{Prop} \) on a primitively encodable type \( \alpha \) is computable if and only if there exists a computable function \( f \colon \alpha \to \text{Bool} \) such that \( p(a) \) holds if and only if \( f(a) = \text{true} \) for all \( a \in \alpha \)." (score: 0.772)

• theorem ComputablePred.of_eq {α} [Primcodable α] {p q : α → Prop} (hp : ComputablePred p) (H : ∀ a, p a ↔ q a) : ComputablePred q := (funext fun a => propext (H a) : p = q) ▸ hp "Let $\alpha$ be a type with a primitive encoding, and let $p, q \colon \alpha \to \text{Prop}$ be predicates. If $p$ is computable and $p(a) \leftrightarrow q(a)$ holds for all $a \in \alpha$, then $q$ is also computable." (score: 0.758)

• /-- A recursively enumerable predicate is one which is the domain of a computable partial function. -/ def REPred {α} [Primcodable α] (p : α → Prop) := Partrec fun a => Part.assert (p a) fun _ => Part.some () "A predicate $p$ on a type $\alpha$ is recursively enumerable if there exists a computable partial function whose domain consists of exactly those elements $a \in \alpha$ for which $p(a)$ holds. This means that for each $a$, the function can assert whether $p(a)$ is true and produce a result if it is." (score: 0.754)

• theorem ComputablePred.not {p : α → Prop} (hp : ComputablePred p) : ComputablePred fun a => ¬p a := by obtain ⟨f, hf, rfl⟩ := computable_iff.1 hp exact ⟨by infer_instance, (cond hf (const false) (const true)).of_eq fun n => by simp only [Bool.not_eq_true] cases f n <;> rfl⟩ "Let \( \alpha \) be a primitively encodable type and \( p \colon \alpha \to \text{Prop} \) a computable predicate. Then the negation predicate \( \neg p \colon \alpha \to \text{Prop} \) defined by \( (\neg p)(a) = \neg (p(a)) \) is also computable." (score: 0.749)

• theorem REPred.of_eq {α} [Primcodable α] {p q : α → Prop} (hp : REPred p) (H : ∀ a, p a ↔ q a) : REPred q := (funext fun a => propext (H a) : p = q) ▸ hp "Let $\alpha$ be a primitive recursively encodable type, and let $p, q \colon \alpha \to \text{Prop}$ be predicates. If $p$ is a recursively enumerable predicate and $p(a) \leftrightarrow q(a)$ holds for all $a \in \alpha$, then $q$ is also a recursively enumerable predicate." (score: 0.736)

• definition RePred {α} [Primcodable α] (p : α → Prop) := Partrec fun a => Part.assert (p a) fun _ => Part.some () "A predicate \( p \colon \alpha \to \text{Prop} \) on a type \( \alpha \) with a primitive encoding is called recursively enumerable if there exists a computable partial function \( f \colon \alpha \to \sigma \) such that \( p(a) \) holds if and only if \( f(a) \) is defined (i.e., \( a \) is in the domain of \( f \))." (score: 0.735)