optimize_plus_mult_l

optimize_plus_mult_l.v

Theorem optimize_plus_mult_l_sound: forall a,
  aeval (optimize_plus_mult_l a) = aeval a.
Proof.
  intros a. induction a.
    Case "ANum". reflexivity.
    Case "APlus". destruct a1.
      SCase "a1 = ANum".
        simpl. rewrite IHa2. reflexivity.
      SCase "a1 = APlus".
        simpl. destruct a1_1;
          (simpl; simpl in IHa1; rewrite IHa1; rewrite IHa2; reflexivity).
      SCase "a1 = AMinus".
        simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity.
      SCase "a1 = AMult". simpl. destruct a1_2.
        SSCase "a1_2 = APlus". destruct a2.
          SSSCase "a2 = ANum". destruct (beq_nat n n0) eqn:Heq.
            SSSSCase "Heq true".
              simpl. simpl in IHa1. apply beq_nat_true in Heq. rewrite <- Heq.
              rewrite IHa1. apply plus_comm.
            SSSSCase "Heq false".
              simpl. simpl in IHa1. rewrite IHa1. reflexivity.
          SSSCase "a2 = APlus".
            simpl. simpl in IHa1. rewrite IHa1. simpl in IHa2. rewrite IHa2. reflexivity.
          SSSCase "a2 = AMinus".
            simpl. simpl in IHa1. rewrite IHa1. simpl in IHa2. rewrite IHa2. reflexivity.
          SSSCase "a2 = AMult".
            simpl. simpl in IHa1. rewrite IHa1. simpl in IHa2. rewrite IHa2. reflexivity.
        SSCase "...".
          simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity.
        SSCase "...".
        simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity.
        SSCase "...".
        simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity.
        SSCase "...".
        simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity.
        SSCase "...".
        simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity.
Qed.

Theorem optimize_plus_mult_l_sound': forall a,
  aeval (optimize_plus_mult_l a) = aeval a.
Proof.
  intros a. induction a.
    Case "ANum". reflexivity.
    Case "APlus". destruct a1.
      SCase "a1 = ANum".
        simpl. rewrite IHa2. reflexivity.
      SCase "a1 = APlus".
        simpl. destruct a1_1;
          (simpl; simpl in IHa1; rewrite IHa1; rewrite IHa2; reflexivity).
      SCase "a1 = AMinus".
        simpl. simpl in IHa1. rewrite IHa1. rewrite IHa2. reflexivity.
(* XXX: Doesn't prove all goals:
      SCase "a1 = AMult". simpl. destruct a1_2;

        try (SSCase "a1_2 = APlus"; destruct a2;
          try (SSSCase "a2 = ANum"; destruct (beq_nat n n0) eqn:Heq;

            try (SSSSCase "Heq true";
              simpl; simpl in IHa1; apply beq_nat_true in Heq; rewrite <- Heq;
              rewrite IHa1; apply plus_comm);
            try (SSSSCase "Heq false";
              simpl; simpl in IHa1; rewrite IHa1; reflexivity));

          try (SSSCase "a2 = APlus; AMinus; AMult";
            simpl; simpl in IHa1; rewrite IHa1; simpl in IHa2; rewrite IHa2; reflexivity));

        try (SSCase "...";
          simpl; simpl in IHa1; rewrite IHa1; rewrite IHa2; reflexivity).
*)
Abort.