The Coq mailing list

[Victor Porton <porton AT narod.ru>]

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