diff options
Diffstat (limited to 'common')
| -rw-r--r-- | common/AST.v | 6 | ||||
| -rw-r--r-- | common/Mem.v | 20 |
2 files changed, 26 insertions, 0 deletions
diff --git a/common/AST.v b/common/AST.v index eab1adf1..ec8053d4 100644 --- a/common/AST.v +++ b/common/AST.v @@ -46,6 +46,12 @@ Definition typesize (ty: typ) : Z := Lemma typesize_pos: forall ty, typesize ty > 0. Proof. destruct ty; simpl; omega. Qed. +Lemma typ_eq: forall (t1 t2: typ), {t1=t2} + {t1<>t2}. +Proof. decide equality. Qed. + +Lemma opt_typ_eq: forall (t1 t2: option typ), {t1=t2} + {t1<>t2}. +Proof. decide equality. apply typ_eq. Qed. + (** Additionally, function definitions and function calls are annotated by function signatures indicating the number and types of arguments, as well as the type of the returned value if any. These signatures diff --git a/common/Mem.v b/common/Mem.v index de3e8c94..e169dfc7 100644 --- a/common/Mem.v +++ b/common/Mem.v @@ -1796,6 +1796,26 @@ Proof. unfold inject_id; intros. congruence. Qed. +Lemma free_left_lessdef: + forall m1 m2 b, + lessdef m1 m2 -> lessdef (free m1 b) m2. +Proof. + intros. destruct H. split. + rewrite <- H. auto. + apply free_left_inj; auto. +Qed. + +Lemma free_right_lessdef: + forall m1 m2 b, + lessdef m1 m2 -> low_bound m1 b >= high_bound m1 b -> + lessdef m1 (free m2 b). +Proof. + intros. destruct H. unfold lessdef. split. + rewrite H. auto. + apply free_right_inj; auto. intros. unfold inject_id in H2. inv H2. + red; intro. inv H2. generalize (size_chunk_pos chunk); intro. omega. +Qed. + Lemma valid_block_lessdef: forall m1 m2 b, lessdef m1 m2 -> valid_block m1 b -> valid_block m2 b. Proof. |