Can this be done more elegantly?

Stream: Is there code for X?

[Ching-Tsun Chou]

I have a proof whose essence is captured by the Lean code below. The theorem extend_lemma takes a list u and shows that it can be extended with certain properties. I use this theorem to construct an infinite sequence seq of lists which satisfies the properties in seq_lemma. Here's my question: Is there a more elegant way to define seq? Currently the definition uses Classical.choose and I find it not very pleasant to reason about anything defined using Classical.choose. (One has to get the unfolding just right in order to use the result produced by Classical.choose_spec. It took me 5~10 min to do just that in the example below.) Or is there a more advanced way to reason about something defined using Classical.choose that I don't know about?

import Mathlib

variable {α : Type*}

theorem extend_lemma (p q : List α → Prop) (u : List α) : ∃ v : List α, p v ∧ q (u ++ v) := sorry

private noncomputable def seq (p q : List α → Prop) (n : ℕ) : List α :=
  Classical.choose <| extend_lemma p q (List.ofFn (fun k : Fin n ↦ seq p q k)).flatten

theorem seq_lemma (p q : List α → Prop) (n : ℕ) :
    p (seq p q n) ∧ q (List.ofFn (fun k : Fin (n + 1) ↦ seq p q k)).flatten := by
  let r u v := p v ∧ q (u ++ v)
  have : r (List.ofFn (fun k : Fin n ↦ seq p q k)).flatten (seq p q n) := by
    rw [seq]
    exact Classical.choose_spec <| extend_lemma p q (List.ofFn (fun k : Fin n ↦ seq p q k)).flatten
  obtain ⟨h1, h2⟩ := this
  refine ⟨h1, ?_⟩
  rw [List.ofFn_succ_last]
  simpa

[Aaron Liu]

how about like this?

import Mathlib

variable {α : Type*}

theorem extend_lemma (p q : List α → Prop) (u : List α) : ∃ v : List α, p v ∧ q (u ++ v) := sorry

private noncomputable def seq (p q : List α → Prop) (n : ℕ) : List α :=
  Classical.choose <| extend_lemma p q (List.ofFn (fun k : Fin n ↦ seq p q k)).flatten

theorem seq_lemma (p q : List α → Prop) (n : ℕ) :
    p (seq p q n) ∧ q (List.ofFn (fun k : Fin (n + 1) ↦ seq p q k)).flatten := by
  simp_rw [List.ofFn_succ_last, List.flatten_append,
    List.flatten_singleton, Fin.val_last, Fin.coe_castSucc]
  rw [seq]
  generalize_proofs h
  exact h.choose_spec

[Jakub Nowak]

∃ v : List α, p v ∧ q (u ++ v) is basically a dependant triple. It's often easier to split this into three separate functions.

Smth like this:

import Mathlib

variable {α : Type*}

noncomputable def extend (p q : List α → Prop) (u : List α) : List α := sorry

theorem extend_lemma_p (p q : List α → Prop) (u : List α) : p (extend p q u) := sorry

theorem extend_lemma_q (p q : List α → Prop) (u : List α) : q (u ++ extend p q u) := sorry

private noncomputable def seq (p q : List α → Prop) (n : ℕ) : List α :=
  extend p q (List.ofFn (fun k : Fin n ↦ seq p q k)).flatten

theorem seq_lemma_p (p q : List α → Prop) (n : ℕ) : p (seq p q n) := by
  unfold seq
  apply extend_lemma_p

theorem seq_lemma_q (p q : List α → Prop) (n : ℕ) :
    q (List.ofFn (fun k : Fin (n + 1) ↦ seq p q k)).flatten := by
  rw [List.ofFn_succ_last]
  simp
  unfold seq
  apply extend_lemma_q p q

[Jakub Nowak]

Although, splitting is not necessary to avoid Classical.choose:

import Mathlib

variable {α : Type*}

noncomputable def extend (p q : List α → Prop) (u : List α) : { v : List α // p v ∧ q (u ++ v) } := sorry

private noncomputable def seq (p q : List α → Prop) (n : ℕ) : List α :=
  extend p q (List.ofFn (fun k : Fin n ↦ seq p q k)).flatten

theorem seq_lemma (p q : List α → Prop) (n : ℕ) :
    p (seq p q n) ∧ q (List.ofFn (fun k : Fin (n + 1) ↦ seq p q k)).flatten := by
  let r u v := p v ∧ q (u ++ v)
  have : r (List.ofFn (fun k : Fin n ↦ seq p q k)).flatten (seq p q n) := by
    rw [seq]
    exact (extend p q (List.ofFn (fun k : Fin n ↦ seq p q k)).flatten).prop
  obtain ⟨h1, h2⟩ := this
  refine ⟨h1, ?_⟩
  rw [List.ofFn_succ_last]
  simpa

Though, it's essentially the same, now you have to use Subtype.prop instead of Classical.choose_spec.

[Ching-Tsun Chou]

Thanks for the suggestions! After reading them and thinking more, I end up with the following code. The idea is to apply Classical.choose to extend_lemma first, so that Classical.choose_spec is very easy to use. Also, the reasoning about List and Fin is now concentrated in a single flatten_lemma, so that we are not distracted by them in the proof of seq_lemma'.

import Mathlib

variable {α : Type*}

theorem extend_lemma (p q : List α → Prop) (u : List α) : ∃ v : List α, p v ∧ q (u ++ v) := sorry

noncomputable def step (p q : List α → Prop) (u : List α) : List α :=
  Classical.choose <| extend_lemma p q u

theorem step_lemma (p q : List α → Prop) (u : List α) :
    p (step p q u) ∧ q (u ++ step p q u) :=
  Classical.choose_spec <| extend_lemma p q u

lemma flatten_lemma {f : ℕ → List α} {n : ℕ} :
    (List.ofFn fun (k : Fin (n + 1)) ↦ f ↑k).flatten =
    (List.ofFn fun (k : Fin n) ↦ f ↑k).flatten ++ f n := by
  rw [List.ofFn_succ_last]
  simp

noncomputable def seq' (p q : List α → Prop) (n : ℕ) : List α :=
  step p q (List.ofFn (fun k : Fin n ↦ seq' p q k)).flatten

theorem seq_lemma' (p q : List α → Prop) (n : ℕ) :
    p (seq' p q n) ∧ q (List.ofFn (fun k : Fin (n + 1) ↦ seq' p q k)).flatten := by
  obtain ⟨h1, h2⟩ := step_lemma p q (List.ofFn (fun k : Fin n ↦ seq' p q k)).flatten
  constructor
  · rw [seq']
    exact h1
  · rw [flatten_lemma, seq']
    exact h2