diff options
Diffstat (limited to 'src/common/Coquplib.v')
-rw-r--r-- | src/common/Coquplib.v | 60 |
1 files changed, 54 insertions, 6 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index c9361c2..469eddc 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -32,6 +32,29 @@ From coqup Require Import Show. 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 := @@ -49,10 +72,11 @@ Ltac invert x := inversion x; subst; clear x. Ltac destruct_match := match goal with | [ |- context[match ?x with | _ => _ end ] ] => destruct x end. -Ltac clear_obvious := +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. @@ -129,16 +153,38 @@ Ltac unfold_constants := end end. -Ltac crush := intros; unfold_constants; simpl in *; - repeat (clear_obvious; nicify_goals; kill_bools); - simpl in *; try discriminate; try congruence; try lia; try assumption. +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. -Global Opaque Nat.div. -Global Opaque Z.mul. +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). *) @@ -189,3 +235,5 @@ Definition debug_show {A B : Type} `{Show A} (a : A) (b : B) : 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. + +Notation "f $ x" := (f x) (at level 60, right associativity, only parsing). |