Discourse Bot (Jun 18 2020 at 16:52): Discourse Bot (Jun 18 2020 at 16:52):Yannick Zakowski @Yannick posted in Would Coq benefit from docstrings?
Hello everyone,
A bit of a light question, almost a poll.
I have been wondering for a bit as to whether Coq would benefit from docstrings, that would get returned by About, both for lemmas and definitions. In many cases the type and name already provide the necessary documentation, but there are definitely cases where a more lengthy explanation can be precious, both to parse the meaning of the s...
Théo Zimmermann (Jun 18 2020 at 16:52):(The above is not really "new" but a test that the Discourse integration correctly works.)
Discourse Bot (Jul 06 2020 at 06:16):@jco posted in How to make verified software more accessible
Sorry if this is a naive question. I’m new to the world of proof assistants, and my goal for the year essentially is to become a proficient user, able to write verified software in some domain.
I’m a deep believer in two things: 1. the state of software is abysmal (look at the 747 max, for example) and 2. we need tools like proof assistants and formal verification to help solve 1. That said, this...
Discourse Bot (Jul 19 2020 at 17:38):@brando90 posted in What is # steps a function of?
I want to understand clearly affects how many steps it might take to completely proof a single goal. i.e. I want to understand the interface to the current function:
steps(goal,...) = # steps to prove goalintuitively it must depend on the current tactic applied to goal and the knowledge we have (e.g. environment & context).
Does this mean that the function has the following signature?
steps(g...
Discourse Bot (Jul 20 2020 at 14:56):@brando90 posted in What do we need to be able to compute reverse tactics application?
I was curious to know what (minimum) knowledge/information was necessary to reverse the application of a tactic.
Let’s say I only have a goal and the tactic application (perhaps atomic tactic) that lead that goal. What information do we need to be able to compute goals that could have lead to that result?
My guess is that we need all the imports (what I cal environment, not sure if that is the r...
Discourse Bot (Jul 21 2020 at 18:49):@brando90 posted in What does it mean that Isabelle has better automation than Coq?
I’ve read before (and heard before) that Isabelle has better automation than Coq. But I don’t really know what that means. Can someone clarify this to me?
My guesses for what this might means:Isabelle’s sledgehammer is more powerful than coq’s coqhammer (which is intuitively weird to me since Coq could just use the same ATPs as Isabelle so I don’t see why this should be the case)
Isabelle’s ta...
Discourse Bot (Aug 03 2020 at 14:39):Rene Sandoval @Pinocchio posted in Can every theorem that has a proof be completed without DSL tactics?
Assume that the statement we want to proof has a proof.
Can we find it with only the “standard” Coq tactics?
i.e. is programming a custom tactic ever necessary? (not sufficient is not what I care, if it has a proof this in theory could be a silly tactic that encodes the proof of the statement which is not interested)
Motivation: I recently learned that one can implement their own tactics…!
Discourse Bot (Aug 03 2020 at 15:05):Rene Sandoval @Pinocchio posted in Can one translate from one ITP language to another automatically?
Is it possible to translate from one language to another (e.g. from Coq to Isabelle or Coq to Lean or Coq to HOL Light etc.) using an intermediate language (e.g. TPTP or whatever Hammers use)?
What I had in mind was that since most ITPs have some sort of ability to talk to ATPs/Hammers it should be possible to translate between languages automatically (e.g. TPTP or whatever Hammers use).
Motivat...
Discourse Bot (Aug 06 2020 at 15:13):@brando90 posted in How does one generate a static proof trees of a whole Coq Proof?
I wanted generate a (AST) of proof tree and potentially save it (as a text file or json or something easy to manipulate, ideally cross plataform/language, ocaml, python…).
How does one do this? I read from the discussion on the Coq grammar that one can use SerAPI or Coq to split the script into sentences. Is that the main thing I need to do to generate a savable proof tree of Coq?
Discourse Bot (Aug 10 2020 at 22:21):Vadim Zaliva @vzaliva posted in Coq trusted kernel code size
Hi! I am writing down an explanation about Coq’s trust model and need some info about the trusted codebase. In particular:
What is the size of the trusted code base?
What steps been taken to assure it is bug-free? Manual code reviews? Paper proofs? etc.
How many bugs were found in it?I recall there was a slide about this at Coq’s workshop but I could not find it. I will appreciate any pointers...
Discourse Bot (Aug 14 2020 at 12:56):OnorioCatenacci @Onorio posted in Proof By Induction On Lists
I apologize–this is pretty vague and general but I am a curious sort and so I feel compelled to ask this.
From what little I know of category theory, it seems as if there should be some sort of category between the idea of Proof By Induction on Natural Number and Induction on Lists. I mean Prove T for 0 seems analogous to Prove T for empty list.
Is there anything to my naive intuition on this p...
Discourse Bot (Aug 30 2020 at 14:10):Karl Palmskog @palmskog posted in Listing and preserving formalized mathematical results in Coq
A lot of mathematics has been formalized in Coq, but unless it ends up in a bigger library such as Stdlib or Mathematical Components, it generally becomes incompatible with the latest stable version of Coq quickly. This hinders incremental progress in formalizing a coherent body of useful mathematics, and may lead to wasted re-formalization effort and obscurity for pioneering researchers.
To addr...
Discourse Bot (Aug 31 2020 at 20:36):Rene Sandoval @Pinocchio posted in How is Coq (or any Proof Assistants) used to for hardware verification?
How is Coq used in hardware verification?
Some of my (very incomplete) thoughts:
hardware is mostly expressing boolean circuits. But that is decidable. Then why even bother with Coq in that case?
Discourse Bot (Aug 31 2020 at 20:38):Rene Sandoval @Pinocchio posted in Why are proof assistants used mostly to catch bugs instead of using it to truly proving correctness?
I remember hearing in class once that formal methods are mostly used to catch bugs. But tools like Coq seem capable to do more than that. So how is it that they are used to catch bugs if they are mostly used for proofs (i.e. showing statements provably work)?
Discourse Bot (Nov 21 2020 at 16:33):ofey @ofeynqed posted in Starting to learn coq
Hi, I’m trying to proof the following th.
forall A B, ((((A -> B) -> A) -> A) -> B) -> B.
As reference I’m looking at this:
Theorem forward_small : (forall A B : Prop, A -> (A->B) -> B).
Proof.
intros A.
intros B.
intros proof_of_A.
intros A_implies_B.
pose (proof_of_B := A_implies_B proof_of_A).
exact proof_of_B.
Qed.
The main problem I think that is about the statement that I want ...
Discourse Bot (Nov 30 2020 at 13:31):Pierre Marie Pédrot @ppedrot posted in Change of default locality for Hint commands in Coq 8.13
This small note describes a plan to change the default semantics of Hint commands w.r.t. scoping.
Summary of the situation
As for most commands, when declaring hints one can choose a locality that will change their scoping behaviour. As of 8.13, we have three possible explicit locality qualifiers for hint commands, namely:“local”
“export” (introduced in 8.12 for basic hint commands, and in 8.1...
Discourse Bot (Dec 24 2020 at 20:00):Hugo Carvalho de Paula @HCP posted in "Mainstream" programming systems with a Coq-like development style?
I rather enjoy the programming style one has to program in when developing in Coq. It’s a fascinating idea: write a specification, then refine it until finished. I read on “test-driven development” and i’m like, but the system can help you so much more if you have full specs and not just tests!
Are there any similar systems for more popular languages? That is, would it be possible to use a specif...
Discourse Bot (Jan 16 2021 at 04:18):Lim Jin Xing @jinxing1990 posted in Cite Coq Library Materials
Hi,
May I know how do I cite materials from Coq Library? For example, I would like to cite the materials from Standard Library | The Coq Proof Assistant, how can I do that? Is there any way to generate the bibtex format?
Any help will be appreciated! Thank you!
Discourse Bot (Mar 31 2021 at 08:32):@larsr posted in Nix package for coq theories with dependencies
I am new to the nix package manager, so perhaps this question is trivial.
I want to add coq-itree to coqPackages in nixpkgs but building fails because it can’t find the Paco and ExtLib libraries.
I have already fixed the nix files for those two by updating their nix files in a local copy of the nixpkgs, so this works:
env NIX_PATH=$HOME/HACK nix-shell --packages coqPackages_8_13.{coq,coq-ext-li...
Discourse Bot (Apr 30 2021 at 09:06):Lim Jin Xing @jinxing1990 posted in Formalized Divide-and-conquer for Lists
Dear all,
I have written some codes on formalizing different variations of divide-and-conquer algorithm design paradigm for lists. As a case study, we will see how these different variations lead to different sorting algorithms. The github page for the codes are as follows:I am still in the midst of providing desciption for each of the files. It would be great if any of you all could provide ...
Discourse Bot (May 14 2021 at 07:32):Gabriel Scherer @gasche posted in Visualizing contributions to the Coq implementation and all Coq opam packages
Hi there,
I recently learned of fornalder, a tool that creates nice visualizations of contributions to open-source projects by analyzing commits to their git repositories (the author used it to analyze GNOME contributions). I decided to use it to study contributions to the Coq implementation and packages in the Coq opam archive, results below.The Coq proof assistant
[Coq contributor cohorts]
...
Discourse Bot (Jun 02 2021 at 20:39):Molly Stewart-Gallus @molossus_spondee posted in How do regular and exact completions fit into Coq's use of setoids?
I’ve been working with a little bit of constructive category theory but because higher inductive types are far from ready I need to work with setoids. In my case I need to use a constructive approach because I hope to work on some type theory/compiler stuff.
I read up on the categorical side of things and I think setoids kind of correspond to a free completion.
https://ncatlab.org/nlab/show/regu...
Discourse Bot (Jun 15 2021 at 18:44):Jason Hu @HuStmpHrrr posted in Coqclub archive is off?
Hi, it seems coqchub mailing lis has turned off its archive? As a result, all history is unaccessible. May I ask why and will the archive be open again?
Discourse Bot (Jun 18 2021 at 20:19):@CrisTeller23 posted in Coq to Why3: with notation
Hi! I know this probably isn’t the right place to ask this, but I can’t get an answer at stackOverflow and Why3 doesn’t really have a community or an easy way to ask questions…
So I have this definition in Coq:
Fixpoint executeBool (state:M.t Z) (stack:list Z) (program:list insStBool) : list Z :=
match program with
[...]
| (SBSkip O)::l => executeBool state stack l
| (SBSkip (S n))::l =>...
Discourse Bot (Jun 18 2021 at 22:29):@CrisTeller23 posted in Coq to Why3: Proof of function correction
Hi! I know this probably isn’t the right place to ask this, but I can’t get an answer at stackOverflow and Why3 doesn’t really have a community or an easy way to ask questions…
So I have this proof in Coq:
Lemma compileCorr : forall (state:M.t Z) (ins:aexp),
execute state nil (compile ins) = (aeval ins state)::nil.
Proof.
intros state ins.
induction ins.- auto.
- auto.
- simpl. appl...
Discourse Bot (Jun 20 2021 at 14:16):@CrisTeller23 posted in Coq to Why3: Proof lemma of function correction
Hi! I know this probably isn’t the right place to ask this, but I can’t get an answer at stackOverflow and Why3 doesn’t really have a community or an easy way to ask questions…
So I have this proof in Coq:
Lemma executeCompile : forall (state:M.t Z) (ins:aexp) (p:list insSt) (stack:list Z),
execute state stack (compile ins ++ p) = execute state ((aeval ins state)::stack) p.
Proof.
intros sta...
Discourse Bot (Jul 04 2021 at 15:52):Gert Smolka @gert-smolka posted in Finite types, historical question
I have a historical question: When did indexed finite types
Inductive fin : nat -> Type :=
| Zero: forall n, fin (S n)
| Succ: forall n, fin n -> fin (S n).appear first in Coq or elsewhere?
I checked Martin-Löf, but there finite types are obtained with n constructors, not just 2. The above definition appears in Chlipala’s CPDT. I did not find it in Coq’Art.
Related: When did the recursive v...
Discourse Bot (Aug 09 2021 at 01:36):Molly Stewart-Gallus @molossus_spondee posted in Confused about hierarchies of functions
Hi
I’m starting to think for my purposes Coq functions are too powerful.
So I want some smaller but still powerful set of functions.
But I’m unsure of how to work with these nicely or hierarchies here.
I’m thinking I could start with functions on finite types somewhat like the pseudocode below and then expand it as needed with products and such.
Class Finite A := {
N: nat ;
to: A -> Fin.t...
Discourse Bot (Aug 27 2021 at 11:37):Liuyinling @lyl posted in Ask For Basic Commands For COQ
I have successfully installed Coq with opam. From the terminal, after typing eval $(opam env) and coqtop, I am able to launch Coq and write Coq code. However, I don’t know how to save the code. I still would like to know how to open the specific .v. So, is there any tutorial illustrating these basic commands for coq from the terminal? Thank you very much!
Julien Puydt (Aug 27 2021 at 12:28):Discourse Bot said:
Liuyinling @lyl posted in Ask For Basic Commands For COQ
I have successfully installed Coq with opam. From the terminal, after typing eval $(opam env) and coqtop, I am able to launch Coq and write Coq code. However, I don’t know how to save the code. I still would like to know how to open the specific .v. So, is there any tutorial illustrating these basic commands for coq from the terminal? Thank you very much!
Hmmm... typing the code directly doesn't save it ; you should perhaps give CoqIde or Proof General a try : there you can edit a .v file and feed it to coq.
Théo Zimmermann (Aug 27 2021 at 16:33):@Julien Puydt This is just a cross posting of a discourse post. If you want to answer, you need to click it to go to discourse.
Discourse Bot (Aug 27 2021 at 16:55):@Atias posted in Learning Real Analysis and Measure Theory together with Coq
Hi, I am a Software Engineer (mainly C++, Rust) currently started getting really interested in Formal Program Verification and interesting programming languages (like: Idris, Agda, ATS, HOL, Curry, Mercury and of course Coq etc…) and also proving Real Analysis theorems that I learned a while ago while I was studying at university a few years back but now by using a computer.
I myself really think...
Pierre Roux (Aug 30 2021 at 12:16):@Reynald Affeldt you might be interested in the above discourse topic
Discourse Bot (Dec 20 2021 at 17:17):@brando90 posted in What is the runtime of Coq's (dependent) Type Inference?
I remember learning in a class that type inference is decidable but usually takes a long time (e.g. type inference in OCaml is EXPTIME).
I was wondering, since Coq allows programs/values themselves to be in the Type somehow my guess would be that type inference is either:Doubly EXPTIME
UndecidableDoes someone know the answer to this? A reference and an intuition would be highly appreciated t...
Discourse Bot (Feb 10 2022 at 10:19):@JonathanBell posted in Is there any (general) formalization of abstract interpretation?
I am specifically looking for something as general as possible, i.e. not just a specific example of abstract interpretation, but a general proof of the concept based on lattice assumptions.
Does anyone have any pointers for me?
Discourse Bot (Feb 19 2022 at 17:45):Molly Stewart-Gallus @molossus_spondee posted in Can you avoid positivity issues with indexing?
Hi
I was curious if you could do some HOAS nonsense like
Unset Positivity Checking.Inductive term: nat :=
| lift {n}: term n -> term (S n)| tt {n}: term n
| fanout {n} (_ _: term n): term n
| fst {n}: term n -> term n
| snd {n}: term n -> term n| lam {n} (term n -> term (S n)): term (S n)
| app {n} (_ _: term n): term n.Set Positivity Checking.
I don’t really get Curry’s paradox though. ...
Discourse Bot (Apr 06 2022 at 13:08):@brando90 posted in Why doesn't Coq assume UIP or Univalence for equality?
I was learning here Class 17: Congruence & Rewriting and here https://arxiv.org/pdf/1701.04391.pdf that due to the dependence type theory (or ITT, not 100% the difference I assume they are the same) – that equality is not easy to define. The paper discusses a bit why but the paper makes me feel that lean assumes the axiom UIP (Uniqueness of Identity Proofs) anyway.
Why does Coq assume UIP or Univ...
Discourse Bot (Apr 08 2022 at 15:46):@brando90 posted in Does Coq have e-graphs (for Dependent Types)?
I was interested in getting e-graphs for Coq terms. Does this exist? I know this exists:
The congruence closure tactic’s source code appears to mention that it does “e-matching”: coq/ccalgo.ml at 63837173f8901ba0f4f078c577aa499c5a257d01 · coq/coq · GitHub
but I remember reading that congruence closure tactic in coq was limited (only FOL? Can’t remember what it was).
Is this true? What is miss...
Discourse Bot (Aug 19 2022 at 19:54):@imaxw (Ian Maxwell) posted in Indefinite description axiom could be simpler?
Putting this in “Miscellaneous” for now because while it feels a bit like a proposal, it is really not important enough to make one formally; I’m just curious about the design consderations of the standard library.
The axiom constructive_indefinite_description, as postulated in Coq.Logic.IndefiniteDescription, has the following type:
Definition indefinite_description :=
forall (A : Type) (P : ...
Discourse Bot (Aug 25 2022 at 06:42):@interworld posted in VST tactic start_function fails
I’m trying to verify following code using VST:
struct region {
size_t offset;
size_t size;
};static inline size_t region_offset(const struct region *r)
{
return r->offset;
}Here is my funspec for region_offset function
Definition t_struct_region := Tstruct _region noattr.
Definition tregion := tptr t_struct_region.
Definition region_offset_spec : ident*funspec :=
DECLARE _region_offset ...
Discourse Bot (Jan 09 2023 at 23:13):@Rani_Deol posted in Need coq tutor
Hello there
I have a unique request. My son is taking fourth year computer science course at university in Vancouver British Columbia canada. Professor has chosen coq language to study for the class. My son finds it difficult. I was wondering where are you located? And if someone with fluent knowledge of the coq language could tutor my son for the next three and half months please. We need tutori...
Discourse Bot (Feb 15 2023 at 20:49):@brando90 posted in What is the tag for menhir for coq 8.12 when instlaling it with opam install -y?
I want to install opam menhir but make the install explicit for coq 8.12 to make my script explicit + robust to installation.
But when I ask it to show me it show the dev tag, which I assume might change at any point and make the install brittle. The project is hosted in gitlab and it doesn’t seem it lets me make a git issue here so asking here. From the available options is dev actually robust/s...
Discourse Bot (Apr 11 2023 at 19:29):@zman313 posted in Finding Coq Freelancers
Hello,
I wanted to ask are there any freelancers here or if anyone can advise as I am in need of assitance.
Discourse Bot (Jun 23 2023 at 11:54):@hmltn2 (hmltn-2) posted in Developing a proven, secure communication protocol from scratch
Here is the content of my recent stack overflow post discussing what I intend to begin working on, immediately:
Formally verified email or communication?
This question is contextualized by having an account hacked which is prompting me to move towards something I’ve long wanted to anyway.
I would like to consider the simplest possible formally verified communication protocol.
Is there a common...
Discourse Bot (Aug 25 2023 at 14:06):@toku-sa-n (Hiroki Tokunaga) posted in Is it possible to get parentheses' positions or an operator's associativity from an AST?
Hi. While I was writing a Coq formatter, I encountered a problem of not being able to get information of parentheses.
Consider the following Theorem (from Induction: Proof by Induction in Software Foundation).
Theorem add_assoc : ∀ n m p : nat,
n + (m + p) = (n + m) + p.The parentheses in (n + m) + p are actually unnecessary as + has left-associativity, but the ones in n + (m + p) are necess...
Discourse Bot (Oct 18 2023 at 16:25):@caverill (Charles Averill) posted in How do each of the three main lambda calculus features impact what coq can represent?
We know that the CoC is essentially a calculus combining dependent typing, parametric polymorphism, and type constructors. What exactly do each of these three give us in terms of representation power when we’re writing theorems/proofs?
Parametric polymorphism obviously gives us the forall operator, which is essential for the majority of proofs, but what exactly do dependent types and type constru...
Last updated: Dec 01 2023 at 06:01 UTC