From c701e6c51faf237dfbd097a81b7a08c92ea1f242 Mon Sep 17 00:00:00 2001
From: Jason Gross <jagro@google.com>
Date: Fri, 29 Jul 2016 11:47:51 -0700
Subject: Add HProp, Isomorphism

---
 _CoqProject            |  2 ++
 src/Util/HProp.v       | 50 ++++++++++++++++++++++++++++++++++++++++++++++++++
 src/Util/Isomorphism.v |  4 ++++
 3 files changed, 56 insertions(+)
 create mode 100644 src/Util/HProp.v
 create mode 100644 src/Util/Isomorphism.v

diff --git a/_CoqProject b/_CoqProject
index ea1b1b4bf..0d45357f9 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -67,6 +67,8 @@ src/Util/Decidable.v
 src/Util/Equality.v
 src/Util/FixCoqMistakes.v
 src/Util/GlobalSettings.v
+src/Util/HProp.v
+src/Util/Isomorphism.v
 src/Util/IterAssocOp.v
 src/Util/ListUtil.v
 src/Util/NatUtil.v
diff --git a/src/Util/HProp.v b/src/Util/HProp.v
new file mode 100644
index 000000000..63de1d037
--- /dev/null
+++ b/src/Util/HProp.v
@@ -0,0 +1,50 @@
+Class IsHProp T := allpath_hprop : forall x y : T, x = y.
+
+Notation IsHPropRel R := (forall x y, IsHProp (R x y)).
+
+Ltac hprop_destruct_trivial_step :=
+  match goal with
+  | [ H : unit |- _ ] => destruct H
+  | [ H : True |- _ ] => destruct H
+  | [ H : False |- _ ] => destruct H
+  | [ H : Empty_set |- _ ] => destruct H
+  | [ H : prod _ _ |- _ ] => destruct H
+  | [ H : and _ _ |- _ ] => destruct H
+  | [ H : sigT _ |- _ ] => destruct H
+  | [ H : sig _ |- _ ] => destruct H
+  | [ H : ex _ |- _ ] => destruct H
+  | [ H : forall x y : ?A, x = y, x0 : ?A, x1 : ?A |- _ ]
+    => destruct (H x0 x1)
+  | [ H : forall a0 (x y : _), x = y, x0 : ?A, x1 : ?A |- _ ]
+    => destruct (H _ x0 x1)
+  | [ H : or _ _ |- _ ] => destruct H
+  | [ H : sum _ _ |- _ ] => destruct H
+  end.
+Ltac hprop_destruct_trivial := repeat hprop_destruct_trivial_step.
+
+Ltac pre_hprop :=
+  repeat (intros
+          || subst
+          || hprop_destruct_trivial
+          || split
+          || unfold IsHProp in *
+          || hnf ).
+
+Ltac solve_hprop_transparent_with tac :=
+  pre_hprop;
+  try solve [ reflexivity
+            | decide equality; eauto with nocore
+            | tac ].
+
+Ltac solve_hprop_transparent := solve_hprop_transparent_with fail.
+
+Local Hint Extern 0 => solve [ solve_hprop_transparent ] : typeclass_instances.
+
+Global Instance ishprop_unit : IsHProp unit. exact _. Defined.
+Global Instance ishprop_True : IsHProp True. exact _. Defined.
+Global Instance ishprop_Empty_set : IsHProp Empty_set. exact _. Defined.
+Global Instance ishprop_False : IsHProp False. exact _. Defined.
+Global Instance ishprop_prod {A B} `{IsHProp A, IsHProp B} : IsHProp (A * B). exact _. Defined.
+Global Instance ishprop_and {A B : Prop} `{IsHProp A, IsHProp B} : IsHProp (A /\ B). exact _. Defined.
+Global Instance ishprop_sigT {A P} `{IsHProp A, forall a : A, IsHProp (P a)} : IsHProp (@sigT A P). exact _. Defined.
+Global Instance ishprop_sig {A} {P : A -> Prop} `{IsHProp A, forall a : A, IsHProp (P a)} : IsHProp (@sig A P). exact _. Defined.
diff --git a/src/Util/Isomorphism.v b/src/Util/Isomorphism.v
new file mode 100644
index 000000000..a02afc3bf
--- /dev/null
+++ b/src/Util/Isomorphism.v
@@ -0,0 +1,4 @@
+Record IsIso {A B} (f : A -> B) :=
+  { iso_inv : B -> A;
+    is_right_inv : forall x, f (iso_inv x) = x;
+    is_left_inv : forall x, iso_inv (f x) = x }.
-- 
cgit v1.2.3