## Stream: Coq users

### Topic: Proving ∀ n : nat, P n → ∀ n0 : nat, P n0?

#### Ricardo Almeida (Aug 16 2023 at 18:38):

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)

#### Gaëtan Gilbert (Aug 16 2023 at 18:47):

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.

``````

#### Jason Gross (Aug 16 2023 at 18:48):

Perhaps you meant `(∀ n : nat, P n) → ∀ n0 : nat, P n0`, which is provable by `auto`?

#### Paolo Giarrusso (Aug 16 2023 at 19:00):

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.

#### Ricardo Almeida (Aug 16 2023 at 19:09):

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