diff options
Diffstat (limited to 'src/Util/Sigma.v')
-rw-r--r-- | src/Util/Sigma.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/src/Util/Sigma.v b/src/Util/Sigma.v index a3d37d133..fc9d14d6f 100644 --- a/src/Util/Sigma.v +++ b/src/Util/Sigma.v @@ -162,3 +162,23 @@ Section ex. destruct H, u; reflexivity. Defined. End ex. + +Ltac simpl_proj_exist_in H := + repeat match type of H with + | context G[proj1_sig (exist _ ?x ?p)] + => let G' := context G[x] in change G' in H + | context G[proj2_sig (exist _ ?x ?p)] + => let G' := context G[p] in change G' in H + | context G[projT1 (existT _ ?x ?p)] + => let G' := context G[x] in change G' in H + | context G[projT2 (existT _ ?x ?p)] + => let G' := context G[p] in change G' in H + end. +Ltac inversion_sigma_step := + match goal with + | [ H : exist _ _ _ = exist _ _ _ |- _ ] + => apply path_sig_uncurried_iff in H; simpl_proj_exist_in H; destruct H + | [ H : existT _ _ _ = existT _ _ _ |- _ ] + => apply path_sigT_uncurried_iff in H; simpl_proj_exist_in H; destruct H + end. +Ltac inversion_sigma := repeat inversion_sigma_step. |