Stream: Coq users

Topic: New Discourse topics


view this post on Zulip Discourse Bot (Jun 18 2020 at 16:43):

Nicolás Ojeda Bär @nojb posted in Naive quotients of types?

Hello,
Trying to transport my set-theoretical intuition to Coq, I tried to define the quotient of a type by an equivalence relation, but I cannot figure out how to prove the universal property of the quotient. Details below. Any comments/suggestions welcome!
(* Types ~ Sets *)
Parameter X Y : Type.

(* P X ~ Power set *)
Definition P (X : Type) : Type := X -> Prop.

(* An equivalence relation on...

view this post on Zulip Théo Zimmermann (Jun 18 2020 at 16:44):

(The above is not really "new" but a test that the Discourse integration correctly works.)

view this post on Zulip Discourse Bot (Jun 20 2020 at 11:41):

@jco posted in Typeclasses: considered harmful? Idiomatic?

I just read the typeclasses section of software foundations part 4 (QuickChick). I’m familiar with type classes from Haskell and Scala, but it seems like the Coq ones are very powerful…but the lack of overlap checking seems very dangerous. I’m curious what is considered a best practice in Coq. Limited use in modules only? Are typeclasses exposed as parts of APIs? Are there ways to manage the non-n...

view this post on Zulip Discourse Bot (Jun 22 2020 at 20:52):

Arthur Azevedo de Amorim @arthuraa posted in Programmable hint databases with Ltac2

I would like to create a database of unfoldable constants and manipulate it programmatically. I wondered whether it would be possible to access an unfolding hint database from Ltac2, or if it is possible to implement my own hint database mechanism using Ltac2 references.

view this post on Zulip Discourse Bot (Jun 27 2020 at 20:08):

Clément Pit-Claudel @cpitclaudel posted in What's a convenient way to install multiple Coq versions side by side?

Hi all,
I work with multiple projects that require different versions of Coq. In the past I built Coq by hand, and switching version was just a matter of changing a few variables in proof-general. Now I use OPAM, but I haven’t found an easy way to switch between Coq versions.
I tried using per-project OPAM switches (in the style of Python virtualenvs), but since I also do a bit of OCaml progra...

view this post on Zulip Discourse Bot (Jun 29 2020 at 08:51):

@cbl posted in Simplify proofs with neested pattern matching

Hi Everyone,
I’m currently working to prove results on a fonction is_valid : A -> bool of the form is_valid a = true -> % some property, where A is an inductive type of the form
Inductive A := | N : B -> (list A) -> A . % N is the only constructor

And B is also an inductive type with around 50 constructors.
The problem I have is that nested pattern matching (on the list) like
| N b1 (N b2 [])...

view this post on Zulip Discourse Bot (Jul 01 2020 at 13:12):

Valentin Robert @Ptival posted in Setoid rewriting with implications

Hi!
I just encountered a limitation that I don’t quite understand the justification for, and would like to know more about it.
Boiled down, the problem is rewriting with an implication in a product:
From Coq Require Import Morphisms.
From Coq Require Import Program.

Goal forall (A B C : Prop) (H : A /\ B) (P : B -> C), A /\ C.
intros.
setoid_rewrite P in H. (* fails *)

After a bit of a he...

view this post on Zulip Discourse Bot (Jul 04 2020 at 02:51):

@jco posted in Where does CompCert fall short?

I just got started with the software foundations that is currently in beta which walks you through the Verificable C project. It’s super cool! I do have one sort of general question: in practice, where does CompCert fall short?
That is to say, let’s say someone needs to use C for some reason…why would they go to gcc or clang over compcert? Compilation speed? Quality of optimizations? Linker optio...

view this post on Zulip Discourse Bot (Jul 05 2020 at 10:08):

@ZWY posted in Arguments in tactics

I am confused about what are arguments in Coq. I have read the documentation, but I have not found a formal definition of arguments thus having some confusion.
The documentation defines the syntax intros ident+, therefore according to the definition, the argument for intros n m can only be n m. A Single n is not the argument of intros n m.
Is there anything wrong with my understanding?

view this post on Zulip Discourse Bot (Jul 07 2020 at 13:04):

OnorioCatenacci @Onorio posted in Suggested Answers

I suspect this is probably a FAQ but I can’t seem to find it anywhere. Apologies in advance for the dumb question but are the suggested answers to the exercises in Software Foundations: Volume 1 Logical Foundations posted somewhere? I’m a bit stumped on a few of the exercises and, honestly, I wouldn’t mind double checking some of my answers against a suggested answer.

view this post on Zulip Discourse Bot (Jul 07 2020 at 19:22):

OnorioCatenacci @Onorio posted in How to Use a Definition in a Proof?

So I am playing with Coq, working through the Software Foundations text and I am trying to do a proof outside of what’s in the text for practice.
Here’s my Gallina code:
Fixpoint add (n m: nat) : nat :=
match n with
| O => m
| S n' => S (add n' m)
end.

Theorem sum_should_be_equal_or_greater: forall n m : nat, add n m >= n.
Proof.
intros n m.
induction n as [| n' IHn'].

- simpl.

I ...

view this post on Zulip Discourse Bot (Jul 09 2020 at 17:09):

@jco posted in Good library or framework for handling extraction, IO, etc?

Note sure if my intent makes sense, but let’s say I have an app I want to write largely with coq, using the extraction method to run it. For at least basic, common data types that one might need, is there a library in Coq that just says “use these and your extraction will be fine,” along with utilities to do common stuff like read a file then put the data into a format that is useful to reason abo...

view this post on Zulip Discourse Bot (Jul 10 2020 at 08:38):

@ZWY posted in Tacarg in Ltac

The Coq manual says
“In tacarg, there is an overlap between qualid as a direct tactic argument and qualid as a particular case of term.”
I can not fully understand this sentence. The tactic split is denoted by tacarg. What does split belong to? A direct tactic argument or a term?

view this post on Zulip Discourse Bot (Jul 11 2020 at 03:11):

@Lasse posted in JMeq and dependent programming

I’m trying to wrap my brain around the essence of the problems with dependent programming and equality. Some proofs are much easier or impossible to do without the JMeq axiom. I’ve been trying to formulate a minimal example that captures the essence of this problem:
| infc : inf tt -> inf tt.

Lemma match_eq (c : inf tt) (e : tt = tt) :
match e in (_ = y) return (inf y) with
| eq_refl => infc c
e...

view this post on Zulip Discourse Bot (Jul 11 2020 at 15:55):

Yannick Zakowski @Yannick posted in Preventing pollution of the instance context during Import

Hello everyone :slight_smile:
In the abstract, my question(s) is the following.

Is there a way to import a file without putting in scope the global instances that it declares?
Alternatively, what is the status of #7342, for having a command to remove an Instance from the Visible scope?
Even better, are there any plans to associate sets of instances to namespaces in the style of hint databases?
And finally, ...

view this post on Zulip Discourse Bot (Jul 12 2020 at 06:34):

@jco posted in Formally verified pieces of the network stack? (eg RPC)

I took a look at the deep specs site, as it seemed like this would be related to that project, but I didn’t see anything directly. The existence of deepspecs (and the project to make a formally verified web server) indicates to me that this is probably still an area of active research/development, but I’d love to know what the state of the art is, and what theory theory is backing things up. I’m r...

view this post on Zulip Discourse Bot (Jul 12 2020 at 12:45):

@ZWY posted in Tactics denoted by qualid

I know there are some tactics denoted by qualid like split and destruct. Do all of such tactics are written in the file “coretactics.mlg”?

view this post on Zulip Discourse Bot (Jul 14 2020 at 01:49):

Jonathan Chan @jon posted in Nested dependent pattern matchin

I currently have the following:
Inductive var {V : nat} :=
| free (name : name)
| bound (l : Fin.t V).

Definition openv a {V} (v : @var (S V)) : @var V :=
match v with
| free n => free (shift_name a n)
| bound l =>
match l in Fin.t (S V) with
| Fin.F1 => free a
| Fin.FS l => bound l
end
end.

where Fin.t is the finite set type from Vectors.Fin. However, I’d like to write o...

view this post on Zulip Discourse Bot (Jul 20 2020 at 21:58):

Maximilian Wuttke @mwuttke97 posted in unshelve evar (x : _)

In some proofs it might be necessary to define some constant using the proof mode. Which of the following variants would you prefer / find more elegant?
poll

view this post on Zulip Discourse Bot (Jul 22 2020 at 07:08):

@jco posted in Cbn vs simpl?

Pardon the dumb question, I was curious if the difference between these two tactics is elaborated somewhere? The manual just says that cbn is considered a “better” version, and it looks like they’re both opaque from within coq.

view this post on Zulip Discourse Bot (Jul 23 2020 at 05:15):

@hhiim posted in Why Coq does not allow the containment relationship between types

English is not my native language
I want to define “integer type”. But encounter obstacles
Although the types of positive integers, negative integers and zero are not exactly the same,
However, positive integers, negative integers and zero are all integers,
But Coq does not seem to allow containment relationships between types.
How to define “integer”?
Coq 8.11.2

view this post on Zulip Discourse Bot (Jul 24 2020 at 09:10):

@ThijsBeurskens posted in Hint databases as argument

Hi everyone,
I am trying to implement a tactic that uses small hint databases to solve simple arithmetic problems:
Ltac pattern_matching_rewriter :=
match goal with
|[ |- context[0] ] => solve[auto with nocore zero_rewriters]
|[ |- context[1] ] => solve[auto with nocore one_rewriters]
|[ |- context[- _] ] => solve[auto with nocore opp_rewriters]
|[ |- context[Rabs _] ] => solve[auto wi...

view this post on Zulip Discourse Bot (Jul 28 2020 at 12:00):

Yannick Forster @yforster posted in Notation for inequality chain

Dear all,
I’d like to be able to write
Unset Printing Notations.
Compute (1 <= 2 <= 3 <= 4 <= 5)

and have that result in
le 1 2 /\ le 2 3 /\ le 3 4 /\ le 4 5

Coq ships with a built-in notation a <= b <= c, but I’d like that for arbitrary chain lengths. (I’m not actually interested in the case for le, but for another relation, which shouldn’t make a difference for the approach.)
Any hints or ...

view this post on Zulip Discourse Bot (Jul 30 2020 at 19:28):

OnorioCatenacci @Onorio posted in Software Foundations/Logical Foundations Exercise

I’m currently working through the Lists portion of Logical Foundations and as I’m working through the “Lists Of Numbers” portion I came to the exercise to build an alternate function. This one:

Fixpoint alternate (l1 l2 : natlist) : natlist
(* REPLACE THIS LINE WITH “:= your_definition .” *). Admitted.

This is what I’ve gotten so far:
Fixpoint alternate (l1 l2 :natlist) : natlist
match l...

view this post on Zulip Discourse Bot (Jul 31 2020 at 22:23):

@LailaElbeheiry posted in Applying hypothesis with unknown variables

I’m trying to prove the following lemma about functions on natural numbers
Lemma nat_funcs :
forall (f : nat -> nat -> nat) (P : (nat -> nat) -> Prop),
(forall n, P (fun m => (f n m))) -> P (fun m => f (m + 1) m).

When I proceed and introduce variables to the context, I end up with a hypothesis:
H : forall n, P (fun m => (f n m))

and my goal is:
P (fun m => f (m + 1) m)

I woul...

view this post on Zulip Discourse Bot (Aug 04 2020 at 12:10):

Karl Palmskog @palmskog posted in Proving existence statements about coinductive predicates constructively

As anyone who has worked with Coq’s machinery for coinduction and corecursion knows, the limitations of the cofix operator and the guardedness condition can easily get in the way of progress. However, these limitations appear to me to be particularly difficult to surpass when trying to prove statements of existence (of some term with coinductive type, which satisfies some coinductive predicate).
S...

view this post on Zulip Discourse Bot (Aug 07 2020 at 07:59):

Natasha Klaus @Natasha posted in Exercise from volume 2, Programming Language Foundations. Simply Typed Lambda-Calculus

Dearest friends,
I am stuck on this exercise: Exercise: 3 stars, standard (STLCE_context_invariance)
https://softwarefoundations.cis.upenn.edu/plf-current/MoreStlc.html
[1]
[2]
please advice.
Nat

view this post on Zulip Discourse Bot (Aug 07 2020 at 14:26):

Nick @nickcollins posted in Spacemacs won't let me retract the proof buffer

I’m having an issue - it looks like a bug, but I don’t know what the proper reporting procedure is or how to express a minimal example so I’m hoping for some advice here.
I can use C^c RET to move the proof buffer past its current point, but not back to a previous point. C^c C^r doesn’t work either. When I do these, i get one of two different errors:
Error: the reference Backtrack was not found ...

view this post on Zulip Discourse Bot (Aug 07 2020 at 18:00):

Joseph Palermo @joepalermo posted in Can't compile packages with coqide

I’m going through the Software Foundations book (https://softwarefoundations.cis.upenn.edu/lf-current/index.html) and it asks to compile several simple packages.
For example at the start of chapter 4, the instruction is:
In CoqIDE:
Open Basics.v. In the “Compile” menu, click on “Compile Buffer”.
But I get the following when I do that:
File “/Users/joe/coq/lf/Basics.v”, line 1345, characters 0...

view this post on Zulip Discourse Bot (Aug 09 2020 at 09:55):

@Ruimin posted in Coq Training App

Hi,
We’ve developed an app to help train you / your students in doing proofs in Coq.

All feedback will be most appreciated (you can leave them in-app or on this page).

view this post on Zulip Discourse Bot (Aug 12 2020 at 10:40):

Natasha Klaus @Natasha posted in Subtyping in Simply Typed Lambda-Calculus

Hello,
I am trying to solve this exercise
Exercise: 1 star, standard (subtype_instances_tf_2)
from this chapter
https://softwarefoundations.cis.upenn.edu/plf-current/Sub.html
This statemen below. Is it true?
∃S,
S <: S→S

This is what I think about it:
Going to use 2 rules:
S_Refl and S_Arrow
exists S,
S <: S->S ??? is it true or false, let’s try Exists (S->S)
then
S -> S <: (...

view this post on Zulip Discourse Bot (Aug 12 2020 at 11:02):

Natasha Klaus @Natasha posted in Extended simply typed lyambda calculus substitution for let term

Hello,
I am trying to solve this Exercise
Exercise: 3 stars, standard (STLCE_definitions)
from this Chapter
https://softwarefoundations.cis.upenn.edu/plf-current/MoreStlc.html
Having problems with definition of term let in Fixpoint subst.
This is how I defined it.
Fixpoint subst (x : string) (s : tm) (t : tm) : tm :=
match t with
....
| tlet y t t' =>
if eqb_string x y then (tlet y...

view this post on Zulip Discourse Bot (Aug 12 2020 at 18:41):

@raffalevy posted in Is it possible to define binary trees without a new inductive type?

Binary trees (without any attached data) can be encoded in Coq as the following inductive type:
Inductive bin :=
| Leaf : bin
| Node : bin -> bin -> bin.

Given just the basic types of Coq (dependent functions, unit, sums, products, equality, dependent pairs) as well as the natural numbers, and their respective induction rules, is it possible to encode the type bin without defining a new inductiv...

view this post on Zulip Discourse Bot (Aug 16 2020 at 06:45):

@cookieli posted in Why in silly_ex (the software foundation)the first hypothesis is useless

Here is the code:
Theorem silly_ex :
(forall n, evenb n = true -> oddb (S n) = true) ->
oddb 3 = true ->
evenb 4 = true.
Proof.
intros cond eq. apply eq. Qed.
Why I can’t apply cond and the Theorem doesn’t need cond to prove?

view this post on Zulip Discourse Bot (Aug 16 2020 at 12:11):

Flávio Leonardo Cavalcanti de Moura @flaviodemoura posted in Not a valid ring equation

Hi there,
I’m confused about the ring tactic for Nat. I have two similar exercises for summing up odd Nat numbers. In the first exercises the goal S (n + S (n + 0) + 1 + S n * S n) = S (S n) * S (S n) is solved by the tactic ring. In the second exercise, the goal is n + S (n + 0) - 0 + n * n = S n * S n and the ring tactic is no longer able to solve it: Error: Tactic failure: not a valid ring equ...

view this post on Zulip Discourse Bot (Sep 05 2020 at 09:31):

Karl Palmskog @palmskog posted in A template for organizing a Coq program verification project

Inspired by Emilio Gallego’s guide and repo for developing Coq plugins, I created a template repository showing how one can organize a Coq program verification project according to current best practices using Coq 8.12:

To go marginally above the toy example level, the project verifies a classic program in C using the Verified Software Toolchain. When compiled with CompCert, the program’s contr...

view this post on Zulip Discourse Bot (Sep 06 2020 at 19:38):

Flávio Leonardo Cavalcanti de Moura @flaviodemoura posted in Article latex document class out of a Coq script

Hi there,
I would like to know if there exists a direct way to generate a pdf out of a Coq script annotated with coqdoc using a given latex document class, like article or llncs. I usually do it by first generating the latex output of the coq script file with coqdoc, and then compiling the latex output separately (after some editing), but this sequence of repetitive steps is a bit annoying.
Best...

view this post on Zulip Discourse Bot (Sep 09 2020 at 20:35):

Vadim Zaliva @vzaliva posted in Coqchk

I have a sizeable Coq project of about 50Kloc. It takes about 30 min to compile. Recently I tried to run coqchk on it using the validate target generated by coq_makefile. It has been running for 4 hours and has not yet finished.
Is it normal for it to take so long? Why this process is longer than the actual compilation?

view this post on Zulip Discourse Bot (Sep 17 2020 at 19:02):

Cristina And Pri @Cristina posted in Software Foundations/ Verified Functional Algorithms Exercise

Hi, I’m trying to solve this exercise. It’s from the merge part
Lemma sorted_merge : forall l1, sorted l1 ->
forall l2, sorted l2 ->
sorted (merge l1 l2).
intros. induction l1.

simpl. induction l2.

auto.
auto.

induction l2.

auto.
simpl. bdestruct (a<=?a0).

inv H.
** auto. constructor. auto. auto.
** apply sorted_merge1. auto. auto. auto.

but in the second part of the proof, I do...

view this post on Zulip Discourse Bot (Sep 20 2020 at 22:01):

@Lasse posted in LL(n) notations in Coq

Does anybody know if there is a trick to parse LL(n) notations in Coq? Since Coq uses Camlp5, the standard way of parsing can only handle LL(1) languages. However, on the Ocaml level one can cheat by looking ahead in the token stream. I am wondering if such a thing is also possible with Coq level notations.
I would already be quite happy with a way to parse LL(2). As a concrete example, is it pos...

view this post on Zulip Discourse Bot (Sep 27 2020 at 00:10):

Shea Levy @shlevy posted in Corecursion via destructors?

Hi all,
I’m trying to explore corecursive definitions as “pattern matching” on the destructors of the (potentially coinductive) type to define a destructor of the left hand side of the function type, along with recursion in the coinductive case. For example, I have this working for products and sums:
Section sum.
Variables A B : Type.

Record sum_elim_cases (source : Type) target :=
{ le...

view this post on Zulip Discourse Bot (Oct 01 2020 at 13:34):

OnorioCatenacci @Onorio posted in Another Proof From Logical Foundations Exercises

I’m working through the list exercises of the Lists portion of Logical Foundations (still) and I’ve got to one that I can’t quite finish proving.
Here’s the code:
Theorem eqblist_refl: forall l:natlist,
true = eqblist l l.
Proof.
intros l. induction l as [| n l’ IHl’].

simpl. reflexivity.
simpl. rewrite <- IHl’.
Qed.

And this is what I get in the output:
1 subgoal
n : nat
l’ : natlist
...

view this post on Zulip Discourse Bot (Oct 03 2020 at 04:02):

@sudgy posted in How to utilize extensionality when rewriting

This is an issue that I’ve come up to time and time again, and I was wondering if there was any solution. In general, I have a term that looks like ∀x, <expression>, and I want to rewrite in a part of the expression. I understand that this is not generally doable in Coq, but I use propositional and functional extensionality, and using those I can prove myself that (∀x, <expression>) = (∀x, <rewr...

view this post on Zulip Discourse Bot (Oct 03 2020 at 05:09):

Dan Johnson @Dan posted in How can I use destruct given the constraint I have for index range of a list?

Hi,
I’m trying to prove that for a list of bytes a, all bytes are x01 from index 2 to (n-m-2), where n is the length of a:
(forall (i : nat), ((i >= 2) /\ (i < ((n - m) - 1))) -> ((nth_error a i) = (Some x01)))
And in the context I do have this:
H : nth_error a ?j =
nth_error ([x00; x00] ++ repeat x01 (n - m - 2) ++ repeat x00 m)%list ?j

So, after intros i i_range. I have:
i : nat
i_r...

view this post on Zulip Discourse Bot (Oct 03 2020 at 09:57):

@Lasse posted in PHOAS encoding of pattern matching notations

Hello everyone,
Today I was inspired by this comment of @herbelin to try and embed a programming language that supports pattern matching of product types in Coq using the PHOAS method. And of course, this needs to come with some reasonable notations.
So, I’m starting with a simple PHOAS encoding of lambda calculus with products types, that can be pattern matched in Lam:
From Ltac2 Require Impor...

view this post on Zulip Discourse Bot (Oct 03 2020 at 23:03):

Shea Levy @shlevy posted in Definition equalities for universal properties?

If we view user-defined types as having the universal properties of sums, products, intial algebras, terminal coalgebras, etc. as a category theoretic perspective would suggest, we might want definitional equalities like the following (when well-typed):
f ≡ λ x, match f x with
| (a, b) => (a, b)
end

f ≡ λ s, match s with
| inl a => f (inl a)
| inr b => f (inr ...

view this post on Zulip Discourse Bot (Oct 05 2020 at 17:00):

Clément Pit-Claudel @cpitclaudel posted in What determines whether a custom entry is used for printing?

Hi all.
The following is a simplified example of a problem I’m running into with custom entries:
Axiom set : string -> nat -> unit.
Axiom incr : nat -> nat.

Declare Custom Entry test.

Notation "'custom_set' a ':=' b" :=
(set a b)
(in custom test at level 91,
a constr at level 1,
b custom test at level 0).
Notation "'+1' b" :=
(incr b)
(in custom test at level 0,
b...

view this post on Zulip Discourse Bot (Oct 09 2020 at 20:23):

Ryan Doenges @rhd posted in Inserting PPX annotations into extracted OCaml

There are PPX macros in OCaml that derive json conversions, pretty printers, etc. for datatypes. So if you write something liketype bool = true | false [@@deriving yojson] you get a pair of JSON conversion functions bool_to_json and bool_of_yojson. Is there a way to insert these annotations on Coq datatypes during extraction?

view this post on Zulip Discourse Bot (Oct 10 2020 at 16:13):

@LessnessR posted in Trying to prove sort algorithm correctness (for specific n), in search for hints

So, I have a homework - sort 8 values using minimum number of comparisons and prove that it’s optimal solution. The number is 16 using merge-insertion sort and no less comparisons are possible (informally, because log_2(8!) > 15).
Using Coq isn’t part of the homework, but I want to do it anyway. The actual homework won’t contain any Coq proofs.
The source code looks like this - nested "if"s (thi...

view this post on Zulip Discourse Bot (Oct 10 2020 at 17:53):

Yishuai Li @Lys posted in Pattern matching: warn unused parameter?

Day 1, I defined a type foo and a function bar:
Variant foo := A | B.

Definition bar (x : foo) : bool :=
match x with
| A => true
| B => false
end.

Day 2, I modified type foo:
Variant foo := A | C | D.

but forgot to update bar accordingly. However, bar still compiles—it treated B as a wildcard rather than constructor.
Is there an equivalent to “unused parameter” warning for Coq? If n...

view this post on Zulip Discourse Bot (Oct 20 2020 at 06:35):

Lim Jin Xing @jinxing1990 posted in Why induction principle such as list_rect cannot be added in Hint database?

Hi all. May I ask why is induction principle, say list_rect, cannot be added to any Hint database?
I tried adding it but the error: “list_rect cannot be used as a hint.” appeared.

view this post on Zulip Discourse Bot (Oct 25 2020 at 09:38):

@brurucy posted in Stuck at an advanced Multiset.v exercise

Hello!
I’m working my way around the Multiset.v file from the VFA book and I am hard stuck on the following proof.
Lemma contents_cons_inv : forall l x n,
S n = contents l x ->
exists l1 l2,
l = l1 ++ x :: l2
/\ contents (l1 ++ l2) x = n.

Proof.
destruct l.
simpl.
unfold empty.
discriminate.
simpl.
unfold union, singleton.
intros x.
bdestruct (x =? v).
intros.
exists [], l.
simpl...

view this post on Zulip Discourse Bot (Oct 25 2020 at 09:46):

@brurucy posted in Stuck at Multiset.v contents_cons_inv

Hello!(sorry for the duplicated post, I accidentally deleted the other one)
I’m working my way around the Multiset.v file from the VFA book and I am hard stuck on the following proof.
Lemma contents_cons_inv : forall l x n,
S n = contents l x ->
exists l1 l2,
l = l1 ++ x :: l2
/\ contents (l1 ++ l2) x = n.
Proof.
destruct l.
simpl.
unfold empty.
discriminate.
simpl.
unfold union, singleton.
...

view this post on Zulip Bruno Carneiro (Oct 25 2020 at 12:23):

I'd love if anyone could drop any hints :D

view this post on Zulip Discourse Bot (Oct 26 2020 at 10:19):

Gert Smolka @gert-smolka posted in Bug in universe inference?

Often it matters that Coq places a type in Prop rather than in Type. Here is an example where a type ascription is needed to place a match in Prop.
Inductive even: nat -> Prop :=
| evenB: even 0
| evenS: forall n, even n -> even (S (S n)).

Goal even 1 -> False.
Proof.
refine (fun a => match a in even n
return match n with 1 => False | _ => True end : Prop
...

view this post on Zulip Discourse Bot (Oct 29 2020 at 04:00):

Lim Jin Xing @jinxing1990 posted in Using CoqGym on my own files

Hi, may I ask how could I run ASTactic on the proofs from my own .v files? From what I understand is that, I need to extract the proofs from my own coq files to .json format. I tried to follow the steps in Section 1.3 from https://github.com/princeton-vl/CoqGym#13-extracting-the-proofs-from-coq-code-optional. But I have encounter an error:
Traceback (most recent call last):
File “check_proofs.py...

view this post on Zulip Discourse Bot (Nov 07 2020 at 11:32):

Gert Smolka @gert-smolka posted in Smart Matches

I’m a big fan of smart matches, they provide an elegant transparent abstraction layer for index-dependent plain matches. In practice the dependent elimination tactic coming with the Equations package is nice, but from the proof terms it generates the translation to index-dependent plain matches is not obvious.
I would guess smart matches appeared around 2013 with the new match compiler. What wa...

view this post on Zulip Discourse Bot (Nov 15 2020 at 19:53):

Gert Smolka @gert-smolka posted in Dependent Pair Injectivity equivalent to K

Ever since I learned Coq I was fascinated by the equivalence between dependent pair injectivity (DPI) and K. There are long winded proofs in the Coq library EqdepFacts. It turns out there are very short proofs for both direction. The trick for the direction K to DPI was given to me by Gaëtan Gilbert on Friday at Coq Club, and this was a real eye opener. Below are short proofs for both directions...

view this post on Zulip Discourse Bot (Dec 11 2020 at 19:37):

@ZWY posted in How to avoid awkward assertions

For a proof state
l : list nat
x, m : nat
H0 : 1 <= m
______________________________________(1/1)
nth (m - 0) l 0 = nth m l 0

we can rely on Nat.sub_0_r: forall n : nat, n - 0 = n to prove it.
However, I only know we can first run assert (I1: m - 0 = m) and then use the assertion I1 rewrite I1. reflexivity. to construct a proof.
I think the assertion is rather awkward and want to avoid such us...

view this post on Zulip Discourse Bot (Dec 16 2020 at 00:52):

@LightQuantum posted in Convert ident to string in ltac

This problem is partly related to coq/7922. In that issue, a hack is proposed to convert strings to idents by using ltac2. However, I’m not quite sure how to do it in the reversed way (say, converting idents to strings).
More specifically, I’m trying to do something like (fun (x y: ty) => ...) with
Goal True.
Proof.
match constr:((fun (x y: nat) => x)) with
| (fun (name:_) => _) => some_tac...

view this post on Zulip Discourse Bot (Dec 28 2020 at 12:30):

Jeremy Dawson @jeremydaw posted in instantiating existentials

Hi,
I'm having difficulty using the tactic
  Variant instantiate (num := term)
because I get
lja_dd_ImpL_p < instantiate (0 := l).
Toplevel input, characters 1-21:

instantiate (0 := l).
^^^^^^^^^^^^^^^^^^^^
Error:
Ltac call to "instantiate ( (int) := (lglob) ) (hloc)" failed.
Incorrect existential variable index.
lja_dd_ImpL_p < instantiate (1 := l).
Toplevel input, characters 0...

view this post on Zulip Discourse Bot (Dec 28 2020 at 12:37):

Jeremy Dawson @jeremydaw posted in naming existentials

Hi,
The documentation says
Existential variables can be named by the user upon creation using the syntax ?[ident].
What does this mean? Specifically, where the existential is created by
eapply nrs_rule_indep in n.
I've tried
eapply nrs_rule_indep in n as ?[xxx].
eapply nrs_rule_indep in n ?[xxx].
neither works. How do I name the existential that is created?
Thanks,
Jeremy

view this post on Zulip Discourse Bot (Dec 30 2020 at 09:05):

Huong Vu @huong-vu posted in Fomalisation of Bell and Lapadula model

I read the report: “A full formalisation of BLP model” and find Coq code.
But I can’t run this code. Maybe I do this wrong.
Please tell me if you can run it.

view this post on Zulip Discourse Bot (Dec 31 2020 at 15:25):

Nika Pona @akinanop posted in Tips and tricks to make VST proof development faster

Dear VST developers and everyone who is using VST,
I am working on an industrial verification project that uses Verified Software Toolchain (until now we have ~300 loc verified, but we aim at ~1800 in the near future), and compilation times for common tactics became an issue. In particular, forward, forward_call, entailer! can take up to 1 min to execute. Since proofs range between 500 and 6000 l...

view this post on Zulip Discourse Bot (Jan 04 2021 at 01:16):

Jeremy Dawson @jeremydaw posted in avoiding type error

Hi,
I have a situation as follows:
  H : [(fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [Imp (Var p0) B0], Var p0);
       (fmlsext (Γ1 ++ Imp (Var p) B :: H2) Γ3 [B0], Var p)] = lpst
   ind2 : in_dersrec d2 d1

view this post on Zulip Discourse Bot (Jan 05 2021 at 16:46):

Nicolás Ojeda Bär @nojb posted in Soundness of program transformation

Hello!
Consider the following small (typed) language with conditionals :
Inductive const :=
| BOOL (b : bool)
| INT (n : nat).

Inductive exp :=
| CONST (c : const)
| IFV (e1 e2 e3 : exp)
| ADD (e1 e2 : exp).

Inductive ty :=
| TINT
| TBOOL.

The typing judgement is given by:
Inductive hastype : exp -> ty -> Prop :=
| T_BOOL : forall b, hastype (CONST b) TBOOL
| T_INT : forall n, hastype (CONST...

view this post on Zulip Discourse Bot (Jan 06 2021 at 20:47):

@brando90 posted in What is the difference between Gallina and Ltac?

As I understand, Gallina is the “programming language” embedded in Coq (that one can write proofs later which are checked using the formal system CoC):

The first half of this chapter introduces the most essential elements of Coq’s native functional programming language, called Gallina . The second half introduces some basic tactics that can be used to prove properties of Gallina programs.

refe...

view this post on Zulip sameer gupta (Jan 06 2021 at 22:28):

let pred = function
| O -> O
| S u -> u
Returning 0 as the predecessor of 0 can come across as somewhat of a hack. In some situations, we might like to be sure that we never try to take the predecessor of 0. We can enforce this by giving pred a stronger, dependent type

view this post on Zulip sameer gupta (Jan 06 2021 at 22:29):

let pred = function
| O -> O
| S u -> u
Returning 0 as the predecessor of 0 can come across as somewhat of a hack. In some situations, we might like to be sure that we never try to take the predecessor of 0. We can enforce this by giving pred a stronger, dependent type

view this post on Zulip Discourse Bot (Jan 07 2021 at 17:18):

Nicolás Ojeda Bär @nojb posted in Program equivalence and substitution

Hello,
I have the following question (look for “QUESTION” below) involving the relationship between evaluation and substitution. The result seems intuitive but I can’t prove it, and I wonder if I’m missing something basic. This feels like the kind of thing that should be well-known, so … help! 🙂 Any pointers will be appreciated.
Thanks!
Cheers,
Nicolas
Require Import Coq.Arith.PeanoNat.

(* A...

view this post on Zulip Discourse Bot (Jan 14 2021 at 13:56):

@cbl posted in Force application of fixpoint to its argument

Hi everyone,
I know a lot of stackoverflow questions are close to this one, but I could not get any proposed solution to work. If one turned out to actually work, I’m sorry for the potential duplicate.
When I define a fixpoint function my_function that does not directly pattern match on its argument a, I cannot unfold it and explicitly see the body of the function in my hypothesis.
Here is a ...

view this post on Zulip Discourse Bot (Jan 20 2021 at 02:56):

Kesha Hietala @khieta posted in Can I extract part of a module instead of the whole module?

Is there a way to tell Coq to only extract a subset of the definitions in a module? Here’s a minimal example:
Require Coq.extraction.Extraction.

Module Type AType.
Parameter a : nat.
End AType.

Module BMod (A : AType).
Definition foo : nat := 4 + A.a.
Definition bar : bool := false.
End BMod.

Module AMod <: AType.
Definition a := 3.
End AMod.

Module B := BMod AMod.
Recursive Extractio...

view this post on Zulip Discourse Bot (Jan 21 2021 at 15:58):

Chris Jensen @Cjen1 posted in Is there a way to prove properties about ocaml programs using a Coq verified library

Hi, I’m looking to make things easier for verifying ocaml state machines. With the specific goal of making a ramp into the world of formal verification.
I believe that this to be impossible, but optimally a user could write their state machine using an extracted library in ocaml, and then at a later point start trying to prove things about that state machine.
I think it could be possible via eva...

view this post on Zulip Discourse Bot (Jan 31 2021 at 06:28):

Jesse Sullivan @jesse.denis.sullivan posted in Proving well-founded recursion using the Program module

Hi.
First time posting but after some extensive googling and reading I’m still not quite sure how I should go about proving that a function that I’m writing is a well-founded relation for a non-trivial recursion. I am using the Program module in order to get the proof obligations in order to prove to Coq that my function will terminate but I’ve having difficulty understanding the proof structure...

view this post on Zulip Discourse Bot (Feb 02 2021 at 03:39):

Jesse Sullivan @jesse.denis.sullivan posted in Composing Propositions

Hello again,
Thanks to the help of this community I have been able to successfully get the Programs module to successfully pull in the necessary predicates in order to prove the well-foundedness of my fixpoint function. The version of the file I am currently dealing with is this:
Require Import Nat String List.
Require Import Row.
Require Coq.Program.Tactics.
Require Coq.Program.Wf.

Open Scope...

view this post on Zulip Discourse Bot (Feb 03 2021 at 21:57):

Itaj Sherman @itaj-sherman posted in Contradicting instructions for installation with OPAM

Two sets of instructions for installation with OPAM.
What’s the difference in purpose?

https://coq.inria.fr/opam-using.html (linked from https://coq.inria.fr/download)
itaj

view this post on Zulip Discourse Bot (Feb 05 2021 at 06:29):

@barryjay posted in Inversion of an axiom is bad

I stumbled on the following “proof” of False:
Inductive Comb: Set :=
| K : Comb
| App : Comb → Comb → Comb .
Axiom k_eq : forall y z, App (App K y) z = y.
Lemma don’t_invert_axioms: False.
Proof.
assert(k_instance: App (App K K) K = K) by apply k_eq;
inversion k_instance.
Qed.
The problem is that the equation K KK = K follows from the axiom but its inversion has no solutions. Where can ...

view this post on Zulip Discourse Bot (Feb 06 2021 at 19:40):

Flávio Leonardo Cavalcanti de Moura @flaviodemoura posted in Application of automatic induction principle versus induction tactic

Hi there,
Consider a binary relation over a type and its reflexive transitive closure:
Definition Rel (A:Type) := A → A → Prop.
Inductive refltrans {A:Type} (R: Rel A) : Rel A :=
| refl: forall a, (refltrans R) a a
| rtrans: forall a b c, R a b → refltrans R b c → refltrans R a c.
The corresponding induction principle is given as follows:
forall (A : Type) (R : Rel A) (P : A → A → Prop),
(...

view this post on Zulip Discourse Bot (Feb 12 2021 at 09:48):

Jeremy Dawson @jeremydaw posted in Add LoadPath in Coq 8.12.2

Hi,
I have just upgraded my operating system, which has also involved
getting Coq 8.12.2 (December 2020)
Previously I was using Coq 8.11.2
The command
Add LoadPath "../tense-lns".
now seems to cause an error.
How do I change the command to get the same behaviour?
BTW, I've had a great deal of advice on the Coq-Club mailing list
about using a _CoqProject file, but it seems I can't do this ...

view this post on Zulip Discourse Bot (Feb 24 2021 at 15:09):

@atagunov posted in What axioms are built-in?

Hi, noob’s question: is there a list somewhere of what axioms are built-in into Coq?

view this post on Zulip Discourse Bot (Feb 26 2021 at 20:52):

Atalay Mert Ileri @atalayileri posted in Extraction to Haskell Int type

Hello,
I am trying to extract my project into Haskell. I have a type that handles memory addresses which I want to extract to Haskell Int (instead of Integer).
Which standard library numeric type should I use for this?

view this post on Zulip Discourse Bot (Mar 03 2021 at 15:53):

Paul Jeanmaire @pjm posted in Parametric rewriting under binders

Dear Coq users,
I have a parametric relation myeq that I would like to rewrite under the predicate P whenever both are used with the same parameter. It works well if I declare the appropriate morphism:
From Coq Require Import Setoid Morphisms.

Parameter A B : Type.
Parameter myeq : A -> relation B.
Add Parametric Relation (a : A) : B (myeq a) as myeq_rel.

Parameter P : A -> B -> Prop.
Add Para...

view this post on Zulip Discourse Bot (Mar 07 2021 at 17:21):

Flávio Leonardo Cavalcanti de Moura @flaviodemoura posted in Equality between inductively defined relations

Hi there,
I have a theorem stating that if a binary relation can be split as the union of two other relations (R = union R1 R2) than a certain property holds, where the union is defined inductively:

Definition Rel (A:Type) := A → A → Prop.
Inductive union {A} (red1 red2: Rel A) : Rel A :=
| union_left: forall a b, red1 a b → union red1 red2 a b
| union_right: forall a b, red2 a b → union red...

view this post on Zulip Discourse Bot (Mar 11 2021 at 20:38):

@Kakadu posted in Syntax with backticks

I’m trying to compile old Coq code with a new version and I can’t figure out how change (or make compilable) the code with backticks.
Inductive avl : tree -> Prop :=
| RBLeaf : avl Leaf
| RBNode : forall (x :elt) (l r :tree) (h:Z),
avl l -> avl r ->
-2 <= (height l) - (height r) <= 2 ->
height_of_node l r h ->
avl (Node l x r h).

How to repair this ...

view this post on Zulip Discourse Bot (Mar 19 2021 at 14:11):

Martin C. Martin @martincmartin posted in Defining mathematical function implicitly

In Coq, how do I define a function implicitly, not using Fixedpoint?
For example, define the square root function by f(x)^2 = x.
I looked at the definition of sqrt in std, but it’s a parameter of a module. Do I need a module to define it? I tried:
Module Type Foo.
Parameter Inline bubba : nat -> nat.
Axiom bubba_spec: forall a, bubba(a) * bubba(a) = a.
End Foo.

But I can neither Import n...

view this post on Zulip Discourse Bot (Mar 22 2021 at 12:54):

Pierre Courtieu @Matafou posted in Poll about proofgeneral: do you use "holes"

Hi there,
I am considering removing from proofgeneral the “holes” completion system, given that company-coq provides a better user experience with its yasnippet-based completion. My feeling is that almost nobody uses it. So please tell if you do.

view this post on Zulip Discourse Bot (Mar 22 2021 at 15:01):

Nicolás Ojeda Bär @nojb posted in Reasoning about higher-order program transformation?

Hello !
I am trying to formalize a program transformation which consists of lifting
“ifs” to the top-level of the term. The natural way to express this
transformation is to use a higher-order function taking a continuation as a
second argument (see function phi below).
However, this definition is hard to reason about due to the higher-order argument.
For example, I would like to prove Lemma ...

view this post on Zulip Discourse Bot (Mar 24 2021 at 20:44):

Ignat Insarov @kindaro posted in Solve an exists goal in a field with proof search?

You can see a complete example code at the bottom of the post.
Many usual computer algebra systems, for example Sage Math, have a feature of solving an equation over a field for a variable. That is to say, they can invert functions. But they do not give you any proof. Also, Sage Math in particular seems to have a less powerful language in comparison to Coq, The example I have seems to be out of r...

view this post on Zulip Discourse Bot (Mar 25 2021 at 18:44):

Martin C. Martin @martincmartin posted in Turning "exists unique" into a function in Coq

Take something like the least upper bound property of the reals. Suppose I assume this axiom, suitably expressed in Coq’s logic, i.e. forall S subset of reals, if S is non-empty and exists x such that x is an upper bound on S, then there exists z such that z is an upper bound and if a is also an upper bound, a >= z."
So this means I can create a function, called supremum, from S to least upper b...

view this post on Zulip Discourse Bot (Mar 26 2021 at 05:00):

@barryjay posted in Bug in the parser?

The proof below fails with the error:
“Error: Syntax error: [tactic:red_expr] expected after ‘eval’ (in [tactic:constr_eval]).”
In the example below, “eval” is sometimes parsed using my definition and sometimes not, in ways that I cannot predict.
Am I doing something wrong or is this a bug in the parser?
Set Default Proof Using “Type”.
Ltac mytac k := rewrite (plus_O_n k).
Definition eval2 :...

view this post on Zulip Discourse Bot (Mar 27 2021 at 00:55):

Zoe777 Alt @Zoe777-alt posted in How to express a list of any type X?

Define function itemAtIndex that receives an index n
and a list of any type X, and returns the item in the
list in the given index n. Note that indexing starts
from 0.

view this post on Zulip Discourse Bot (Mar 27 2021 at 12:01):

Ignat Insarov @kindaro posted in What does auto do differently under the hood?

Consider this code:
From Coq Require Import ZArith.
Notation ℤ := Z.
Open Scope Z_scope.

Hint Resolve Z.sub_add: localHints.

Definition f (x: ℤ): ℤ := x - 100.
Definition g (x: ℤ): {y | f y = x} := ltac:(debug eauto with localHints).

It does not type check. But this does:
From Coq Require Import ZArith.
Notation ℤ := Z.
Open Scope Z_scope.
Definition f (x: ℤ): ℤ := x - 100.

Definition g (x: ...

view this post on Zulip Discourse Bot (Mar 29 2021 at 06:12):

@jeromejh posted in Not an inductive product

Hello,
I am experimenting a bit with the Ensembles library (Coq.Sets.Ensembles) trying to prove various trivial things.
When I try to use “destruct” tactic on an Union, I get the error “Not an inductive product”, whereas “apply Union_ind” works fine.
Small self contained example:

Require Import Coq.Sets.Ensembles.
Lemma union_empty_inc: forall U:Type, forall A:Ensemble U,
Included U A (Unio...

view this post on Zulip Discourse Bot (Mar 29 2021 at 18:23):

Frédéric Besson @fajb posted in Rtauto slower than tauto

Hi,
The manual says that rtauto may be sometimes slower than tauto. I am curious, are there concrete example out there?
Is the reason understood?
Thanks,
Frédéric

view this post on Zulip Discourse Bot (Apr 10 2021 at 16:56):

@pat0rb posted in Apparently bad installation of coq (im a newbie)

Hi everyone,
I am new to programming in general and learning to use coq with Software Foundations, so sorry if my questions seem kinda tedious. I can’t access coq IDE by clicking on the icon but only by running coqide from my terminal, and when I do I get the following message:
Gtk-Message: 11:15:01.106: Failed to load module “xapp-gtk3-module”
Also, I get these warnings anytime I try open some...

view this post on Zulip Discourse Bot (Apr 16 2021 at 19:36):

Nicolás Ojeda Bär @nojb posted in Tactics for pattern matching?

Hello,
Is there a way to tell Coq to rewrite a goal/hypothesis of the form
f (match e with p1 => e1 | ... | pn => en end)

by
match e with p1 => f e1 | ... | pn => f en end

?
When reasoning with functions defined using Fixpoint which contain nested pattern matching, I find myself doing a lot of destruct e in order to achieve the same effect, which is tedious and repetitive.
Any additional ad...

view this post on Zulip Discourse Bot (Apr 19 2021 at 18:25):

Atalay Mert Ileri @atalayileri posted in Passing parameters to coqc in dune

How can I enable multicore and/or quick(no proof check) compilation in dune?

view this post on Zulip Discourse Bot (Apr 19 2021 at 21:28):

Atalay Mert Ileri @atalayileri posted in Applying a tactic in depth-first manner

Hello,
I have a tactic, lets call it branch which creates, some number of goals. I have another tactic, let’s call it solve that solves the goal if there is enough information in the context. I want to apply combination of tactics in a depth-first manner. In other words, I want to branch, then try solve new goals, then branch in first goal only. Do this recursively until that branch of goal tree ...

view this post on Zulip Discourse Bot (May 04 2021 at 06:10):

@hhiim posted in Should we need Coq on Android?

The Coq installer is huge (at least on Windows), so is it possible to port Coq to Android phones?
This way, we can prove theorems at our leisure time without having to open the computer.
We can also use it to make a “math game” with the goal of proving theorems.
This looks like interesting!

view this post on Zulip Discourse Bot (May 09 2021 at 19:40):

@saad posted in Finding the right tactics to proof a theorem

Hi!
I’ve been doing a little bit of reading about coq, and I’m not sure how best to prove the following:
Theorem mult_neg: forall (E: Type) (P: (E -> Rbar) -> Prop),
(forall a h, P h -> P (fun t => Rbar_mult a (h t))) ->
forall h, non_neg h -> P h.

Thank you in advance !

view this post on Zulip Discourse Bot (May 12 2021 at 12:43):

@zhengpushi posted in Why Coq cannot compute the equality of two Real number (like R1,1,2,3) directly?

Hi everyone:
I am designing some functions about R type in the Coq standard library Coq.Reals.
I’m so sad that I can’t find/write a function to calculate equality of two Real numbers.
code detail (under Coq 8.13):

From Coq Require Import Reals RMicromega RingMicromega.
Open Scope R_scope.
(* find any boolearn function )
Search (R → R → bool). ( found this:
Reval_bop2: Op2 → R → R → bool
...

view this post on Zulip Discourse Bot (May 23 2021 at 17:06):

@AJ2018 posted in Strong specification of haskell's Replicate function

I’m having a bit of trouble understanding the difference between strong and weak specification in Coq. For instance, if I wanted to write the replicate function (given a number n and a value x, it creates a list of length n, with all elements equal to x) using the strong specification way, how would I be able to do that? Apparently I have to write an Inductive “version” of the function but how?
A...

view this post on Zulip Discourse Bot (May 23 2021 at 23:20):

@CrisTeller23 posted in Using exists in pair proof

Hi! I have wrote this Inductive predicate and part of the proof for its specification:
Inductive SumPairs : (natnat) -> list (natnat) -> Prop :=
| sp_base : SumPairs (0,0) nil
| sp_step : forall (l0:list (natnat)) (n0 n1: nat) (y:(natnat)), SumPairs (n0,n1) l0 -> SumPairs ((n0+(fst y)),(n1+(snd y))) (cons y l0).

Theorem sumPairs_correct : forall (l:list (nat*nat)), { n: nat | SumPairs (n,n) ...

view this post on Zulip Discourse Bot (May 25 2021 at 15:08):

@larsr posted in Evaluating Real numbers to decimal representation

Require Import Reals.
(* Euler's formula in Horner's form *)
Definition pi := (nat_rect _ 0 (fun n p => 2 + p * INR n / (2 * INR n + 1)))%R.

What is the easiest way to evaluate pi 100 and print the first 15 decimals?

view this post on Zulip Discourse Bot (Jun 05 2021 at 15:59):

Donald Sebastian Leung @DonaldKellett posted in Verifiable C: Getting the front element in a linked list based queue

Consider an efficient linked list based implementation of a FIFO queue linked_list_queue.c, achieved by keeping pointers to the both the head and last nodes (labelled front and back respectively) of the linked list so enqueueing at the back of the list can be done in O(1) time:
#include <stddef.h>

extern void *malloc(size_t);
extern void free(void *);
extern void exit(int);

struct node {
int ...

view this post on Zulip Discourse Bot (Jun 13 2021 at 11:20):

@CrisTeller23 posted in Cannot coerce aeval to an evaluable reference

Hi! I have got this code:
Inductive aexp : Type :=
| num : Z -> aexp
| var : string -> aexp
| ONg : aexp -> aexp
| OPl : aexp -> aexp -> aexp
| OMi : aexp -> aexp -> aexp
| OMl : aexp -> aexp -> aexp.

Definition getVal (s:string) (st:M.t Z) : Z :=
match (find s st) with
| Some val => val
| None => 0
end.

Fixpoint aeval (ex:aexp) (st:M.t Z) : Z :=
match ex with
...

view this post on Zulip Discourse Bot (Jun 13 2021 at 15:29):

@CrisTeller23 posted in Cannot guess decreasing argument of fix

Hi! I have got this code:
Inductive insStBool : Type :=
| SBPush : Z -> insStBool
| SBLoad : string -> insStBool
| SBNeg : insStBool
| SBCon : insStBool
| SBDis : insStBool
| SBEq : insStBool
| SBLt : insStBool
| SBSkip : nat -> insStBool.

Definition getVal (s:string) (st:M.t Z) : Z :=
match (find s st) with
| Some val => val
| None ...

view this post on Zulip Discourse Bot (Jun 18 2021 at 16:26):

@brando90 posted in What is the syntax to give an explicit proof object (lambda term) to a lemma in Coq?

I figure out that one can print them (the lambda terms) with Show proof. in the middle of a proof (proof mode) and Print lemma_name but I wasn’t able to actually give one. I won;t print all different attempts I did but here are a few of the identity function/P->P implication I did:
thm_identity' := fun (P : Type) (X : P) => X
: forall P : Type, P -> P.

Lemma thm_identity2 : forall (P:Type), P ...

view this post on Zulip Discourse Bot (Jun 19 2021 at 19:37):

@Kakadu posted in Need help to define CoFixpoint

We have a cofixpoint mplus and going to define cofixpoint bind which just calls mplus in one of the match cases. But Coq complains that definition of bind is ill-formed.
We tried:

To look cofixpoint analogue of fixpoint’s struct trik but no luck
To inline mplus into bind but it introduce other nested recursive calls, and a new definition is still ill-formed.
to look at paco tutorial but we sti...

view this post on Zulip Discourse Bot (Jun 23 2021 at 16:07):

@brando90 posted in How to unset printing everything? (e.g. implicits, notations, etc)

I wanted to unset printing everything. For that, I started of my attempt to only unset printing notation but somehow it’s not working as I expected. e.g.
Print my_notation_eq_fun_def.
Unset Printing Notations.
Print my_notation_eq_fun_def.

Prints the same as the first one:
my_notation_eq_fun_def =
fun x1 x2 : my_nat => eq_refl
: forall x1 x2 : my_nat, x1 [+] x2 = x1 [+] x2

what ...

view this post on Zulip Discourse Bot (Jun 23 2021 at 23:00):

Molly Stewart-Gallus @molossus_spondee posted in Redefining prod as a record?

In my code I enable primitive projections and redefine prod like the following:
Record prod A B := pair { fst: A ; snd: B }.
Full code theories/Defaults.v · master · Molly Stewart-Gallus / Category Fun · GitLab
I need this sort of weirdness because pattern matching on an inductive type has weird behavior. Without this change:
Definition tupleprod '(A, B): Type := A * B.
Has different inference ...

view this post on Zulip Discourse Bot (Jun 25 2021 at 15:54):

@brando90 posted in Does Coq do alpha conversion on it's own?

I recently discovered the Eval cbv in term strategy for reduction but I noticed that my terms were already printed with unique names (alpha-conversion). Does Coq already do alpha-conversion on it’s own?
e.g.
Definition l := forall x y : nat, x = y \/ forall x:nat, x < y.

Print l.

displays:
l = forall x y : nat, x = y \/ (forall x0 : nat, x0 < y)
: Prop

view this post on Zulip Discourse Bot (Jul 04 2021 at 00:31):

@brando90 posted in Why is the crush tactic not found?

Going through a trivial exercise from Adam’s book but my proof general can’t find the tactic crush:
Error: The reference crush was not found in the current environment.

Why? And how do I put it in?
Module nn.
Theorem add_induct2:
forall n, n+0 = n.
Proof.
induction n; crush.
End nn.

view this post on Zulip Discourse Bot (Jul 04 2021 at 19:48):

@YaVeremos posted in Software foundations: stuck at exercise binary_inverse in the Induction chapter

Hi all, this my first time posting. I apologise in advance for any inaccuracies in my handling of the English language.
I’m a self-taught developer currently going through the exercises in Software Foundations. I’m stuck at the Induction chapter’s last exercise, binary_inverse.
The book provides two hints which unfortunately didn’t help me much.
The first is:

You may find you need to go back ...

view this post on Zulip Discourse Bot (Jul 08 2021 at 00:21):

Molly Stewart-Gallus @molossus_spondee posted in Defining and working with trivial finite sets like {x, y, z} easily

Hi
Not sure of the best name for these kinds of sets but it’d be nice if there was a way of defining very trivial finite sets like {x, y, z} easily.
These sort of sets are useful for handling free variables. The free polynomial on two variables x, y N[{x, y}] is an example of the sort of thing I’m interested in. I’m really interested in figuring out variable binders and quantifiers in programmin...

view this post on Zulip Discourse Bot (Jul 18 2021 at 14:27):

@YaVeremos posted in Software Foundations: minustwo not found in Poly.v

I am currently going through the exercises in the file Poly.v from the book Logical Foundations. When trying to step forward to the line Example test_doit3times: doit3times minustwo 9 = 3. I get the error The reference minustwo was not found in the current environment.
I tried running make Basics.vo Induction.vo Lists.vo but that didn’t help.
I suppose I must have missed a step somewhere but I’m...

view this post on Zulip Discourse Bot (Jul 22 2021 at 11:50):

@niuzhi posted in Coq Prove code security

1.Recently, I am studying how to use Coq to prove the security of the code, and whether I can recommend some documents or materials. thank you very much.
2.Does Coq have a plugin for translating source code into HOL?
for eample。Memory leak security issue。
#include <stdio.h>
#include <stdlib.h>
int main(){
char p = (char)malloc(100 * sizeof(char));
p = (char*)malloc(50 * sizeof(char));
free...

view this post on Zulip Discourse Bot (Jul 26 2021 at 13:19):

@KilledTheKat posted in Software Foundations: Normalization Function Exercise

Hey all, I just started making my way through Software Foundations since it seems like a good resource for learning to work with proofs in a computational context, and I’m pretty darn stuck on the last part of first 5 star exercise (binary_inverse in the induction chapter).
I’ve defined the relevant functions as follows:
Fixpoint bin_to_nat (m:bin) : nat :=
match m with
| B0 m' => 2 * (bin_t...

view this post on Zulip Discourse Bot (Jul 28 2021 at 15:48):

Liuyinling @lyl posted in Extraction - System error

I am currently learning Coq from the book “software foundations”. I’ve met one problem when I did the exercise on Extraction. The CoqIDE 8.13.2 cannot execute “Extraction “impl.ml” ceval_step.” The error shows in the console is: System error: “impl.ml: Read-only file system”. I am using MacPro M1.
I tried to change the property of the folder to be readable and writable but it didn’t work. Is it a...

view this post on Zulip Discourse Bot (Aug 01 2021 at 18:36):

Molly Stewart-Gallus @molossus_spondee posted in Dealing with associativity in reduction relations

I’ve run into a problem with giving semantics to categorical programming languages.
Associativity of composition makes reduction relations icky.
A toy example to illustrate the problem (my real code uses actual typing judgments.)
The basic grammar
Inductive obj := unit | empty | prod (_ _: obj) | sum (_ _: obj).
Inductive term : sort -> sort -> Type :=
| id A: term A A
| compose {A B C}: term ...

view this post on Zulip Discourse Bot (Aug 05 2021 at 14:08):

@ZWY posted in A question of understanding the paper "Parametric Higher-Order Abstract Syntax for Mechanized Semantics"

Hi, I am reading the paper “Parametric Higher-Order Abstract Syntax for Mechanized Semantics” and have a question.
[fig5]
The paper says “Figure 5 shows Coq code for this syntax formalization scheme.
We use Coq’s “sections” facility to parameterize the term type
with a type family var without needing to mention var repeatedly
within the definition.” I cannot understand the sentence. Why we d...

view this post on Zulip Discourse Bot (Sep 09 2021 at 23:53):

Molly Stewart-Gallus @molossus_spondee posted in Awkwardness with coinductive universes

I’ve been playing with coinductive universes.

It’s very awkward to manipulate though.
I think my problem might be related to subject reduction?
I think I ought to refactor
CoInductive U :=
| const (T: Type)
| sum (_ _: U)
| prod (_ _: U)
.
To a style like
Variant Tag := Const | Sum | Prod.
CoInductive U := {
tag: Tag ;
const_u: if tag is Const then Type else Unit: Type ;
}.
Not quite su...

view this post on Zulip Discourse Bot (Sep 12 2021 at 06:28):

Piyush P Kurur @piyush-kurur posted in Dune + proof general

So far my understanding is that a project should contain

the dune related files because it is overall a better build system (especially when one has pluggins

Should contain the _CoqProject file and may be the generate make file so that Proof general is easily able to locate the .vo files in interactive setup.

Is my understanding wrong ? Can I setup proof general to look for the .vo files ...

view this post on Zulip Discourse Bot (Sep 14 2021 at 13:11):

Liuyinling @lyl posted in How to use tactic forward_if Q?

I am doing exercise 2 of Verfi_stack. I got stuck because of the tactic forward_if.
The subgoal is illustrated as follows:
1 subgoal
Espec : OracleKind
p : val
i : Z
il : list Z
gv : globals
Delta_specs := abbreviate : Maps.PTree.t funspec
Delta := abbreviate : tycontext
H : Int.min_signed <= i <= Int.max_signed
POSTCONDITION := abbreviate : ret_assert
MORE_COMMANDS := abbreviate : statement
H0 ...

view this post on Zulip Discourse Bot (Sep 17 2021 at 13:29):

@Neo posted in Simple recursive proof

Hello, I try to understand how to prove recusivity.
P(0) is good but P(n+1) with P(n) as hypothesis is harder.
How should I finish the proof here ?
Fixpoint myplus (a b:nat) {struct a} : nat :=
match a with
| 0 => b
| S n => S (myplus n b)
end.

Lemma myplus_assoc : forall a b c : nat,
myplus (myplus a b) c = myplus a (myplus b c).
Proof.
intros.
induction a.
simpl.
reflexivity.

view this post on Zulip Discourse Bot (Sep 20 2021 at 06:52):

Liuyinling @lyl posted in How to define the SEP(R) clauses?

I am now working on proving one lemma of Verif_triang of VC:
Lemma body_push_increasing: semax_body Vprog Gprog
f_push_increasing push_increasing_spec.
Here are my current proofs:

Proof.
start_function.
forward.
forward_loop
(EX i:Z,
PROP(0 <= i <= n)
LOCAL(temp _i (Vint(Int.repr i));
temp _n (Vint(Int.repr n));
temp _st st)
SEP(stack nil st; mem_mgr gv)).

view this post on Zulip Discourse Bot (Sep 20 2021 at 16:09):

@Boytjie posted in An awkward inductive definition that resists destruct

I’m a fairly new user of Coq. I came up with an inductive definition FiniteSet : nat -> Set, for which FiniteSet n is intended to have exactly n elements:
Inductive FiniteSet : nat -> Set :=
(* Taking the successor means we introduce a new element. *)
| Fin_n (n : nat) : FiniteSet (S n)
(* We may lift the elements from the previous set into the next. *)
| Fin_s {n : ...

view this post on Zulip Discourse Bot (Sep 21 2021 at 15:55):

Clément Pit-Claudel @cpitclaudel posted in Can the Equations plugin generate a graph that does not reference the original function?

I’m experimenting with the equations plugin, and I’m surprised by the graphs that it generates. Here is an example:
From Equations Require Import Equations.

Inductive Arith :=
| Const (n: nat)
| Plus (a1 a2: Arith).

Equations eval (a: Arith) : nat :=
eval (Const n) := n;
eval (Plus a1 a2) := eval a1 + eval a2.

The resulting eval_graph is this; notice how it makes references to eval:
Indu...

view this post on Zulip Discourse Bot (Sep 23 2021 at 10:03):

Liuyinling @lyl posted in Why the tactic "apply... with..." cannot be applied to hypotheses?

I am wondering why the tactic apply ... with ... cannot be applied to hypotheses.
Here is an example.
Theorem in_not_nil :
forall A (x : A) (l : list A), In x l -> l <> [].
Proof.
intros A x l H. unfold not. intro Hl. destruct l eqn:HE.

- simpl in H. destruct H.
- discriminate Hl.
Qed.

Lemma in_not_nil_42_take2_no_second_implication :
forall l : list nat, In 42 l -> l <> [].
Proof.
...

view this post on Zulip Discourse Bot (Sep 24 2021 at 12:05):

Paul Jeanmaire @pjm posted in Overload list notation

I have defined a type for non-empty lists and some notations to be able to build them like standard lists.
From Coq Require Import List.
Import ListNotations.

Inductive nlist (A : Type) : Type :=
| nsing : A -> nlist A
| ncons : A -> nlist A -> nlist A.

Declare Scope nlist_scope.
Delimit Scope nlist_scope with nlist.
Notation "[ x ]" := (nsing _ x) : nlist_scope.
Notation "[ x ; .. ; y ; z ]" :...

view this post on Zulip Discourse Bot (Sep 29 2021 at 07:05):

@sudgy posted in Does Universe Polymorphism extend the theory of Coq?

I recently heard about universe polymorphism. From the look of it, it seems to solve a few of the problems I’ve been having. However, before using it, I want to be sure that I won’t run into any unforeseen issues. My main question is this: does universe polymorphism extend the underlying theory of Coq itself, or is it all just a notational trick that re-defines objects in different universes im...

view this post on Zulip Discourse Bot (Oct 05 2021 at 17:01):

Ike Mulder @snyke7 posted in Instances created with ':= ltac:(_)' are much slower than Definitions

I’m trying to have a succinct notation for defining instances using a tactic. However, it seems that defining instances this way may cause a significant slowdown. I’m afraid a self-contained example will be hard to extract, but my situation is similar to the following:
Class C (arg : Prop) :=
class_def : arg -> arg. (* some complicated prop dependent on arg *)

Ltac solve := unfold C; intros a...

view this post on Zulip Discourse Bot (Oct 12 2021 at 16:57):

ELLIS COOPER @taker posted in Newbie Needs Tutor on ZOOM

Howdy,
I am a Coq newbie studying the nahas_tutorial.v (and things like that) in the Coq Ide.
Progress is tough enough for me to ask whether there might be a non-beginner who is willing to take some time, say, via ZOOM (login to be provided), to accelerate my progress.
My goal is to prove theorems in yet-to-be-specified but relatively simple multi-sorted first-order theories-with-equality-per-s...

view this post on Zulip Discourse Bot (Oct 14 2021 at 15:13):

Quinn @quinn-dougherty posted in Importing with aliasing

I’d really like to
From Coq.Vectors Require Import Fin (fin := t).
From Coq Require Import Vector

Check fin. (* nat -> Set *)
Check t. (* Type -> nat -> Type *)

The top line is my made-up syntax that I think conveys the idea. The intuition is python’s from numpy import random as ran.
How can I accomplish this?

view this post on Zulip Discourse Bot (Oct 15 2021 at 15:39):

Quinn @quinn-dougherty posted in Definitions completed with proof scripts are opaque, how to make them compute

I’d like to pass a proof that n > 0 into hd because the type signature t A (S n) -> A is causing me issues.
I’ve been experimenting with filling out Definitions by writing proofs instead of specifying the combinator, because another function I wrote only worked that way for reasons I’ll tell you another time. But this seems to have gone well:
Definition hd_proof {A : Type} {n : nat} (v : t A n...

view this post on Zulip Discourse Bot (Oct 22 2021 at 04:47):

@famubu posted in Constructing heterogeneous lists

Hi.
I wanted to construct a heterogeneous list like
[Vector.t bool 2, Vector.t bool 3]

I was trying to follow Adam Chlipala’s CPDT book and defined an hlist as:
Inductive hlist {A : Type} {B : A -> Type} : list A -> Type :=
| HNil : hlist nil
| HCons : forall (x : A) (ls : list A), A -> hlist ls -> hlist (x :: ls).

The definition was executed without error.
But I couldn’t figure out how to c...

view this post on Zulip Discourse Bot (Oct 22 2021 at 05:06):

@famubu posted in Notation for a coinductive type

I made something like a list that keeps repeating using CoInductive with
CoInductive ilist {A : Type} : Type :=
| icons : A -> ilist -> ilist.

and I can construct its objects without error:
(* Means a list like [[3;4; 3;4; 3;4; 3;4; .....]] *)
CoFixpoint foo := (icons 3 (icons 4 foo)).

How can we make a notation to do the list construction?
I was trying to make a notation that will allow cons...

view this post on Zulip Discourse Bot (Oct 24 2021 at 20:35):

Sami Liedes @sliedes posted in Thinking of using hammer/automation to guide the order of proving lemmas

I’m thinking of ways in which I could use proof automation (currently I’ve tried coq-hammer) in a wider way than merely to help me prove a lemma and then move to a next one. I have a few thoughts here, but especially since I’m rather new to Coq, I’d like to hear if you think my thoughts make any sense.
Background: I’ve been working on an implementation of integer log3 and log3_up (that is, ceilin...

view this post on Zulip Discourse Bot (Nov 02 2021 at 09:40):

Natasha Klaus @Natasha posted in Tvals in my code is the total map, why coq insists it is not?

Hello, I am not able to make this code work.
I expect that tvals in formulaTrue inductive type is a total map. So I should be able to check in
TVar constructor if (tvals var) equals true or not. But Coq gives an error:
Error: Illegal application (Non-functional construction):
The expression “tvals” of type “Type” cannot be applied to the term
“var” : “?T”
Definition var := nat % type.

Defi...

view this post on Zulip Discourse Bot (Nov 02 2021 at 15:33):

Aritz Erkiaga @aerkiaga posted in 'rewrite' doesn't want to match large expression

I have a proven lemma which goes something along the lines of:
Lemma my_lemma : forall (x y : some_type), Foo x y = expression .
Proof.
actual proof
Qed.

And I want to use it in a goal that contains:
Foo (large_expression1) (large_expression2)

However, rewrite * -> my_lemma doesn’t seem to identify that particular occurrence. To further complicate things, expression, large_expression1 and larg...

view this post on Zulip Discourse Bot (Nov 04 2021 at 04:34):

Pratap Singh @pratapsingh1729 posted in Existentially quantified coinductive predicates

How does one prove theorems where the conclusion is an existentially quantified coinductive proposition?
I am attempting to adapt Xavier Leroy’s compiler correctness tutorial; this involves adding traces of events to the source and target languages. For the coinductive infseq predicate, I have done this as follows:
(* the type of states *)
Variable A: Type.
Variable event: Type....

view this post on Zulip Discourse Bot (Nov 13 2021 at 17:29):

Mamuka Jibladze @jib posted in Failing to prove that substituting "by hand" is equivalent to... well, substituting

Posted this on stack overflow, then decided that it is even more appropriate here.
After many failures I discovered a strange thing Coq does that I don’t understand.
Sorry for involved code, I was not able to isolate a simpler example.
I have a formula I call trident in three variables p, q, r.
I then simply write out an instance of this formula with a <-> b in place of p, a in place of q and b...

view this post on Zulip Discourse Bot (Dec 07 2021 at 18:33):

D. Ben Knoble @benknoble posted in Induction with (deprecated) even

Background
I’m exploring different ways of proving the following otherwise tedious proposition:
Lemma tauto1 p: p ↔ (p ↔ (p ↔ (p ↔ (p ↔ (p ↔ (p ↔ (p ↔ (p ↔ p)))))))).

Here are a few sample tactic-based proofs (each line is a separate proof).
tauto.

repeat (split; easy || intros ->).
repeat (repeat split; assumption || (intros; assumption) || intros ->).

But the point of the exercise fo...

view this post on Zulip Discourse Bot (Dec 09 2021 at 07:52):

Natasha Klaus @Natasha posted in SAT solver with a dependent type that guarantees its correctness

Hello,
I am reading book by Adam Chlipala.
http://adam.chlipala.net/cpdt/cpdt.pdf
In chapter Programming with dependent types → Subset types and variations, I faced this exercise:
Implement the DPLL satisfiability decision procedure for boolean formulas in conjunctive normal form, with a dependent type that guarantees its correctness.
An example of a reasonable type for this function would be ...

view this post on Zulip Discourse Bot (Dec 15 2021 at 15:57):

Arthur Charguéraud @charguer posted in How to use a local installation of Coq

Until 8.13, ./configure -local would give me a local installation of coq, for which I had a /bin/ folder that I could include in my $PATH for local use (without the need for an opam switch).
Now the -local flag is gone. I can provide a custom folder to ./configure -prefix, but then it seems that I must provide -coqlib whenever I invoke coqc.
Is there a way to have my bin/coqc automatically look...

view this post on Zulip Discourse Bot (Dec 16 2021 at 14:07):

Piyush P Kurur @piyush-kurur posted in Html/PDF documentation building with dune

With coq_makefile generated Makefile we could do make html for html documentation generation ; what is its dune counterpart. dune build @doc only seems to work for ocaml.

view this post on Zulip Discourse Bot (Dec 17 2021 at 21:28):

Molly Stewart-Gallus @molossus_spondee posted in Confused about nested inductive coinductive types

Given the following definition of ordinals how would you define a nice induction principle over them?
CoInductive stream A := {
head: A ;
tail: stream A ;
}.
Inductive ord := O | S (n: nat) | Sup (s: stream ord).

view this post on Zulip Discourse Bot (Jan 05 2022 at 09:21):

Natasha Klaus @Natasha posted in QuickChick : ternary trees properties

Hello,
I am reading this book
https://softwarefoundations.cis.upenn.edu//qc-current/QC.html
and trying to solve next exercise from the chapter QC : Core QuickChick :

Exercise: 4 stars, standard (bug_finding_tern_tree)
My problem is: I couldn’t find any bug, all tests show “Success”, for both properties:
tern_mirror_path_flip
and
tern_mirrorP
Maybe someone faced same problem.
| TLeaf : Te...

view this post on Zulip Discourse Bot (Jan 08 2022 at 05:43):

Natasha Klaus @Natasha posted in Coq QuickChick : Making propery Checkable, Decidable, Arbitrary (Gen)

Hello,
I am trying to test simple conjecture with QuickChick:
Conjecture lists_eq : forall (l : list string), l = l.

QuickChick lists_eq.

but I get this error:
Unable to satisfy the following constraints: ?arg_2 : “Checkable (forall l : list string, l = l)”
I know I need to make my property Instance of class Checkable, but how should I do it?
I made decidability on two lists (successfully)...

view this post on Zulip Discourse Bot (Jan 10 2022 at 11:47):

@MathieuDehouck posted in Difference between P -> Q and P /\ Q

Dear Coq users,
I’ve been using Coq like 5 years ago, and then decided to use it again recently.
I’m starting to make harder proofs and I have two main problems.
In general I find it really hard to find simple answer to simple questions like how to replace “~ a <> b” with “a = b” (I think I lost 4 hours online and trying other stuffs on this one).
I have similar problem with using “exists!”.
A...

view this post on Zulip Discourse Bot (Jan 21 2022 at 17:05):

@MathieuDehouck posted in Prooving the length of a list under constraint

Dear all,
I am going a bit further in my Coq journey and I am confronted with a new problem.
I don’t exactly know if it’s the property that I have illdefined or if it is the proof process that I miss, si here it is:
I want essentially to prove that a list of booleans where each element is different (unique) has at most a size of 2.
My lemma looks like that :
Lemma there_are_two_bools :
foral...

view this post on Zulip Discourse Bot (Jan 25 2022 at 15:51):

Sam Lasser @slasser posted in Building a project with coq_makefile, using a library specified in .coqrc

I have two Coq projects with the following structure:
A/
_CoqProject
Foo.v
B/
_CoqProject
Bar.v
My .coqrc file contains the following command:
Add LoadPath “path/to/A” as A.
After building project A, I can use Proof General to open Bar.v and import definitions from project A (e.g., Require Import A.Foo), which is what I expect because of the contents of .coqrc.
However, when I use coq_ma...

view this post on Zulip Discourse Bot (Jan 25 2022 at 21:17):

Mark Raynsford @io7m posted in Ill-formed recursive definition using let fix

Hello!
I’m trying to write a specification for a binary file format. The format can be expressed fairly tidily using an expression language, but the inductive expression definition contains a couple of lists and so needs a special induction principle. There’s a well-known tree example in the Coq codebase, and I used that as a guide. Unfortunately, the resulting Fixpoint is apparently ill-formed, ...

view this post on Zulip Discourse Bot (Jan 27 2022 at 21:33):

@l1yefeng posted in How to assume an identifier bound to a type with decidable equality using Coq.Structures.Equalities?

Hi. Within a section I can use
Parameter A : Type.

to assume A to be a type. I would like to constrain A so that it is any type with decidable equality. I found Coq.Structures.Equalities.HasEqDec but don’t know how to use it.

view this post on Zulip Discourse Bot (Feb 06 2022 at 03:19):

@sudgy posted in Applying a theorem that doesn't match exactly

Let’s say I’m trying to prove something of the form “P a”. In the context, I have “P b”. Now I know that “a = b”, which I can then use to complete the proof. However, at times “a” and “b” are complicated expressions, and I would like to be able to tell Coq to use “P b” and generate the goal “a = b” itself rather than me having to type the complicated expressions in.
That being said, my questio...

view this post on Zulip Discourse Bot (Feb 14 2022 at 20:24):

@brando90 posted in How to install Coq when it says the repository cannot be found?

This seems like a a weird question. I got a new mac m1 machine and I can’t install coq (maybe its unrealted to that). Opam seems fine but when I try to pin a new coq version it can’t find the repo:
(base) brandomiranda~ ❯ opam pin add coq 8.15.0
[ERROR] Package coq has no known version 8.15.0 in the repositories

anyone know how to fix this?
cross: How does one install a new version of Coq when ...

view this post on Zulip Discourse Bot (Feb 21 2022 at 05:25):

Georgio Nicolas @georgio posted in How to create a Powerset of MSetList?

Hello,
I am creating an MSetList of Strings P, and I would like to obtain the Powerset of P. I am not being able to figure it out.
Code below.
Thanks for your help :smile:
Require Import
Coq.MSets.MSetList
Coq.Strings.String
Coq.Structures.OrdersEx.

Module set := Make OrdersEx.String_as_OT.

Definition P := set.add "A"%string (set.add "B"%string (set.add "C"%string (set.ad...

view this post on Zulip Discourse Bot (Feb 23 2022 at 14:41):

Péter Bereczky @berpeti posted in How to use coqc's verbose option?

Hello,
I noticed that the -verbose option of coqc does nothing anymore (in version 8.15.0), however, it is still in the manual of coqc. Has this functionality been removed?
Thanks for your help!

view this post on Zulip Discourse Bot (Mar 02 2022 at 08:31):

Vincent @vsiles posted in How to state mutual/nested lemmas

Hi ! I have a nested inductive type that look like a tree, with a custom induction principle to account for the nested usage of list: shack/lang.v at main · facebookresearch/shack · GitHub
So far I never had to state mutually recursive properties on both lang_ty and list lang_ty, so this induction principle was enough.
I am now facing a situation where I want to mutually prove something on them....

view this post on Zulip Discourse Bot (Mar 03 2022 at 09:53):

Vincent @vsiles posted in Help with notations that "look alike"

Hi !
To make my files more readable, I’d like to use two notations:

T <: U on one hand
Ts <: vs :> Us on the other hand. For the curious, vs is about variance so this one reads as “forall i, Ti <: UI if vi is Invariant / Covariant and Ui <: Ti if vi is Invariant / Contravariant”

I’m a bit lost in the notation/priority two allow both notations to use the <: symbol.
Is this possible ? Or should...

view this post on Zulip Discourse Bot (Mar 03 2022 at 20:33):

@brando90 posted in How to have vscode fidn coq?

I was trying to use coq in vscode but I can’t seem to make it to work.
Error:
Could not start coqtop (coqtop)

I get this option:
[enter image description here]
which is puzzling since my terminal seems to know just fine where coq is:
(meta_learning) brandomiranda~/sketching-learning-coq ❯ coqc -v
The Coq Proof Assistant, version 8.14.1
compiled with OCaml 4.10.2
(meta_learning) brandomiranda...

view this post on Zulip Discourse Bot (Mar 04 2022 at 14:09):

@brando90 posted in How to activate the messages window in vscode like the coqide has?

I am expecting something in my messages bar but I don’t see it
Example script:
Fixpoint add_left (n m : nat) : nat :=
match n with
| O => m
| S p => S (add_left p m)
end.

Lemma demo_1 :
forall (n : nat),
add_left n O = n.
Proof.
intros. (* goal : add_left n O = n *)
let add_left_red := eval red in add_left in (* reduce add_left, but leav...

view this post on Zulip Discourse Bot (Mar 06 2022 at 13:38):

John Weston @jwnhy posted in Verify a intrusive linked list is memory safe with Coq

Hello, I am new to this community and just finish reading Logic Foundation & TAPL.
After reading these two books, I plan to prove something in my own field, system programming.
So I took a “intrusive list” implementation and hope to prove some property of it.
As it is related to memory, I decide to use a FMapList to represent the memory.
Inductive LinkedList : Type :=
| node (self: nat) (n: ...

view this post on Zulip Discourse Bot (Mar 13 2022 at 03:30):

Molly Stewart-Gallus @molossus_spondee posted in Indeterminate value for partial functions trick

There’s an old truck for encoding partial functions with opaque or postulated values.
Axiom unknown: nat -> nat.

Fixpoint sub m n :=
match m, n with
| _, O => m
| S m', S n' => sub m' n'
| O, S n' => unknown n'
end.

Instead of axiom I think you can do
Definition unknown (n: nat) := n.
#[global]
Opaque unknown.

But I’m not quite sure how opaque values work in Coq.
I think you m...

view this post on Zulip Discourse Bot (Mar 14 2022 at 02:35):

John Weston @jwnhy posted in More informative response to stucked proofs?

When using Coq, I am kind of tending to focus my current goal the Coq gives me.
However, there are cases where the current goal is inpossible to prove.
this is a (inproper?) example
Theorem double_injective_take2 : ∀ n m,
double n = double m →
n = m.
Proof.
intros n m.
(* n and m are both in the context *)
generalize dependent n.
(* Now n is back in the goal and we can do induction ...

view this post on Zulip Discourse Bot (Mar 20 2022 at 01:44):

Ian @nobrowser posted in Stdlib documentation online?

The is a hyperlink in the online manual which purports to point to the stdlib modules documentation:

The different modules of the Coq standard library are documented online at https://coq.inria.fr/stdlib.

However, when I click on that I get a 404. Does that document exist? If not online, maybe in a PDF version?

view this post on Zulip Discourse Bot (Mar 21 2022 at 01:21):

Ian @nobrowser posted in Saerch in VSCoq

Somehow none of the Search commands seems to do anything for me. Check and About works.
I have coqtop inside an opam switch, but I know that’s not a problem because I can check my proofs normally.
I’m using VSCodium 1.65.2.

view this post on Zulip Discourse Bot (Mar 24 2022 at 20:54):

@brando90 posted in What is a hammer/atp within the logic of coq that does things like induction in coq?

I was curious about ATPs within the logic of Coq itself (e.g. that do induction sort of smartly). Do people know of tools better than sauto, coqhammer? (note SMTCoqhammer also uses FOL solvers/atps so I don’t think that’s quite what I’m curious about)
I had a similar discussion (that sort of ended) in Coq hammer’s gitissues: Extending hammer/sauto to use induction? · Issue #125 · lukaszcz/coqham...

view this post on Zulip Discourse Bot (Mar 27 2022 at 03:48):

Ian @nobrowser posted in Completely confused by a trivial SSR proof with case

Given this:
Inductive color := Black | White.

Inductive point_state :=
| Occupied of color
| Empty
.

this works:

Fact ps_case ps:
ps = Occupied White ∨ ps = Occupied Black ∨ ps = Empty.
Proof.
case: ps => [c|].

- by case: c; auto.
- by auto.

Qed.

but this doesn’t (it complains “no applicable tactic”):
Fact ps_case ps:
ps = Occupied White ∨ ps = Occupied Black ∨ p...

view this post on Zulip Discourse Bot (Mar 28 2022 at 06:25):

Ian @nobrowser posted in Annoying warnings when Requiring/Importing ssreflect

I use Ssreflect by including this line at the top of my .v files:
From mathcomp Require Import ssreflect ssrfun ssrbool.
When compiling my code I always get a bunch of warnings like this:
File "./Board_definitions.v", line 3, characters 0-54:
Warning: Notation "[ rel _ _ | _ ]" was already used in scope fun_scope.

I thought I could work around it by wrapping the import line like this:
Set War...

view this post on Zulip Discourse Bot (Apr 01 2022 at 02:33):

Flávio Leonardo Cavalcanti de Moura @flaviodemoura posted in Functional induction with remember

Hello, I am playing with a formalization mergesort based on the following merge function:
Definition len (p: list nat * list nat) :=
length (fst p) + length (snd p).

Function merge (p: list nat * list nat) {measure len p} :=
match p with
| (nil, l2) => l2
| (l1, nil) => l1
| ((hd1 :: tl1) as l1, (hd2 :: tl2) as l2) =>
if hd1 <=? hd2 then hd1 :: merge (tl1, l2)
else hd2 :: merge (l...

view this post on Zulip Discourse Bot (Apr 13 2022 at 03:19):

Eden Chan @onlychans1 posted in How to import Basics.v in Induction.v of LF

https://coq.vercel.app/ext/sf/lf/full/Induction.html
I am using VSCode Coq extension.
I am having an error with
From LF Require Export Basics.
in Induction.v
[image]
I am running

view this post on Zulip Discourse Bot (Apr 13 2022 at 16:12):

@chokristine posted in DFA In COQ

Im trying to define a generalized DFA in COQ. I think I did it with this
[Screen Shot 2022-04-13 at 12.03.47 PM]
But Now I am trying to make an example DFA that accepts strings with an even number of 1s. (which i can’t attach because i can only attach one image)
The problem I’m running into is saying that it accepts all strings that have an even number of 1s. I think we would do that by saying ...

view this post on Zulip Discourse Bot (Apr 25 2022 at 22:22):

Molly Stewart-Gallus @molossus_spondee posted in One weird trick to encode modal types

You can encode modal logics using the module system.
Also private inductive types work for this.
But I’m not really sure this is quite correct or meaningful.
Module ATheorem.
Axiom t: Set.
Axiom v: t.
End ATheorem.

Module Type Modal.
Axiom N: Set -> Set.
Axiom extract: forall {A}, N A -> A.
Module Necessity (M: ATheorem).
Axiom necessity: N M.t.
Axiom extract_necessity: extra...

view this post on Zulip Discourse Bot (Apr 26 2022 at 16:03):

Anthony Peterson @apeterson-BFI posted in Using Add Relation for Setoid equivalence of rationals

I like the build up the basic types such as Integers and rationals to understand how the Coq system works, and I’m trying to establish Setoid equivalence of the rationals, but I’m not sure quite how to tell the system that I’m doing that.
In the standard library for the rationals, it starts doing Instance stuff, which is something I have not learned yet, so I was trying to go back to what is in G...

view this post on Zulip Discourse Bot (Jun 04 2022 at 17:49):

@io7m (Mark Raynsford) posted in Induction hypothesis vs. termination checker

Hello!
I have the following slightly odd induction hypothesis for lists:
Definition list_induction_3 :
∀ (A : Type),
∀ (P : list A → Prop),
P [] →
(∀ (r : A), P (r :: [])) →
(∀ (r0 r1 : A) (rest : list A), P rest → P (r1 :: rest) → P (r0 :: r1 :: rest)) →
∀ (L : list A), P L :=
λ A
P
P_nil
P_1
P_more,
fix f (l : list A) :=
match l with
| [] ...

view this post on Zulip Discourse Bot (Jun 08 2022 at 21:12):

@brando90 posted in Official place to learn how to setup Coq make files for beginner

I come from interpreted languages, so I have little to no knowledge how the set up for Coq should be so that I can have it in the right project structure and so that it works with make etc.
Is there an official place to learn this? I found a list of a few but didn’t feel they were super beginner friendly (or perhaps they assumed I have experience with make files, compiled languages? not sure). Bu...

view this post on Zulip Discourse Bot (Jun 11 2022 at 16:56):

@io7m (Mark Raynsford) posted in Decidable equality with Prop-carrying type

Hello!
In a development I’m working on, I have a type that represents the combination of a string and a proof that the string is “valid” according to some rules. Validity is decidable, and I’m trying to show that equality of names is decidable, but I’m running up against something I don’t know how to solve:
Require Import Coq.Lists.List.
Require Import Coq.Unicode.Utf8_core.
Require Import Coq.S...

view this post on Zulip Discourse Bot (Jun 13 2022 at 05:02):

@angelbeats posted in Setoid_rewrite failed, but succeeded when using '<-' or 'at'

Only l4 failed. What instance should I add to make this work?
Require Export Coq.Strings.String.

Definition eqb_string (x y : string) : bool :=
if string_dec x y then true else false.
Definition total_map (A : Type) := string -> A.
Definition t_update {A : Type} (m : total_map A)
(x : string) (v : A) :=
fun x' => if eqb_string x x' then v else m x'.

Definition f {A : Typ...

view this post on Zulip Discourse Bot (Jun 23 2022 at 06:31):

@nobrowser (Ian) posted in Apply: versus apply

I am really, really confused by the difference between the normal apply tactic and the ssreflect apply: tactic.
Here’s a script, the beginning of a toy formalization of Go/Weiqi/Baduk rules. In the last proof, in the intermediate sub-lemma H2, if I replace apply with apply: , I get an error. Why?
(* Support ssreflect tactic language and finitary modules. *)
Set Warnings "-notation-overridden".
F...

view this post on Zulip Discourse Bot (Jul 01 2022 at 16:25):

@Andreas-Hofmeister (Andreas Hofmeister) posted in "Qed." takes a long time

I am writing a chess program in Coq and encountered a strange problem. The “Qed.” command after one of my proofs seemed not to terminate. The proof itself is ok (all green in CoqIDE).
I simplified the code to isolate the problem and found that the time it takes for the “Qed.” to finish depends on the size of the chess board. If the board is 4x4, it takes a few seconds. If the board is 5x5, it tak...

view this post on Zulip Discourse Bot (Jul 05 2022 at 18:48):

@imaxw (Ian Maxwell) posted in SProp question: What can I actually do with a (Squash P) value?

Hi all, new to Discourse in general and this group in particular. I’ve known about Coq for years and played with it on and off, never done much serious development in it.
I recently learned about SProp and was particularly interested in its sigma types since I assume they would behave more like “real subsets”. But at the moment it looks like, short of reinventing the entire logic library in SProp...

view this post on Zulip Gaëtan Gilbert (Jul 05 2022 at 19:32):

anyone else getting "page not found"?

view this post on Zulip Discourse Bot (Jul 06 2022 at 22:31):

@imaxw (Ian Maxwell) posted in Indiscernibility of bisimilar coinductive values: can I prove it?

I’m attempting to follow along in Coq with this paper showing that the statement of the Cantor-Bernstein Theorem implies the law of excluded middle (but using coinductively defined conatural numbers rather than the definition of ℕ∞ given in the paper), and I’m hitting a wall right around Lemma 3.5:

Let Q ∈ 2^ℕ∞ be given. If Q(ω) = 1 and ∀n ∈ ℕ. Q(n) = 1, then ∀p ∈ 2^ℕ∞. Q(p) = 1.

My understand...

view this post on Zulip Discourse Bot (Jul 07 2022 at 18:56):

@HuStmpHrrr (Jason Hu) posted in Using Coq platform on Mac

Hi,
I follow the steps here platform/README_macOS.md at 2022.01.0 · coq/platform · GitHub
to install 8.15.2022.04 release on my Mac Pro M1. I am now able to launch CoqIDE on applications.
However, I am not able to run coqc on command line. The doc says that I need to add a path to PATH, but I expect that Coq platform somehow manages to hook up with opam and create a switch, but it is not happen...

view this post on Zulip Discourse Bot (Jul 22 2022 at 16:08):

@brando90 posted in Print the curried version of a function (i.e. explicitly printing the functions as an explicit chain)

I have functions (e.g. proof terms) like:
(fun (A B : Prop) (a0 a1 : A) => ?Goal).

but I’d like to print the curried version (I want to curry it):
(fun (A B : Prop) => fun (a0 a1 : A) => ?Goal).

How does one do this in Coq? It seems:
Set Printing All.

didn’t do what I wanted nor does googling "pretty printing in coq lead to too many useful results.

references:

currying, In mathematics an...

view this post on Zulip Discourse Bot (Jul 24 2022 at 20:49):

@randl (MRandl) posted in Reusing values from inductive relation

Hi !
I recently found out about encoding relations as inductives. I am currently experimenting with these. I tried to create a simple stack automaton with two operations : Const a, which puts the value a on top of the stack, and Plus, which takes two values from the top of the stack and puts back their sum.
I encoded a relation that says that an operation is legal on a given stack :
Require Imp...

view this post on Zulip Discourse Bot (Jul 26 2022 at 19:00):

@egrr posted in Is it possible to suppose the falsity of the goal and proof False in Coq?

Hi,
Here is my lemma:
Lemma dummy (P : Prop) (h : P) : P.

And now I would like to add nh : ~P to my context and let the goal be False.
I have this question because I can see that there are many lemmas of contrapositive in mathcomp (like contra_not_eq, contra_not_neq…), and quite a long ago when I was using Lean there was the by_contradiction tactic that does this. We can then use by_contradict...

view this post on Zulip Discourse Bot (Jul 31 2022 at 07:50):

@LuoYI posted in The reference omega was not found in the current environment

I am reading Software Foundation and it used tactic “omega” in a proof. But coq says “The reference omega was not found in the current environment.” There are only OmegaLemmas and PreOmega under “coq-platform\lib\coq\theories\omega”

view this post on Zulip Discourse Bot (Aug 09 2022 at 12:10):

@io7m (Mark Raynsford) posted in "Correct" way to structure modules

Hello. I’m going through what I assume is the normal rite of passage for Coq users, which I assume usually ends in a vow never to use the module system for anything ever again. 🙂
I’m trying to work out the “correct” way to structure something. This isn’t a real project, I’m just trying to work out what the best practices are. Here’s a trivial example:
Require Import Coq.Arith.PeanoNat.

Module T...

view this post on Zulip Discourse Bot (Aug 09 2022 at 21:08):

@imaxw (Ian Maxwell) posted in Choosing between SProp and axiomatic proof irrelevance

Although the SProp sort is still marked as experimental in the Coq documentation, given that it has been present for some three years I think one can guess it is here to stay in one form or another. Given that, I’ve started looking into using it as an alternative to importing Coq.Logic.ProofIrrelevance when I need or want a proof-irrelevant sort.
In my handful of experiments, working with SProp h...

view this post on Zulip Discourse Bot (Aug 10 2022 at 21:02):

@io7m (Mark Raynsford) posted in Is there a solution for the problematic induction hypotheses generated using eqn:H?

Hello!
The following is a severely stripped down piece extracted from a larger development. The proof (at least in the real development) appears to require the use of the eqn:... construct:
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.

Inductive identifier := {
id_number : nat;
id_name : string
}.

De...

view this post on Zulip Discourse Bot (Aug 12 2022 at 02:06):

@sudgy posted in Speed of Program Instance

When giving an instance of a type class, I’ve been preferring using Program Instance instead of proving a lemma then using Instance because it feels cleaner and then I won’t have a lemma I never use polluting the namespace. However, I recently found that at times using Program Instance has a noticeable slowdown compared to the lemma approach. Is this something that people have encountered before...

view this post on Zulip Discourse Bot (Aug 14 2022 at 13:20):

@io7m (Mark Raynsford) posted in Print Module [Type] lacks types

Hello!
Consider this file:
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.FSets.FMaps.
Require Import Coq.FSets.FMapAVL.

Module StringMaps <: FMapInterface.S := FMapAVL.Make (String_as_OT).

Calling Print Module or Print Module Type on StringMaps shows useful information about the members of the module:
Module
StringMaps
: Sig
Module E
Module...

view this post on Zulip Discourse Bot (Aug 16 2022 at 19:28):

@Suneel posted in Efficient algorithms using tree

Dear friends,
I want to write an efficient algorithm for some task in hand. Currently, I am doing it using lists. The main operations I need to use are remove minimum/maximum and insert. For this, currently I am keeping a sorted list but the issue is this takes O(n) comparisons for insert. Hence, I am planning to use tree to make it work O(logn) on extracted programs.
One way I can see , this is...

view this post on Zulip Discourse Bot (Aug 18 2022 at 10:53):

@io7m (Mark Raynsford) posted in Modules vs. generalized rewrite

Hello!
I have the following file:
Require Coq.FSets.FMaps.
Require Coq.FSets.FMapAVL.

Require Coq.Strings.String.
Require Coq.Structures.OrderedTypeEx.

Module Maps : FMapInterface.S with Definition E.t := String.string :=
FMapAVL.Make OrderedTypeEx.String_as_OT.

(* Maps.E.t = String.string *)
Print Maps.E.t.
(* eq = Logic.eq *)
Print OrderedTypeEx.String_as_OT.eq.
(* eq = ??? *)
Print Maps....

view this post on Zulip Discourse Bot (Aug 27 2022 at 13:05):

@MMY posted in Coq and denotational semantics

Hello,
I am very new to Coq.
As part of a project, I need to create denotational semantics and test it with Coq.
I’m trying to transform a piece of code into Coq but I don’t know how!
Below is the part of the sematics and my test in Coq:
[image]
Definition assignment (var:Exp)( e:Exp) (rhoF :Envf )(rho:Env )(s:State)(Ks :Cs): mSStm :=
let (K0e : Ce) := (v0 , s0) => Ks((rho var) → v0)
in le...

view this post on Zulip Discourse Bot (Sep 08 2022 at 20:39):

@jeanas (Jean Abou Samra) posted in Defining functions in proof mode

I’m relatively new to Coq. I’ve learnt that proof mode is not restricted to constructing proofs (terms whose type is a proposition), but can in fact construct any term. I like this a lot because I’m not yet familiar with all Gallina ways of doing things, and more familiar with tactics. So, instead of doing
Fixpoint even (n : nat) :=
match n with
| O => True
| S O => False
| S (S n') => ev...

view this post on Zulip Discourse Bot (Sep 09 2022 at 10:54):

@louih0 posted in Divmod equation

I’m stuck with a proof because I don’t know how to deal with divmod equations. Here’s what I need to prove.
fst (Nat.divmod (n * (n - 1)) 1 0 1) + n =
fst(Nat.divmod (n - 0 + n * (n - 0)) 1 0 1)

view this post on Zulip Discourse Bot (Sep 13 2022 at 15:39):

@jeanas (Jean Abou Samra) posted in Best way to express that a type is inhabited in a way that allows getting the habitant

Hi,
Here is a small example demonstrating the gist of my question:
Definition injective {A B : Type} (f : A -> B)
:= forall a a', f a = f a' -> a = a'.

Definition infinite (T : Type) := exists (f : nat -> T), injective f.

Goal
forall P,
let S := {n : nat | P n} in
(exists s : S, True) /\ (forall s : S, exists s' : S, proj1_sig s < proj1_sig s')
-> infinite S.
Proof.
intro...

view this post on Zulip Discourse Bot (Sep 16 2022 at 20:41):

@yiyunliu posted in What is unsafe about the Ltac2.Constr.Unsafe module?

I find it very handy to have the AST of constr around for writing tactics. However, it is a little unnerving that kind is placed under the Unsafe submodule.
In what sense is it unsafe? Will it cause coq to crash or make my proof unsound?
I saw functions such as is_constructor are exported as safe functions. My guess is that as long as I don’t use the AST to construct terms but only traverse/read...

view this post on Zulip Discourse Bot (Sep 23 2022 at 18:59):

@sudgy posted in Typeclasses on functions

I was trying to use typeclasses to generalize the different notions of homomorphisms, but I’ve run into an annoying issue. Consider this code which demonstrates the issue:
(* Note that I don't actually have this class in my real code, this is just the
simplest way I could find to demonstrate the issue. *)
Class Trivial {U V} (f : U -> V) := {
trivial : forall a b, f a = f b
}.

Definition ze...

view this post on Zulip Discourse Bot (Sep 25 2022 at 21:37):

@brando90 posted in Generating latex from coq theorems (Coq to Latex)

I wanted to generate latex from coq. Not sure what the different options that exist but one that would be nice for me would be to do it in coqtop (or serapi) e.g.
print_coq2latex theorem_name.

or
print_coq2latex forall n: Nat, n + 0 = n.
$ forall n \in \matbbb N, n + 0 = n $ (or whatever latex)

Generating latex files might be fine too but the focs here don’t provide concrete examples of how to...

view this post on Zulip Discourse Bot (Sep 28 2022 at 09:41):

@absalom posted in Can I achieve some specific project with Coq?

Hi, I am a ~50 years old teacher in Computer Science; I have encountered references to Coq for many years without taking the time to investigate more about it yet. I am much into functional programming and curious about learning new languages/systems.
However I have a very specific project in mind and I would like if learning Coq for it would be the best choice.
I am expecting to teach some shor...

view this post on Zulip Discourse Bot (Oct 05 2022 at 12:47):

@robuloidacea posted in How to be good in formal verification?

Today I don’t believe in software. Errors are easy to do. When I write code, I have error. I feel that I am not a reliable coder.
To avoid that, I decide to learn formal verification. I start with the lessons on the Software Foundations website. I can understand the content of the lesson. It is theoretical but practical. Still, I think I’m not good in that yet.
Every time I try the theorem, I ha...

view this post on Zulip Discourse Bot (Oct 16 2022 at 19:28):

@AssertionError (Tiago Cogumbreiro) posted in Is it possible to share binary-only libraries across OSes?

Hi everyone,
Is it possible to distribute Coq binaries (.vo) across OSes?
I noticed that Coq complains when I use different versions of Coq and if I use different versions of OCaml. So if I were using the same version of ocamlc and coqc work?
Alternatively, is anyone aware of free CI/CD services for coq and macOS?

Context
I use Coq to teach a couple of courses and one of the main challenges I...

view this post on Zulip Discourse Bot (Nov 04 2022 at 17:01):

@jeanas (Jean Abou Samra) posted in Type (let (a, b) = ... in something a) vs. (something (let (a, b) = ... in a))

Hi,
I’m stuck on proving something that seems very basic.
(* The type of binary relations *)
Definition Relation (A : Type) := A -> A -> Prop.

(* A relation terminates if it has no infinite chain *)
Definition terminates (A : Type) (R : Relation A) : Prop :=
~(exists u : nat -> A, forall k, R (u k) (u (S k))).

(* The "parallel product" of two relations *)
Definition parallel_product (A B : T...

view this post on Zulip Discourse Bot (Dec 05 2022 at 19:53):

@brando90 posted in How does one print proof terms as de bruijn indices instead of random named variables in Coq?

I wanted to print/see my proof terms as de bruijn indices. How do I do this?
I know Show Proof. shows me the proof term.
Thanks!

view this post on Zulip Discourse Bot (Dec 06 2022 at 15:50):

@ZWY posted in Understand the reduction behind apply

I am working on Software Foundation, the volume of Verified Functional Algorithm. I encounter a state Permutation [] ([] ++ []).
Although [] is not equal to [] ++ [], I can finish the proof by apply Permutation_refl. It seems that apply perform some reduction before matching Permutation_refl with the current goal.
From the Coq manual, Tactics — Coq 8.16.1 documentation, I find no information abo...

view this post on Zulip Discourse Bot (Dec 10 2022 at 20:43):

@brando90 posted in How to install the coq 8.14 package with opam pin when it says it can't find it?

I am on ubuntu. I’m trying to install coq 8.14. I’m sure it must exist. Why doesn’t it let me install it? Commands and error msg:
(iit_synthesis) brando9~/proverbot9001 $ opam switch create coq-8.14 4.07.1

<><> Installing new switch packages <><><><><><><><><><><><><><><><><><><><><><>
Switch invariant: ["ocaml-base-compiler" {= "4.07.1"} | "ocaml-system" {= "4.07.1"}]

<><> Processing action...

view this post on Zulip Discourse Bot (Dec 20 2022 at 13:03):

@neilt (Neil) posted in Problems rewriting with type valued relations

Hello! I’m trying to define relations as "Type"s so that the values are not erased like values of "Prop"s are. I also want to use rewriting rules, eventually including rewriting under binders. I’ve successfully done this using Prop valued relations, but am having trouble with Type valued relations even without trying to rewrite under binders. I found a brief section on the website [1] describi...

view this post on Zulip Discourse Bot (Jan 08 2023 at 16:46):

@icarosadero (Icaro Costa) posted in How do I write a summation on Coq?

I have just started getting acquainted with Coq and I would like to write this sum on it:
\sum_{p=1}^{n} \frac{\mathrm{d}^p}{\mathrm{d}x^p} f(x)
This is what I have tried:
Require Import Coquelicot.Coquelicot.

Require Import Coq.Sets.Finite_sets.

Require Import Coq.Reals.Reals.

Section test.

Local Open Scope R_scope.

Variable f : R -> R.

Definition f_p (m : nat)(x : R) := Derive_n f m x.
...

view this post on Zulip Discourse Bot (Jan 17 2023 at 21:52):

@jeanas (Jean Abou Samra) posted in Stuck on destructing

Hi,
I am working on the following proof that ∀ n, ⟦1, n⟧ is finite (for “finite” defined as "no injection from ℕ to this type”). Please note that there could be more elegant definitions, stdlib use, etc. but my goal is more to increase my understanding of Coq than to do this fast 🙂
I have omitted parts of the proof that are not relevant here, using admit.
While I can see other ways, I went for ...

view this post on Zulip Discourse Bot (Jan 31 2023 at 20:24):

@arjunvish (Arjun Viswanathan) posted in Is there a way to redirect Coqide messages and errors to the same output?

This is cross-posted from StackOverflow, FYI. I have a tactic whose expected behavior is to output an error message, and I want to run it in batch mode on a series of goals and for each goal, I want to record the goal and the error message from the tactic. It seems like I can’t do this with coqc since it will not continue on failure, so I’m doing this on Coqide. The closest I’ve been able to come ...

view this post on Zulip Discourse Bot (Feb 11 2023 at 02:53):

@louih0 posted in Permutation with firstn and skipn

I’ve been struggling with this part of a proof because of the firstn and skipn part.
Permutation (x :: a :: a0 :: l)
(firstn (length (a :: a0 :: l) / 2) (a :: a0 :: l) ++
x :: skipn (length (a :: a0 :: l) / 2) (a :: a0 :: l))

view this post on Zulip Discourse Bot (Feb 22 2023 at 14:27):

@tbrk (Timothy Bourke) posted in Abstract and concrete access to a data structure

We are developing a verified compiler. The frontend abstracts over the low-level values and operations (e.g., unary and binary operations). The backend instantiates these from CompCert’s Clight language.
In the frontend, we would like to guarantee that the concrete definitions cannot be exploited. In the backend, however, we need to reason about them.
So far we considered three different soluti...

view this post on Zulip Discourse Bot (Mar 07 2023 at 18:41):

@drcicero (David Richter) posted in Is it possible to define a cbn-able universe cast with universe checking disabled?

I was hoping to use unset universe checking to disable universes, and temporarily work in Type:Type bliss. However, occasionally my code still fails on a universe constraint even though i have disabled universe checking. I tried to minimize the problem and came up with the idea to define an identity universe cast function. And indeed it does not work; the error message “Universe constraints are no...

view this post on Zulip Discourse Bot (Mar 08 2023 at 15:51):

@gadmm (Guillaume Munch-Maccagnoni) posted in Request for feedback: new convenience tactics/options for deterministic timouts & memory limits in Coq

Hello,
We are looking for feedback regarding a new timeout feature based on allocation limits: PR Experiment: command modifier and tactic for allocation limits by SkySkimmer · Pull Request #17266 · coq/coq · GitHub. Similar to deterministic timouts in Lean, allocation limits use a more portable and more reliable measure of how long the tactic runs: number of allocations done by the computation ra...

view this post on Zulip Discourse Bot (Mar 11 2023 at 04:54):

@doside (Landersing) posted in Compute 121393+121393 causes stack overflow

Hello!
I tried to test this line of code in CoqIDE, but got a confusing error.
Compute 121393+121393.

To avoid stack overflow, large numbers in nat
are interpreted as applications of
Nat.of_num_uint.
[abstract-large-number,numbers]
To avoid stack overflow, large numbers in nat
are interpreted as applications of
Nat.of_num_uint.
[abstract-large-number,numbers]
Stack overflow.
It seems ...

view this post on Zulip Discourse Bot (Mar 14 2023 at 18:57):

@Kalyani posted in Coqtop Cannot Add File to Load Path

Hello, I have Coq 8.16.0 on Windows 10, and am using Coqtop. I’m trying to add files to the load path using -Q, but Coqtop can’t access the files:

coqtop -Q theories/Monad.v theories.Monad
Warning: cannot open theories/Monad.v [cannot-open-path,filesystem]

How should I go about fixing this?
Thanks in advance,
Kalyani

view this post on Zulip Discourse Bot (Mar 19 2023 at 15:16):

@io7m (Mark Raynsford) posted in Unexpectedly accepted eapply hypothesis

Hello!
Coq did something earlier that I didn’t quite understand or expect. This is extracted from a larger development. The following is a straightforward linear interpolation function over reals:
Require Import Coq.Lists.List.
Require Import Coq.Init.Nat.
Require Import Coq.Arith.Peano_dec.
Require Import Coq.Arith.PeanoNat.

Require Import Coq.Reals.Reals.
Require Import Coq.Reals.ROrderedType...

view this post on Zulip Discourse Bot (Mar 26 2023 at 14:38):

@io7m (Mark Raynsford) posted in Possible lra bug

Hello!
It seems that lra can fail if name mangling is enabled:
Require Import Coq.Reals.Reals.
Require Import Psatz.

Open Scope R_scope.

Unset Mangle Names.

Lemma div2mult05_0 : forall r, r / 2 = r * 0.5.
Proof.
intros r.
lra.
Qed.

Set Mangle Names.

Lemma div2mult05_1 : forall r, r / 2 = r * 0.5.
Proof.
intros r.
lra.

The div2mult05_0 lemma is proven without issue. Turn on name man...

view this post on Zulip Discourse Bot (Mar 27 2023 at 16:41):

@nobody posted in Can I access Coq's way of generating readable names from inside tactics?

If I destruct a thing involving a bool (or remember a bool), the resulting bool will most likely be called b, b0, b1, …; a natural number will be n, …; and so on. Can I access the same name generation mechanism from Ltac? fresh defaults to H no matter what, I can only pass in a name or string (or several) to use in place of H. What if I don’t have any?
The concrete context I currently want that i...

view this post on Zulip Discourse Bot (Apr 01 2023 at 06:32):

@zhengpushi posted in How to organize a Coq library?

How to organize a Coq library?

view this post on Zulip Discourse Bot (Apr 07 2023 at 01:35):

@yiyunliu posted in Parameterizing a type system over an abstract data type with Coq's module system

I want to parameterize my type system over an abstract data type. The goal is to show that the system is type sound for all instances of the abstract data type. However, there are some special properties that only hold for specific instances. It’s unclear to me how to use Coq’s module system to structure my development. Here’s a minimal example that illustrates the problem I ran into with modules: ...

view this post on Zulip Discourse Bot (Apr 07 2023 at 15:04):

@io7m (Mark Raynsford) posted in Can FSets have decidable equality?

Hello!
I suspect the answer to this question is “no”, but can FSets have decidable Leibniz equality given elements that have decidable Leibniz equality? A simple example with nat:
Require Import Coq.FSets.FSetInterface.
Require Import Coq.FSets.FSetWeakList.
Require Import Coq.FSets.FSetFacts.
Require Import Coq.Structures.Equalities.
Require Import Coq.Arith.PeanoNat.

(** A mini decidable type...

view this post on Zulip Discourse Bot (Apr 09 2023 at 16:02):

@io7m (Mark Raynsford) posted in Getting List.Exists into an induction principle

Hello!
This is a severely reduced example from a larger development, so apologies if some of it seems a bit silly. I’m running into an issue (once again) with custom induction principles. I’ll try to illustrate. Here’s a subset of a small expression language:
Require Import Coq.Lists.List.

Import ListNotations.

Inductive exp0 :=
| E0_True : exp0
| E0_False : exp0
| E0_And : list exp0 ...

view this post on Zulip Discourse Bot (Apr 14 2023 at 12:55):

@tizuck (Tilman Zuckmantel) posted in Trying to get a parameterized inductive type into induction

I have defined the following inductive datatype:
Inductive action : ioh -> Type :=
| inputEvent: nat -> list types -> string -> nat -> nat -> action Input
| outputEvent: nat -> list (nat + bool) -> string -> nat -> nat -> action Output
| matchEvent: nat -> nat -> action Input -> action Output -> action Internal
| dbAccess : nat -> nat -> dbacc -> nat -> action Internal
| guard : nat -> nat -> boo...

view this post on Zulip Discourse Bot (Apr 19 2023 at 22:49):

@trj2059 posted in CBV with pretty syntax

Hi, I’m looking for a way to show the individual steps in the “simpl” tactic, but without having to use the
delta conversion so I can “trace” the steps using “pretty” syntax. So for example if I have
Lemma sum_closed_expr_basic : forall n : nat, 2 * sum n = n * (n + 1).
Proof.
intros. induction n.

simpl.
reflexivity.
cbv delta [mult].

On the last step. You get the following as the curre...

view this post on Zulip Discourse Bot (May 05 2023 at 16:24):

@jeanas (Jean Abou Samra) posted in Anonymous example

This is just a mundane syntax question. Is there something similar to Example x : foo., except it doesn’t require me to give a name to the example? I’d like to have a number of trivial examples/tests, and find it annoying to write Example ex1, Example ex2, etc.
I am aware of Goal foo, but I was hoping to keep “example” or a similar keyword, just to clarify that the goal is illustrative.

view this post on Zulip Discourse Bot (May 06 2023 at 12:09):

@jp-diegidio (Julio Di Egidio) posted in How to do simple structural coercion

Hello everybody,
Here is a beginner’s question: general speaking, I’d like to define a type that is a “restriction/subtype” of some other inductive type.
I have already been wading through a lot of material as to the several ways this can actually be approached: I am specifically after the simplest possible “structural” solution.
Here is an attempt where I am trying to use a “side condition” (a...

view this post on Zulip Discourse Bot (May 11 2023 at 19:52):

@fms-1988 (FELIPE MORELLI) posted in Help to criate my first proof

Hi
I what to proof this proposition:

But I’m facing difficult to finish the coq code.
someone can help me?
regards
Require Import Reals.
Open Scope R_scope.

(f(xj) is non-linear)
(/\ represent 'and')
Definition additive (f : R -> R) := forall x y : R, f (x + y) = f x + f y.
Definition homogeneous_deg_one (f : R -> R) := forall x a : R, f (a * x) = a * f x.
Definition linear (f : R -> R)...

view this post on Zulip Discourse Bot (Jun 06 2023 at 00:54):

@nobody posted in Extraction: adding file prefix (open …) & suffix (e.g. function call), from Coq or dune?

After asking a question on stackoverflow and then re-reading the documentation a couple more times, I’m pretty sure that it’s currently not possible to

insert stuff at the top of an extracted file (like library imports), or
insert stuff at the end of an extracted file (like a call to the main function),

either on the Coq or the dune side. Duplicating the example I included over there, the code
...

view this post on Zulip Discourse Bot (Jun 06 2023 at 16:26):

@brando90 posted in How to parse coq statements from a coq .v file the official way?

The parser I wrote doesn’t seem to be good enough to go through a coq statement from a coq file. We assumed that a coq statement would always end in a ".\s" with the exception of strings and comments.
However after parsing though some of the simple files it looks like also “- intros.” is really two statements, one for “-” and another for whatever comes after. “*” has a similar problem.

Option ...

view this post on Zulip Discourse Bot (Jun 08 2023 at 03:14):

@Logan posted in Stuck on Software Foundatoins Pigeonhole Principle

Hi everyone. I’m new to formal methods and have started with Software Foundations and I’m finally properly stuck at the pigeonhole principle proof in the Inductive Propositions chapter. IndProp: Inductively Defined Propositions
I’ve tried to find other proofs applying Excluded Middle as the book suggests, but I’ve only been able to find a couple proofs that do not use EM and everything else I can...

view this post on Zulip Discourse Bot (Jun 15 2023 at 09:22):

@faremy posted in Generating depth-indexed variant of an inductive

Hello,
Is there an already existing plugin to automatically derive, from an Inductive type or predicate, a version of it enriched with the depth/size of the tree? For example, if I have
Inductive Has0 A : list A -> Prop :=
| Has0_head : forall L,
Has0 (0 :: L)
| Has0_tail : forall x L,
Has0 L -> Has0 (x :: L).

Then I would like to automatically derive another Inductive looking l...

view this post on Zulip Discourse Bot (Jul 04 2023 at 17:10):

@nadeemabdulhamid posted in Automated reasoning about list permutations

Are there any tactics/tools/libraries for fully automating proofs about Permutations on lists, for example, like this:
Lemma ex : forall A (a:list A) b c d e f,
Permutation (a ++ b) c ->
Permutation (d ++ e) f ->
Permutation (a ++ d ++ e ++ b) (f ++ c).

In working with a few of these, I’ve developed tactics to help guide the proof (e.g. below), but it seems like it might be possible ...

view this post on Zulip Discourse Bot (Jul 25 2023 at 20:43):

@kalyani.tt posted in Name proof from Next Obligation

Is it possible to name the proofs written under a Next Obligation?
E.g something like
Next Obligation as foo_proof
(* ... *)
Qed.

Print foo_proof.

view this post on Zulip Discourse Bot (Aug 01 2023 at 08:41):

@randl (MRandl) posted in How does one import native cyclic integers in coq?

Hi,
I’m looking to work with native OCaml integers in Coq, with the objective of extracting the program and running it natively.
My problem is that I can’t seem to understand what “Require Import” command to use to import these integers. My understanding is that they are stored in stdlib (as suggested by Standard Library | The Coq Proof Assistant) but all of my attempts (Require Import Numbers, ...

view this post on Zulip Discourse Bot (Aug 03 2023 at 18:07):

@jp-diegidio (Julio Di Egidio) posted in Class/type hierarchies

Hello guys,
I am trying to find my way to building hierarchies of “reusable/extensible” classes/types. I have already learned that Modules are too limited for that since every sub-module has to reimplement all members of the super-module (i.e. there is in fact no “inheritance”), and that the suggested way to go is Records or, even better, Typeclasses.
So, here is an attempt with Typeclasses and...

view this post on Zulip Discourse Bot (Aug 07 2023 at 09:25):

@BismaBRJ posted in Naming inconsistency in proofs using BinInt, Zorder, and its deprecation

Hello, I am a beginner to Coq (and this is my first time posting here) and I tried to prove that for two integers each larger than zero, their sum is also larger than zero. I am using jsCoq (0.16.0), which is running Coq 8.16.0 at the time of writing this.
(I am aware of the existence of nat and the “positive” type, especially when dealing with the QArith module, but for now I am interested in th...

view this post on Zulip Discourse Bot (Aug 16 2023 at 10:50):

@zyang posted in Coq official website inaccessible?

Just found out I cannot access any page of coq.inria.fr like some basic library
https://coq.inria.fr/library/Coq.Lists.List.html
for about a week.

view this post on Zulip Discourse Bot (Aug 19 2023 at 17:15):

@flaviodemoura (Flávio Leonardo Cavalcanti de Moura) posted in Rewrite set equality inside a let expression

Hello! Is it possible to make a rewriting inside a let expression that in turn is inside an Inductive definition? More precisely, I am using the Metalib package where [=] represents set equality. I have an hypothesis of the form H: a [=] b, and I want to replace some occurrences of a for b (rewrite H) inside a let expression that, in turn, is inside an Inductive definition. My current proof contex...

view this post on Zulip Discourse Bot (Sep 01 2023 at 09:14):

@doside (Landersing) posted in How to read this in-clause in the match construct?

Hi,I am trying to figure out what the in-clause component of match expression effects.
Consider the following examples.
Inductive list :nat->Set :=
| nil :list 0
| cat: forall (n:nat),nat->list n->list (S n).
Notation "{| x , .. , y |}" :=
(cat _ x ..(cat _ y nil)..).

Check {| 1,2,3,4 |}.

Definition Head {n} (v :list (S n)) :=
match v in list (S n) return nat with
| nil => nil
| cat _ h ...

view this post on Zulip Discourse Bot (Sep 03 2023 at 07:07):

@zhengpushi posted in Failing when use "destruct" tactic to "or" hypothesis if the conclusion is sumbool

Please check the code in ex1, why “destruct H” fail? what’s the meaning of this error message?
(* the hypothesis is "or" and the conclusion is "sumbool" *)
Example ex1 : forall m : nat, (m = 1 \/ m = 2) -> {m = 1} + {m = 2}.
Proof.
intros.
Fail destruct H.
(* Case analysis on sort Set is not allowed for inductive definition or. *)
(* why failed here? *)
Abort.

(* the hypothesis is "or" and...

view this post on Zulip Discourse Bot (Sep 04 2023 at 05:48):

@liuxingpeng520521 posted in Controlling Extraction of Specific Types

Why would Coq want to extract the specific Inductive definition to a specific OCaml type before extraction, isn’t that redundant?

view this post on Zulip Discourse Bot (Sep 04 2023 at 13:57):

@jp-diegidio (Julio Di Egidio) posted in Coq's equality is not Leibniz (?)

Hello guys,
I just don’t understand why the docs (*) say that the built-in equality is Leibniz, when it seems evident to me that it’s plain definitional equality, i.e. x = y iff x and y are “convertible”, whence eq_refl applies:
Inductive eq (A : Type) (x : A) : A -> Prop :=
eq_refl : eq x x.

For comparison, here is how I’d write Leibniz equality:
Definition leibniz_eq (U : Type) (x y : U) :...

view this post on Zulip Discourse Bot (Sep 08 2023 at 11:33):

@liuxingpeng520521 posted in Coqtop is not running

I’m having a problem with my vscoq plugin, it keeps showing ‘coqtop is not running’. it was fine in the morning but when I used it again in the afternoon I got this error.

view this post on Zulip Discourse Bot (Sep 13 2023 at 14:03):

@kalyani.tt posted in Trouble installing coq-core on Windows

I am trying to install coq-lsp on Windows, and because of that I need to install coq-core. I have successfully installed opam using Cygwin, but now I am trying to install coq-core and am getting this error message:
[image]
I have successfully installed zarith though, and can find dllzarith.so. Do I need to copy it to a certain directory? What should I do to fix this? Let me know of any more det...

view this post on Zulip Discourse Bot (Sep 19 2023 at 12:30):

@zhengpushi posted in An inductive definition failed with error "Non strictly positive occurrence..."

Problem: this definition cannot be accepted by Coq.
(* kind means different data types: value or array *)
Inductive kind :=
| kval
| karray (n:nat) (k:kind).

(* exp is expression with "kind" type, including: constant, negative, mapping *)
Fail Inductive exp : kind -> Type :=
| e_cnst (n:nat) : exp kval
| e_neg (t:exp kval) : exp kval
(* An idea: mapping element of an array to result. But I faile...

view this post on Zulip Discourse Bot (Sep 25 2023 at 11:59):

@liuxingpeng520521 posted in CertiuCOS2

Has anyone studied CertiuCOS2 for this project? The code looks abstract without comments, and I’m looking for someone to share it with.

view this post on Zulip Discourse Bot (Oct 03 2023 at 11:05):

@alx (Aleksy) posted in Ocaml native int63 extraction

Hello everybody,
I have a file Sample.v with the content
Require Import String.
Require Import Int63.Sint63.
Require Import PArray.
Require Import Ascii String Coq.Strings.Byte.
Module Sample.
Definition bytes : Set := string.
Definition len_bytes (s:bytes) := 1+ length s.
End Sample.
and a file with the content

Require Export Sample.
Require Extraction.
Require ExtrOcamlBasic.
Requir...


Last updated: Oct 04 2023 at 22:01 UTC