主页 / coding / 问题 / 79261145
Accepted
nnarek
Asked: 2024-12-08 02:28:16 +0800 CST

如何在 Coq 中使用策略来证明关于互归纳类型的定理？

  • 772

考虑以下相互归纳命题

Inductive TypeA : Prop :=
  | ConstructorA : TypeB -> TypeA
with TypeB : Prop :=
  | ConstructorB : TypeA -> TypeB.

以下是~TypeA函数式风格的证明

Fixpoint TypeA_is_empty' (a : TypeA) : False :=
  match a with 
  | ConstructorA b' => TypeB_is_empty' b'
  end
with TypeB_is_empty' (b : TypeB) : False :=
  match b with 
  | ConstructorB a' => TypeA_is_empty' a'
  end.

战术风格上如何证明~TypeA？

如果 Coq 中存在类似的东西，我希望能够将它们证明为相互定理

Theorem TypeA_is_empty : ~ TypeA.
Theorem TypeB_is_empty : ~ TypeB.
Proof.
  unfold not.
  intros b.
  inversion b as [a].
  apply (TypeA_is_empty a).
Qed.
Proof.
  unfold not.
  intros a.
  inversion a as [b].
  apply (TypeB_is_empty b).
Qed.

编辑：发现 Coq 有这样的相互定理语法，但它会抛出错误

Lemma TypeA_is_empty : ~ TypeA 
  with TypeB_is_empty : ~ TypeB.

**Cannot find common (mutual) inductive premises or coinductive conclusions in the statements.**
coq

2 个回答

  1. Best Answer

    （为了方便起见，我已更改了名字。）

    首先，您不能not在语句中使用，这个语句可以编译：

    Lemma A_is_empty : A -> False
  with B_is_empty : B -> False.

    也就是说，这段代码似乎可以做到这一点。请参阅注释以获取解释：

    Inductive A : Prop :=
  | mkA : B -> A
with B : Prop :=
  | mkB : A -> B.

Fixpoint A_is_empty' (a : A) : False :=
  match a with
  | mkA b => B_is_empty' b
  end
with B_is_empty' (b : B) : False :=
  match b with
  | mkB a => A_is_empty' a
  end.

Lemma A_is_empty : A -> False
  with B_is_empty : B -> False.
Proof.
  - intros a.
    apply A_is_empty.
    exact a.
  - intros b.
    apply B_is_empty.
    exact b.
Fail Qed. (* Recursive call to A_is_empty
  has principal argument equal to
  "a" instead of a subterm of "a". *)
Abort.

Lemma A_is_empty : A -> False
  with B_is_empty : B -> False.
Proof.
  - intros a.
    destruct a as [b].  (* !! *)
    apply B_is_empty.
    exact b.
  - intros b.
    destruct b as [a].  (* !! *)
    apply A_is_empty.
    exact a.
Qed.

Check A_is_empty : ~ A.
Check B_is_empty : ~ B.
    • 1 
  2. Fixpoint TypeA_is_empty (a:TypeA) : False.
  enough (forall (b:TypeB), False) as TypeB_is_empty.
  destruct a as [b]. apply (TypeB_is_empty b). 
  intros b. destruct b as [a']. apply (TypeA_is_empty a').
Defined.

    使用Fixpoint而不是Lemma因为你需要TypeA_is_empty里面的证明。

    • 0

相关问题