WIP: Start working on splitting of soundness proof into 2 separate proofs

coq/Environments.v

@@ -108,15 +108,16 @@ Proof.
       rewrite x_x0_neq in x_typed; auto.
 Qed.
 
-Lemma approxEnv_dVar_bounded v2 m:
+Lemma approxEnv_dVar_bounded v2 m e:
   E1 x = Some v ->
   E2 x = Some v2 ->
   NatSet.In x dVars ->
   Gamma x = Some m ->
-  (Rabs (v - v2) <= Q2R (snd (A (Var Q x))))%R.
+  snd (A (Var Q x)) = e ->
+  (Rabs (v - v2) <= Q2R e)%R.
 Proof.
   induction approxEnvs;
-    intros E1_def E2_def x_def x_typed.
+    intros E1_def E2_def x_def x_typed A_e; subst.
   - unfold emptyEnv in *; simpl in *; congruence.
   - assert (x =? x0 = false) as x_x0_neq.
     { rewrite Nat.eqb_neq; hnf; intros; subst.

coq/Infra/Ltacs.v

@@ -66,4 +66,4 @@ Ltac destruct_if :=
     intros name;
     rewrite name in *;
     try congruence
-  end .
+  end .
\ No newline at end of file

coq/Infra/MachineType.v

@@ -81,6 +81,13 @@ Proof.
   - case_eq m1; intros; case_eq m2; intros; subst; cbv; congruence.
 Qed.
 
+Ltac type_conv :=
+  repeat
+    (match goal with
+     | [H : mTypeEq _ _ = true |- _] => rewrite mTypeEq_compat_eq in H; subst
+     | [H : mTypeEq _ _ = false |- _] => rewrite mTypeEq_compat_eq_false in H
+     end).
+
 Lemma mTypeEq_sym (m1:mType) (m2:mType):
   forall b, mTypeEq m1 m2 = b -> mTypeEq m2 m1 = b.
 Proof.