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
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).
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.
/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 zulipvlj @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.
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 motiveQ ∶ (x ∶ A) → B(x) → P (x) → Set
depends on the first componentP ∶ A → Set
.
SearchAbout
does
SearchAbout
's behavior with Search
?
/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