From b4af6cbe24b1108b4e49d3c17fecc37255bd6151 Mon Sep 17 00:00:00 2001 From: David Monniaux Date: Wed, 9 Dec 2020 09:07:32 +0100 Subject: avancement dans les preuves --- backend/CSE3proof.v | 35 ++++++++++++++++++++++++++++++++++- 1 file changed, 34 insertions(+), 1 deletion(-) (limited to 'backend') 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. -- cgit