## Stream: math-comp users

### Topic: ✔ [forall _, true] doesn't eval to true

#### Ricardo (Feb 11 2023 at 03:49):

Hi everyone. I just found out that `[forall _, true]` doesn't evaluate to `true`. Is this intended? Or rather an unpleasant consequence of the implementation of forall?

#### Ricardo (Feb 11 2023 at 03:52):

Also, I couldn't find a lemma to rewrite `[forall _, true]` into `true` so I wrote it myself. Any reason why this isn't part of mathcomp?

``````Lemma forall_true (T : finType) :
[forall x : T, true] = true.
Proof. by apply/forallP. Qed.
``````

#### Pierre Roux (Feb 11 2023 at 10:03):

Don't see any good reason, that could be worth a pull request (along with forall_false).

#### Laurent Théry (Feb 11 2023 at 14:33):

It does not evaluate because it is implemented as a cardinal of something. You could think it is because `T` is unknown but even

``````[forall x : bool, true]
``````

does not evaluate to `true`.
There are few theorems about `[forall _, _]`, so there is clearly a need for a good contribution, for example

``````[forall x : T, P1 x && P2 x]  = [forall x : T, P1 x] && [forall x : T, P2 x]
``````

is also missing.
I second Pierre's advice, a PR contributing to the mathcomp github would be more than welcome!

I see. Thanks.

#### Ricardo (Feb 11 2023 at 19:27):

Last and only time I prepared a PR took me a bit of time to understand how to do it and then do it. Is there a short guide to PRs? I don't remember how to do one.

#### Ricardo (Feb 11 2023 at 20:30):

Lemma `forall_false` doesn't seem to be as easy to prove.

``````Lemma forall_false (T : finType) :
[forall x : T, false] = false.
Proof. have x : T by admit.
by apply/forallP => /(_ x) H.
``````

It requires that the finType T isn't empty. Is there any guarantees that a finType isn't empty? I think probably that's not the case since the `fintype.v` file says "We define or propagate the finType structure appropriately for all basic types : unit, bool, void, ..."

#### Ricardo (Feb 11 2023 at 20:34):

Or is there a different path to prove this lemma?

#### Ricardo (Feb 11 2023 at 20:39):

What are the semantics of `[forall x : T, false]` for a fintype T that's empty?

#### Ricardo (Feb 11 2023 at 20:48):

This question is kind of analogous to the question of what `fold andb []` should be.

#### Pierre Jouvelot (Feb 11 2023 at 21:08):

One simple way to ensure that `T` is inhabited is to ask one `x0 : T` to be passed when using this lemma:

``````Lemma forall_false (T : finType) (x0 : T) :
[forall x : T, false] = false.
Proof. by apply/forallP => /(_ x0). Qed.
``````

#### Laurent Théry (Feb 11 2023 at 21:18):

For empty type. it is true

``````Lemma foo : [forall x : void, false].
by apply/forallP.
Qed.
``````

You should prove something like

``````[forall x : T, false] = (#|T| != 0).
``````

#### Laurent Théry (Feb 11 2023 at 21:22):

To contribute to mathcomp, you should follow this

#### Ricardo (Feb 11 2023 at 22:34):

Laurent Théry said:

To contribute to mathcomp, you should follow this

The only unease I have with mathcomp's contributing guide for code is the point that reads "Lines end with a point `.` and only have `;` inside them". To me `;` are annoying when they don't apply to several subgoals as they don't allow a step-by-step analysis of the proof. In my view the use of `;` should be limited to when the same code with `.` substituted for `;` doesn't compile.

#### Ricardo (Feb 11 2023 at 22:37):

Thank you both @Laurent Théry and @Pierre Jouvelot for the suggestions :smile:

#### Ricardo (Feb 11 2023 at 22:41):

Laurent Théry said:

You should prove something like

``````[forall x : T, false] = (#|T| != 0).
``````

Strangly, when I write the following lemma it complains about `#|T|` having type `nat` instead of `Equality.sort ?T`.

``````From mathcomp Require Export eqtype fintype ssrbool ssreflect.
Lemma forall_false (T : finType) :
[forall x : T, false] = (#|T| != 0).
``````

#### Laurent Théry (Feb 11 2023 at 22:54):

you are missing ssrnat

#### Pierre Jouvelot (Feb 11 2023 at 22:57):

This should by `(#|T| == 0)`, I guess.

#### Laurent Théry (Feb 11 2023 at 22:59):

Ricardo said:

Laurent Théry said:

To contribute to mathcomp, you should follow this

The only unease I have with mathcomp's contributing guide for code is the point that reads "Lines end with a point `.` and only have `;` inside them". To me `;` are annoying when they don't apply to several subgoals as they don't allow a step-by-step analysis of the proof. In my view the use of `;` should be limited to when the same code with `.` substituted for `;` doesn't compile.

don't worry too much, submit your PR, then the reviewer will ask you for changes if needed.

#### Pierre Jouvelot (Feb 11 2023 at 23:24):

I got this draft proof:

``````Lemma forall_false (T : finType) : [forall x : T, false] = (#|T| == 0).
Proof.
have [/existsP [x _]|] := boolP ([exists x, x \in T]).
- have -> : [forall x : T, false] = false by apply/forallP => /(_ x).
apply: esym.
move/eqP: (fintype0 x).
by apply: contra_neqF => /eqP.
- have [/card_gt0P/existsP -> //|] := boolP (0 < #|T|).
by rewrite -eqn0Ngt.
Qed.
``````

#### Laurent Théry (Feb 11 2023 at 23:55):

or

``````Lemma forallb_false (T : finType) : [forall x : T, false] = (#|T| == 0).
Proof.
by rewrite -(negb_exists xpredT) eqn0Ngt; congr (~~ _); apply/existsP/card_gt0P.
Qed.
``````

#### Laurent Théry (Feb 12 2023 at 00:03):

As a matter of fact :smile:

``````Lemma forallb_false (T : finType) : [forall x : T, false] = (#|T| == 0).
Proof. by []. Qed.
``````

Wow.

#### Pierre Jouvelot (Feb 12 2023 at 09:59):

Laurent Théry said:

As a matter of fact :smile:

``````Lemma forallb_false (T : finType) : [forall x : T, false] = (#|T| == 0).
Proof. by []. Qed.
``````

Indeed, I had a redundant case in my draft. And hehe, this last one is a good one :grinning: The power of computation, I guess...

#### Notification Bot (Feb 13 2023 at 03:59):

Ricardo has marked this topic as resolved.

Last updated: Jul 25 2024 at 15:02 UTC