Where communities thrive


  • Join over 1.5M+ people
  • Join over 100K+ communities
  • Free without limits
  • Create your own community
People
Repo info
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
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.

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 :-)