Stream: Coq users

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


view this post on Zulip 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)

view this post on Zulip 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.

Definition bad' : False := bad 0 I 1.

view this post on Zulip Jason Gross (Aug 16 2023 at 18:48):

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

view this post on Zulip 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.

view this post on Zulip 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