Finished proofs in QhasmEvalCommon for formalizing mappings

2 files changed, 33 insertions, 34 deletions

diff --git a/src/Assembly/QhasmEvalCommon.v b/src/Assembly/QhasmEvalCommon.v
index eaab0a185..fba8428ee 100644
--- a/src/Assembly/QhasmEvalCommon.v
+++ b/src/Assembly/QhasmEvalCommon.v
@@ -250,4 +250,37 @@ Fixpoint regNames {n} (lst: list (Mapping n)): list nat :=
     end
   end.
 
+(* Mapping Identifier-Triples *)
+
+Definition mappingId {n} (x: Mapping n): nat * nat * nat :=
+  match x with
+  | regM (reg n _ v) => (0, n, v)
+  | stackM (stack n _ v) => (1, n, v)
+  | constM (const n _ w) => (2, n, wordToNat w)
+  | memM _ (mem n m _ v) => (3, m, v)
+  end.
 
+Lemma id_equal: forall {n: nat} (x y: Mapping n),
+    x = y <-> mappingId x = mappingId y.
+Proof.
+  intros; split; intros; try abstract (rewrite H; intuition);
+    destruct x as [x | x | x | x], y as [y | y | y | y];
+    destruct x, y; unfold mappingId in H; simpl in H;
+
+    repeat match goal with
+    | [X: (_, _, _) = (_, _, _) |- _ ] =>
+      apply Triple_as_OT.conv in X
+    | [X: _ /\ _ /\ _ |- _ ] => destruct X
+    | [X: _ /\ _ |- _ ] => destruct X
+    | [A: Width _, B: Width _ |- _ ] =>
+      replace A with B by (apply width_eq)
+    | [X: context[match ?a with | _ => _ end] |- _ ] =>
+      destruct a
+    end; try subst; try omega; intuition.
+
+  rewrite <- (natToWord_wordToNat w0);
+    rewrite <- (natToWord_wordToNat w2);
+    rewrite H1; intuition.
+Qed.
+
+Definition id_dec := Triple_as_OT.eq_dec.
diff --git a/src/Assembly/StringConversion.v b/src/Assembly/StringConversion.v
index abd5b9367..47741cb43 100644
--- a/src/Assembly/StringConversion.v
+++ b/src/Assembly/StringConversion.v
@@ -161,40 +161,6 @@ Module StringConversion <: Conversion Qhasm QhasmString.
   End Elements.
 
   Section Parsing.
-    Inductive Entry :=
-      | intEntry: forall n, IReg n -> Entry
-      | stackEntry: forall n, Stack n -> Entry.
-
-    Definition entryId (x: Entry): nat * nat * nat :=
-      match x with
-      | intEntry n (regInt32 v) => (0, n, v)
-      | intEntry n (regInt64 v) => (1, n, v)
-      | stackEntry n (stack32 v) => (2, n, v)
-      | stackEntry n (stack64 v) => (3, n, v)
-      | stackEntry n (stack128 v) => (4, n, v)
-      end.
-
-    Lemma id_equal: forall {x y}, x = y <-> entryId x = entryId y.
-    Proof.
-      intros; split; intros;
-        destruct x as [nx x | nx x];
-        destruct y as [ny y | ny y];
-        try rewrite H;
-
-        destruct x, y; subst;
-        destruct (Nat.eq_dec n n0); subst;
-
-        simpl in H; inversion H; intuition.
-    Qed.
-
-    Definition entry_dec (x y: Entry): {x = y} + {x <> y}.
-      refine (_ (triple_dec (entryId x) (entryId y))).
-      intros; destruct x0.
-
-      - left; abstract (apply id_equal in e; intuition).
-      - right; abstract (intro; apply id_equal in H; intuition).
-    Defined.
-
     Fixpoint entries (prog: Program): list Entry :=
       match prog with
       | cons s next =>