Can any one help me how to prove this theorem in Coq

Link:: https://stackoverflow.com/q/69540976

Display all goals and responses

Question

This is the first part of my code:

Parameter D: Set.
Parameter x: D.
Parameter y: D.
Parameter R: D->Prop.

Lemma b: ~(exists x:D, ~ R x)->(forall y:D, R y).~ (exists x : D, ~ R x) -> forall y : D, R y

I have worked on it for quite a long time, but it seems that I cannot use the left part of the implication well.

Can anyone help me figure out how to write the rest of of the code?

Answer

Your question is a bit vague, as you don't specify what D and R are, and where you are stuck in your proof. Try providing a minimal working example, with an explicit fail tactic for where you're stuck in the proof.

In classical logic (the one you're use to in maths), as you have the excluded middle rule, you can always do a case analysis on whether something is true or false. In vanilla Coq, built for intuitionistic logic, it's not the case. Your result is actually not provable if the predicate R is not decidable (if it's not either true or false on every input : forall (x:D), R x \/ ~R x), if the type D is not empty.

Try adding the decidability of R as an hypothesis and reprove it. It should follow more or less this structure (the key being the case analysis on whether (R y) is true or false):

Lemma yourGoal :
  (forall x, R x \/ ~ R x) -> (* Decidability of R *)
  ~ (exists x, ~ R x) -> forall y, R y.(forall x : D, R x \/ ~ R x) ->
~ (exists x : D, ~ R x) -> forall y : D, R y
Proof.(forall x : D, R x \/ ~ R x) ->
~ (exists x : D, ~ R x) -> forall y : D, R y
  intros Hdec Hex y. (* naming the hypothesis for convenience *)Hdec: forall x : D, R x \/ ~ R x
Hex: ~ (exists x : D, ~ R x)
y: D
R y
  specialize (Hdec y).y: D
Hdec: R y \/ ~ R y
Hex: ~ (exists x : D, ~ R x)
R y
  (* case analysis, creates two goals *)
  destruct Hdec as [H_Ry_is_true | H_Ry_is_false].y: D
H_Ry_is_true: R y
Hex: ~ (exists x : D, ~ R x)
R y
y: D
H_Ry_is_false: ~ R y
Hex: ~ (exists x : D, ~ R x)
R y
  + (* (R y) is true, which is our goal. *)y: D
H_Ry_is_true: R y
Hex: ~ (exists x : D, ~ R x)
R y
    assumption.
  + (* (R y) is false, which contradicts Hex *)y: D
H_Ry_is_false: ~ R y
Hex: ~ (exists x : D, ~ R x)
R y
    exfalso. (* transform your goal into False *)y: D
H_Ry_is_false: ~ R y
Hex: ~ (exists x : D, ~ R x)
False
    apply Hex.y: D
H_Ry_is_false: ~ R y
Hex: ~ (exists x : D, ~ R x)
exists x : D, ~ R x
    (* should be easy from here, using the [exists] tactic *)
    now exists y.
Qed.

PS: this exact result (and its link with excluded middle) is mentioned in Software foundations, which is a great resource to learn Coq and logic: https://softwarefoundations.cis.upenn.edu/lf-current/Logic.html#not_exists_dist