diff options
author | Yann Herklotz <git@yannherklotz.com> | 2022-03-02 18:06:18 +0000 |
---|---|---|
committer | Yann Herklotz <git@yannherklotz.com> | 2022-03-02 18:06:18 +0000 |
commit | c2ba535604cef5bc86369512e6f3c2833753a55a (patch) | |
tree | fd0b83022443a3806a5bac4e82299c513f5d2f8d /src/hls/AssocMap.v | |
parent | 88d015ba178665ee21b282f364ccf047522e3b1c (diff) | |
download | vericert-c2ba535604cef5bc86369512e6f3c2833753a55a.tar.gz vericert-c2ba535604cef5bc86369512e6f3c2833753a55a.zip |
Update Coq version to 8.14.1
Diffstat (limited to 'src/hls/AssocMap.v')
-rw-r--r-- | src/hls/AssocMap.v | 86 |
1 files changed, 49 insertions, 37 deletions
diff --git a/src/hls/AssocMap.v b/src/hls/AssocMap.v index 8dbc6b2..10bd8eb 100644 --- a/src/hls/AssocMap.v +++ b/src/hls/AssocMap.v @@ -42,63 +42,75 @@ Module AssocMapExt. | Some v => v end. - Fixpoint merge (m1 m2 : t A) : t A := - match m1, m2 with - | Node l1 (Some a) r1, Node l2 _ r2 => Node (merge l1 l2) (Some a) (merge r1 r2) - | Node l1 None r1, Node l2 o r2 => Node (merge l1 l2) o (merge r1 r2) - | Leaf, _ => m2 - | _, _ => m1 + Definition merge_atom (new : option A) (old : option A) : option A := + match new, old with + | Some _, _ => new + | _, _ => old end. + Definition merge (m1 m2 : t A) : t A := + PTree.combine merge_atom m1 m2. + Lemma merge_base_1 : - forall am, - merge (empty A) am = am. - Proof. auto. Qed. + forall am x, + (merge (empty A) am) ! x = am ! x. + Proof using. + unfold merge; intros. + rewrite PTree.gcombine; eauto. + Qed. Lemma merge_base_2 : - forall am, - merge am (empty A) = am. - Proof. - unfold merge. - destruct am; trivial. - destruct o; trivial. + forall am x, + (merge am (empty A)) ! x = am ! x. + Proof using. + unfold merge; intros. + rewrite PTree.gcombine; eauto. + cbv [merge_atom]. destruct_match; crush. Qed. Lemma merge_add_assoc : - forall r am am' v, - merge (set r v am) am' = set r v (merge am am'). - Proof. - induction r; intros; destruct am; destruct am'; try (destruct o); simpl; - try rewrite IHr; try reflexivity. + forall r am am' v x, + (merge (set r v am) am') ! x = (set r v (merge am am')) ! x. + Proof using. + unfold merge. intros; rewrite PTree.gcombine by auto. + unfold merge_atom. destruct_match. + destruct (peq r x); subst. + rewrite PTree.gss in Heqo. inv Heqo. rewrite PTree.gss. auto. + rewrite PTree.gso in Heqo by auto. rewrite PTree.gso by auto. + rewrite PTree.gcombine by auto. rewrite Heqo. auto. + destruct (peq r x); subst. + rewrite PTree.gss in Heqo. inv Heqo. + rewrite PTree.gso in Heqo by auto. rewrite PTree.gso by auto. + rewrite PTree.gcombine by auto. rewrite Heqo. auto. Qed. Lemma merge_correct_1 : forall am bm k v, - get k am = Some v -> - get k (merge am bm) = Some v. - Proof. - induction am; intros; destruct k; destruct bm; try (destruct o); simpl; - try rewrite gempty in H; try discriminate; try assumption; auto. + am ! k = Some v -> + (merge am bm) ! k = Some v. + Proof using. + unfold merge; intros. rewrite PTree.gcombine by auto. + rewrite H; auto. Qed. Lemma merge_correct_2 : forall am bm k v, - get k am = None -> - get k bm = Some v -> - get k (merge am bm) = Some v. - Proof. - induction am; intros; destruct k; destruct bm; try (destruct o); simpl; - try rewrite gempty in H; try discriminate; try assumption; auto. + am ! k = None -> + bm ! k = Some v -> + (merge am bm) ! k = Some v. + Proof using. + unfold merge; intros. rewrite PTree.gcombine by auto. + rewrite H. rewrite H0. auto. Qed. Lemma merge_correct_3 : forall am bm k, - get k am = None -> - get k bm = None -> - get k (merge am bm) = None. - Proof. - induction am; intros; destruct k; destruct bm; try (destruct o); simpl; - try rewrite gempty in H; try discriminate; try assumption; auto. + am ! k = None -> + bm ! k = None -> + (merge am bm) ! k = None. + Proof using. + unfold merge; intros. rewrite PTree.gcombine by auto. + rewrite H. rewrite H0. auto. Qed. Definition merge_fold (am bm : t A) : t A := |