diff options
| -rw-r--r-- | _CoqProject | 1 | ||||
| -rw-r--r-- | src/Util/Option.v | 16 | ||||
| -rw-r--r-- | src/Util/Prod.v | 70 |
3 files changed, 80 insertions, 7 deletions
diff --git a/_CoqProject b/_CoqProject index 40804dcd9..7dcfb9728 100644 --- a/_CoqProject +++ b/_CoqProject @@ -89,6 +89,7 @@ src/Util/NatUtil.v src/Util/Notations.v src/Util/NumTheoryUtil.v src/Util/Option.v +src/Util/Prod.v src/Util/Sigma.v src/Util/Sum.v src/Util/Tactics.v diff --git a/src/Util/Option.v b/src/Util/Option.v index 86e9a6d4f..4868c1f62 100644 --- a/src/Util/Option.v +++ b/src/Util/Option.v @@ -70,10 +70,12 @@ Definition option_eq {A} eq (x y : option A) := end end. -Ltac congruence_option := - repeat match goal with - | [ H : Some _ = Some _ |- _ ] => inversion H; clear H - | [ H : None = Some _ |- _ ] => solve [ inversion H ] - | [ H : Some _ = None |- _ ] => solve [ inversion H ] - | [ H : None = None |- _ ] => clear H - end. +Ltac inversion_option_step := + match goal with + | [ H : Some _ = Some _ |- _ ] => inversion H; clear H + | [ H : None = Some _ |- _ ] => solve [ inversion H ] + | [ H : Some _ = None |- _ ] => solve [ inversion H ] + | [ H : None = None |- _ ] => clear H + end. + +Ltac inversion_option := repeat inversion_option_step. 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. |