adding inverse to smt_expr_eq

coq/SMTArith.v

@@ -189,6 +189,7 @@ Fixpoint smt_expr_eq (e: SMTArith) (e': expr Q) : bool :=
   | Expressions.Const _ r', ConstQ r => Qeq_bool r r'
   | Var _ x', VarQ x => beq_nat x x'
   | Unop Neg e', UMinusQ e => smt_expr_eq e e'
+  | Unop Inv e', DivQ (ConstQ (1#1)) e => smt_expr_eq e e'
   | Binop Plus e1' e2', PlusQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
   | Binop Sub e1' e2', MinusQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
   | Binop Mult e1' e2', TimesQ e1 e2 => (smt_expr_eq e1 e1') && (smt_expr_eq e2 e2')
@@ -214,11 +215,23 @@ Proof.
   - destruct e; try discriminate. intros H. apply Qeq_bool_eq in H.
     apply Qeq_eqR in H. cbn. now rewrite H.
   - destruct e, u; try discriminate.
-    intros Heq H.
-    inversion H; subst.
-    econstructor; eauto.
-    destruct m; try discriminate.
-    eapply IHe'; auto.
+    + intros Heq H.
+      inversion H; subst.
+      econstructor; eauto.
+      destruct m; try discriminate.
+      eapply IHe'; auto.
+    + destruct e1; try discriminate.
+      destruct r as [n d].
+      destruct n; try discriminate.
+      destruct p; try discriminate.
+      destruct d; try discriminate.
+      cbn. intros Heq H.
+      inversion H; subst.
+      destruct m; try discriminate.
+      eapply Binop_dist'; eauto.
+      cbn.
+      rewrite RMicromega.IQR_1.
+      apply RealSimps.inv_eq_1_div.
   - intros Heq H.
     inversion H; subst.
     assert (m1 = REAL) by (eapply toRTMap_eval_REAL; eauto).