Ssreflect Users Discussion List

[Florian Steinberg <>]

The unpickle function of countTypes is not required to be injective on its 
domain. This confused me a lot in a proof and can easily be fixed by 
replacing the  unpickling function with the following function, which I think 
should be saved as the unpickling function of a countType in the first place:

Definition unpickle' n: option C := if
    match unpickle n with
        | None => None
        | Some c => Some (@pickle C c)
    end == Some n
    then unpickle n else None.

Lemma pickleK' (c:C):
    unpickle' (pickle c) = Some c.
Proof. by rewrite /unpickle' pickleK; case: ifP => //; rewrite eqxx. Qed.

Lemma unpickle_inj:
    forall n c, unpickle' n = some c -> pickle c = n.
Proof.
move => n c.
rewrite /unpickle'.
case (unpickle n) => [s | ] //.
by case: eqP => // - [<-] [<-].
Qed.

-- 
Florian Steinberg
Marelle-team
INRIA Sophia-Antipolis
Email: 

 
You can find me on github, bitbucket and researchgate