The Coq mailing list

[Bruno Barras <bruno.barras AT inria.fr>]

Akuma GnacGnac wrote:

> Hi Li-Yang,
>
> I'm not sure I pointed out the problem but it seems this lemma can 
> easily be proven via the f_equal function of type (forall (A B : Type) 
> (f : A -> B) (x y : A), x = y -> f x = f y) when applied with the 
> following instance of f :
> fun (A : Set) (P : A -> Set) (e : sigS P) :=
>  match e with
> | existS _ p => p end.
Unfortunately no. f_equal applies only to non-dependent functional types 
(A->B). Your function f can be defined but has type forall (e:sigS P), P 
(projS1 e), which is dependent. The generalization of f_equal to 
dependent function types is ill-typed (since f x and f y do not have 
*convertable* types).
Lemma projS2_eq is indeed independent in Coq's theory. However it is 
widely accepted as consistent. Standard library Eqdep contains an axiom 
equivalent to Streicher's K axiom, and several corollaries, such as the 
2nd projection of dependent pairs.

But, going back to Li-Yang's problem, this axiom is not necessary since 
the domain of the first component (binary trees merely) has a decidable 
equality. In this case equality on 2nd projections holds. See Eqdep_dec 
for a proof.

Hope this helps,
Bruno Barras.