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?

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.

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

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

Pierre Jouvelot has marked this topic as resolved.

Last updated: Jul 25 2024 at 16:02 UTC