partial fun eq equivalent total one.

Stream: new members

[Somo S.]

Is it possible to prove that a partial function is identical to a version of it that has been proven to be total assuming a what is necessary for termination is available as an additional assumed precondition? Here is the example I have been working with as I have been wondering about this. (It seems to me the following should be provable somehow, but I can't seem to think of how):

variable {α : Type u}

def Array.findIdxRev.loop (p : α → Bool) (as : Array α)
    (j : Fin as.size) (h : ∃ (j' : Fin as.size), j' ≤ j.val ∧ p as[j']) : Fin as.size :=
  if _ : p as[j] then
    j
  else
    Array.findIdxRev.loop p as ⟨j - 1, by grind [Nat.pred_le]⟩ (by grind)
termination_by j.val
decreasing_by grind


partial def Array.findIdxRev.loop! (p : α → Bool) (as : Array α)
    (j : Fin as.size) : Fin as.size :=
  if _ : p as[j] then
    j
  else
    Array.findIdxRev.loop! p as ⟨j - 1, by grind [Nat.pred_le]⟩

theorem Array.findIdxRev.loop_part_eq_tot {p : α → Bool} {as : Array α}
    {j : Fin as.size} (h : ∃ (j' : Fin as.size), j' ≤ j.val ∧ p as[j']) :
    Array.findIdxRev.loop! p as j = Array.findIdxRev.loop p as j h := by
  sorry

[Robin Arnez]

Not with a partial one, but a partial_fixpoint one:

variable {α : Type u}

def Array.findIdxRev.loop (p : α → Bool) (as : Array α)
    (j : Fin as.size) (h : ∃ (j' : Fin as.size), j' ≤ j.val ∧ p as[j']) : Fin as.size :=
  if _ : p as[j] then
    j
  else
    Array.findIdxRev.loop p as ⟨j - 1, by grind [Nat.pred_le]⟩ (by grind)
termination_by j.val
decreasing_by grind

def Array.findIdxRev.loop! (p : α → Bool) (as : Array α)
    (j : Fin as.size) : Fin as.size :=
  if _ : p as[j] then
    j
  else
    Array.findIdxRev.loop! p as ⟨j - 1, by grind [Nat.pred_le]⟩
partial_fixpoint

theorem Array.findIdxRev.loop_part_eq_tot {p : α → Bool} {as : Array α}
    {j : Fin as.size} (h : ∃ (j' : Fin as.size), j' ≤ j.val ∧ p as[j']) :
    Array.findIdxRev.loop! p as j = Array.findIdxRev.loop p as j h := by
  fun_induction Array.findIdxRev.loop <;> rw [Array.findIdxRev.loop!] <;>
    simp only [*, ↓reduceDIte, Bool.false_eq_true]

[Robin Arnez]

partial is completely opaque

[Somo S.]

Thanks @Robin Arnez I had no idea about this. This was helpful