## Where communities thrive

• Join over 1.5M+ people
• Join over 100K+ communities
• Free without limits
##### Activity
• Nov 24 2020 10:46
SkySkimmer commented #13464
• Nov 24 2020 10:40
herbelin commented #13460
• Nov 24 2020 10:18
jakobbotsch opened #13465
• Nov 24 2020 10:18
gares commented #13464
• Nov 24 2020 10:12
Zimmi48 updated the wiki
• Nov 24 2020 10:11
gares synchronize #13463
• Nov 24 2020 10:10
Zimmi48 updated the wiki
• Nov 24 2020 10:05
Zimmi48 commented #11390
• Nov 24 2020 10:00
herbelin commented #11390
• Nov 24 2020 09:56
Zimmi48 commented #11390
• Nov 24 2020 09:52
herbelin commented #11390
• Nov 24 2020 09:46
gares commented #13457
• Nov 24 2020 09:46
gares review_requested #13457
• Nov 24 2020 09:46
gares synchronize #13457
• Nov 24 2020 09:43
Zimmi48 assigned #13457
• Nov 24 2020 09:38
gares commented #13464
• Nov 24 2020 09:36
gares commented #13464
• Nov 24 2020 09:35
Zimmi48 commented #13449
• Nov 24 2020 09:34
gares commented #13464
• Nov 24 2020 09:33
gares commented #13464
alexm98
@alexm98_gitlab
So does simpl but I don't seem to understand how to proceed with this. Can i force the evaluation further so insert x l becomes [x;l] somehow?
Théo Winterhalter
@TheoWinterhalter
No, because you have leb x a and you don’t know if x ≤ a or not.
You have to do a case analysis on this as well.
Théo Winterhalter
@TheoWinterhalter

The simplest woul be to use

destruct (Nat.leb_spec0 x a).

which you could have found by searching lemmata about leb.

Search leb.
Also you should take care in writing your proofs in a more robust way. Naming the variables you introduce and using bullets to separate the diffrent goals.
Lemma stronger_insert_sorted :
forall x l,
sorted l ->
sorted (insert x l) /\ (forall y, sorted (y::l) -> sorted (insert x (y::l))).
Proof.
intros x l hl.
split.
- induction l.
+ simpl. constructor.
+ simpl. destruct (Nat.leb_spec0 x a).
alexm98
@alexm98_gitlab
I see, thank you! I am very new to Coq
Théo Winterhalter
@TheoWinterhalter
:)
@Modalee
hello guys ! Can someone help me with this code and explain a little bit how it works ? im very new to coq and i have to do a homework, but i dont know how to start and how to make it
@Modalee
@TheoWinterhalter i saw u helped @alexm98_gitlab with a similar exercise and it helped me alot too , can u please help me again ? i would be very grateful. Ive searched all day but i just cant understand this language
Théo Zimmermann
@Zimmi48
@Modalee Don't expect help by asking such vague questions. And don't tag random people you don't know. That's rude.
@Modalee
Yeah , you're right , but i didn't know how to solve that and i was so desperate yesterday
Bohdan Liesnikov
@liesnikov

Hi!
I'm working on rewriting Iris Proof Mode in Ltac2 (with Derek) and wanted to ask what's the current status of (or plans for) some of the features.

For example, the doc mentions that used-defined scopes are planned, but so far it's not there yet, right?

Another thing is that intropatterns is an opaque scope. Which means that while I can match on intropattens value as a list, that there isn't really anything else it's useful for? (except passing to Std.intro, as in Notations.v)
And are there any plans for making intropatterns extensible?

Not sure who is this addressed to, Pierre-Marie, perhaps? But I'd appreciate any answer.

Cyril Cohen
@CohenCyril
Dear @/all the gitter data until May 6 at 4:24 has been imported in a new zulip chat.
I need a mapping from your user github name to your email for you to recover your account. Please click on my picture, then "Chat Privately", then type: /me your-email-adress@yourprovider.org. This mail should be associated with a github, gitlab or even google account if you want to use one of these plateform to log in zulip
I will notify you when you have access, it takes a guy on PDT timezone to answer my mail, I send him batches of username->mail as I receive the data from you guys.

vlj @vlj mai 14 13:44
What is the zulip server to use ?

Cyril Cohen
@CohenCyril

Dear Coq community,
we are happy to announce the openning of https://coq.zulipchat.com a chatroom with which we intend to replace our use of gitter[*].
Together with https://coq.discourse.group this will become one of the main tools to communicate with each other about coq and related projects (e.g. coq-community projects, mathematical components, etc). While the discourse is meant to work as a forum, the zulip chatroom is meant to work as a chat/IRC, with messages written in a more casual way and a possibly higher traffic, although Zulip offers the way to sort messages by topics and thus being selective about what one wants to follow, cf https://zulipchat.com/why-zulip/. We hope that between these two tools we find more opportunities to communicate in the way that each of us is most comfortable with.

[*] If you had a gitter account and posted at least one message in one of the coq related channels, there is a high chance that we automatically ported your account, please send a private message to @CohenCyril, on gitter, with you email address, so do not register on Zulip on your own.

Cyril Cohen
@CohenCyril
@liesnikov @vsiles @strub @tchajed @jakobbotsch @RalfJung @samuelgruetter @Matafou @ionathanch @vlj, you have access to Coq zulip through "login with github", at https://coq.zulipchat.com
Pierre Courtieu
@Matafou
Thanks! Works for me.
vlj
@vlj
Thanks !
It works too
Ralf Jung
@RalfJung
@CohenCyril thanks :)
Ali Caglayan
@Alizter

When you define odd and even mutually you can reduce it down to a single fixpoint by defining a function oddeven : nat -> Type * Type instead. Under the hood, the first way generates a mutual fixpoint whilst the second way is just a regular fixpoint.

I want to define something silly like the following:

Fixpoint A (n : nat) : Type
with B {n : nat} : A n -> Type.

but coq rejects it since it has no knowledge of A in the type of B. However I know how to reduce this to a single fixpoint Fixpoint AB (n : nat) : {A : Type & A -> Type}. to get the same effect. Is there some way to define a mutual fixpoint with dependency?

Paolo G. Giarrusso
@Alizter seems everybody’s moving to zulip? your question reminds me of “induction-recursion”, but what you want sounds like “recursion-recursion”, which I’ve never heard of (maybe because its semantics is clear, using the encoding you describe?)
Gaëtan Gilbert
@SkySkimmer
recursion-recursion is when you have some mutual fixpoints where one appears in the type of the other
it comes up eg when you want to define the induction principles for an inductive-inductive type
the AB example is a case where it can be encoded with regular recursion
Gaëtan Gilbert
@SkySkimmer

you can see the terminology used in the wild eg in https://personal.cis.strath.ac.uk/fredrik.nordvall-forsberg/thesis/thesis.pdf 5.4

Interpreting the general elimination rules The translation from inductive-inductive
definitions to indexed inductive definitions only worked for the simple elimination
rules from 3.2.5.2, and not the general elimination rules. The reason is simple: the
elimination rules of the target theory does not support the “recursive-recursive” nature
of the inductive-inductive elimination rules, where the second component of the motive
Q ∶ (x ∶ A) → B(x) → P (x) → Set
depends on the first component P ∶ A → Set.

Amin Timany
@amintimany
The SearchAbout command is deprecated and Coq issues warnings when it is used and says we should use Search instead. However, when I use Search with a name I also get a warning, e.g., the following for Search eq: Warning: Listing only lemmas with conclusion matching (_ = _).
Indeed the result that is returned only has lemmas that contain equality in their conclusion.
This is different from what SearchAbout does
is there a way to get SearchAbout's behavior with Search?
Théo Zimmermann
@Zimmi48
@amintimany That's because you are using ssreflect's Search. If you update to the latest version of master, it should be different (ssreflect's Search has been bundled into a separate plugin and deprecated).
Amin Timany
@amintimany
@Zimmi48: oh, I see, thanks
Théo Zimmermann
@Zimmi48
BTW, are you aware that we've migrated our chat to Zulip? Cf. the message of @CohenCyril above (https://gitter.im/coq/coq?at=5ebeb020ecc55a312d050f75) on how to get back your account there.
Amin Timany
@amintimany
I am using 8.11.1. this was fixed after that?
Théo Zimmermann
@Zimmi48
Sorry, I read your comment too fast and was not clear in my answer. Yes, this is only in master and v8.12. The beta for 8.12 should be released soon.
Amin Timany
@amintimany
ok, thanks :-)
@Zimmi48 also, thanks for the heads up for Zulip, I sent a message to Cyril asking for access thre
Cyril Cohen
@CohenCyril
Dear gitter user,
if you posted at least one message in a Coq related gitter channel, your account has been ported to https://coq.zulipchat.com, with all the messages in your history. You have until June 5th 14:00 CEST to give me privately[*] an email associated with your github, gitlab or google account, in order for you to reclaim ownership.
After that we will archive your zulip account and if you want to log into zulip, you will have to create a fresh account.
Best wishes
[*] Please click on my picture, then "Chat Privately", then type: /me your-email-adress@yourprovider.org. This mail should be associated with a github, gitlab or even google account if you want to use one of these plateform to log in zulip
Cyril Cohen
@CohenCyril
if you have not done it yet
Cyril Cohen
@CohenCyril
Gaëtan Gilbert
@SkySkimmer
does anything bad happen if someone doesn't bother?
Théo Zimmermann
@Zimmi48

No, that's not a big deal. AFAICT, the only things you lose is:

• your full sent message history (through Zulip, I can see all the messages I sent on Gitter)
• the ability to edit the messages that you sent on Gitter (but given that those are pretty old, you normally don't need to do that)

And if someone does find some old message and want to talk to the person that sent them, they might reach out to the wrong account.

Cyril Cohen
@CohenCyril

And if someone does find some old message and want to talk to the person that sent them, they might reach out to the wrong account.

This last part is the most problematic, although when we will ask for old account to be archived, they will add a "(archived)" mention, so we can hope one would see it.

I also openned an issue on zulip to merge users zulip/zulip#14912, to be able to merge accounts after the fact, later on.

Also, every time one posts something here, I have to repost the announcement to move to zulip... so please refrain ;)
(otherwise it looses visibility)

Dear @/all
if you posted at least one message in a Coq related gitter channel, your account has been ported to https://coq.zulipchat.com, with all the messages in your history. You have until June 5th 14:00 CEST to give me privately[*] an email associated with your github, gitlab or google account, in order for you to reclaim ownership, if you did not do it yet.
After that we will archive your zulip account and if you want to log into zulip, you will have to create a fresh account.
Best wishes

[*] Please click on my picture, then "Chat Privately", then type: /me your-email-adress@yourprovider.org. This mail should be associated with a github, gitlab or even google account if you want to use one of these plateform to log in zulip