Add tactic "destr_factorize" refactoring matches on option type functions

coq/ErrorValidation.v

@@ -203,10 +203,9 @@ Proof.
     apply H.
     canonize_hyps.
     rewrite Q2R_mult in error_valid.
-    rewrite A_var in find_v; inversion find_v; subst.
+    repeat destr_factorize.
     rewrite <- maxAbs_impl_RmaxAbs in error_valid.
     eapply Rle_trans; eauto.
-    rewrite Heqo0 in H5; inversion H5; subst.
     eapply Rmult_le_compat_r.
     + apply mTypeToQ_pos_R.
     + destruct bounds_valid as [valid_lo valid_hi].
@@ -292,9 +291,7 @@ Proof.
     try eauto.
   pose proof (typingSoundnessExp _ _ R2 e1_float).
   pose proof (typingSoundnessExp _ _ R1 e2_float).
-  rewrite H in Heqo0; inversion Heqo0; subst;
-    rewrite H0 in Heqo1; inversion Heqo1; subst.
-  clear H H0.
+  repeat destr_factorize.
   rename R0 into valid_error.
   eapply Rle_trans.
   apply Rplus_le_compat_l.
@@ -318,22 +315,23 @@ Proof.
   rewrite <- maxAbs_impl_RmaxAbs.
   assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
   assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
-  rewrite <- H, <- H0.
+  subst.
   assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
-  pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded).
+  pose proof (distance_gives_iv (a:=nR1) _ (Q2R e1lo, Q2R e1hi) contained_intv1 err1_bounded)
+       as contained_widen1.
   assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
-  pose proof (distance_gives_iv (a:=nR2) _ (Q2R e2lo, Q2R e2hi) contained_intv2 err2_bounded).
-  pose proof (IntervalArith.interval_addition_valid _ _ H1 H2).
+  pose proof (distance_gives_iv (a:=nR2) _ (Q2R e2lo, Q2R e2hi) contained_intv2 err2_bounded)
+       as contained_widen2.
+  pose proof (IntervalArith.interval_addition_valid _ _ contained_widen1 contained_widen2).
   simpl in *.
-  destruct H3.
   subst; simpl in *.
   apply RmaxAbs; simpl.
   - rewrite Q2R_min4.
     repeat rewrite Q2R_plus;
-      repeat rewrite Q2R_minus; auto.
+      repeat rewrite Q2R_minus; lra.
   - rewrite Q2R_max4.
     repeat rewrite Q2R_plus;
-      repeat rewrite Q2R_minus; auto.
+      repeat rewrite Q2R_minus; lra.
 Qed.
 
 Lemma validErrorboundCorrectSubtraction E1 E2 A
@@ -367,8 +365,7 @@ Proof.
   eapply (subtract_abs_err_bounded e1 e2); try eauto.
   pose proof (typingSoundnessExp _ _ R2 e1_float).
   pose proof (typingSoundnessExp _ _ R1 e2_float).
-  rewrite H in Heqo0; rewrite H0 in Heqo1; inversion Heqo0; inversion Heqo1; subst.
-  clear H H0.
+  repeat destr_factorize.
   rename R0 into valid_error.
   canonize_hyps.
   repeat rewrite Q2R_plus in valid_error.
@@ -387,28 +384,28 @@ Proof.
   rewrite <- maxAbs_impl_RmaxAbs.
   assert (ivlo iv = ivl) by (rewrite iv_unf; auto).
   assert (ivhi iv = ivh) by (rewrite iv_unf; auto).
-  rewrite <- H, <- H0.
-    assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
-  pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded).
+  subst.
+  assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto.
+  pose proof (distance_gives_iv (a:=nR1) _ _ contained_intv1 err1_bounded)
+       as contained_widen1.
   assert (contained nR2 (Q2R e2lo, Q2R e2hi)) as contained_intv2 by auto.
-  pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded).
-  pose proof (IntervalArith.interval_subtraction_valid _ _ H1 H2).
+  pose proof (distance_gives_iv (a:=nR2) _ _ contained_intv2 err2_bounded)
+       as contained_widen2.
+  pose proof (IntervalArith.interval_subtraction_valid _ _ contained_widen1 contained_widen2).
   simpl in *.
-  destruct H3.
-  subst; simpl in *.
   apply RmaxAbs; simpl.
   - rewrite Q2R_min4.
     repeat rewrite Q2R_plus;
       repeat rewrite Q2R_minus;
       repeat rewrite Q2R_opp;
       repeat rewrite Q2R_plus;
-      repeat rewrite Q2R_minus; auto.
+      repeat rewrite Q2R_minus; lra.
   - rewrite Q2R_max4.
     repeat rewrite Q2R_plus;
       repeat rewrite Q2R_minus;
       repeat rewrite Q2R_opp;
       repeat rewrite Q2R_plus;
-      repeat rewrite Q2R_minus; auto.
+      repeat rewrite Q2R_minus; lra.
 Qed.
 
 Lemma validErrorboundCorrectMult E1 E2 A

coq/Infra/Ltacs.v

@@ -85,6 +85,14 @@ Ltac pair_factorize :=
   | [H: context[let (_, _) := ?p in _] |- _] => destruct p; cbn in H
   end.
 
+Ltac destr_factorize :=
+  match goal with
+  | [H1: _ ?v = Some ?a, H2: _ ?v = Some ?b |- _]
+      => rewrite H1 in H2; inversion H2; subst; clear H2
+  | [H1:  _ ?k ?M = Some ?a, H2: _ ?k ?M = Some ?b |- _]
+    => rewrite H1 in H2; inversion H2; subst; clear H2
+  end.
+
 Ltac match_simpl :=
   try remove_conds;
   try remove_matches;