The Coq mailing list

[Beta Ziliani <beta AT mpi-sws.org>]

HI Ashish, unless I’m mistaken you just need to specialize the hypothesis with some a and b, right? You can do this with the specialize tactic:
specialize (H a b)
and then destruct as usual.

Best,
Beta

On Sat, Sep 26, 2020 at 11:13 AM Kumar, Ashish <azk640 AT psu.edu> wrote:

In a particular proof I was working on, I had the following hypothesis and goal:

H: forall a b, P <-> Q.
------------------
False

Context: a and b are user defined inductive types, and P and Q are propositions which use a and b.
Idea on how to prove it: Informally, the above proof holds as (for all a b, ~Q ) holds and I can supply some specific value of a and b, for which P holds. 

So using the above idea, I proved the result, using a bottom-up approach i.e. by proving the following intermediate results using 'assert'.
Proof.
assert{H1: forall a b, ~Q}. { ... }
assert{H2: P' }. { ... }  (* P' is an instance of P with specific a and b values.*)
assert(H3: ~(P' -> Q') ). { ... }
assert(H4: ~(P' <-> Q') ). {... }
unfold not in H4, apply H4; apply H. Qed.

My question is that is there some way I could have use 'destruct' on the original H, to produce variables a0, b0 and hypothesis H1: P -> Q and H2 : Q -> P, i.e. a top-down approach? If so, I could have gotten a contradiction very easily by H1 and H2. I can't use it now, as I don't have any variables in proof context to supply a and b with.

With regards,
Ashish