## Stream: Coq users

### Topic: Multiple hypotheses matches the goal

#### 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.
``````

#### 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.
``````

#### 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...

#### Laurent Théry (Dec 15 2023 at 09:48):

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

#### 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