From bf6a002380555cb3d690102523ec29cdde97c3b5 Mon Sep 17 00:00:00 2001 From: Yann Herklotz Date: Fri, 17 Jul 2020 21:36:16 +0100 Subject: Rename to Vericertlib --- src/common/Coquplib.v | 237 -------------------------------------------------- 1 file changed, 237 deletions(-) delete mode 100644 src/common/Coquplib.v (limited to 'src/common/Coquplib.v') diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v deleted file mode 100644 index d9176db..0000000 --- a/src/common/Coquplib.v +++ /dev/null @@ -1,237 +0,0 @@ -(* - * Vericert: Verified high-level synthesis. - * Copyright (C) 2019-2020 Yann Herklotz - * - * 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 - * the Free Software Foundation, either version 3 of the License, or - * (at your option) any later version. - * - * This program is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with this program. If not, see . - *) - -From Coq Require Export - String - ZArith - Znumtheory - List - Bool. - -Require Import Lia. - -From vericert Require Import Show. - -(* Depend on CompCert for the basic library, as they declare and prove some - useful theorems. *) -From compcert.lib Require Export Coqlib. -From compcert Require Import Integers. - -Local Open Scope Z_scope. - -(* This tactic due to Clement Pit-Claudel with some minor additions by JDP to - allow the result to be named: https://pit-claudel.fr/clement/MSc/#org96a1b5f *) -Inductive Learnt {A: Type} (a: A) := - | AlreadyKnown : Learnt a. - -Ltac learn_tac fact name := - lazymatch goal with - | [ H: Learnt fact |- _ ] => - fail 0 "fact" fact "has already been learnt" - | _ => let type := type of fact in - lazymatch goal with - | [ H: @Learnt type _ |- _ ] => - fail 0 "fact" fact "of type" type "was already learnt through" H - | _ => let learnt := fresh "Learn" in - pose proof (AlreadyKnown fact) as learnt; pose proof fact as name - end - end. - -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 unfold_rec c := unfold c; fold c. - -Ltac solve_by_inverts n := - match goal with | H : ?T |- _ => - match type of T with Prop => - inversion H; - match n with S (S (?n')) => subst; try constructor; solve_by_inverts (S n') end - end - end. - -Ltac solve_by_invert := solve_by_inverts 1. - -Ltac invert x := inversion x; subst; clear x. - -Ltac destruct_match := - match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end. - -Ltac nicify_hypotheses := - repeat match goal with - | [ H : ex _ |- _ ] => invert H - | [ H : Some _ = Some _ |- _ ] => invert H - | [ H : ?x = ?x |- _ ] => clear H - | [ H : _ /\ _ |- _ ] => invert H - end. - -Ltac nicify_goals := - repeat match goal with - | [ |- _ /\ _ ] => split - | [ |- Some _ = Some _ ] => f_equal - | [ |- S _ = S _ ] => f_equal - end. - -Ltac kill_bools := - repeat match goal with - | [ H : _ && _ = true |- _ ] => apply andb_prop in H - | [ H : _ || _ = false |- _ ] => apply orb_false_elim in H - - | [ H : _ <=? _ = true |- _ ] => apply Z.leb_le in H - | [ H : _ <=? _ = false |- _ ] => apply Z.leb_gt in H - | [ H : _ apply Z.ltb_lt in H - | [ H : _ apply Z.ltb_ge in H - | [ H : _ >=? _ = _ |- _ ] => rewrite Z.geb_leb in H - | [ H : _ >? _ = _ |- _ ] => rewrite Z.gtb_ltb in H - - | [ H : _ =? _ = true |- _ ] => apply Z.eqb_eq in H - | [ H : _ =? _ = false |- _ ] => apply Z.eqb_neq in H - end. - -Ltac unfold_constants := - repeat match goal with - | [ |- context[Integers.Ptrofs.modulus] ] => - replace Integers.Ptrofs.modulus with 4294967296 by reflexivity - | [ H : context[Integers.Ptrofs.modulus] |- _ ] => - replace Integers.Ptrofs.modulus with 4294967296 in H by reflexivity - - | [ |- context[Integers.Ptrofs.min_signed] ] => - replace Integers.Ptrofs.min_signed with (-2147483648) by reflexivity - | [ H : context[Integers.Ptrofs.min_signed] |- _ ] => - replace Integers.Ptrofs.min_signed with (-2147483648) in H by reflexivity - - | [ |- context[Integers.Ptrofs.max_signed] ] => - replace Integers.Ptrofs.max_signed with 2147483647 by reflexivity - | [ H : context[Integers.Ptrofs.max_signed] |- _ ] => - replace Integers.Ptrofs.max_signed with 2147483647 in H by reflexivity - - | [ |- context[Integers.Ptrofs.max_unsigned] ] => - replace Integers.Ptrofs.max_unsigned with 4294967295 by reflexivity - | [ H : context[Integers.Ptrofs.max_unsigned] |- _ ] => - replace Integers.Ptrofs.max_unsigned with 4294967295 in H by reflexivity - - | [ |- context[Integers.Int.modulus] ] => - replace Integers.Int.modulus with 4294967296 by reflexivity - | [ H : context[Integers.Int.modulus] |- _ ] => - replace Integers.Int.modulus with 4294967296 in H by reflexivity - - | [ |- context[Integers.Int.min_signed] ] => - replace Integers.Int.min_signed with (-2147483648) by reflexivity - | [ H : context[Integers.Int.min_signed] |- _ ] => - replace Integers.Int.min_signed with (-2147483648) in H by reflexivity - - | [ |- context[Integers.Int.max_signed] ] => - replace Integers.Int.max_signed with 2147483647 by reflexivity - | [ H : context[Integers.Int.max_signed] |- _ ] => - replace Integers.Int.max_signed with 2147483647 in H by reflexivity - - | [ |- context[Integers.Int.max_unsigned] ] => - replace Integers.Int.max_unsigned with 4294967295 by reflexivity - | [ H : context[Integers.Int.max_unsigned] |- _ ] => - replace Integers.Int.max_unsigned with 4294967295 in H by reflexivity - - | [ |- context[Integers.Ptrofs.unsigned (Integers.Ptrofs.repr ?x) ] ] => - match (eval compute in (0 <=? x)) with - | true => replace (Integers.Ptrofs.unsigned (Integers.Ptrofs.repr x)) - with x by reflexivity - | false => idtac - end - end. - -Ltac substpp := - repeat match goal with - | [ H1 : ?x = Some _, H2 : ?x = Some _ |- _ ] => - let EQ := fresh "EQ" in - learn H1 as EQ; rewrite H2 in EQ; invert EQ - | _ => idtac - end. - -Ltac simplify := intros; unfold_constants; simpl in *; - repeat (nicify_hypotheses; nicify_goals; kill_bools; substpp); - simpl in *. - -Infix "==nat" := eq_nat_dec (no associativity, at level 50). -Infix "==Z" := Z.eq_dec (no associativity, at level 50). - -Ltac liapp := - repeat match goal with - | [ |- (?x | ?y) ] => - match (eval compute in (Z.rem y x ==Z 0)) with - | left _ => - let q := (eval compute in (Z.div y x)) - in exists q; reflexivity - | _ => idtac - end - | _ => idtac - end. - -Ltac crush := simplify; try discriminate; try congruence; try lia; liapp; try assumption. - -Global Opaque Nat.div. -Global Opaque Z.mul. - -(* Definition const (A B : Type) (a : A) (b : B) : A := a. - -Definition compose (A B C : Type) (f : B -> C) (g : A -> B) (x : A) : C := f (g x). *) - -Module Option. - -Definition default {T : Type} (x : T) (u : option T) : T := - match u with - | Some y => y - | _ => x - end. - -Definition map {S : Type} {T : Type} (f : S -> T) (u : option S) : option T := - match u with - | Some y => Some (f y) - | _ => None - end. - -Definition liftA2 {T : Type} (f : T -> T -> T) (a : option T) (b : option T) : option T := - match a with - | Some x => map (f x) b - | _ => None - end. - -Definition bind {A B : Type} (f : option A) (g : A -> option B) : option B := - match f with - | Some a => g a - | _ => None - end. - -Definition join {A : Type} (a : option (option A)) : option A := - match a with - | None => None - | Some a' => a' - 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). -End Notation. - -End Option. - -Parameter debug_print : string -> unit. - -Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : B := - let unused := debug_print (show a) in b. - -Definition debug_show_msg {A B : Type} `{Show A} (s : string) (a : A) (b : B) : B := - let unused := debug_print (s ++ show a) in b. -- cgit