The Coq mailing list

[Olivier Uanelineur <o.uanelineur AT gmail.com>]

Hi Victor,

May I suggest this one-liner?

=================================================================

Require Import Logic.ProofIrrelevance.

Parameter A : Set.

Parameter B : A -> Prop.

Structure Foo := mkFoo { a : A; b : B a }.

Theorem thm (u v : Foo) : (a u = a v -> u = v).

Proof.

intros ; destruct u ; destruct v ; simpl in * ; subst ; f_equal ; apply proof_irrelevance.

Qed.

=================================================================

Good luck with your work,

--

Olivier

On Tue, Dec 18, 2012 at 5:35 PM, Victor Porton <porton AT narod.ru> wrote:

Even despite I was labeled a "troll" by some members of this mailing list, I wish to remind you my proposal for an enhancement for a future version of Coq.

I want one-line tactic scripts to prove that two objects of a dependent record type are equal if all their data fields are equal.

Currently it is done in a very long way presented below (both is Gallina and plain tactic scripts). And math is about making formulas shorter. Please to effective math.

In the past I have started to formalize order/lattice theory in Coq but has given up after realized that equality of two records is so difficult to prove.

Please hear my opinion even despite of I am a little troll: Someone should be assigned to do this work.

====

Require Import Logic.ProofIrrelevance.

Parameter A : Set.
Parameter B : A -> Prop.

Structure Foo := mkFoo { a : A; b : B a }.

(*Axiom proof_irrelevance: forall (P:Prop), forall (p q:P), p=q.*)

Theorem thm (u v : Foo) : (a u = a v -> u = v).
proof.
  consider x0 such that y0:(B x0) from u.
  consider x1 such that y1:(B x1) from v.
  assume e:(x0=x1).
  claim (forall y:B x1,  mkFoo x0 y0 = mkFoo x1 y). (* generalize *)
  per cases on e.
    suppose it is (refl_equal). (* dependent elim *)
    let y':(B x0).
    thus thesis by (proof_irrelevance _ y0 y'). (* automation sometimes needs help *)
  end cases.
  end claim.
  hence thesis.
end proof.
Qed.

Theorem thm2 (u v : Foo) : (a u = a v -> u = v).
Proof.
  intros.
  destruct u as [a0 b0].
  destruct v as [a1 b1].
  assert (a0 = a1).
  assumption.
  destruct H0. (* It does the magic. *)
  assert (b0 = b1).
  apply proof_irrelevance.
  destruct H0.
  reflexivity.
Qed.

--
Victor Porton - http://portonvictor.org