Partial functions, again

Stream: new members

[Huỳnh Trần Khanh]

Well, I really need partial functions. I really, really need partial functions. There is a specific class of competitive programming problems called 'interactive problems' which requires contestants to interact with a secret library, and functions from that library often have some preconditions. If the contestant violates a precondition then their submission is judged as Wrong Answer—a generic verdict given by the automatic judge system when the submitted code doesn't work as expected.

So with that out of the way, I am experimenting with the "useless" hypothesis parameter. May I ask a few questions:

• Why are some hypotheses replaced with _ in the infoview?
• Why does the rw tactic dislike the extra hypothesis parameter so much? It even says "rewrite tactic failed, motive is not type correct" when I directly prove the retrieve_replace lemma without the helper lemma.

[Huỳnh Trần Khanh]

import data.list.basic
import tactic.linarith

universe u

def retrieve { α : Type u } : ∀ array: list α, ∀ index: ℕ, ∀ h: index < array.length, α
| [] index h := begin
  -- I can't provide a sane value. I'm relying on the principle of explosion to produce an instance of the desired type.
  rw list.length_eq_zero.mpr at h,
  linarith,
  refl,
end
| (head::rest) 0 h := head
| (head::rest) (n + 1) h := begin
  have : (head::rest).length = rest.length + 1 := list.length_cons head rest,
  rw this at h,
  have : n < rest.length := by linarith,
  exact retrieve rest n this,
end

def replace { α : Type u } : ∀ array: list α, ∀ index: ℕ, ∀ h: index < array.length, ∀ target: α, list α
| [] index h target := begin
  -- I can't provide a sane value. I'm relying on the principle of explosion to produce an instance of the desired type.
  rw list.length_eq_zero.mpr at h,
  linarith,
  refl,
end
| (head::rest) 0 h target := target::rest
| (head::rest) (n + 1) h target := begin
  have : (head::rest).length = rest.length + 1 := list.length_cons head rest,
  rw this at h,
  have : n < rest.length := by linarith,
  exact head::replace rest n this target,
end

lemma length_equal { α : Type u } : ∀ array : list α, ∀ index : ℕ, ∀ h : index < array.length, ∀ value : α, array.length = (replace array index h value).length
| [] index h target := begin
  rw list.length_eq_zero.mpr at h,
  linarith,
  refl,
end
| (head::rest) 0 h target := begin
  rw replace,
  rw list.length_cons head rest,
  rw list.length_cons target rest,
end
| (head::rest) (n + 1) h target := begin
  rw replace,
  rw list.length_cons head rest,
  rw list.length_cons head _,
  rw (length_equal rest n _ target).symm,
end

lemma transform_hypothesis { α : Type u } : ∀ array : list α, ∀ index : ℕ, ∀ h : index < array.length, ∀ value : α, index < (replace array index h value).length := begin
  intro array,
  intro index,
  intro h,
  intro value,
  rw (length_equal array index h value).symm,
  exact h,
end

-- This auxiliary lemma is there because the rw tactic doesn't like the transformed hypothesis for some reason.
lemma retrieve_replace_aux { α : Type u } : ∀ array : list α, ∀ index : ℕ, ∀ h : index < array.length, ∀ value : α, ∀ h' : index < (replace array index h value).length, retrieve (replace array index h value) index h' = value
| [] index h target := begin
  rw list.length_eq_zero.mpr at h,
  exfalso,
  linarith,
  refl,
end
| (head::rest) 0 h target := begin
  rw replace,
  intro h',
  rw retrieve,
end
| (head::rest) (n + 1) h target := begin
  rw replace,
  intro h',
  rw retrieve,
  rw retrieve_replace_aux rest n _ target _,
end

lemma retrieve_replace { α : Type u } : ∀ array : list α, ∀ index : ℕ, ∀ h : index < array.length, ∀ value : α, retrieve (replace array index h value) index (transform_hypothesis array index h value) = value := begin
  intro array,
  intro index,
  intro h,
  intro value,
  rw retrieve_replace_aux,
end

[Eric Wieser]

Isn't your retrieve just docs#list.nth_le?

[Huỳnh Trần Khanh]

Oh. And my replace is just docs#list.update_nth with the extra hypothesis paramater. Interesting.

[Kevin Buzzard]

You can have partial functions -- the issue is that they are a bit messier to prove things about. If you're just doing competitive programming stuff, especially if you're just running functions and don't mind supplying the proofs that you're within the right bounds, then that's fine. I think I already told you my experience with partial functions when doing mathematical proofs -- when I was proving sqrt(2)+sqrt(3)<sqrt(10) by squaring things out, it was painful. But if you're not in this use case, or if you're in a use case where those proofs really do feel necessary for you, then go ahead and use partial functions -- they work fine :-)

[Huỳnh Trần Khanh]

Why are proofs of hypotheses represented as _ in the infoview? Is it because proofs are irrelevant?

[Eric Wieser]

Yes

[Bryan Gin-ge Chen]

You can tell Lean to show proofs with the option set_option pp.proofs true.