diff options
| author | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-30 14:33:35 +0200 |
|---|---|---|
| committer | David Monniaux <david.monniaux@univ-grenoble-alpes.fr> | 2020-03-30 14:33:35 +0200 |
| commit | d1adc4858ec70963233945542b717fcd1459a96a (patch) | |
| tree | 9977d10813e6ba01be4464d64a06b54e8a921a58 /backend/Injectproof.v | |
| parent | a117ebbcb63ef0d73772e0073f23238a5642723a (diff) | |
| download | compcert-kvx-d1adc4858ec70963233945542b717fcd1459a96a.tar.gz compcert-kvx-d1adc4858ec70963233945542b717fcd1459a96a.zip | |
injector injects the end
Diffstat (limited to 'backend/Injectproof.v')
| -rw-r--r-- | backend/Injectproof.v | 23 |
1 files changed, 19 insertions, 4 deletions
diff --git a/backend/Injectproof.v b/backend/Injectproof.v index 7a991a8c..eeaadb2a 100644 --- a/backend/Injectproof.v +++ b/backend/Injectproof.v @@ -96,16 +96,31 @@ Proof. induction l; simpl; intros. - lia. - simpl. - destruct k as [ | k]. - + admit. - + simpl pos_add_nat. - rewrite pos_add_nat_succ. + destruct k as [ | k]; simpl pos_add_nat. + + simpl bounded_nth. + rewrite inject_list_preserves by lia. + apply PTree.gss. + + rewrite pos_add_nat_succ. erewrite IHl. f_equal. f_equal. simpl. apply bounded_nth_proof_irr. + Unshelve. + lia. Qed. +Lemma inject_list_injected_end: + forall l prog pc dst, + PTree.get (pos_add_nat pc (List.length l)) + (snd (inject_list prog pc dst l)) = + Some (Inop dst). +Proof. + induction l; simpl; intros. + - apply PTree.gss. + - rewrite pos_add_nat_succ. + apply IHl. +Qed. + Lemma inject_at_preserves : forall prog pc extra_pc l pc0, pc0 < extra_pc -> |