## Stream: math-comp users

### Topic: ✔ Missing logic lemma?

#### Pierre Jouvelot (Jan 26 2022 at 16:30):

I needed this small logic-based lemma, which has an easy proof:

``````Lemma forallD T F G (H : (forall x : T, F x -> G x)) : (forall x : T, F x) -> (forall y : T, G y).
``````

I was convinced it must already be present in some standard Coq library, but couldn't find it. Does it already exist?

#### Cyril Cohen (Jan 27 2022 at 07:19):

Pierre Jouvelot said:

I needed this small logic-based lemma, which has an easy proof:

``````Lemma forallD T F G (H : (forall x : T, F x -> G x)) : (forall x : T, F x) -> (forall y : T, G y).
``````

I was convinced it must already be present in some standard Coq library, but couldn't find it. Does it already exist?

With the ssreflect tactic language, this is typically the kind of transformation for which no lemma is required:

``````Lemma forallD T F G (H : (forall x : T, F x -> G x)) :
(forall x : T, F x) -> (forall y : T, G y).
Proof. by move=> /(_ _)/H. Qed.
``````

Indeed `move=> /(_ _)` instanciates the first argument of `forall x, F x` with an hole so that we can chain with forward view `/H`.

Note that a "relevant" (as in proof-relevant) version of this "theorem" can also be seen as a form dependent function composition, and while non-dependent composition is in mathcomp, the dependent version is not.

#### Cyril Cohen (Jan 27 2022 at 07:21):

PS: the advantage of using the combination of view, is that it allows to deal with many variations (several variables, multiple argument compositions, etc)

#### Pierre Jouvelot (Jan 27 2022 at 08:49):

Thanks a lot, Cyril. This looks a bit like magic; this is very slick :)

#### Notification Bot (Jan 27 2022 at 08:50):

Pierre Jouvelot has marked this topic as resolved.

Last updated: Feb 08 2023 at 07:02 UTC