diff options
Diffstat (limited to 'src/Util/Logic.v')
-rw-r--r-- | src/Util/Logic.v | 19 |
1 files changed, 19 insertions, 0 deletions
diff --git a/src/Util/Logic.v b/src/Util/Logic.v new file mode 100644 index 000000000..d518069a9 --- /dev/null +++ b/src/Util/Logic.v @@ -0,0 +1,19 @@ +Require Import Crypto.Util.FixCoqMistakes. + +(* WHY does this solve goals that [intuition] does not solve? *) +Ltac logic := + repeat match goal with + | |- _ => intro + | H:exists _, _ |- _ => destruct H + | H:_ /\ _ |- _ => destruct H + | |- _ => solve [eauto] + | |- _ => split + end. + +Lemma exists_and_indep_l {A B} P Q : + (exists a b, P a /\ Q a b) <-> (exists a:A, P a /\ exists b:B, Q a b). +Proof. logic. Qed. + +Lemma exists_and_indep_r {A B} P Q : + (exists a b, Q a b /\ P a) <-> (exists a:A, P a /\ exists b:B, Q a b). +Proof. logic. Qed. |