Record equality in Coq

Link:: https://stackoverflow.com/q/50924127

Display all goals and responses

Question

For example I have this sample record:

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

When I want to proof this Lemma:

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

I see this:

1 subgoal

  ============================
  forall a b : Sample, a = b <-> a = b /\ a = b

Question 1: How to force Coq to show SA a instead of a?

Question 2: How to proof this Lemma?

Answer

Question 1

Coq prints SA because you declared it as a coercion. You can prevent this by adding the option Set Printing Coercions. to your file. As far as I know, there is no way of just making Coq print only SA but not other coercions such as SB. You can, however, replace the :> by : to prevent SA from being declared as a coercion.

Question 2

Your lemma cannot be proved without assuming extra axioms into Coq's theory. The problem is that you need to show that two proofs of Z.abs_nat SB <> SA are equal in order to show that two records of type Sample are equal, and there is nothing in Coq's theory that can help you with that. You have two options:

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.a, b: Sample
SA a = SA b -> SB a = SB b -> a = b
Proof.a, b: Sample
SA a = SA b -> SB a = SB b -> a = b
  destruct a as [x1 y1 p1], b as [x2 y2 p2].x1: nat
y1: Z
p1: Z.abs_nat y1 <> x1
x2: nat
y2: Z
p2: Z.abs_nat y2 <> x2
SA {| SA := x1; SB := y1; SCond := p1 |} =
SA {| SA := x2; SB := y2; SCond := p2 |} ->
SB {| SA := x1; SB := y1; SCond := p1 |} =
SB {| SA := x2; SB := y2; SCond := p2 |} ->
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x2; SB := y2; SCond := p2 |} simpl.x1: nat
y1: Z
p1: Z.abs_nat y1 <> x1
x2: nat
y2: Z
p2: Z.abs_nat y2 <> x2
x1 = x2 ->
y1 = y2 ->
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x2; SB := y2; SCond := p2 |}
  intros e1 e2.x1: nat
y1: Z
p1: Z.abs_nat y1 <> x1
x2: nat
y2: Z
p2: Z.abs_nat y2 <> x2
e1: x1 = x2
e2: y1 = y2
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x2; SB := y2; SCond := p2 |} revert p1 p2.x1: nat
y1: Z
x2: nat
y2: Z
e1: x1 = x2
e2: y1 = y2
forall (p1 : Z.abs_nat y1 <> x1)
  (p2 : Z.abs_nat y2 <> x2),
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x2; SB := y2; SCond := p2 |}
  rewrite <- e1, <- e2.x1: nat
y1: Z
x2: nat
y2: Z
e1: x1 = x2
e2: y1 = y2
forall p1 p2 : Z.abs_nat y1 <> x1,
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x1; SB := y1; SCond := p2 |} intros p1 p2.x1: nat
y1: Z
x2: nat
y2: Z
e1: x1 = x2
e2: y1 = y2
p1, p2: Z.abs_nat y1 <> x1
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x1; SB := y1; SCond := 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.)

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.a, b: Sample
SA a = SA b -> SB a = SB b -> a = b
Proof.a, b: Sample
SA a = SA b -> SB a = SB b -> a = b
  destruct a as [x1 y1 p1], b as [x2 y2 p2].x1: nat
y1: Z
p1: (Z.abs_nat y1 =? x1) = false
x2: nat
y2: Z
p2: (Z.abs_nat y2 =? x2) = false
SA {| SA := x1; SB := y1; SCond := p1 |} =
SA {| SA := x2; SB := y2; SCond := p2 |} ->
SB {| SA := x1; SB := y1; SCond := p1 |} =
SB {| SA := x2; SB := y2; SCond := p2 |} ->
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x2; SB := y2; SCond := p2 |} simpl.x1: nat
y1: Z
p1: (Z.abs_nat y1 =? x1) = false
x2: nat
y2: Z
p2: (Z.abs_nat y2 =? x2) = false
x1 = x2 ->
y1 = y2 ->
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x2; SB := y2; SCond := p2 |}
  intros e1 e2.x1: nat
y1: Z
p1: (Z.abs_nat y1 =? x1) = false
x2: nat
y2: Z
p2: (Z.abs_nat y2 =? x2) = false
e1: x1 = x2
e2: y1 = y2
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x2; SB := y2; SCond := p2 |} revert p1 p2.x1: nat
y1: Z
x2: nat
y2: Z
e1: x1 = x2
e2: y1 = y2
forall (p1 : (Z.abs_nat y1 =? x1) = false)
  (p2 : (Z.abs_nat y2 =? x2) = false),
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x2; SB := y2; SCond := p2 |}
  rewrite <- e1, <- e2.x1: nat
y1: Z
x2: nat
y2: Z
e1: x1 = x2
e2: y1 = y2
forall p1 p2 : (Z.abs_nat y1 =? x1) = false,
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x1; SB := y1; SCond := p2 |} intros p1 p2.x1: nat
y1: Z
x2: nat
y2: Z
e1: x1 = x2
e2: y1 = y2
p1, p2: (Z.abs_nat y1 =? x1) = false
{| SA := x1; SB := y1; SCond := p1 |} =
{| SA := x1; SB := y1; SCond := p2 |}
  now rewrite (BoolDecidableEqDepSet.UIP _ _ p1 p2).
Qed.