Stream: Coq users

Topic: Multiple hypotheses matches the goal


view this post on Zulip Li Zhou (Dec 14 2023 at 16:00):

Hi, is there any control on multiple hypotheses that match the goal (writing Ltac)?

Following is a simple example:
Is there a way to write a Ltac that achieves similar results to the following two lines starting with move.

Require Import ssreflect.
Variable (P : nat -> Prop).
Lemma PP (n : nat) : P n. Admitted.

Lemma foo (x y : nat) : True.
move: (PP x) (PP y) => Px Py.
(* for every nat i that appears in Hyptheses, introduce PP i to the Hyptheses*)
(* any Ltac to do this? *)
Abort.

Lemma foo (x y z: nat) : True.
move: (PP x) (PP y) (PP z) => Px Py Pz.
(* for every nat i that appears in Hyptheses, introduce PP i to the Hyptheses*)
(* any Ltac to do this? *)
Abort.

view this post on Zulip Laurent Théry (Dec 14 2023 at 16:33):

one solution is to progressively push in the goal what has been processed but this could not be applicable to your specific problem.

Variable (P : nat -> Prop).
Lemma PP (n : nat) : P n. Admitted.

Lemma foo (x y z : nat) : True.
Proof.
repeat (match goal with X : nat |- _ => generalize (PP X); generalize dependent X end);
intros.

view this post on Zulip Li Zhou (Dec 15 2023 at 01:39):

Laurent Théry said:

one solution is to progressively push in the goal what has been processed but this could not be applicable to your specific problem.

Variable (P : nat -> Prop).
Lemma PP (n : nat) : P n. Admitted.

Lemma foo (x y z : nat) : True.
Proof.
repeat (match goal with X : nat |- _ => generalize (PP X); generalize dependent X end);
intros.

yes, it won't work since repeat will rematch the hypotheses after each application...

view this post on Zulip Laurent Théry (Dec 15 2023 at 09:48):

not if you generalize the hypothesis to put it in the goal

view this post on Zulip Li Zhou (Dec 17 2023 at 13:38):

Laurent Théry said:

not if you generalize the hypothesis to put it in the goal

thanks, I think it already solves my problem!


Last updated: Jun 23 2024 at 05:02 UTC