The Coq mailing list

[Victor Porton <porton AT narod.ru>]

I am stepping Andrej Bauer's code in Proof General trying to grasp the idea 
but I haven't yet succeed to understand. Maybe somebody may hint me what is 
the main idea of that code?

What concerns Daniel Schepler's code:

It mentions [eq_rect]. I found a link to [eq_rect] at [Implicit Arguments 
eq_rect [A]] at http://coq.inria.fr/stdlib/Coq.Init.Logic.html#eq_rect but ;
that link is apparently broken.

So I fail to understand what eq_rect means. Could you explain?

20.11.2011, 19:13, "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

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