Ssreflect Users Discussion List

[Cyril <>]

Isn't that the point of the pickle_inv function?
--
Cyril

On 07/03/2018 15:55, Florian Steinberg wrote:
> 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.