neg.v

Require Import Classical.

Class Neg (P:Prop) :=
  { neg : Prop;
    neg_ok : ~ P -> neg }.

Arguments neg P {_}.
Arguments neg_ok P {_} _.

Lemma neg_right (A B:Prop) `{!Neg A} : (neg A -> B) -> A \/ B.
Proof.
  intros H;destruct (classic A).
  - left;assumption.
  - right. apply H, neg_ok. assumption.
Qed.

Instance neg_default P : Neg P | 10 := { neg := ~ P; neg_ok := id }.

Instance neg_not P : Neg (~ P) := { neg := P; neg_ok := NNPP _ }.

Lemma test1 (A B:Prop) (H : A -> B) : ~ A \/ B.
Proof.
  refine (neg_right _ _ _).
  simpl. (* TODO make some tactic to do the refine + simpl *)
  exact H.
Qed.

Instance neg_arrow (A B : Prop) `{!Neg B} : Neg (A -> B)
  := { neg := A /\ neg B }.
Proof.
  intros N.
  apply imply_to_and in N.
  destruct N;split;[|apply neg_ok];assumption.
Defined.

(* Give it a bit less priority than neg_arrow *)
Instance neg_forall A (B:A -> Prop) `{!forall x:A, Neg (B x)} : Neg (forall x, B x) | 2
  := { neg := exists x, neg (B x) }.
Proof.
  intros N.
  apply not_all_ex_not in N. destruct N as [x N].
  exists x. apply neg_ok, N.
Defined.

Instance neg_and A B `{!Neg A} `{!Neg B} : Neg (A /\ B)
  := { neg := neg A \/ neg B }.
Proof.
  intros N.
  apply not_and_or in N.
  destruct N;[left|right];apply neg_ok;assumption.
Defined.

Lemma test2 : forall A B, (forall x, x=0 -> ~A/\~B) \/ A.
Proof.
  intros.
  refine (neg_right _ _ _).
  simpl. (* (exists x : nat, x = 0 /\ (A \/ B)) -> A *)
Abort.