Use of contradiction tactic

Using Coq
1

Hi all, I am working on the following proof (independently of the meaning):

Section Property.

Hypothesis Helper: forall A, A \/ ~A.
Hypothesis Hypn : exists n : nat, True.
Variable P : nat -> Prop.

Theorem test : exists n : nat, (P n -> forall m : nat, P m).
Proof.
  destruct Hypn as [n T].
  exists n. 
  assert (H : (P n -> forall m : nat, P m) \/ ~(P n -> forall m : nat, P m)).
  { apply Helper. }
  destruct H as [H1 | H2].
  + exact H1.
  + 
Admitted.

End Property.

In the second bullet of the destruct Hex, I can clearly see a contradiction between my hypothesis H2 and the goal, unfortunately I don’t know how to proceed to conclude the proof (still a beginner sorry).
Any help please (or explanation on the way to solve it).
Thanks!

2

Contradiction between hypothesis and goal just means the goal is false, with the extreme example Lemma foo (H:True) : False.

To make progress using contradiction it must be between hypotheses with the goal being irrelevant (since contradiction proves anything).

3

Okay I understand, this means that this case here cannot be proven right? (just confirming to rework my theorem) -I did not write all hypothesis-

H2 : (P n -> forall m : nat, P m) -> False 
---------------------
P n -> forall m : nat, P m

Thanks.

4

yes

word filler word filler

1 Like
5

For future people who might find it helpful, here is how I solved it, it was not the theorem, just a trick in the proof to get the contradiction.

Theorem test : exists n : nat, (P n -> forall m : nat, P m).
Proof.
  destruct Hypn as [n T].
  assert (Hn : (forall z : nat, P z) \/ ~((forall z : nat, P z))).
  { apply Helper. }
  destruct Hn as [H1 | H2].
  - exists n.
    intros _.
    exact H1.
  - assert (Hz : exists z, ~P z).
  {
    apply not_all_ex_not. 
    exact H2.
  }
  destruct Hz as [z H_not_z].
  exists z.
  intros Hz.
  contradiction.
  Qed.

Thanks for the help!

6

The Drinker’s paradox…

1 Like