avancement dans les preuves

1 files changed, 34 insertions, 1 deletions

diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v
index 972cae5f..69e779cd 100644
--- a/backend/CSE3proof.v
+++ b/backend/CSE3proof.v
@@ -930,7 +930,40 @@ Proof.
         TR_AT. unfold transf_instr. fold invs. fold ctx. rewrite FIND_COND. reflexivity.
       * replace bfound with b.
         { econstructor; eauto.
-          admit.
+             (* BEGIN INVARIANT *)
+        fold ctx. fold invs.
+      assert ((check_inductiveness f tenv invs)=true) as IND by (eapply transf_function_invariants_inductive; eauto).
+      unfold check_inductiveness in IND.
+      rewrite andb_true_iff in IND.
+      destruct IND as [IND_entry IND_step].
+      rewrite PTree_Properties.for_all_correct in IND_step.
+      pose proof (IND_step pc _ H) as IND_step_me.
+      clear IND_entry IND_step.
+      destruct (invs # pc) as [inv_pc | ] eqn:INV_pc; cbn in REL.
+      2: contradiction.
+      cbn in IND_step_me.
+      rewrite andb_true_iff in IND_step_me.
+      rewrite andb_true_iff in IND_step_me.
+      destruct IND_step_me as [IND_so [IND_not ZOT]].
+      clear ZOT.
+      destruct (invs # ifso) as [inv_so | ] eqn:INV_so; cbn in *.
+      2: discriminate.
+      destruct (invs # ifnot) as [inv_not | ] eqn:INV_not; cbn in *.
+      2: discriminate.
+      rewrite rel_leb_correct in IND_so.
+      rewrite rel_leb_correct in IND_not.
+      destruct b.
+      {
+        rewrite INV_so.
+        cbn.
+        eapply rel_ge; eauto.
+      }
+      {
+        rewrite INV_not.
+        cbn.
+        eapply rel_ge; eauto.
+      }
+      (* END INVARIANT *)
         }
         unfold sem_rel_b in REL.
         destruct (invs # pc) as [rel | ] eqn:FIND_REL.