Move a couple of lemmas up in the file

1 files changed, 68 insertions, 68 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 8366ae14..e656b199 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -757,6 +757,74 @@ Proof.
   repeat (rewrite <- length_agree). assumption.
 Qed.
 
+Lemma exec_arith_instr_dont_move_PC ai rs rs': forall
+  (BASIC: exec_arith_instr lk ai rs = rs'),
+  rs PC = rs' PC.
+Proof.
+  destruct ai; simpl; intros;
+  try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate).
+  - destruct i; simpl in BASIC.
+    + unfold compare_long in BASIC; rewrite <- BASIC.
+      repeat rewrite Pregmap.gso; try discriminate. reflexivity.
+    + unfold compare_long in BASIC; rewrite <- BASIC.
+      repeat rewrite Pregmap.gso; try discriminate. reflexivity.
+    + destruct sz;
+      try (unfold compare_single in BASIC || unfold compare_float in BASIC);
+      destruct (rs r1), (rs r2);
+      try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
+  - destruct i; simpl in BASIC; destruct is;
+      try (unfold compare_int in BASIC || unfold compare_long in BASIC);
+      try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
+  - destruct i; simpl in BASIC; destruct sz;
+    try (unfold compare_single in BASIC || unfold compare_float in BASIC);
+    destruct (rs r1);
+    try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
+  - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity).
+  - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity).
+Qed.
+
+Lemma exec_basic_dont_move_PC bi rs m rs' m': forall
+  (BASIC: exec_basic lk ge bi rs m = Next rs' m'),
+  rs PC = rs' PC.
+Proof.
+  destruct bi; simpl; intros.
+  - inv BASIC. exploit exec_arith_instr_dont_move_PC; eauto.
+  - unfold exec_load in BASIC.
+    destruct Mem.loadv. 2: { discriminate BASIC. }
+    inv BASIC. rewrite Pregmap.gso; try discriminate; auto.
+  - unfold exec_store in BASIC.
+    destruct Mem.storev. 2: { discriminate BASIC. }
+    inv BASIC; reflexivity.
+  - destruct Mem.alloc, Mem.store. 2: { discriminate BASIC. }
+    inv BASIC. repeat (rewrite Pregmap.gso; try discriminate). reflexivity.
+  - destruct Mem.loadv. 2: { discriminate BASIC. }
+    destruct rs, Mem.free; try discriminate BASIC.
+    inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
+  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
+  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
+  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
+  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
+Qed.
+
+Lemma exec_body_dont_move_PC_aux:
+  forall bis rs m rs' m'
+  (BODY: exec_body lk ge bis rs m = Next rs' m'),
+  rs PC = rs' PC.
+Proof.
+  induction bis.
+  - intros; inv BODY; reflexivity.
+  - simpl; intros.
+    remember (exec_basic lk ge a rs m) as bi eqn:BI; destruct bi. 2: { discriminate BODY. }
+    symmetry in BI; destruct s in BODY, BI; simpl in BODY, BI.
+    exploit exec_basic_dont_move_PC; eauto; intros AGPC; rewrite AGPC.
+    eapply IHbis; eauto.
+Qed.
+
+Lemma exec_body_dont_move_PC bb rs m rs' m': forall
+  (BODY: exec_body lk ge (body bb) rs m = Next rs' m'),
+  rs PC = rs' PC.
+Proof. apply exec_body_dont_move_PC_aux. Qed.
+
 Lemma find_instr_bblock:
   forall n lb pos bb tlb
   (FINDBB: find_bblock pos lb = Some bb)
@@ -922,74 +990,6 @@ Proof.
     eapply plus_star; eauto.
 Qed.
 
-Lemma exec_arith_instr_dont_move_PC ai rs rs': forall
-  (BASIC: exec_arith_instr lk ai rs = rs'),
-  rs PC = rs' PC.
-Proof.
-  destruct ai; simpl; intros;
-  try (rewrite <- BASIC; rewrite Pregmap.gso; auto; discriminate).
-  - destruct i; simpl in BASIC.
-    + unfold compare_long in BASIC; rewrite <- BASIC.
-      repeat rewrite Pregmap.gso; try discriminate. reflexivity.
-    + unfold compare_long in BASIC; rewrite <- BASIC.
-      repeat rewrite Pregmap.gso; try discriminate. reflexivity.
-    + destruct sz;
-      try (unfold compare_single in BASIC || unfold compare_float in BASIC);
-      destruct (rs r1), (rs r2);
-      try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
-  - destruct i; simpl in BASIC; destruct is;
-      try (unfold compare_int in BASIC || unfold compare_long in BASIC);
-      try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
-  - destruct i; simpl in BASIC; destruct sz;
-    try (unfold compare_single in BASIC || unfold compare_float in BASIC);
-    destruct (rs r1);
-    try (rewrite <- BASIC; repeat rewrite Pregmap.gso; try (discriminate || reflexivity)).
-  - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity).
-  - destruct fsz; rewrite <- BASIC; rewrite Pregmap.gso; try (discriminate || reflexivity).
-Qed.
-
-Lemma exec_basic_dont_move_PC bi rs m rs' m': forall
-  (BASIC: exec_basic lk ge bi rs m = Next rs' m'),
-  rs PC = rs' PC.
-Proof.
-  destruct bi; simpl; intros.
-  - inv BASIC. exploit exec_arith_instr_dont_move_PC; eauto.
-  - unfold exec_load in BASIC.
-    destruct Mem.loadv. 2: { discriminate BASIC. }
-    inv BASIC. rewrite Pregmap.gso; try discriminate; auto.
-  - unfold exec_store in BASIC.
-    destruct Mem.storev. 2: { discriminate BASIC. }
-    inv BASIC; reflexivity.
-  - destruct Mem.alloc, Mem.store. 2: { discriminate BASIC. }
-    inv BASIC. repeat (rewrite Pregmap.gso; try discriminate). reflexivity.
-  - destruct Mem.loadv. 2: { discriminate BASIC. }
-    destruct rs, Mem.free; try discriminate BASIC.
-    inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-  - inv BASIC; rewrite Pregmap.gso; try discriminate; auto.
-Qed.
-
-Lemma exec_body_dont_move_PC_aux:
-  forall bis rs m rs' m'
-  (BODY: exec_body lk ge bis rs m = Next rs' m'),
-  rs PC = rs' PC.
-Proof.
-  induction bis.
-  - intros; inv BODY; reflexivity.
-  - simpl; intros.
-    remember (exec_basic lk ge a rs m) as bi eqn:BI; destruct bi. 2: { discriminate BODY. }
-    symmetry in BI; destruct s in BODY, BI; simpl in BODY, BI.
-    exploit exec_basic_dont_move_PC; eauto; intros AGPC; rewrite AGPC.
-    eapply IHbis; eauto.
-Qed.
-
-Lemma exec_body_dont_move_PC bb rs m rs' m': forall
-  (BODY: exec_body lk ge (body bb) rs m = Next rs' m'),
-  rs PC = rs' PC.
-Proof. apply exec_body_dont_move_PC_aux. Qed.
-
 Lemma list_nth_z_range_exceeded A (l : list A) n:
   n >= list_length_z l ->
   list_nth_z l n = None.