#1. 谓词与互归纳证明

来源：First Theorem Proving Competition3 AC / 7 提交 · 43%

题目描述

给定谓词 PP、QQ、RR，以及如下互归纳定义的谓词 AA、BB：

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

任务

(50 分) 试证明定理 neg_a。

lemma neg_a :
  (∀ n, ¬ P n ∧ ¬ Q n) →
  (∀ n1, ∃ n2, R n1 n2) →
  (∀ n, A P Q R n → False)

提示

根据 AA 或 BB 的互归纳原理证明。在 Lean4 中使用 A.rec, B.rec。

分值

  • neg_a 引理证明：50 分