Coq transform does not exist for forall operator

Question

Coq transform does not exist for forall operator

I am new to Coq. Here is my problem. I have an expression:

H : forall x : term, ~ (exists y : term, P x y /\ ~ P y x)

I think this is equivalent to:

forall x y : term, (P x y /\ ~ P y x) -> false

But what tactics can I use to transform a hypothesis?

0

forall coq

Pika 08 Feb '14 at 9:35

source to share

2 answers

You can use unfold not at 1 in H

. ~ P

is just a notation for not P

and not P = (P -> False)

by definition. Part at 1

means you only want the unfold

first occurrence not

, and part in H

means you only want that unfold

in a hypothesis H

.

0

user1861759 08 Feb 14 at 14:17

source to share

nobody · Accepted Answer · 2014-02-11T01:08:06+0000

I do not know how tactics turn into not will, but you can always just assert

prove it. (If you need it many times, you can package it in a tactical definitionLtac

or a simple theorem [1].)

Here are three ways to accomplish this. (You should just copy / paste this transcript into CoqIDE or Emacs / ProofGeneral and run the code.)

[1] There Coq.Logic.Classical_Pred_Type

is a lemma in the library not_ex_all_not

, but loading will pull the axiom for classical logic (which is not even required here).

(* dummy context to set up H of the correct type, for testing it out *)
Lemma SomeName (term : Type) (P : term -> term -> Prop) :
  (forall x : term, ~ (exists (y : term), P x y /\ ~ P y x)) ->
  True. (* dummy goal *)
Proof.
  intro H.
  (* end dummy context *)

(*

Here's a long version with some clarification: *)

  (* this states the goal, result will be put into the context as H' *)
  assert (forall (x y : term), (P x y /\ ~ P y x) -> False) as H'.
    (* get rid of unneeded variables in context, get new args *)
    clear - H; intros x y Pxy.
    (* unfolding the not shows the computational structure of this *)
    unfold not at 1 in H.
    (* yay... (x, y, Pxy) will produce False via H *)
    (* specialize to x and apply... *)
    apply (H x).
    (* ...and provide the witness. *)
    exists y.  exact Pxy.
    (* done. *)

  (* let do it again... *)
  clear H'.

(*

you can also do it in one expression: *)

  assert (forall x y, (P x y /\ ~ P y x) -> False) as H'
    by (clear -H; intros x y Pxy; apply (H x (ex_intro _ y Pxy))).

  (* and again... *)
  clear H'.

(*

Simple things like this can also be written by hand: *)

  pose proof (fun x y Pxy => H x (ex_intro _ y Pxy)) as H'; simpl in H'.

(*

you now have H 'of the correct type; it is not necessary to get rid of the old H:*)

  clear H; rename H' into H.

Coq transform does not exist for forall operator

More articles: