- Join over
**1.5M+ people** - Join over
**100K+ communities** - Free
**without limits** - Create
**your own community**

- May 26 23:49satnam6502 opened #12418
- May 26 21:29jfehrle commented #12103
- May 26 21:26jfehrle commented #12103
- May 26 21:25jfehrle synchronize #12103
- May 26 21:12JasonGross commented #12412
- May 26 21:07Zimmi48 commented #12103
- May 26 20:14MSoegtropIMC commented #12186
- May 26 19:52jfehrle commented #12103
- May 26 19:28VincentSe commented #12186
- May 26 19:14MSoegtropIMC commented #12186
- May 26 19:12MSoegtropIMC synchronize #12186
- May 26 19:06ppedrot commented #12414
- May 26 18:29SkySkimmer commented #12383
- May 26 18:24ejgallego labeled #12417
- May 26 18:23Janno commented #12383
- May 26 18:22Janno commented #12383
- May 26 18:08CohenCyril commented #12383
- May 26 18:08SkySkimmer commented #12383
- May 26 18:06bfbonatto opened #12417
- May 26 18:00JasonGross commented #12383

Hello everyone! I am struggling with trying to prove the following lemma:`Lemma sorted_sorted: forall a l, sorted (a::l) -> sorted l.`

Now I do have an inductive definition of what sorted is, it looks something like this:

```
Inductive sorted : list nat -> Prop :=
| snil : sorted nil
| s1 : forall x, sorted (x::nil)
| s2 : forall x y l, sorted (y::l) -> x <= y -> sorted (x::y::l).
```

I just don't know where to start with this, and would be happy to get some pointers. Thanks

Jacques Garrigue Is there a plan for a matrix bridge to the zulip chats?

I found it very convenient to access gitter from the matrix bridge.

Is this what you have in mind? https://coq.zulipchat.com/integrations/doc/matrix

or do I have to create a non opaque version of it ?

@vlj You need to send your e-mail to @CohenCyril to get access. Cf. https://gitter.im/coq/coq?at=5eb971373f5b010319406583

@mattam82 Hi ! Question about

`Program`

(see https://pastebin.com/uuxa96K9) why using `if then else`

doesn't lead to a `Heq_anonymous`

when `match with`

does ? Also with this particular piece of code, is it possible to have the induction hypothesis (Fixpoint) in the obligations ?
Hello! I'm struggling to prove the following lemma:`Lemma stronger_insert_sorted : forall x l, sorted l -> sorted (insert x l) /\ (forall y, sorted (y::l) -> sorted (insert x (y::l))).`

I of course have a definition for what sorted is, that is:

```
Inductive sorted : list nat -> Prop :=
| snil : sorted nil
| s1 : forall x, sorted (x::nil)
| s2 : forall x y l, sorted (y::l) -> x <= y -> sorted (x::y::l).
```

Insert is also defined as:

```
Fixpoint insert x l :=
match l with
| nil => x::nil
| y::tl => if leb x y then x::l else y::insert x tl
end.
```

What I've tried so far is:

```
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.
split.
induction l.
simpl.
constructor.
```

But this gets me to the goal `sorted (insert x (a :: l))`

which is where I don't know how to proceed

You have to do a case analysis on this as well.

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

hello guys ! Can someone help me with this code and explain a little bit how it works ? i

`m very new to coq and i have to do a homework, but i don`

t know how to start and how to make it
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.

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

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`

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

Please send me your mail in private (cf my previous message)

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

@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

It works too

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?

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`

.