Commit f1ffdc4d authored by Jakob Botsch Nielsen's avatar Jakob Botsch Nielsen
Browse files

Prove that serialize is injective

parent 458189b2
......@@ -70,6 +70,16 @@ Class Serializable (ty : Type) :=
Global Opaque serialize deserialize deserialize_serialize.
Lemma serialize_injective {T : Type} `{Serializable T} x y :
serialize x = serialize y ->
x = y.
Proof.
intros eq.
enough (Some x = Some y) by congruence.
rewrite <- 2!deserialize_serialize.
now rewrite eq.
Qed.
Program Instance unit_serializable : Serializable unit :=
{| serialize u := build_ser_value ser_unit u;
deserialize := extract_ser_value ser_unit; |}.
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment