From 0cc8a44bf6bb66ae15b544c41c5f580de0e55b5a Mon Sep 17 00:00:00 2001 From: Heiko Becker Date: Mon, 12 Jun 2017 16:14:16 +0200 Subject: [PATCH] Simplify transitivity proof of transitivity of equality --- coq/Expressions.v | 68 ++++++++++++++++++++++++----------------------- 1 file changed, 35 insertions(+), 33 deletions(-) diff --git a/coq/Expressions.v b/coq/Expressions.v index 2882725..a013257 100644 --- a/coq/Expressions.v +++ b/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. -- GitLab