FormalConjecturesForMathlib/Computability/Primrec.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Formal Conjectures paper, arXiv v1

1 declarations, 0 contain sorry, 0 declared as axioms

Primcodable instances from retractions

Primcodable.ofLeftInverse builds a Primcodable instance on a type β from a map f : β → α into a Primcodable type α together with a left inverse finv of f such that f ∘ finv is primitive recursive. This is the Primcodable analogue of Encodable.ofLeftInverse, and applies in particular to sigma types, for which Mathlib provides no Primcodable instance.

Imports (1)
Imported by 1 file
  1. def Primcodable.ofLeftInverse If f : β → α has a left inverse finv such that f ∘ finv is primitive recursive, then β is Primcodable, with b encoded as Encodable.encode (f b) line 38 source

    Source documentation

    If f : β → α has a left inverse finv such that f ∘ finv is primitive recursive, then β is Primcodable, with b encoded as Encodable.encode (f b).

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: Primcodable, Eq, Primrec

    Proof uses: Primcodable.mk, Encodable.ofLeftInverse

    2 instances, coercions and auxiliary constants left out.

    Tactic trace: 4 steps

    Open to load the checked before-and-after goal states.

    def ofLeftInverse (f : β → α) (finv : α → β) (linv : ∀ b, finv (f b) = b)
    (hf : Primrec fun a => f (finv a)) : Primcodable β :=
…