Merge branch 'vcoq86' into vcoq87

aa755 · Jan 30, 2018 · 1636d75 · 1636d75
2 parents 0d05e8d + 10bf25c
commit 1636d75
Show file tree

Hide file tree

Showing 7 changed files with 791 additions and 17 deletions.
diff --git a/UsefulTypes.v b/UsefulTypes.v
@@ -765,3 +765,16 @@ Definition pairMapl {A B A2:Type} (f: A-> A2) (p:A*B) : A2*B :=
 
 Definition pairMapr {A B B2:Type} (f: B-> B2) (p:A*B) : A*B2 :=
   let (a,b) := p in (a, f b).
+
+
+Ltac destructDecideP :=
+  match goal with
+    [ |-  context [@decideP ?p ?d] ] => destruct (@decideP p d)
+  end.
+
+Lemma rewritePairMatch {A B C:Type} (p:A*B)
+(f : A->B->C):
+(let (a,b) := p in f a b) = f (fst p) (snd p).
+Proof using.
+  destruct p; auto.
+Qed.