Stream: math-comp users

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


view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip 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!

view this post on Zulip Ricardo (Feb 11 2023 at 19:24):

I see. Thanks.

view this post on Zulip 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.

view this post on Zulip 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.
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, ..."

view this post on Zulip Ricardo (Feb 11 2023 at 20:34):

Or is there a different path to prove this lemma?

view this post on Zulip Ricardo (Feb 11 2023 at 20:39):

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

view this post on Zulip Ricardo (Feb 11 2023 at 20:48):

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

view this post on Zulip 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.

view this post on Zulip 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).

view this post on Zulip Laurent Théry (Feb 11 2023 at 21:22):

To contribute to mathcomp, you should follow this

view this post on Zulip 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.

view this post on Zulip Ricardo (Feb 11 2023 at 22:37):

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

view this post on Zulip 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).

view this post on Zulip Laurent Théry (Feb 11 2023 at 22:54):

you are missing ssrnat

view this post on Zulip Pierre Jouvelot (Feb 11 2023 at 22:57):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Ricardo (Feb 12 2023 at 00:21):

Wow.

view this post on Zulip 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...

view this post on Zulip Notification Bot (Feb 13 2023 at 03:59):

Ricardo has marked this topic as resolved.


Last updated: Jul 25 2024 at 15:02 UTC