NyaOJ

提交信息

题目	#1. 谓词与互归纳证明
提交者	jkjkmxmx
状态	Compile Error
分数	0
提交时间	2026/02/13 20:18:56

源代码

mutual
inductive A : Nat → Prop
| ca0 : ∀ n, P n → A n
| ca1 : ∀ n1, (∀ n2, R n1 n2 → B n2) → A n1

inductive B : Nat → Prop
| cb0 : ∀ n, Q n → B n
| cb1 : ∀ n1 n2, R n1 n2 → A n2 → B n1
end

theorem neg_a : (∀ n, ¬P n ∧ ¬Q n) → (∀ n₁, ∃ n₂, R n₁ n₂) → (∀ n, A P Q R n → False) := by
  intro h₁ h₂ n a
  refine @A.rec P Q R (λ _ _ ↦ False) (λ _ _ ↦ False) ?_ ?_ ?_ ?_ n a <;> simp [h₁]
  exact λ n _ ↦ h₂ n

评测详情

compilecompile_problem

704 ms1087 MBOK

Built: problem

输出 (stdout / stderr)

[lean -o] /work/problem.lean:22:6: warning: declaration uses 'sorry'

[lean -c] /work/problem.lean:22:6: warning: declaration uses 'sorry'

compilecompile_usersol

72 ms318 MBFailed

Compile failed: UserSol

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

Note: Expected a function because this term is being applied to the argument
  n
/work/UserSol.lean:4:21: error: Function expected at
  R
but this term has type
  ?m.7

Note: Expected a function because this term is being applied to the argument
  n1
/work/UserSol.lean:7:13: error: Function expected at
  Q
but this term has type
  ?m.15

Note: Expected a function because this term is being applied to the argument
  n
/work/UserSol.lean:8:17: error: Function expected at
  R
but this term has type
  ?m.21

Note: Expected a function because this term is being applied to the argument
  n1
/work/UserSol.lean:2:0: error: (kernel) declaration has metavariables 'A.ca0'
/work/UserSol.lean:11:23: error: Function expected at
  P
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  n
/work/UserSol.lean:11:30: error: Function expected at
  Q
but this term has type
  ?m.2

Note: Expected a function because this term is being applied to the argument
  n
/work/UserSol.lean:11:50: error: Function expected at
  R
but this term has type
  ?m.3

Note: Expected a function because this term is being applied to the argument
  n₁
/work/UserSol.lean:14:2: error: No goals to be solved

输出 (stdout / stderr)

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

Note: Expected a function because this term is being applied to the argument
  n
/work/UserSol.lean:4:21: error: Function expected at
  R
but this term has type
  ?m.7

Note: Expected a function because this term is being applied to the argument
  n1
/work/UserSol.lean:7:13: error: Function expected at
  Q
but this term has type
  ?m.15

Note: Expected a function because this term is being applied to the argument
  n
/work/UserSol.lean:8:17: error: Function expected at
  R
but this term has type
  ?m.21

Note: Expected a function because this term is being applied to the argument
  n1
/work/UserSol.lean:2:0: error: (kernel) declaration has metavariables 'A.ca0'
/work/UserSol.lean:11:23: error: Function expected at
  P
but this term has type
  ?m.1

Note: Expected a function because this term is being applied to the argument
  n
/work/UserSol.lean:11:30: error: Function expected at
  Q
but this term has type
  ?m.2

Note: Expected a function because this term is being applied to the argument
  n
/work/UserSol.lean:11:50: error: Function expected at
  R
but this term has type
  ?m.3

Note: Expected a function because this term is being applied to the argument
  n₁
/work/UserSol.lean:14:2: error: No goals to be solved

提交 #14