diff options
Diffstat (limited to 'contrib/subtac/Heq.v')
-rw-r--r-- | contrib/subtac/Heq.v | 34 |
1 files changed, 34 insertions, 0 deletions
diff --git a/contrib/subtac/Heq.v b/contrib/subtac/Heq.v new file mode 100644 index 00000000..f2b216d9 --- /dev/null +++ b/contrib/subtac/Heq.v @@ -0,0 +1,34 @@ +Require Export JMeq. + +(** Notation for heterogenous equality. *) + +Notation " [ x : X ] = [ y : Y ] " := (@JMeq X x Y y) (at level 0, X at next level, Y at next level). + +(** Do something on an heterogeneous equality appearing in the context. *) + +Ltac on_JMeq tac := + match goal with + | [ H : @JMeq ?x ?X ?y ?Y |- _ ] => tac H + end. + +(** Try to apply [JMeq_eq] to get back a regular equality when the two types are equal. *) + +Ltac simpl_one_JMeq := + on_JMeq + ltac:(fun H => let H' := fresh "H" in + assert (H' := JMeq_eq H) ; clear H ; rename H' into H). + +(** Repeat it for every possible hypothesis. *) + +Ltac simpl_JMeq := repeat simpl_one_JMeq. + +(** Just simplify an h.eq. without clearing it. *) + +Ltac simpl_one_dep_JMeq := + on_JMeq + ltac:(fun H => let H' := fresh "H" in + assert (H' := JMeq_eq H)). + + + + |