Destructing fixed-length list

Stream: Program verification

[Hanno Becker]

Hi :wave: Another example of 'how would an expert do this'... I have a very simple lemma the type of which a serious program verification effort would likely encounter hundreds or thousands. Therefore, I am interested in a short proof which requires as little human intervention as possible. Also, I think the lemma is so trivial that no specialized tactics should be required -- ideally, I'd like to stay in the core lib.

The lemma is x.length = 4 --> x = [x[0], x[1], x[2], x[3]] and here are my clumsy attempts. You will find numerous QUESTIONs where I'm not sure what's going on, and I'd be grateful about clarification on any of them.

I am particularly interested in knowing how the core tactics would allow me to repeatedly and anonymously (without naming hypotheses explicitly) split _any_ disjunction in the set of hypotheses, which is one stumbling block below.

import Lean
import Std.Data.List.Lemmas
open Lean Meta Elab.Tactic

theorem lt_succ_iff_lt_or_eq {n m : Nat} (h : 0 < m) : (n < m) <-> (n = m-1 ∨ n < m-1) := by
  sorry

theorem or_forall {a b : Prop} {P : a ∨ b → Prop} : (∀(h : a ∨ b), P h) <-> ((∀h: a, P (Or.inl h)) ∧ (∀h: b, P (Or.inr h))) := by
  sorry

theorem destruct_length4_list_0 {x : List α} (h : x.length = 4) : x = [x[0], x[1], x[2], x[3] ] := by
  -- Not idiomatic -- why not call `ext`? See below...
  apply List.ext_get <;> simp_all [h, lt_succ_iff_lt_or_eq, Nat.not_lt_zero, or_forall]

theorem destruct_length4_list' {x : List α} (h : x.length = 4) : x = [x[0], x[1], x[2], x[3] ] := by
  -- `ext` leads to a formulation with `get?` which does not seem easy to handle automatically?
  -- If `List.get_ext` was the `ext`-rule for lists... then we would end up with this (?)
  apply List.ext_get
  · intros; assumption
  · intros i hi hi'
    -- Get `i < 4` by simplifying `h: List.length x = 4`
    -- QUESTION: Why do neither `simp_all` nor `simp [h] at *` do this?
    -- Doesn't work: simp [h] at *
    -- Doesn't work: simp_all
    simp [h] at hi
    -- QUESTION: Now we need to split `i < 4` into cases. `interval_cases` from mathlib does this, but how
    -- can this be done on the basis of core tactics? It seems like a common thing to do.
    -- QUESTION: Why _does_ `simp ... at *` work here, i.e. hi does not have to be named explicitly?
    simp [lt_succ_iff_lt_or_eq, Nat.not_lt_zero] at *
    -- QUESTION: `cases_type* Or` does the case splitting here, but this should be something
    -- the core lib should be able to do, ideally without having to name hypotheses explicitly?
    --
    -- Can be done with general-purpose `elim`, see below, but that does not exist.
    sorry

----------------------------- custom elim -----------------------------------------------------

/-- Try to close goal by assumption. Upon succes, return fvar id of
  matching assumption. Otherwise, return none. --/
def assumptionCore' (mvarId : MVarId) : MetaM (Option FVarId) :=
  mvarId.withContext do
    mvarId.checkNotAssigned `assumption
    match (← findLocalDeclWithType? (← mvarId.getType)) with
    | none => return none
    | some fvarId => mvarId.assign (mkFVar fvarId); return (some fvarId)

/-- Close goal `mvarId` using an assumption. Throw error message if failed. -/
def assumption' (mvarId : MVarId) : MetaM FVarId := do
  let res ← assumptionCore' mvarId
  match res with
  | none => throwTacticEx `assumption mvarId "assumption' tactic failed"
  | some fvarid => return fvarid

def erule (e : Expr) (mvid : MVarId) (with_intro : Bool := true) : MetaM (List MVarId) := do
  let s ← saveState
  try
    let mvids ← mvid.apply e
    match mvids with
    | [] => throwError "ill-formed elimination rule {e}"
    | main :: other =>
      -- Try to solve main goal by assumption, remember fvar of hypothesis
      let fvid ← assumption' main
      -- Remove hypothesis from all other goals
      let other' ← other.mapM (fun mvid => do
        if (← mvid.isAssignedOrDelayedAssigned) then
          return mvid
        let mvid ← mvid.clear fvid
        if with_intro then
          let (_, mvid) ← mvid.intros
          return mvid
        else
          return mvid
      )
      return other'
  catch _ =>
    restoreState s
    throwError "erule_tac failed"

-- Run erule repeatedly
def elim (e : Expr) (mvid : MVarId) : MetaM (List MVarId) := do
   Meta.repeat1' (erule e) [mvid]

elab "erule" e:term : tactic => do
   let e ← elabTermForApply e
   Elab.Tactic.liftMetaTactic (erule e)

elab "elim" e:term : tactic => do
   let e ← elabTermForApply e
   Elab.Tactic.liftMetaTactic (elim e)

--------------------------------- end custom elim -------------------------------------------------------

theorem destruct_length4_list'' {x : List α} (h : x.length = 4) : x = [x[0], x[1], x[2], x[3] ] := by
  -- `ext` leads to a formulation with get? which does not seem easy to handle automatically.
  -- Let's pretend `List.get_ext` was the `ext`-rule for lists... then we would end up with this:
  apply List.ext_get
  · intros; assumption
  · intros i hi hi'
    -- Get `i < 4` by simplifying `h: List.length x = 4`
    -- QUESTION: Why do neither `simp_all` nor `simp [h] at *` do this?
    -- Doesn't work: simp [h] at *
    -- Doesn't work: simp_all
    simp [h] at hi
    -- QUESTION: Now we need to split `i < 4` into cases. `interval_cases` from mathlib does this, but how
    -- can this be done on the basis of core tactics? It seems like a common thing to do.
    -- QUESTION: Why _does_ `simp ... at *` work here, i.e. hi does not have to be named explicitly?
    simp [lt_succ_iff_lt_or_eq, Nat.not_lt_zero] at *
    -- QUESTION: `cases_type* Or` does the case splitting here, but this should be something
    -- the core lib should be able to do, ideally without having to name hypotheses explicitly?
    --
    -- Can be done with general-purpose `elim`:
    elim Or.elim <;> simp_all
    done

[Markus Himmel]

This doesn't answer any of your questions, and you might already be aware of this, but just for completeness I should mention that the specific lemma you're trying to prove can be proved by pattern matching:

theorem destruct_length4_list'' : ∀ {x : List α} (h : x.length = 4), x = [x[0], x[1], x[2], x[3]]
  | [_, _, _, _], _ => rfl

[Hanno Becker]

@Markus Himmel No, I wasn't aware -- thank you very much, that's useful to know. Can one reformulate this so it is generic in the length, though?

[Markus Himmel]

I'm not sure, but since we're relying on the equation compiler to perform the case analysis here my guess would be that making that approach generic in the length will require metaprogramming of some kind.

[Eric Wieser]

I would guess you can copy the approach of docs#FinVec.etaExpand_eq

[Mario Carneiro]

It depends on how you want to state the variable length version, but one version of this theorem is docs#List.ofFn_get