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?

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

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

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.

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.

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

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*, ..."

Or is there a different path to prove this lemma?

What are the semantics of `[forall x : T, false]`

for a fintype T that's empty?

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

should be.

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

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

To contribute to mathcomp, you should follow this

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.

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

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

you are missing ssrnat

This should by `(#|T| == 0)`

, I guess.

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.

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

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

As a matter of fact :smile:

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

Wow.

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

Ricardo has marked this topic as resolved.

Last updated: Jul 25 2024 at 15:02 UTC