Documentation

LeanPool.PointwiseComposition.FailureOfComposition.ArithmeticProgramOperations

Supporting results for pointwise provable equality.

Arithmetic correctness of the compiled program operations.

source
def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.addProgram :
Nat.Partrec.Code

Mathlib program performing addition on the two components of its input.

Equations
Instances For
    source
    def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.mulProgram :
    Nat.Partrec.Code

    Mathlib program performing multiplication on the two input components.

    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.predProgram :
      Nat.Partrec.Code

      Mathlib program for truncated predecessor.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For
        source
        def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.subProgram :
        Nat.Partrec.Code

        Mathlib program for truncated subtraction of the input components.

        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          source
          def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.isZeroProgram :
          Nat.Partrec.Code

          Mathlib program returning one at zero and zero at positive inputs.

          Equations
          Instances For
            source
            def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.ltProgram :
            Nat.Partrec.Code

            Mathlib program deciding strict order of the input components.

            Equations
            • One or more equations did not get rendered due to their size.
            Instances For
              source
              def PointwiseComposition.FailureOfComposition.ConcreteEvaluator.eqProgram :
              Nat.Partrec.Code

              Mathlib program deciding equality of the input components.

              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                source
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.pa_formula_induction {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] {P : M → Prop} (φ : FFL.FirstOrder.ArithmeticSemiformula M 1) (hφ : ∀ (x : M), P x ↔ (FFL.FirstOrder.Semiformula.Eval ![x] id) φ) (hz : P 0) (hs : ∀ (x : M), P x → P (x + 1)) (x : M) :
                P x

                Full PA induction with arbitrary model parameters in its defining formula.

                source
                @[simp]
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.runs_pair {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (f g : Nat.Partrec.Code) (x z : M) :
                ProgramGraph.Computes (f.pair g) x z ↔ ∃ (a : M) (b : M), ProgramGraph.Computes f x a ∧ ProgramGraph.Computes g x b ∧ z = ⟪a, b⟫
                source
                @[simp]
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.runs_prec_zero {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (f g : Nat.Partrec.Code) (a y : M) :
                ProgramGraph.Computes (f.prec g) ⟪a, 0⟫ y ↔ ProgramGraph.Computes f a y
                source
                @[simp]
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.runs_prec_succ {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (f g : Nat.Partrec.Code) (a b y : M) :
                ProgramGraph.Computes (f.prec g) ⟪a, b + 1⟫ y ↔ ∃ (z : M), ProgramGraph.Computes (f.prec g) ⟪a, b⟫ z ∧ ProgramGraph.Computes g ⟪a, ⟪b, z⟫⟫ y
                source
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_add {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : M) :
                ProgramGraph.Computes addProgram ⟪a, b⟫ (a + b)
                source
                @[simp]
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_add_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b z : M) :
                ProgramGraph.Computes addProgram ⟪a, b⟫ z ↔ z = a + b
                source
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_mul {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : M) :
                ProgramGraph.Computes mulProgram ⟪a, b⟫ (a * b)
                source
                @[simp]
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_mul_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b z : M) :
                ProgramGraph.Computes mulProgram ⟪a, b⟫ z ↔ z = a * b
                source
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_pred {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (b : M) :
                ProgramGraph.Computes predProgram b (b - 1)
                source
                @[simp]
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_pred_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (b z : M) :
                ProgramGraph.Computes predProgram b z ↔ z = b - 1
                source
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_sub {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b : M) :
                ProgramGraph.Computes subProgram ⟪a, b⟫ (a - b)
                source
                @[simp]
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_sub_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b z : M) :
                ProgramGraph.Computes subProgram ⟪a, b⟫ z ↔ z = a - b
                source
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_isZero_zero {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] :
                ProgramGraph.Computes isZeroProgram 0 1
                source
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_isZero_succ {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (b : M) :
                ProgramGraph.Computes isZeroProgram (b + 1) 0
                source
                @[simp]
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_isZero_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (b z : M) :
                ProgramGraph.Computes isZeroProgram b z ↔ b = 0 ∧ z = 1 ∨ b ≠ 0 ∧ z = 0
                source
                @[simp]
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_lt_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b z : M) :
                ProgramGraph.Computes ltProgram ⟪a, b⟫ z ↔ a < b ∧ z = 1 ∨ ¬a < b ∧ z = 0
                source
                @[simp]
                theorem PointwiseComposition.FailureOfComposition.ConcreteEvaluator.computes_eq_iff {M : Type u_1} [FFL.ORingStructure M] [M↓[ℒₒᵣ] ⊧* 𝐏𝐀] [M↓[ℒₒᵣ] ⊧* 𝐈𝐎𝐩𝐞𝐧] (a b z : M) :
                ProgramGraph.Computes eqProgram ⟪a, b⟫ z ↔ a = b ∧ z = 1 ∨ a ≠ b ∧ z = 0