在 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

问题 1

Coq 打印SA是因为您将其声明为强制转换。您可以通过将选项添加Set Printing Coercions.到您的文件来防止这种情况发生。据我所知，也没有只使勒柯克打印的方式只 SA而不是其他的强制如SB。但是，您可以替换:>by:以防止SA被声明为强制。

问题2

如果不对 Coq 的理论假设额外的公理，就无法证明您的引理。问题是你需要证明 的两个证明Z.abs_nat SB <> SA是相等的，才能证明两个类型的记录Sample是相等的，而 Coq 的理论中没有任何内容可以帮助你解决这个问题。您有两个选择：

1. 使用证明无关公理，即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。）

2. 将不等式替换为在没有额外公理的情况下证明无关性有效的命题。典型的解决方案是使用命题的布尔版本。该DecidableEqDepSet模块显示具有可判定相等性的类型（例如布尔值）的相等性证明满足证明无关性。

   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.