The Coq mailing list

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

Adam Chlipala a écrit :
> M. Scott Doerrie wrote:
> > You are correct that I've been assuming FSetLists as my structure.  I 
> > had not considered the AVL structure, for which this wouldn't hold.
> > I do not understand where proof-irrelevance would enter for 
> > FSetLists.  I had thought that with identical representations, the 
> > proofs of sorting would also be identical.  What did I miss here?
>
> A proof of sortedness can involve arbitrary mathematical machinery.  
> What is it that makes you think that any two such proofs can be shown 
> equal in Coq?  This would require showing that, modulo the definitional 
> equality, the proofs have the same syntax.  There can be many proofs of 
> the same proposition that use very different proof strategies and so 
> have very different syntax.

[Georges has already proposed a solution. Let me just give a more 
concrete way of proceeding, given the current state of Coq's standard 
library. Here we do need to explicitely exhibit a characteristic 
function of your set.]

Sortedness can be defined in a way that you have only one proof for a 
given list. Take Coq.Sorting.Sorting.sort.
Then, using heavy dependently typed machinery (Eqdep_dec, and equality 
on lists is decidable since equality of its members is), you can prove 
that if your inequality proofs are irrelevent, then so are proofs of 
sortedness:

(forall x y (p1 p2: leA x y), p1=p2) ->
forall l (p1 p2:sort leA l l), p1=p2

We don't even need irrelevence of inequality proofs, since the total 
ordering property lets you "normalize" even further your proofs.
If you change the definition of lelistA from (UOT being your 
UsualOrderedType structure)

 Inductive lelistA (a:A) : list A -> Prop :=
    | nil_leA : lelistA a nil
    | cons_leA :
       forall (b:A) (l:list A), UOT.lt a b -> lelistA a (b :: l).

to

 Inductive lelistA (a:A) : list A -> Prop :=
    | nil_leA : lelistA a nil
    | cons_leA : forall (b:A) (l:list A) (p:UOT.lt a b),
        UOT.Compare a b = LT p -> lelistA a (b :: l).

Then irrelevance should be derivable.

Bruno Barras.