diff options
author | James Pollard <james@pollard.dev> | 2020-07-01 20:09:15 +0100 |
---|---|---|
committer | James Pollard <james@pollard.dev> | 2020-07-01 20:09:15 +0100 |
commit | 0e0c64bf93f33044d299bfd5456d9a6b00992a0d (patch) | |
tree | 59289787f1e1520f39e666583207b5c3ff60322a /src/common/Coquplib.v | |
parent | 24b07d3b719072482f609954f584232534ed93eb (diff) | |
download | vericert-kvx-0e0c64bf93f33044d299bfd5456d9a6b00992a0d.tar.gz vericert-kvx-0e0c64bf93f33044d299bfd5456d9a6b00992a0d.zip |
Improve (?) automation.
Diffstat (limited to 'src/common/Coquplib.v')
-rw-r--r-- | src/common/Coquplib.v | 19 |
1 files changed, 12 insertions, 7 deletions
diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v index ba0a5dc..c9361c2 100644 --- a/src/common/Coquplib.v +++ b/src/common/Coquplib.v @@ -23,12 +23,14 @@ From Coq Require Export List Bool. +Require Import Lia. + From coqup 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 Integers. +From compcert Require Import Integers. Ltac unfold_rec c := unfold c; fold c. @@ -44,18 +46,21 @@ 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 clear_obvious := repeat match goal with | [ H : ex _ |- _ ] => invert H - | [ H : ?C _ = ?C _ |- _ ] => invert H + | [ H : Some _ = Some _ |- _ ] => invert H | [ H : _ /\ _ |- _ ] => invert H end. Ltac nicify_goals := repeat match goal with | [ |- _ /\ _ ] => split - | [ |- Some _ = Some _ ] => try reflexivity - | [ _ : ?x |- ?x ] => assumption + | [ |- Some _ = Some _ ] => f_equal + | [ |- S _ = S _ ] => f_equal end. Ltac kill_bools := @@ -124,9 +129,9 @@ Ltac unfold_constants := end end. -Ltac simplify := unfold_constants; simpl in *; - repeat (clear_obvious; nicify_goals; kill_bools); - simpl in *; try discriminate. +Ltac crush := intros; unfold_constants; simpl in *; + repeat (clear_obvious; nicify_goals; kill_bools); + simpl in *; try discriminate; try congruence; try lia; try assumption. Global Opaque Nat.div. Global Opaque Z.mul. |