The Coq mailing list

[Victor Porton <porton AT narod.ru>]

One more novice question:

Can we prove the following theorem as a consequence of equal_foo?

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

22.11.2011, 23:11, "Victor Porton" 
<porton AT narod.ru>:
> 20.11.2011, 18:07, "Andrej Bauer" 
>Â <andrej.bauer AT andrej.com>:
>
>> š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.)
>
> I don't say that Coq design decisions are bad. I understand that Coq is 
> built on a set of highly orthogonal principles. Following orthogonal 
> principles is good.
>
> But excuse me to ask one more dumb question with suspicion that in the 
> current version of Coq there are some deficiency. If I don't ask, I can't 
> be 100% sure.
>
> Dear Andrej Bauer, I've read your code (below) and I somehow understand 
> (honestly not 100%) its idea. I am going to put it into real use.
>
> But the question arises: Should I repeat it every time I introduces a 
> dependent structure?
>
> Can it be put into a coherent way for every dependent record I declare, 
> allowing to not repeat the same proof each time?
>
> I don't thing anything is wrong, just I am confused with this question/
>
>> šWhat version of Coq are you using?
>
> 8.3pl2
>
>> š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.:
>
> I repeat (a little modified for simplicity) code by Andrej Bauer:
>
> [[[[
> Parameter A : Set.
> Parameter B : A -> Prop.
>
> 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.
>
> (*Print tran.*)
>
> 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.
> --
> Victor Porton - http://portonvictor.org

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