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: Apr 19 2024 at 15:02 UTC