Proof for Pmovz

Adding Ltac to simplify code and improve readability

1 files changed, 29 insertions, 7 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 4851da90..35d30d06 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1036,6 +1036,30 @@ Qed.
 Proof.
 Admitted.*)
 
+Ltac inv_ok_eq :=
+  repeat match goal with
+  | [EQ: OK ?x = OK ?y |- _ ]
+      => inversion EQ; clear EQ; subst
+  end.
+
+Ltac reg_rwrt :=
+  match goal with
+  | [e: DR _ = DR _ |- _ ]
+      => rewrite e in *
+  end.
+
+Ltac destruct_reg_inv :=
+  repeat match goal with
+  | [ H : match ?reg with _ => _ end = _ |- _ ]
+      => destruct reg; try congruence; try inv_ok_eq; try reg_rwrt
+  end.
+
+Ltac destruct_reg_size :=
+  repeat match goal with
+  | [ |- context [ match ?reg with _ => _ end = _ ] ]
+      => destruct reg; try congruence
+  end.
+
 Lemma exec_basic_simulation:
   forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi
   (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
@@ -1058,14 +1082,12 @@ Proof.
     + (* Pmovz *)
       destruct i;
       try ( destruct sumbool_rec; try congruence);
-      try (monadInv TRANSBI; simpl in *; destruct rd; try congruence; inversion EQ; subst;
-      try (destruct i; try congruence; inversion EQ; subst; rewrite e in *);
-      try (destruct rs; try congruence; inversion EQ1; subst);
+      try (monadInv TRANSBI; simpl in *; destruct rd; try congruence; inversion EQ; subst);
+      try (destruct_reg_inv);
       try (inversion MATCHI; subst; rewrite <- AG; try congruence);
-      exploit next_inst_preserved; eauto).
-      try (intros; simpl in *; try destruct sz; eauto).
-      (*intros; simpl in *; try destruct sz; eauto.*)
-            
+      try (exploit next_inst_preserved; eauto);
+      try (destruct_reg_size).
+
       all:admit.
     all:admit.