Simplify transitivity proof of transitivity of equality

coq/Expressions.v

@@ -2,7 +2,7 @@
   Formalization of the base expression language for the daisy framework
  **)
 Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals.
-Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps.
+Require Import Daisy.Infra.RealRationalProps Daisy.Infra.RationalSimps Daisy.Infra.Ltacs.
 Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType.
 
 (**
@@ -38,6 +38,12 @@ Proof.
   case b; auto.
 Qed.
 
+Lemma binopEqBool_prop b1 b2:
+  binopEqBool b1 b2 = true <-> b1 = b2.
+Proof.
+  split; case b1; case b2; intros; simpl in *; try congruence; auto.
+Qed.
+
 (**
    Expressions will use unary operators.
    Define them first
@@ -57,6 +63,12 @@ Proof.
   case b; auto.
 Qed.
 
+Lemma unopEqBool_prop b1 b2:
+  unopEqBool b1 b2 = true <-> b1 = b2.
+Proof.
+  split; case b1; case b2; intros; simpl in *; try congruence; auto.
+Qed.
+
 (**
    Define evaluation for unary operators on reals.
    Errors are added in the expression evaluation level later.
@@ -132,40 +144,30 @@ Lemma expEqBool_trans e f g:
   expEqBool e g = true.
 Proof.
   revert e f g; induction e;
-    destruct f; intros;
-      simpl in H; inversion H; rewrite H; clear H;
-        destruct g; simpl in H0; inversion H0; rewrite H0; clear H0;
-          try (apply andb_true_iff in H1; destruct H1; apply andb_true_iff in H2; destruct H2; simpl).
-  - apply beq_nat_true in H2.
-    apply beq_nat_true in H1.
-    subst.
-    unfold expEqBool.
-    rewrite <- beq_nat_refl.
-    auto.
-  - apply EquivEqBoolEq in H1.
-    apply EquivEqBoolEq in H.
-    subst.
+    destruct f; intros g eq1 eq2;
+      destruct g; simpl in *; try congruence;
+        try rewrite Nat.eqb_eq in *;
+        subst; try auto.
+  - andb_to_prop eq1;
+      andb_to_prop eq2.
+    apply EquivEqBoolEq in L.
+    apply EquivEqBoolEq in L0; subst.
     rewrite mTypeEqBool_refl; simpl.
-    apply Qeq_bool_iff in H2.
-    apply Qeq_bool_iff in H0.
-    apply Qeq_bool_iff.
-    lra.
-  - assert (u = u0) by (destruct u; destruct u0; inversion H1; auto).
-    assert (u0 = u1) by (destruct u0; destruct u1; inversion H; auto).
-    subst.
-    assert (unopEqBool u1 u1 = true) by (destruct u1; auto).
-    apply andb_true_iff; split; try auto.
+    rewrite Qeq_bool_iff in *; lra.
+  - andb_to_prop eq1;
+      andb_to_prop eq2.
+    rewrite unopEqBool_prop in *; subst.
+    rewrite unopEqBool_refl; simpl.
     eapply IHe; eauto.
-  - apply andb_true_iff; split.
-    + destruct b; destruct b0; destruct b1; auto.
-    + apply andb_true_iff in H2; destruct H2.
-      apply andb_true_iff in H0; destruct H0.
-      apply andb_true_iff; split.
-      eapply IHe1; eauto.
-      eapply IHe2; eauto.
-  - apply EquivEqBoolEq in H1.
-    apply EquivEqBoolEq in H.
-    subst.
+  - andb_to_prop eq1;
+      andb_to_prop eq2.
+    rewrite binopEqBool_prop in *; subst.
+    rewrite binopEqBool_refl; simpl.
+    apply andb_true_iff.
+    split; [eapply IHe1; eauto | eapply IHe2; eauto].
+  - andb_to_prop eq1;
+      andb_to_prop eq2.
+    rewrite EquivEqBoolEq in *; subst.
     rewrite mTypeEqBool_refl; simpl.
     eapply IHe; eauto.
 Qed.