diff options
Diffstat (limited to 'src/common')
| -rw-r--r-- | src/common/ListExtra.v | 27 | ||||
| -rw-r--r-- | src/common/Maps.v | 50 | ||||
| -rw-r--r-- | src/common/Monad.v | 32 | ||||
| -rw-r--r-- | src/common/Statemonad.v | 8 | ||||
| -rw-r--r-- | src/common/Vericertlib.v | 54 |
5 files changed, 169 insertions, 2 deletions
diff --git a/src/common/ListExtra.v b/src/common/ListExtra.v new file mode 100644 index 0000000..6b14a50 --- /dev/null +++ b/src/common/ListExtra.v @@ -0,0 +1,27 @@ +Require Export Coq.Lists.List. + +Require Import Coq.micromega.Lia. +Require Import vericert.common.Vericertlib. + +From Hammer Require Import Tactics. + +Lemma nth_error_length : forall {A} (l : list A) n x, + nth_error l n = Some x -> (n < length l)%nat. +Proof. + induction l; intros; simpl in *. + - destruct n; crush. + - destruct n; crush. + edestruct IHl; eauto with arith. +Qed. + +Lemma length_nth_error : forall {A} (l : list A) n, + (n < length l)%nat -> exists x, nth_error l n = Some x. +Proof. + induction l; intros; simpl in *. + - lia. + - destruct n; crush; eauto with arith. +Qed. + +Lemma combine_split : forall {A B} (l : list (A * B)), + List.combine (fst (List.split l)) (snd (List.split l)) = l. +Proof. hfcrush use: split_combine unfold: fst, snd inv: prod. Qed. diff --git a/src/common/Maps.v b/src/common/Maps.v index f0f264d..3aa0b33 100644 --- a/src/common/Maps.v +++ b/src/common/Maps.v @@ -61,4 +61,54 @@ 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). +Definition filter (A: Type) (pred: PTree.elt -> A -> bool) (m: t A) : t A := + PTree.map (fun _ a => snd a) (PTree.filter1 (fun a => pred (fst a) (snd a)) (PTree.map (fun i x => (i, x)) m)). + +Theorem filter_spec: forall (A: Type) (pred: PTree.elt -> A -> bool) (m: PTree.t A) (i: PTree.elt) (x : A), + (filter pred m) ! i = + match m ! i with + | None => None + | Some x => if pred i x then Some x else None + end. +Proof. + intros. + unfold filter. + + rewrite gmap. + unfold option_map. + + rewrite gfilter1. + + rewrite gmap. + unfold option_map. + + destruct (m ! i). + - simpl. + destruct (pred i a); simpl; reflexivity. + - reflexivity. +Qed. + +Definition contains (A: Type) (i: positive) (m: t A) : bool := + match get i m with + | Some _ => true + | None => false + end. End PTree. + +Definition max_pc_map {A: Type} (m : Maps.PTree.t A) := + PTree.fold (fun m pc i => Pos.max m pc) m 1%positive. + +Lemma max_pc_map_sound: + forall A m pc i, m!pc = Some i -> Ple pc (@max_pc_map A m). +Proof. + intros until i. unfold max_pc_map. + apply PTree_Properties.fold_rec with (P := fun c m => c!pc = Some i -> Ple pc m). + (* extensionality *) + intros. apply H0. rewrite H; auto. + (* base case *) + rewrite PTree.gempty. congruence. + (* inductive case *) + intros. rewrite PTree.gsspec in H2. destruct (peq pc k). + inv H2. xomega. + apply Ple_trans with a. auto. xomega. +Qed. diff --git a/src/common/Monad.v b/src/common/Monad.v index 5e8385e..c9cdc1a 100644 --- a/src/common/Monad.v +++ b/src/common/Monad.v @@ -1,6 +1,7 @@ (* * Vericert: Verified high-level synthesis. * Copyright (C) 2020 Yann Herklotz <yann@yannherklotz.com> + * 2021 Michalis Pardalos <mpardalos@gmail.com> * * This program is free software: you can redistribute it and/or modify * it under the terms of the GNU General Public License as published by @@ -16,7 +17,8 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. *) -From Coq Require Import Lists.List. +From Coq Require Import BinNums Lists.List. +From compcert Require Import Maps. Module Type Monad. @@ -57,10 +59,38 @@ Module MonadExtra(M : Monad). ret (r::rs) end. + Definition sequence {A} : list (mon A) -> mon (list A) := traverselist (fun x => x). + + Definition traverseoption {A B: Type} (f: A -> mon B) (opt: option A) : mon (option B) := + match opt with + | None => ret None + | Some x => + do r <- f x; + ret (Some r) + end. + Fixpoint collectlist {A : Type} (f : A -> mon unit) (l : list A) {struct l} : mon unit := match l with | nil => ret tt | x::xs => do _ <- f x; collectlist f xs end. +Fixpoint xtraverse_ptree {A B : Type} (f : positive -> A -> mon B) (m : PTree.t A) (i : positive) + {struct m} : mon (PTree.t B) := + match m with + | PTree.Leaf => ret PTree.Leaf + | PTree.Node l o r => + do no <- match o with + | None => ret None + | Some x => do no <- f (PTree.prev i) x; ret (Some no) + end; + do nl <- xtraverse_ptree f l (xO i); + do nr <- xtraverse_ptree f r (xI i); + ret (PTree.Node nl no nr) + end. + +Definition traverse_ptree {A B : Type} (f : positive -> A -> mon B) m := xtraverse_ptree f m xH. + +Definition traverse_ptree1 {A B : Type} (f : A -> mon B) := traverse_ptree (fun _ => f). + End MonadExtra. diff --git a/src/common/Statemonad.v b/src/common/Statemonad.v index 16dcbbf..20558e0 100644 --- a/src/common/Statemonad.v +++ b/src/common/Statemonad.v @@ -63,6 +63,14 @@ Module Statemonad(S : State) <: Monad. | Error _ => g s end. + Definition handle_opt {A : Type} (err : Errors.errmsg) (val : option A) + : mon A := + fun s => + match val with + | Some a => OK a s (S.st_refl s) + | None => Error err + end. + Definition error {A: Type} (err: Errors.errmsg) : mon A := fun (s: S.st) => Error err. Definition get : mon S.st := fun s => OK s s (S.st_refl s). diff --git a/src/common/Vericertlib.v b/src/common/Vericertlib.v index b58ebd4..84c272b 100644 --- a/src/common/Vericertlib.v +++ b/src/common/Vericertlib.v @@ -57,6 +57,19 @@ Ltac learn_tac fact name := Tactic Notation "learn" constr(fact) := let name := fresh "H" in learn_tac fact name. Tactic Notation "learn" constr(fact) "as" simple_intropattern(name) := learn_tac fact name. +Ltac auto_apply fact := + let H' := fresh "H" in + match goal with + | H : _ |- _ => pose proof H as H'; apply fact in H' + end. + +(** Specialize all hypotheses with a forall to a specific term *) +Tactic Notation "specialize_all" constr(v) := + let t := type of v in + repeat match goal with + | [H : (forall (x: t), _) |- _ ] => learn H; destruct H with v + end. + Ltac unfold_rec c := unfold c; fold c. Ltac solve_by_inverts n := @@ -71,12 +84,30 @@ Ltac solve_by_invert := solve_by_inverts 1. Ltac invert x := inversion x; subst; clear x. +(** For a hypothesis of a forall-type, instantiate every variable to a fresh existential *) +Ltac insterU1 H := + match type of H with + | forall x : ?T, _ => + let x := fresh "x" in + evar (x : T); + let x' := eval unfold x in x in + clear x; specialize (H x') + end. + +Ltac insterU H := + repeat (insterU1 H). + Ltac destruct_match := match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x eqn:? | [ H: context[match ?x with | _ => _ end] |- _ ] => destruct x eqn:? end. +Ltac unfold_match H := + match type of H with + | context[match ?g with _ => _ end] => destruct g eqn:?; try discriminate + end. + Ltac auto_destruct x := destruct x eqn:?; simpl in *; try discriminate; try congruence. Ltac nicify_hypotheses := @@ -187,9 +218,21 @@ Ltac liapp := | _ => idtac end. -Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; +Ltac plia := solve [ unfold Ple in *; lia ]. + +Ltac crush := simplify; try discriminate; try congruence; try plia; liapp; try assumption; try (solve [auto]). +Ltac crush_trans := + match goal with + | [ H : ?g = ?inter |- ?g = _ ] => transitivity inter; crush + | [ H : ?inter = ?g |- ?g = _ ] => transitivity inter; crush + | [ H : ?g = ?inter |- _ = ?g ] => transitivity inter; crush + | [ H : ?inter = ?g |- _ = ?g ] => transitivity inter; crush + end. + +Ltac maybe t := t + idtac. + Global Opaque Nat.div. Global Opaque Z.mul. @@ -229,6 +272,15 @@ Definition join {A : Type} (a : option (option A)) : option A := | Some a' => a' end. +Fixpoint map_option {A B : Type} (f : A -> option B) (l : list A) : list B := + match l with + | nil => nil + | x::xs => match f x with + | None => map_option f xs + | Some x' => x'::map_option f xs + end + end. + Module Notation. Notation "'do' X <- A ; B" := (bind A (fun X => B)) (at level 200, X ident, A at level 100, B at level 200). |