diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 21:08:21 +0100 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-13 21:08:21 +0100 |
| commit | 886c7426af936fc84b0a284a853b659fea386de3 (patch) | |
| tree | f7d4868efc4c674f4eaad857ddda6651faf98c66 /backend/CSE3proof.v | |
| parent | 7e4b3b10367e71e74b8eca57d94e4413336411bf (diff) | |
| download | compcert-kvx-886c7426af936fc84b0a284a853b659fea386de3.tar.gz compcert-kvx-886c7426af936fc84b0a284a853b659fea386de3.zip | |
CSE3 proofs: REL is inductive
Diffstat (limited to 'backend/CSE3proof.v')
| -rw-r--r-- | backend/CSE3proof.v | 14 |
1 files changed, 13 insertions, 1 deletions
diff --git a/backend/CSE3proof.v b/backend/CSE3proof.v index 3fbac9ea..319b7f7e 100644 --- a/backend/CSE3proof.v +++ b/backend/CSE3proof.v @@ -413,6 +413,15 @@ Proof. Qed. Hint Resolve sem_rel_top : cse3. + +Lemma sem_rel_b_top: + forall ctx sp rs m, sem_rel_b sp ctx (Some RELATION.top) rs m. +Proof. + intros. simpl. + apply sem_rel_top. +Qed. + +Hint Resolve sem_rel_b_top : cse3. Ltac IND_STEP := match goal with @@ -574,7 +583,10 @@ Proof. assumption. * apply checked_is_inductive_allstep. apply transf_function_invariants_inductive with (tf:=tf); auto. - + * rewrite @checked_is_inductive_entry with (tenv:=tenv) (ctx:=(context_from_hints (snd (preanalysis tenv f)))). + ** apply sem_rel_b_top. + ** apply transf_function_invariants_inductive with (tf:=tf); auto. + - (* external *) simpl in FUN. inv FUN. |