Best way to instantiate nested existential statement in Coq

Question

Suppose I have a nested existential statement H : exists ( a : A ) ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... z in the context. What is the best way instantiate H and obtain a new hypothesis H' : P a b c ... z? Doing so by repeated inversion takes a long time and leaves all the unwanted intermediate steps like H0 : exists ( b : B ) ( c : C ) ... ( z : Z ), P a b c ... z.

My previous question is very similar to this one. Maybe there's some way to use pose proof or generalize to make this one work as well.

Unknown Unknown · Accepted Answer · 2014-09-10T12:56:02

What you want to do is not called "instantiation." You can instantiate a universally quantified hypothesis and you can instantiate an existentially quantified conclusion, but not vice versa. I'm thinking the proper name is "introduction". You can introduce existential quantification in a hypothesis and you can introduce universal quantification in the conclusion. If it seems like you're "eliminating" instead, that's because, when proving something, you start at the bottom of a sequent calculus deriviation, and work your way backwards to the top.

Anyway, use the tactic firstorder. Also, use the command Set Firstorder Depth 0 to turn off proof search if you only want to simplify your goal.

If your goal has higher order elements though, you'll probably get an error message. In that case, you can use something like simplify.

Ltac simplify := repeat
  match goal with
  | h1 : False |- _ => destruct h1
  | |- True => constructor
  | h1 : True |- _ => clear h1
  | |- ~ _ => intro
  | h1 : ~ ?p1, h2 : ?p1 |- _ => destruct (h1 h2)
  | h1 : _ \/ _ |- _ => destruct h1
  | |- _ /\ _ => constructor
  | h1 : _ /\ _ |- _ => destruct h1
  | h1 : exists _, _ |- _ => destruct h1
  | |- forall _, _ => intro
  | _ : ?x1 = ?x2 |- _ => subst x2 || subst x1
  end.

Best way to instantiate nested existential statement in Coq

1 Answers