The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Olivier, it is great. My experimentation shows that it works even with records with more than one data field and more than one condition.

 

Based on the Olivier's work I've written a short theory which I recommend to add to Coq core (whether you'd call me a troll for this suggestion to add features or not).

 

[[[[

(* DependentRecordEq.v *)

Require Import Logic.ProofIrrelevance.
(*Axiom proof_irrelevance: forall (P:Prop), forall (p q:P), p=q.*)

Ltac dep_rec_eq u v := intros ; destruct u ; destruct v ; simpl in * ; subst ; f_equal ; apply proof_irrelevance.
]]]]

 

Here is the experiment which shows that this work great:

 

[[[[

(* Test of DependentRecordEq *)
Require Import DependentRecordEq.

Parameter A0 A1 : Set.
Parameter B0 : A0 -> Prop.
Parameter B1 : A1 -> Prop.

Structure Foo := mkFoo { a0 : A0; a1: A1; b0 : B0 a0 ; b1 : B1 a1 }.

Theorem thm1 (u v : Foo) : (a0 u = a0 v -> a1 u = a1 v -> u = v).
Proof.
  dep_rec_eq u v.
Qed.
]]]]

 

18.12.2012, 21:49, "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

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