NyaOJ

提交信息

题目	#2. 列表前缀和列表连续段证明
提交者	jkjkmxmx
状态	Compile Error
分数	0
提交时间	2026/02/13 20:42:35

源代码

variable {A : Type}

theorem in_prefixes (l₁ l₂ : List A) : l₁ ∈ prefixes (l₁ ++ l₂) := by
  induction l₁ with
  | nil => unfold prefixes; grind
  | cons head tail h => simp [prefixes, h]

theorem in_prefixes_inv (l₁ l : List A) : l₁ ∈ prefixes l → ∃ l₂, l₁ ++ l₂ = l := by
  induction l generalizing l₁ with
  | nil =>
    intro h
    simp [prefixes] at h
    simp [h]
  | cons head tail h =>
    intro h'
    simp [prefixes] at h'
    cases h' with
    | inl e => simp [e]
    | inr l₂i =>
      have ⟨l₂, l₂p, hl₂⟩ := l₂i
      have ⟨l₃, l₂₃⟩ := h l₂ l₂p
      refine ⟨l₃, ?_⟩
      rw [← hl₂, ← l₂₃, List.cons_append]

theorem empty_sublists (l : List A) : [] ∈ sublists l := by
  induction l with
  | nil => simp [sublists]
  | cons head tail h => simp [sublists, h]

theorem in_sublists (l₁ l₂ l₃ : List A) : l₂ ∈ sublists (l₁ ++ l₂ ++ l₃) := by
  induction l₁ with
  | nil =>
    unfold sublists
    simp
    split
    · next h => simp at h; simp [h]
    next head tail l₂₃ =>
      simp
      cases l₂ with
      | nil => exact Or.inr (empty_sublists tail)
      | cons head' tail' =>
        simp at l₂₃
        left
        refine ⟨tail', ?_, ?_⟩
        · rw [← l₂₃.2]
          exact in_prefixes tail' l₃
        · rw [l₂₃.1]
  | cons head tail h =>
    simp at h
    simp [sublists, h]

theorem in_sublists_inv (l₂ l : List A) : l₂ ∈ sublists l → ∃ l₁ l₃, l₁ ++ l₂ ++ l₃ = l := by
  induction l with
  | nil => simp [sublists]
  | cons head tail h =>
    intro h'
    simp [sublists] at h'
    cases h' with
    | inl l₂p =>
      have ⟨l₃, l₃p, hl₂⟩ := l₂p
      have ⟨l₄, l₃₄⟩ := in_prefixes_inv l₃ tail l₃p
      refine ⟨[], l₄, ?_⟩
      rw [← hl₂]
      simp [l₃₄]
    | inr l₂t =>
      have ⟨l₁, l₃, l₁₂₃⟩ := h l₂t
      refine ⟨head :: l₁, l₃, ?_⟩
      rw [← l₁₂₃]
      simp

评测详情

compilecompile_problem

752 ms1089 MBOK

Built: problem

输出 (stdout / stderr)

[lean -o] /work/problem.lean:10:8: warning: declaration uses 'sorry'
/work/problem.lean:13:8: warning: declaration uses 'sorry'
/work/problem.lean:22:8: warning: declaration uses 'sorry'
/work/problem.lean:26:8: warning: declaration uses 'sorry'

[lean -c] /work/problem.lean:10:8: warning: declaration uses 'sorry'
/work/problem.lean:13:8: warning: declaration uses 'sorry'
/work/problem.lean:22:8: warning: declaration uses 'sorry'
/work/problem.lean:26:8: warning: declaration uses 'sorry'

compilecompile_usersol

108 ms338 MBFailed

Compile failed: UserSol

/work/UserSol.lean:3:44: error: Function expected at
  prefixes
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  (l₁ ++ l₂)
/work/UserSol.lean:5:18: error: Tactic `unfold` failed: Local variable `prefixes` has no definition
/work/UserSol.lean:6:30: error: Invalid argument: Variable `prefixes` is not a proposition or let-declaration
/work/UserSol.lean:6:21: error: unsolved goals
case cons
A : Type
x✝ : Sort u_1
prefixes : x✝
l₂ : List A
head : A
tail : List A
h : tail ∈ sorry
⊢ head :: tail ∈ sorry ()
/work/UserSol.lean:6:40: warning: This simp argument is unused:
  h

Hint: Omit it from the simp argument list.
  simp [prefixes,̵ ̵h̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
/work/UserSol.lean:8:47: error: Function expected at
  prefixes
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  l
/work/UserSol.lean:12:10: error: Invalid argument: Variable `prefixes` is not a proposition or let-declaration
/work/UserSol.lean:10:8: error: unsolved goals
case nil
A : Type
x✝ : Sort u_1
prefixes : x✝
l₁ : List A
h : l₁ ∈ sorry ()
⊢ l₁ = []
/work/UserSol.lean:16:10: error: Invalid argument: Variable `prefixes` is not a proposition or let-declaration
/work/UserSol.lean:13:10: warning: This simp argument is unused:
  h

Hint: Omit it from the simp argument list.
  simp ̵[̵h̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
/work/UserSol.lean:25:43: error: Function expected at
  sublists
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  l
/work/UserSol.lean:27:17: error: Invalid argument: Variable `sublists` is not a proposition or let-declaration
/work/UserSol.lean:27:8: error: unsolved goals
case nil
A : Type
x✝ : Sort u_1
sublists : x✝
⊢ [] ∈ sorry ()
/work/UserSol.lean:28:30: error: Invalid argument: Variable `sublists` is not a

输出 (stdout / stderr)

[lean -o] /work/UserSol.lean:3:44: error: Function expected at
  prefixes
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  (l₁ ++ l₂)
/work/UserSol.lean:5:18: error: Tactic `unfold` failed: Local variable `prefixes` has no definition
/work/UserSol.lean:6:30: error: Invalid argument: Variable `prefixes` is not a proposition or let-declaration
/work/UserSol.lean:6:21: error: unsolved goals
case cons
A : Type
x✝ : Sort u_1
prefixes : x✝
l₂ : List A
head : A
tail : List A
h : tail ∈ sorry
⊢ head :: tail ∈ sorry ()
/work/UserSol.lean:6:40: warning: This simp argument is unused:
  h

Hint: Omit it from the simp argument list.
  simp [prefixes,̵ ̵h̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
/work/UserSol.lean:8:47: error: Function expected at
  prefixes
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  l
/work/UserSol.lean:12:10: error: Invalid argument: Variable `prefixes` is not a proposition or let-declaration
/work/UserSol.lean:10:8: error: unsolved goals
case nil
A : Type
x✝ : Sort u_1
prefixes : x✝
l₁ : List A
h : l₁ ∈ sorry ()
⊢ l₁ = []
/work/UserSol.lean:16:10: error: Invalid argument: Variable `prefixes` is not a proposition or let-declaration
/work/UserSol.lean:13:10: warning: This simp argument is unused:
  h

Hint: Omit it from the simp argument list.
  simp ̵[̵h̵]̵

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
/work/UserSol.lean:25:43: error: Function expected at
  sublists
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  l
/work/UserSol.lean:27:17: error: Invalid argument: Variable `sublists` is not a proposition or let-declaration
/work/UserSol.lean:27:8: error: unsolved goals
case nil
A : Type
x✝ : Sort u_1
sublists : x✝
⊢ [] ∈ sorry ()
/work/UserSol.lean:28:30: error: Invalid argument: Variable `sublists` is not a proposition or let-declaration
/work/UserSol.lean:28:21: error: unsolved goals
case cons
A : Type
x✝ : Sort u_1
sublists : x✝
head : A
tail : List A
h : [] ∈ sorry
⊢ [] ∈ sorry ()
/work/UserSol.lean:28:40: warning: This simp argument is unused:
  h

Hint: Omit it from the simp argument list.
  simp [sublists,̵ ̵h̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
/work/UserSol.lean:30:47: error: Function expected at
  sublists
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  (l₁ ++ l₂ ++ l₃)
/work/UserSol.lean:33:11: error: Tactic `unfold` failed: Local variable `sublists` has no definition
/work/UserSol.lean:50:10: error: Invalid argument: Variable `sublists` is not a proposition or let-declaration
/work/UserSol.lean:48:21: error: unsolved goals
case cons
A : Type
x✝ : Sort u_1
sublists : x✝
l₂ l₃ : List A
head : A
tail : List A
h : l₂ ∈ sorry ()
⊢ l₂ ∈ sorry ()
/work/UserSol.lean:50:20: warning: This simp argument is unused:
  h

Hint: Omit it from the simp argument list.
  simp [sublists,̵ ̵h̵]

Note: This linter can be disabled with `set_option linter.unusedSimpArgs false`
/work/UserSol.lean:52:47: error: Function expected at
  sublists
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  l
/work/UserSol.lean:54:17: error: Invalid argument: Variable `sublists` is not a proposition or let-declaration
/work/UserSol.lean:54:8: error: unsolved goals
case nil
A : Type
x✝ : Sort u_1
sublists : x✝
l₂ : List A
⊢ l₂ ∈ sorry () → l₂ = []
/work/UserSol.lean:57:10: error: Invalid argument: Variable `sublists` is not a proposition or let-declaration

提交 #16