coq - 在 coq 中记录相等

Question

例如我有这个示例记录:

Record Sample := {
  SA :> nat ; 
  SB :> Z ; 
  SCond : Z.abs_nat SB <> SA
}.

当我想证明这个引理时:

Lemma Sample_eq : forall a b : Sample , a = b <-> SA a = SA b /\ SB a = SB b.

我看到这个:

1 subgoal
______________________________________(1/1)
forall a b : Sample, a = b <-> a = b /\ a = b

问题 1:如何强制 Coq 显示 SA a 而不是 a？

问题2:如何证明这个引理？

Answer 1

问题一

Coq 打印 SA因为您将其声明为强制。您可以通过添加选项 Set Printing Coercions. 来防止这种情况发生。到你的文件。据我所知，没有办法只让 Coq 打印 SA但不是其他强制，例如 SB .但是，您可以替换 :>通过 :防止SA免于被宣布为胁迫。

问题2

如果不对 Coq 的理论假设额外的公理，就无法证明您的引理。问题是您需要证明 Z.abs_nat SB <> SA 的两个证明相等以显示 Sample 类型的两条记录是平等的，在 Coq 的理论中没有任何东西可以帮助你。你有两个选择:

使用证明无关公理，即 forall (P : Prop) (p1 p2 : P), p1 = p2 .例如:

Require Import Coq.ZArith.ZArith.
Require Import Coq.Logic.ProofIrrelevance.

Record Sample := {
  SA : nat;
  SB : Z;
  SCond : Z.abs_nat SB <> SA
}.

Lemma Sample_eq a b : SA a = SA b -> SB a = SB b -> a = b.
Proof.
  destruct a as [x1 y1 p1], b as [x2 y2 p2].
  simpl.
  intros e1 e2.
  revert p1 p2.
  rewrite <- e1, <- e2.
  intros p1 p2.
  now rewrite (proof_irrelevance _ p1 p2).
Qed.

(注意对 revert 的调用:使用 e1 和 e2 进行重写时需要它们来防止相关类型错误。)

用一个没有额外公理的证明无关性有效的命题代替不等式。一个典型的解决方案是使用命题的 bool 版本。 DecidableEqDepSet模块显示具有可判定相等性的类型(例如 bool 值)的相等性证明满足证明无关性。

Require Import Coq.ZArith.ZArith.
Require Import Coq.Logic.ProofIrrelevance.
Require Import Coq.Logic.Eqdep_dec.

Module BoolDecidableSet <: DecidableSet.

Definition U := bool.
Definition eq_dec := Bool.bool_dec.

End BoolDecidableSet.

Module BoolDecidableEqDepSet := DecidableEqDepSet BoolDecidableSet.

Record Sample := {
  SA : nat;
  SB : Z;
  SCond : Nat.eqb (Z.abs_nat SB) SA = false
}.

Lemma Sample_eq a b : SA a = SA b -> SB a = SB b -> a = b.
Proof.
  destruct a as [x1 y1 p1], b as [x2 y2 p2].
  simpl.
  intros e1 e2.
  revert p1 p2.
  rewrite <- e1, <- e2.
  intros p1 p2.
  now rewrite (BoolDecidableEqDepSet.UIP _ _ p1 p2).
Qed.