在 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？

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

- hamid k

Answer 1

问题1

Coq打印“SA”，因为您将其声明为强制转换。您可以通过在文件中添加选项Set Printing Coercions.来防止这种情况发生。据我所知，没有办法只让Coq打印“SA”，而不打印其他强制转换，例如“SB”。但是，您可以将“:>”替换为“:”以防止将“SA”声明为强制转换。

问题2

您的引理需要在Coq的理论中假定额外的公理才能证明。问题在于您需要证明Z.abs_nat SB <> SA的两个证明相等，以便证明两个类型为Sample的记录相等，而Coq的理论中没有任何内容可以帮助您做到这一点。您有两个选项：

1. Use the axiom of proof irrelevance, which says forall (P : Prop) (p1 p2 : P), p1 = p2. For example:

   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.
   

   (Note the calls to revert: they are needed to prevent dependent type errors when rewriting with e1 and e2.)

2. Replace inequality with a proposition for which proof irrelevance is valid without extra axioms. A typical solution is to use a boolean version of the proposition. The DecidableEqDepSet module shows that the proofs of equality for a type that has decidable equality, such as the booleans, satisfies proof irrelevance.

   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.
   

- Arthur Azevedo De Amorim