Rename congrunce_option to inversion_option, add [inversion_prod]

1 files changed, 70 insertions, 0 deletions

diff --git a/src/Util/Prod.v b/src/Util/Prod.v
new file mode 100644
index 000000000..599ba6a9e
--- /dev/null
+++ b/src/Util/Prod.v
@@ -0,0 +1,70 @@
+(** * Classification of the [×] Type *)
+(** In this file, we classify the basic structure of [×] types ([prod]
+    in Coq).  In particular, we classify equalities of non-dependent
+    pairs (inhabitants of [×] types), so that when we have an equality
+    between two such pairs, or when we want such an equality, we have
+    a systematic way of reducing such equalities to equalities at
+    simpler types. *)
+Require Import Crypto.Util.Equality.
+Require Import Crypto.Util.GlobalSettings.
+
+Local Arguments fst {_ _} _.
+Local Arguments snd {_ _} _.
+Local Arguments f_equal {_ _} _ {_ _} _.
+
+(** ** Equality for [prod] *)
+Section prod.
+  (** *** Projecting an equality of a pair to equality of the first components *)
+  Definition fst_path {A B} {u v : prod A B} (p : u = v)
+  : fst u = fst v
+    := f_equal fst p.
+
+  (** *** Projecting an equality of a pair to equality of the second components *)
+  Definition snd_path {A B} {u v : prod A B} (p : u = v)
+  : snd u = snd v
+    := f_equal snd p.
+
+  (** *** Equality of [prod] is itself a [prod] *)
+  Definition path_prod_uncurried {A B : Type} (u v : prod A B)
+             (pq : prod (fst u = fst v) (snd u = snd v))
+    : u = v.
+  Proof.
+    destruct u as [u1 u2], v as [v1 v2]; simpl in *.
+    destruct pq as [p q].
+    destruct p, q; simpl in *.
+    reflexivity.
+  Defined.
+
+  (** *** Curried version of proving equality of sigma types *)
+  Definition path_prod {A B : Type} (u v : prod A B)
+             (p : fst u = fst v) (q : snd u = snd v)
+    : u = v
+    := path_prod_uncurried u v (pair p q).
+
+  (** *** Equivalence of equality of [prod] with a [prod] of equality *)
+  (** We could actually use [IsIso] here, but for simplicity, we
+      don't.  If we wanted to deal with proofs of equality of × types
+      in dependent positions, we'd need it. *)
+  Definition path_prod_uncurried_iff {A P}
+             (u v : @prod A P)
+    : u = v <-> (prod (fst u = fst v) (snd u = snd v)).
+  Proof.
+    split; [ intro; subst; split; reflexivity | apply path_prod_uncurried ].
+  Defined.
+End prod.
+
+(** ** Useful Tactics *)
+(** *** [inversion_prod] *)
+Ltac simpl_proj_pair_in H :=
+  repeat match type of H with
+         | context G[fst (pair ?x ?p)]
+           => let G' := context G[x] in change G' in H
+         | context G[snd (pair ?x ?p)]
+           => let G' := context G[p] in change G' in H
+         end.
+Ltac inversion_prod_step :=
+  match goal with
+  | [ H : pair _ _ = pair _ _ |- _ ]
+    => apply path_prod_uncurried_iff in H; simpl_proj_pair_in H; destruct H
+  end.
+Ltac inversion_prod := repeat inversion_prod_step.