Automatically choose an assumption from local context

user_1056174 0
Viewed 60

I have a proof script with a section that looks like this:

  - destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence.
  - destruct (IHx1 _ _ H6). congruence.
  - destruct (IHx1 _ _ H3). subst. destruct (IHx2 _ _ H7). congruence.
  - destruct (IHx1 _ _ H6). congruence.
  - destruct (IHx  _ _ H2). congruence.
  - destruct (IHx  _ _ H5). congruence.
  - destruct (IHx  _ _ H2). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H8). congruence.
  - destruct (IHx  _ _ H7). congruence.
  - destruct (IHx  _ _ H4). congruence.
  - destruct (IHx1 _ _ H8). congruence.
  - destruct (IHx1 _ _ H5). subst. destruct (IHx2 _ _ H9).

It seems like it would be a choice candidate for using ; to solve cleanly, unfortunately the hypotheses are all over the place. How can I collapse the various sub-proofs together?

coq-tactic coq
1 Answers
Related