From c2ba535604cef5bc86369512e6f3c2833753a55a Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Wed, 2 Mar 2022 18:06:18 +0000 Subject: Update Coq version to 8.14.1 --- src/common/Maps.v | 3 +- src/common/Show.v | 30 +++++++------------ src/common/ZExtra.v | 18 ----------- src/hls/AssocMap.v | 86 ++++++++++++++++++++++++++++++----------------------- 4 files changed, 61 insertions(+), 76 deletions(-) (limited to 'src') diff --git a/src/common/Maps.v b/src/common/Maps.v index f0f264d..13ca276 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -17,7 +17,7 @@ * along with this program. If not, see . *) -Set Implicit Arguments. +(*Set Implicit Arguments. Require Export compcert.lib.Maps. @@ -62,3 +62,4 @@ Definition traverse (A B : Type) (f : positive -> A -> res B) m := xtraverse f m Definition traverse1 (A B : Type) (f : A -> res B) := traverse (fun _ => f). End PTree. +*) diff --git a/src/common/Show.v b/src/common/Show.v index 4c66725..20c07e7 100644 --- a/src/common/Show.v +++ b/src/common/Show.v @@ -1,4 +1,4 @@ -(* +(* * Vericert: Verified high-level synthesis. * Copyright (C) 2019-2020 Yann Herklotz * @@ -24,15 +24,11 @@ From Coq Require Import Local Open Scope string. -Class Show A : Type := - { - show : A -> string - }. +Class Show A : Type := { show : A -> string }. +#[export] Instance showBool : Show bool := - { - show := fun b:bool => if b then "true" else "false" - }. + { show := fun b:bool => if b then "true" else "false" }. Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string := let d := match n mod 10 with @@ -52,17 +48,11 @@ Fixpoint string_of_nat_aux (time n : nat) (acc : string) : string := Definition string_of_nat (n : nat) : string := string_of_nat_aux n n "". -Instance showNat : Show nat := - { - show := string_of_nat - }. +#[export] +Instance showNat : Show nat := { show := string_of_nat }. -Instance showZ : Show Z := - { - show a := show (Z.to_nat a) - }. +#[export] +Instance showZ : Show Z := { show a := show (Z.to_nat a) }. -Instance showPositive : Show positive := - { - show a := show (Zpos a) - }. +#[export] +Instance showPositive : Show positive := { show a := show (Zpos a) }. diff --git a/src/common/ZExtra.v b/src/common/ZExtra.v index 62ca54d..3a27cc6 100644 --- a/src/common/ZExtra.v +++ b/src/common/ZExtra.v @@ -45,12 +45,6 @@ Proof. - apply Z.mod_divide; assumption. Qed. -Lemma mod_0_r: forall (m: Z), - m mod 0 = 0. -Proof. - intros. destruct m; reflexivity. -Qed. - Lemma sub_mod_0: forall (a b m: Z), a mod m = 0 -> b mod m = 0 -> @@ -89,18 +83,6 @@ Proof. reflexivity. Qed. -Lemma mod_pow2_same_cases: forall a n, - a mod 2 ^ n = a -> - 2 ^ n = 0 /\ a = 0 \/ 0 <= a < 2 ^ n. -Proof. - intros. - assert (n < 0 \/ 0 <= n) as C by lia. destruct C as [C | C]. - - left. rewrite (Z.pow_neg_r 2 n C) in *. rewrite mod_0_r in H. auto. - - right. - rewrite <- H. apply Z.mod_pos_bound. - apply Z.pow_pos_nonneg; lia. -Qed. - Lemma mod_pow2_same_bounds: forall a n, a mod 2 ^ n = a -> 0 <= n -> 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 := -- cgit