proved most of point encoding admits, fixed some build system issues (dead imports of PointFormats and Galois things)

1 files changed, 14 insertions, 0 deletions

diff --git a/src/Encoding/EncodingTheorems.v b/src/Encoding/EncodingTheorems.v
new file mode 100644
index 000000000..f53ad0319
--- /dev/null
+++ b/src/Encoding/EncodingTheorems.v
@@ -0,0 +1,14 @@
+Require Import Crypto.Spec.Encoding.
+
+Section EncodingTheorems.
+  Context {A B : Type} {E : encoding of A as B}.
+  
+  Lemma encoding_inj : forall x y, enc x = enc y -> x = y.
+  Proof.
+    intros.
+    assert (dec (enc x) = dec (enc y)) as dec_enc_eq by (f_equal; auto).
+    do 2 rewrite encoding_valid in dec_enc_eq.
+    inversion dec_enc_eq; auto.
+  Qed.
+
+End EncodingTheorems.