by

Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
Activity
  • May 26 23:49
    satnam6502 opened #12418
  • May 26 21:29
    jfehrle commented #12103
  • May 26 21:26
    jfehrle commented #12103
  • May 26 21:25
    jfehrle synchronize #12103
  • May 26 21:12
    JasonGross commented #12412
  • May 26 21:07
    Zimmi48 commented #12103
  • May 26 20:14
    MSoegtropIMC commented #12186
  • May 26 19:52
    jfehrle commented #12103
  • May 26 19:28
    VincentSe commented #12186
  • May 26 19:14
    MSoegtropIMC commented #12186
  • May 26 19:12
    MSoegtropIMC synchronize #12186
  • May 26 19:06
    ppedrot commented #12414
  • May 26 18:29
    SkySkimmer commented #12383
  • May 26 18:24
    ejgallego labeled #12417
  • May 26 18:23
    Janno commented #12383
  • May 26 18:22
    Janno commented #12383
  • May 26 18:08
    CohenCyril commented #12383
  • May 26 18:08
    SkySkimmer commented #12383
  • May 26 18:06
    bfbonatto opened #12417
  • May 26 18:00
    JasonGross commented #12383
Pierre Roux
@proux01

I did, should I add your comment there ?

not needed, thanks!

alexm98
@alexm98_gitlab

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

Théo Winterhalter
@TheoWinterhalter
If you do inversion on your hypothesis you should get what you want I think.
alexm98
@alexm98_gitlab
@TheoWinterhalter you are right! thanks!
Lemma sorted_sorted: forall a l, sorted (a::l) -> sorted l.
Proof.
  intros.
  inversion H.
  constructor.
  trivial.
Qed.
matrixbot
@matrixbot
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.
Emilio Jesús Gallego Arias
@ejgallego

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.

@CohenCyril

Cyril Cohen
@CohenCyril

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

matrixbot
@matrixbot
Jacques Garrigue I suppose this would be the way. The bridge with gitter is fully bidirectional (i.e. this message comes from matrix, not gitter), I don't know how far the zulip one goes.
Vincent
@vsiles
Is it possible to make a standard definition (like andb_prop from 'Init.Datatypes') not opaque ?
or do I have to create a non opaque version of it ?
vlj
@vlj
What is the zulip server to use ?
Paolo G. Giarrusso
@Blaisorblade
@vsiles you need your own version. Qed-status cannot be changed. Opaque/Transparent is a different (and weaker) form of opacity. And there are reasons for the difference.
Vincent
@vsiles
ok, thanks for confirming that
Théo Zimmermann
@Zimmi48
@vlj You need to send your e-mail to @CohenCyril to get access. Cf. https://gitter.im/coq/coq?at=5eb971373f5b010319406583
Vincent
@vsiles
@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 ?
Matthieu Sozeau
@mattam82
The first is a FAQ, you can use the dec combinator. The default obligation tactic clears fixpoint prototypes so you don’t shoot yourself in the foot with it IIRC
Vincent
@vsiles
What's the dec combinator ?
Vincent
@vsiles
ok, found in the doc :) I'll try to see how to tweak the tactic to keep the hypothesis. Thanks !
Vincent
@vsiles
I used Obligation Tactic := idtac and I still don't have the induction hypothesis. If you remember anything, ping me :)
alexm98
@alexm98_gitlab

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

Théo Winterhalter
@TheoWinterhalter
If you use cbn it should reduce to
if leb x a then x :: l else a :: insert x l.
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
:)
Croitoru Madalin
@Modalee
image.png
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
image.png
image.png
image.png
Croitoru Madalin
@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.
Croitoru Madalin
@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 ?

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

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