aux — Mathlib

English

If a computation c is an element of a finite list of computations, and c terminates, then the corecursive construction corec parallel.aux1(l,S) terminates.

Русский

Если вычисление c является элементом конечного списка вычислений и прекращает работу, то ядро-циклическая конструкция corec parallel.aux1(l,S) завершается.

LaTeX

$$$ \text{If } l \text{ is a finite list } c \in l \text{ and } c\ \text{terminates},\ \\text{then } \ \mathrm{Terminates}(\mathrm{corec}(\mathrm{parallel.aux1})(l,S)).$$$

Lean4

theorem aux : ∀ {l : List (Computation α)} {S c}, c ∈ l → Terminates c → Terminates (corec parallel.aux1 (l, S)) :=
  by
  have lem1 : ∀ l S, (∃ a : α, parallel.aux2 l = Sum.inl a) → Terminates (corec parallel.aux1 (l, S)) :=
    by
    intro l S e
    obtain ⟨a, e⟩ := e
    have : corec parallel.aux1 (l, S) = return a :=
      by
      apply destruct_eq_pure
      simp only [parallel.aux1, rmap, corec_eq]
      rw [e]
    rw [this]
    exact ret_terminates a
  intro l S c m T
  revert l S
  apply @terminatesRecOn _ _ c T _ _
  · intro a l S m
    apply lem1
    induction l with
    | nil => simp at m
    | cons c l IH => ?_
    simp only [List.mem_cons] at m
    rcases m with e | m
    · rw [← e]
      simp only [parallel.aux2, rmap, List.foldr_cons, destruct_pure]
      split <;> simp
    · obtain ⟨a', e⟩ := IH m
      simp only [parallel.aux2, rmap, List.foldr_cons] at ⊢ e
      rw [e]
      exact ⟨a', rfl⟩
  · intro s IH l S m
    have H1 (l') (e' : parallel.aux2 l = Sum.inr l') : s ∈ l' :=
      by
      induction l generalizing l' with
      | nil => simp at m
      | cons c l IH' => ?_
      simp only [List.mem_cons] at m
      rcases m with e | m <;> simp only [parallel.aux2, rmap, List.foldr_cons] at e'
      · rw [← e] at e'
        revert e'
        split
        · simp
        · simp only [destruct_think, Sum.inr.injEq]
          rintro rfl
          simp
      · rcases e :
            List.foldr
              (fun c o =>
                match o with
                | Sum.inl a => Sum.inl a
                | Sum.inr ls => rmap (fun c' => c' :: ls) (destruct c))
              (Sum.inr List.nil) l with
            a' | ls <;> erw [e] at e'
        · contradiction
        have := IH' m _ e
        revert e'
        cases destruct c <;> intro e' <;> [injection e'; injection e' with h']
        rw [← h']
        simp [this]
    rcases h : parallel.aux2 l with a | l'
    · exact lem1 _ _ ⟨a, h⟩
    · have H2 : corec parallel.aux1 (l, S) = think _ :=
        destruct_eq_think
          (by
            simp only [parallel.aux1, rmap, corec_eq]
            rw [h])
      rw [H2]
      refine @Computation.think_terminates _ _ ?_
      have := H1 _ h
      rcases Seq.destruct S with (_ | ⟨_ | c, S'⟩) <;> apply IH <;> simp [this]

Похожие утверждения