The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

Filou Vincent wrote:
> Hi all,
>
> I  was wondering if there was any way to prove the lemma stated at the 
> end of this mail.
> I suppose the fact that FMaps implementations carry proofs prevents it.
> I have proven a weaker version with an equivalence relation, but I'd 
> rather use the coq equality version.
> Would adding a proof irrelevance axiom in the FMapList module solve 
> the problem?
> (if so, has anybody implemented such a solution?)
> What would be the consequences of the adjonction of this axiom?
> In other words, would I "break something" by adding it?
>
> Thanks
>
> Vincent Filou
>
> ...
Questions of proof irrelevance can sometimes be simplified if you state 
your logical property in the right way.  In particular, proofs of 
decidable properties should not pose any problem with respect to proof 
irrelevance.

For instance, there is a result initially due to Hedberg,  " Showing 
uniqueness of identity proofs on a set with decidable identities"[1].  
This result was obtained in Alf, which implemented Martin-Löf's type 
theory, but this is just a fragment of what you can do in Coq, so that 
the result also holds for us. Here is a short example, in the case of 
the bool type.
--- start Coq code here

Definition nu (x y:bool) : x = y -> x = y :=
match x return x = y -> x = y with
  true =>
  match y return true = y -> true = y with
    true => fun _ => refl_equal true
  | false => fun h => h
  end
| false =>
  match y return false = y -> false = y with
    true => fun h => h
  | false => fun _ => refl_equal false
  end
end.

(* The function is designed to return refl_equal whenever the two arguments 
can
 be observed to be the same boolean value.  The other cases make no sense, but
 can be fulfilled nonetheless. *)


(* We then prove that the function nu is both constant (because it returns 
refl_equal)
  and the identity function. *)

Lemma nu_id : forall x y (u:x=y), nu _ _ u = u.
Proof. intros x y []; case x; reflexivity.
Qed.

Lemma book_K : forall (x y : bool)(p q:x = y), p = q.
Proof. intros x y p q; rewrite <- (nu_id _ _ p), <- (nu_id _ _ q).
revert p q; case x; case y; reflexivity || (intros p; discriminate).
Qed.
--- end Coq code here


Now, this lemma, book_K, gives you proof-irrelevance for every property 
that you can express through a boolean function, in other words, for 
every decidable property.

For example, you can use the function beq_nat to compare two numbers, 
and you can write you own gcd function.  Now, you can build normalized 
fractions with the following type.

Inductive frac : Type := Frac : forall n d, beq_nat (gcd n d) 1 = true 
-> frac.

Using book_K, you can easily prove that fractions are equal as soon as 
their numerator and denominator
are equal, you don't need to bother about the proof that they are 
co-primes, since it is a proof between two
boolean values, hence it is unique.  This is an example to show that a 
place where you would normally use a setoid can be replaced by a data 
type where you can directly use Leibniz equality.

This approach, based on using boolean test functions is used extensively 
in the ssreflect library.   Actually, I learned the proof of bool_K 
above by studying the first files of ssreflect (although, as I already 
mentioned,
the proof was already known to others before).  In the ssreflect 
library, you will find a recurrent effort to use boolean functions 
whenever decidability is given, so that proof-irrelevance is inherited 
in many data-structures:
For instance, finite types are described using an enumeration of the 
type and a proof that this enumeration contains exactly once all 
elements of the type, this proof being described by a boolean 
computation.  Finite maps, that is functions whose input domain is a 
finite type are also describe by data with a proof.  None of the proofs 
really is a problem, because they are always unique.

Now, how can you have the best of both worlds?  Can Fmaps be completed 
in such a way that (Leibniz) equality can be used on Fmaps as soon as 
the setoid for the keys is shown to rely on a decidable property or a 
boolean function?  I haven't looked in the development of Fmaps so I 
can't tell.

On the broader topic of proof-irrelevance, you may also want to look at 
Barbanera and Berardi's article [2].
This says that you can deduce proof-irrelevance from excluded middle and 
the axiom of choice.  Now, if you decide to perform proofs in classical 
logic, admitting both excluded middle and the axiom of choice, you will 
be able to deduce unicity of proofs and use that in your proofs...   As 
far as I know, there is no inconsistency in using Coq with 
excluded-middle and the axiom of choice (for instance, I like to use 
ClassicalEpsilon, which has the strength of the axiom of choice, I believe).

references:
* A coherence theorem for Martin-Löf's type theory.* 
<http://www.cs.chalmers.se/%7Ehedberg/coh.ps>
/J. Functional Programming/ *8* (4): 413 - 436, July 1998.
available through http://www.cs.chalmers.se/~hedberg/

/*Proof-irrelevance out of Excluded-middle and Choice in the Calculus of 
Constructions,*/ 
<http://www.di.unito.it/%7Elambda/biblio/entry-Barbanera-Berardi-JFP96.html>
/J. Functional Programming/ *6* (3): 519 - 525, 1996.
available through http://www.di.unito.it/~lambda/biblio/author-berardis.html


I hope this helps,

Yves