The Coq mailing list

[Victor Porton <porton AT narod.ru>]

Much thanks, Carlos.

Your proof of my theorem [thm] is exactly what I need!

I am going to learn Ltac specifically to generalize your proof for arbitrary 
dependent records with arbitrary number of both "data fields" and 
"dependencies" (propositions). Well, as I now don't yet know Ltac, I am not 
sure whether it is possible with Ltac programming at all.

24.11.2011, 16:44, "Carlos Simpson" 
<Carlos.Simpson AT unice.fr>:
> Dear Victor,
> Here is a script which does the proof. I don't know how to do it
> in declarative language but that isn't important, you should listen when
> all of the people who reply tell you that the declarative language isn't 
> ready
> yet.
> Note, however, and we must insist on this fact, that you cannot prove
> the theorem you want if you don't assume the axiom ``proof_irrelevance''
> or something else that would be functionally equivalent in this situation
> (maybe just ``uniqueness of identity proofs''). There are interpretations
> of the language such that different proofs are different, in which case your
> two terms u and v can be different.
> ---Carlos
>
> 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.
>
> Axiom proof_irrelevance:
> forall (P:Prop), forall (p q:P), p=q.
>
> Theorem thm (u v : Foo) : (a u = a v -> u = v).
> intros.
> induction u.
> induction v.
> assert (a0 = a1).
> assumption.
> induction H0.
> (* that was a main step where eq_rect will
> be used, so that now b0 and b1 are in
> the same proposition, it was called trans
> above but it can be done with just this
> tactic here. *)
> assert (b0 = b1).
> apply proof_irrelevance.
> induction H0.
> reflexivity.
> Qed.

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