Possibly a silly question, but can you prove in just a couple of tactics `∀ n : nat, P n → ∀ n0 : nat, P n0`

? It's the name difference between `n`

and `n0`

that's slowing me down. (it's not important what `P`

is here)

it's not important what P is here

but it's not true for all P

```
Definition P n := match n with 0 => True | S _ => False end.
Axiom bad : forall n : nat, P n -> forall n0 : nat, P n0.
Definition bad' : False := bad 0 I 1.
```

Perhaps you meant `(∀ n : nat, P n) → ∀ n0 : nat, P n0`

, which is provable by `auto`

?

another way to see why this isn't provable: the original statement is equivalent to `((∃ n : nat, P n) → ∀ n0 : nat, P n0)`

: that's more clearly false, the only reason this is false is the difference between `n`

and `n0`

, _and_ the equivalence is easy to show:

```
From Coq Require Import Utf8.
Definition V1 (P : nat -> Prop) := ∀ n : nat, (P n → (∀ n0 : nat, P n0)).
Definition V2 (P : nat -> Prop) := (∃ n : nat, P n) → (∀ n0 : nat, P n0).
Lemma nope P :
V1 P ↔ V2 P.
Proof.
Succeed firstorder.
unfold V1, V2; split.
- intros HV1 [n HPn] n0. apply (HV1 n HPn n0).
- intros HV2 n Hpn n0. apply HV2. exists n. apply Hpn.
Qed.
```

as that proof show, `V1 P`

and `V2 P`

take the same arguments `n : nat`

and `HPn : P n`

— but `V2`

takes them as a kind-of pair `∃ n : nat, P n`

, while `V1`

is a "curried" statement that takes them separately.

Indeed. I was reading the goal as if the `(`

and `)`

were there and trying `auto`

on it. Thanks.

Last updated: Jun 13 2024 at 19:02 UTC