From f02b7b9a3879781ae332e4a967f605d961210000 Mon Sep 17 00:00:00 2001
From: James Pollard <james@pollard.dev>
Date: Tue, 30 Jun 2020 20:18:18 +0100
Subject: Heavy automation of proofs.

---
 src/common/Coquplib.v | 9 ++++++++-
 1 file changed, 8 insertions(+), 1 deletion(-)

(limited to 'src/common')

diff --git a/src/common/Coquplib.v b/src/common/Coquplib.v
index 5de1e7c..ba0a5dc 100644
--- a/src/common/Coquplib.v
+++ b/src/common/Coquplib.v
@@ -51,6 +51,13 @@ Ltac clear_obvious :=
          | [ H : _ /\ _ |- _ ] => invert H
          end.
 
+Ltac nicify_goals :=
+  repeat match goal with
+         | [ |- _ /\ _ ] => split
+         | [ |- Some _ = Some _ ] => try reflexivity
+         | [ _ : ?x |- ?x ] => assumption
+         end.
+
 Ltac kill_bools :=
   repeat match goal with
          | [ H : _ && _ = true |- _ ] => apply andb_prop in H
@@ -118,7 +125,7 @@ Ltac unfold_constants :=
          end.
 
 Ltac simplify := unfold_constants; simpl in *;
-                 repeat (clear_obvious; kill_bools);
+                 repeat (clear_obvious; nicify_goals; kill_bools);
                  simpl in *; try discriminate.
 
 Global Opaque Nat.div.
-- 
cgit