aboutsummaryrefslogtreecommitdiff
path: root/src/Util/Equality.v
diff options
context:
space:
mode:
authorJason Gross <jagro@google.com>2016-07-29 11:56:08 -0700
committerJason Gross <jagro@google.com>2016-07-29 11:56:08 -0700
commit8cdbaf69e02f5784b392adb99abc89d2be663ad2 (patch)
tree36b06933c23138defe0b7af5ded488a56aa5b838 /src/Util/Equality.v
parentf4e85257de36e77fa45f1e60e4cfea8b3378f4f8 (diff)
Add a lemma about hprop and eq
Diffstat (limited to 'src/Util/Equality.v')
-rw-r--r--src/Util/Equality.v53
1 files changed, 53 insertions, 0 deletions
diff --git a/src/Util/Equality.v b/src/Util/Equality.v
index 1ff76a009..733b145c6 100644
--- a/src/Util/Equality.v
+++ b/src/Util/Equality.v
@@ -1,4 +1,6 @@
(** * Lemmas about [eq] *)
+Require Import Crypto.Util.Isomorphism.
+Require Import Crypto.Util.HProp.
Definition concat_1p {A x y} (p : x = y :> A) : eq_trans eq_refl p = p.
Proof. case p; reflexivity. Defined.
@@ -23,3 +25,54 @@ Proof. case q; case p; reflexivity. Defined.
Lemma inv_V {A x y} (p : x = y :> A)
: eq_sym (eq_sym p) = p.
Proof. case p; reflexivity. Defined.
+
+Section gen.
+ Context {A : Type} {x : A} (code : A -> Type)
+ (encode : forall y, x = y -> code y)
+ {code_hprop : IsHProp { a : A & code a } }.
+
+ Definition decode' {y} (p : code y) : x = y
+ := f_equal (@projT1 _ _) (code_hprop (existT _ x (encode x eq_refl)) (existT _ y p)).
+
+ Definition decode {y} (H : code y) : x = y
+ := eq_trans (eq_sym (decode' (encode x eq_refl))) (decode' H).
+
+ Definition deencode {y} (H : x = y) : decode (encode y H) = H.
+ Proof.
+ destruct H.
+ unfold decode.
+ edestruct decode'.
+ reflexivity.
+ Defined.
+
+ Global Instance isiso_encode {y} : IsIso (encode y).
+ Proof.
+ exists (@decode y).
+ { intro H.
+ unfold decode.
+ set (yH := (existT _ y H)).
+ change H with (projT2 yH).
+ change y with (projT1 yH).
+ clearbody yH; clear y H.
+ destruct (code_hprop (existT _ x (encode x eq_refl)) yH); simpl.
+ abstract (rewrite concat_Vp; reflexivity). }
+ { intro p.
+ apply deencode. }
+ Defined.
+End gen.
+
+Section hprop.
+ Context {A} `{IsHProp A}.
+
+ Let hprop_encode {x y : A} (p : x = y) : unit := tt.
+
+ Local Hint Resolve (fun x => @isiso_encode A x (fun _ => unit)) : typeclass_instances.
+
+ Global Instance ishprop_path_hprop : IsHPropRel (@eq A).
+ Proof.
+ intros x y p q.
+ pose proof (is_left_inv (@hprop_encode x y)) as H'.
+ rewrite <- (H' p), <- (H' q).
+ apply f_equal, allpath_hprop.
+ Qed.
+End hprop.