The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Sunday, November 20, 2011 06:07:10 AM Andrej Bauer wrote:
> Dear Victor,
> 
> I have sent you a message like this one privately, but it did not
> work, so I am going to say this publicly.
> 
> You are flooding the list with trivialities. In addition, your
> messages are arrogant because you keep saying things like "Coq can't
> compare dependent records" where in reality the source of trouble is
> (in most cases) your ignorance. There is nothing wrong with being
> ignorant, and we're happy to help, but not if you keep implying that
> everyone on this list, the designers of Coq included, are so dumb that
> they can't even get the basic things right and that the design
> decisions made in Coq are obviously bad. (This _is_ what you are
> implying, even if you are not aware of it.)
> 
> There is another source of help for beginners which might work better
> for you, namely the IRC #coq channel irc://irc.freenode.net/#coq where
> you can get help immediately.
> 
> Now, regarding comparison of dependent records:
> >Theorem ax2: @v A = @v B.
> >Proof.
> >
> > auto.
> >
> >Qed.
> 
> Here I get:
> 
>    The term "@v B" has type "@x B = 0" while it is expected to have
> type  "@x A = 0".
> 
> What version of Coq are you using?
> 
> Anyhow, you can of course compare dependent records, but you must
> transport the dependent component of one record along the proof of
> equality so that things typecheck, i.e.:
> 
> -----
> Parameter A : Type.
> Parameter B : A -> Type.
> 
> Structure Foo := mkFoo { a : A; b : B a }.
> 
> Definition tran {u v : Foo} (p : a u = a v) : B (a u) -> B (a v).
> Proof.
>   induction p.
>   auto.
> Defined.
> 
> Lemma equal_foo (u v : Foo) (p : a u = a v) : tran p (b u) = b v -> u = v.
> Proof.
>   intro H.
>   destruct u as [x y].
>   destruct v as [s t].
>   simpl in * |- *.
>   destruct p.
>   simpl in H.
>   rewrite H.
>   reflexivity.
> Qed.
> ------
> 
> Lemma equal_foo says that the dependent records u and v are equal,
> provided that their first components are equal, and the second
> component of u is equal to the second component of v, after we have
> converted it from type B (a u) to type B (a v) via the proof p of
> equality a u = a v.

Here's a way to express things like this that I've been playing around with:

Require Import Program.

Notation "x ## a := b" :=
  (eq_rect a _ x b _) (at level 50).

Inductive dep_and (P:Prop) (Q:P->Prop) : Prop :=
| dep_conj: forall p:P, Q p -> dep_and P Q.

Notation "P &&& Q" := (dep_and P (fun _ => Q))
  (right associativity, at level 80).

Record A := {
  x : nat;
  q : x = 0
}.

Require Import ProofIrrelevance.

Program Lemma A_uniqueness: forall X Y:A,
  x X = x Y &&& q X = q Y.
Proof.
intros.
destruct X, Y; simpl.
assert (x0 = x1) by congruence.
apply dep_conj with (p:=H).
destruct H; simpl.
apply proof_irrelevance.
Qed.

Lemma A_uniqueness_2: forall X Y:A,
  X = Y.
Proof.
destruct X, Y.
subst.
reflexivity.
Qed.

Program Lemma dep_pair_eq: forall B (P:B->Type)
  (x y:sigT P),
  x = y <-> projT1 x = projT1 y &&&
            projT2 x = projT2 y.
Proof.
split; intros.
destruct H.
apply dep_conj with (p:=eq_refl).
apply eq_rect_eq.

destruct x0 as [b1 p1], y as [b2 p2].
simpl in H.
destruct H.
destruct p.
rewrite <- eq_rect_eq in H.
destruct H.
reflexivity.
Qed.

So "P &&& Q" represents a sort of "short circuit and", where for Program to 
even make sense of Q it has to assume P.  In this case, it used the 
hypothesis 
"x X = x Y" to generate a correct conversion to make sense of "q X = q Y".
-- 
Daniel Schepler