The Coq mailing list

["jonikelee AT gmail.com" <jonikelee AT gmail.com>]

If the question is whether Coq can supply actual instantiations of a and
b instead of evars (holes), the problem is that those type(s) might not
be inhabited.  Note that if either the type of a or b is not inhabited,
then there is no proof of False, as H is never contradictory in that
case.

On Sat, 26 Sep 2020 14:12:54 +0000
"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
> 
>