Stream: Coq users

Topic: New Discourse topics

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

Théo Zimmermann (Jun 18 2020 at 16:44):

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

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

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.

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

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 [])...

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

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

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?

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.

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

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

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?

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

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, ...

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

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”?

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

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

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.

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

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

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

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

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

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

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

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

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

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

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 <: (...

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

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

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?

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

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

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

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?

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

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

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

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

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

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

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

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

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

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?

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

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

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.

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

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

Bruno Carneiro (Oct 25 2020 at 12:23):

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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),
(...

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

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?

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?

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

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

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

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

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.

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

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

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

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

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.

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

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

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

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

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

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?

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

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!

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 !

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

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

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

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?

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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

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

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

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

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

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.

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

• Set Nested Proofs Allow...

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

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

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

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 ]" :...

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

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

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

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?

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

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

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

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

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

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

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

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

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

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

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

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.

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

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

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

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

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

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

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, ...

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.

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

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

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

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!

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

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

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

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

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

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

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

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?

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.

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

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

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

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

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

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

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

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

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
| [] ...

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

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

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

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

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

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

Gaëtan Gilbert (Jul 05 2022 at 19:32):

anyone else getting "page not found"?

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

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

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

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

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

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”

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

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

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

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

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

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

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

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

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

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)

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

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

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

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

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

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

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

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

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!

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Discourse Bot (Apr 01 2023 at 06:32):

@zhengpushi posted in How to organize a Coq library?

How to organize a Coq library?

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

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

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

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

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

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.

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

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

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

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

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

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

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

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.

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, ...

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

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

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.

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

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

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

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?

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

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.

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

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

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.

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

Discourse Bot (Oct 09 2023 at 14:00):

@elefthei (Lef Ioannidis) posted in Register a custom induction scheme for use with the 'induction' tactic

I have an inductive predicate F with induction scheme F_ind that is not very useful. I defined a custom induction scheme F_ind' and I would like to replace the autogenerated scheme for my own.
Am I remembering wrong there is a way to either,

Delete F_ind and rename F_ind' → F_ind and the induction tactic will use it.
Use a vernacular command (perhaps Scheme?) to register F_ind' as the default ...

Discourse Bot (Oct 18 2023 at 23:31):

@sudgy posted in Using Bundled and Unbundled Typeclasses Simultaneously

I’ve seen a big topic regarding typeclasses being whether or not they should be bundled or unbundled. Over time I’ve found that you can actually pull off doing them both at the same time and getting the best of both worlds! I mad a gist showing it off here: Using Bundled and Unbundled Typeclasses Simultaneously in Coq · GitHub

Discourse Bot (Oct 19 2023 at 05:16):

@tomlogo posted in About 'syntax error: lexer: undefined token' at the beginning

When I tried to copy some code from the book, I faced some messages like “syntax error: lexer: undefined token”.
I realized the problem which is the ⇒ is not the same as => in code.

Discourse Bot (Nov 02 2023 at 16:53):

@randl (MRandl) posted in Implicit argument resolution

Hi all,
I am perplexed by this piece of Coq code, which defines the bijectivity of a function:
Definition injective {A B} (f : A -> B) := forall x y : A, f x = f y -> x = y.
Definition surjective {A B} (f : A -> B) := forall y : B, exists x, f x = y.
Definition bijective {A B} (f : A -> B) := injective f /\ surjective f.

Definition idf {A} (x : A) := x.

Lemma id_bij {A : Type} : bijective idf....

Discourse Bot (Nov 03 2023 at 09:41):

@ElectreAAS (Ambre Austen Suhamy) posted in Recursive definitions best practices

Hi all. I am returning to Coq after a long pause, and I am wondering what are the best practices when it comes to defining recursive functions.
In my situation, I am trying to write a function that checks if a needle string is a substring of a haystack.
I can think of at least 7 different ways of expressing that, using either Inductive or Fixpoint, Prop or bool and whatnot.
Ultimately I want to...

Discourse Bot (Nov 08 2023 at 08:25):

@liuxingpeng520521 posted in The Lemma body_push in Verif_stack of VC

I am now working on proving the Lemma body_push in Verif_stack of VC:
Lemma body_push: semax_body Vprog Gprog f_push push_spec.https://softwarefoundations.cis.upenn.edu/vc-current/Verif_stack.html
But I’m stuck.
Here are my current proofs:
Lemma body_push: semax_body Vprog Gprog f_push push_spec.

Proof.

start_function.

forward_call (Tstruct _cons noattr, gv).

unfold stack. Intros vret q.

...

Discourse Bot (Nov 22 2023 at 13:12):

@tolearn posted in [Very basic] stack overflow and computability

I’m new to Coq. I have two questions for the following code.
Fixpoint plus (n : nat) (m : nat) : nat :=
match n with
| O => m
| S n' => S (plus n' m)
end.

Notation "x + y" := (plus x y)
(at level 50, left associativity)
: nat_scope.

Check 10000 + 10000 = 20000. ( stack overflow occurs )

This is the simple implementation of addition and ...

Discourse Bot (Nov 23 2023 at 15:10):

@Kalernor posted in Modularizing Coq scripts with defining Parameters/proving Axioms

I have this coq file, for example aFile.v, that has a bunch of definitions and parameters and axioms and lemmas, some depending on each other. So for example, let’s say aFile.v looks something like this:
Definition def1 := .. Parameter param1 :=.. Definition def2 :=.. (* uses parameters & definitions from above ) Axiom ax1 :.. ( uses parameters & definitions from above ) Lemma lem1: ( uses pa...

Discourse Bot (Nov 29 2023 at 08:49):

@anolmar posted in Windows installation from sources failure due to symbolic link

I’m trying to install Coq on Cygwin, so that I can later compile e.g. CompCert.
First, I tried just installing an opam switch on Cygwin, and then installing the coq package, but I got errors due to it not finding dllzarith.so, as the person in this topic.
So, following the advice, I tried following the installation instructions for Windows with source compilation.
I downloaded the 2023.03.0.zip...

Discourse Bot (Dec 10 2023 at 20:38):

@chluebi posted in Using coqnative compiled files in other files

I was planning on running some tests on native_compute and as such I was trying to get native compilation to work.

How do I use theorems generated .cmx (or is it .cmxs) files generated by coqnative in my normal proofchecking needs, i.e. use the theorems in a normal .v proof in coqide
How do I compile to .cmx without needing to have the file proofchecked with native_compute disabled?

Details:
Gi...

Discourse Bot (Dec 14 2023 at 22:54):

@zepalmer (Zachary Palmer) posted in Newbie Question: Match Case Analysis and Propagation

Hello! I’m new to Coq and to writing machine-verified proofs in general – I just started at this yesterday – and have occasionally been stymied because I know what I want to do but have no idea about the basic syntax to express it. I’m currently working on an exercise to prove a relationship between two functions and need to gather some information out of a hypothesis I have. At present, my hyp...

Discourse Bot (Dec 19 2023 at 21:17):

@zepalmer (Zachary Palmer) posted in Generally Mapping Inequality through Unary Constructors

I’m very much new to automated theorem proving, so please feel free to point out anything especially gross that I’m doing. :smile: I’m in a situation where I’m writing a bunch of tiny helper lemmas that prove that inequality maps through constructors. For instance, I have a constructor VInt that wraps around an integer and I write the following:
Lemma integer_not_equal_implies_vint_not_equal :
for...

Discourse Bot (Dec 21 2023 at 21:31):

@zepalmer (Zachary Palmer) posted in Trying a Tactic with All Visible Goals

As a beginner, I sometimes find myself in a situation like this:
Lemma expression_is_value_or_not :
forall e:expression,
(exists v:value, e = EValue v) \/ (forall v:value, e <> EValue v).
Proof.
intros.
destruct e eqn:He.

- apply or_introl. exists v. reflexivity.
- apply or_intror. intros. discriminate.
- apply or_intror. intros. discriminate.
- apply or_intror. intros. discrimina...

Discourse Bot (Dec 21 2023 at 22:19):

@VvSsNPk posted in Software foundations theorem

i am trying to learn coq on my own so that i can better understand the logic part of ai lectures in my university . i am trying to do all the exercises on my own to better understand coq. but i think some part of the exercises are to much time consuming so i need help to solve them . i dont want to check the complete solutions just need some kind of hint to solve them quickly.
example :-
Theorem...

Discourse Bot (Dec 22 2023 at 16:55):

@randl (MRandl) posted in Define inductive branch with constraint on branch parameters

Hello,
I am trying to define first-order logic terms with an inductive set.
Such terms include function applications which typically have the constraint that their arity must match the size of the argument list provided during the call of the function. I.e, I am trying to write this :
Inductive Term :=
| Var (name : string)
| FunApp (f: Function) (terms : list Term) (correct_size : arit...

Discourse Bot (Dec 24 2023 at 06:07):

@hhiim posted in Do multiple theorems allow the same name?

We need to make a name correspond to many different (but similar) theorems.
For example, unordered sets {a, b}, Obviously a∈{a, b} and b∈{a, b}
Similar trivial theorems should have the same name.
Otherwise the context will be full of garbage lemmas …

Discourse Bot (Jan 02 2024 at 09:03):

@florath (Andreas Florath) posted in How to get rid of warnings like "Warning: Cannot open directory /usr/games/."?

Hello!
Every time I run coqc (using dune), I get a bunch of warnings about directories which cannot be opened., like (excerpt from the log):
(cd _build/default && /snap/bin/coqc -q -w -deprecated-native-compiler-option -w -native-compiler-disabled -native-compiler ...
Warning: Cannot open directory /usr/games/. [cannot-open-dir,filesystem]
Warning: Cannot open directory /sbin/. [cannot-open-dir,...

Discourse Bot (Jan 08 2024 at 23:23):

@zepalmer (Zachary Palmer) posted in Defining Mutual Induction Principles Manually

Hello!
Summary: I’m defining my own induction principle for inductively defined types which use the standard library list in their definitions. I’ve encountered a problem: it seems that I need to define a new induction principle for each of the types in the mutually defined set even though their contents are essentially identical. Is there a better way to define mutual induction principles manu...

Discourse Bot (Jan 12 2024 at 18:02):

@wdcraft posted in Various installation attempts on MacbookPro M3 Max stall or hang

Recently migrated from older MacBook Pro intel-based processor to MacBook Pro M3 Max and have tried everything I can think of to get Coq (8.17.1) installed, following the instructions and trying both the platform installation script and the more independent manual opam approach. I hope to continue use VSCode and its vscoq for working with coq. The good news is that the result is quite consistent; ...

Discourse Bot (Jan 16 2024 at 23:03):

@zepalmer (Zachary Palmer) posted in Match Case Analysis and Propagation (redux)

Hi, all! This question is similar to one I posted last month during my first week of learning Coq, but I think I can ask it properly this time. I’ll have a brief description of my general question first and then a concrete MWE after.
The Question
I frequently want to destructure match expressions based upon what I know them to be equal to. For instance, consider the following hypothesis:
H : ...

Discourse Bot (Jan 20 2024 at 18:19):

@dodos posted in Coq platform script downloads are triggering my antivirus

I’m trying to download the zip file from https://github.com/coq/platform/blob/2021.02.1/README_Windows.mdvv so that I can use it with unimath but my antivirus is blocking the file download. Should I just disable it and keep going? Is there another way of me using unimath on windows? Is there another library that has category theory constructs that would be easier to download?
TIA

Discourse Bot (Jan 22 2024 at 10:35):

@zyang posted in Coq/Ocaml project using heuristic function written in C?

Hi,
I’m writing to seek some knowledge/suggestions about the building system of Coq/OCaml:
I’m implementing a compiler pass for CompCert. This pass uses a heuristic to optimize a program (which does not influence the correctness proof).
We have an existing implementation of this heuristic in C, but not in Coq. The specification of this heuristic is as simple a function from a list of numbers (p...

Discourse Bot (Feb 01 2024 at 06:09):

@caverill (Charles Averill) posted in Dependent-typed terms as return values / function parameters

I’m getting some hard-to-decipher errors regarding type checking on some Coq code that I’m generating. Specifically, I have a dependently-typed function that reads a list from a store and returns it - if the list does not exist in the store, it returns an empty unit list.
This function was easy enough to write in a proof environment, but I’m now running into issues in my auto-generated code. Spec...

Discourse Bot (Feb 06 2024 at 04:09):

@caverill (Charles Averill) posted in Simplifying/rewriting inside of an anonymous fixpoint

I’m working on a lifter from a low-level imperative language to Coq and have been using anonymous fixpoints with loop limits to represent standard loops. The loops pass around a store to maintain state. This works out fairly well for computation, but it’s fairly difficult to deal with in a proof. Here’s an example, where the fixpoint code is significantly simpler than what I’m actually dealing wit...

Discourse Bot (Feb 07 2024 at 15:34):

@gasche (Gabriel Scherer) posted in Coq examples of cut elimination in sequent calculi?

I am trying to prove a cut-elimination result for a sequent calculus in Coq. I have a derivation of A \vdash B and a derivation of B \vdash C, and I build a derivation of A \vdash C. (My actual sequent calculus is more complex than that, but this is the idea.)
Do you have examples of such cut-elimination proofs already done in this style? I found that doing it in Coq is harder than I thought (det...

Discourse Bot (Feb 09 2024 at 15:03):

@io7m (Mark Raynsford) posted in Induction hypotheses, again

Hello!
Revisiting Is there a solution for the problematic induction hypotheses generated using eqn:H? slightly, I’ve run into a similar problem again. To summarize the original post, the behaviour of the induction tactic has a recognized design flaw and there’s a GitHub issue filed for it ("induction ... eqn" creates unusable hypothesis without error · Issue #11784 · coq/coq · GitHub).
In the or...

Discourse Bot (Feb 13 2024 at 15:11):

@imaxw (Ian Maxwell) posted in Is constructive indefinite description a conservative extension?

Recall that the axiom of constructive indefinite description is given as
Axiom constructive_indefinite_description :
forall (A : Type) (P : A->Prop),
(exists x, P x) -> { x : A | P x }.

Let P : Prop be a proposition whose definition does not depend on the constructive_indefinite_description axiom. If P is provable using CID, does it follow that it was already provable without it?
My reaso...

Discourse Bot (Feb 17 2024 at 03:08):

@imaxw (Ian Maxwell) posted in Negative definitions of coinductive propositions

I am working with the following coinductive definition of the conatural numbers (using primitive projections):
CoInductive t : Set := mk {| pred : option t |}.

This definition is chosen over the traditional one with two constructors because positive coinductive definitions are of course officially discouraged. But I am having trouble figuring out how to define a bisimulation on this type in term...

Discourse Bot (Feb 20 2024 at 11:58):

@JanM (Jan Menz) posted in Destructing term when match generates equality involving that term

Hello everyone,
recently I have run into problems with dependencies preventing me from destructing terms I match on when the branches of the match use the equality generated by the match.
For example I have something like the following scenario:
I have types function and type as well as functions get_type and has_type that infer a type for a function (if possible) and check that a function has ...

Discourse Bot (Feb 28 2024 at 15:20):

@tolearn posted in [Question; very basic] Stack-based virtual machine test

Hello everyone,
I’m relatively new to using Coq and am currently working on verifying a stack-based virtual machine. My main goal is to ensure that illegal instructions are not generated by the compiler. To get up to speed, I’ve been familiarizing myself with the basics of Coq.
One of my objectives is to verify that the instruction executor only processes valid instructions. For instance, the AD...

Discourse Bot (Mar 03 2024 at 16:23):

@randl (MRandl) posted in Ltac with variadic argument

Hello,
I am trying to write a tactic that wraps around rewrite, like this:
Ltac sire H := simpl; rewrite H; simpl.

However, rewrite is variadic, but it seems that
sire tactic1, tactic2.

is rejected by Coq since it only expects one argument. I would expect it to expand something like
simpl; rewrite tactic1, tactic2; simpl.

Is there any way to do this in Ltac?
Best,
Mrandl

Discourse Bot (Mar 19 2024 at 11:40):

@caverill (Charles Averill) posted in How to automatically extract anonymous subterms in a goal

I’m writing proofs about Coq functions that frequently contain non-reducable terms constructed of a series of let ... := ... in expressions, as well as anonymous fixpoints and functions. If I want to reduce these terms, I have to extract, say, each anonymous fixpoint as its own object, write a subproof about what it evaluates to for a generic input, and then rewrite the result. I would really like...

Discourse Bot (Mar 26 2024 at 09:21):

@florath (Andreas Florath) posted in How to proof a simple statement about rational numbers

Hello!
I’m completely stuck with this. Could anybody give me a hint how to proof the following?
Require Import QArith.
Local Open Scope Q_scope.

Lemma example1 : forall (v : Q), (12.0 = (2.0 * (v - 4.0))) -> v = 10.0.

Discourse Bot (Apr 04 2024 at 13:10):

@yanson posted in How to use binary floats in Flocq

Hi! I’m very new to Coq (and provers in general). I’m trying to figure out how binary floats in Flocq work. My end goal is performing calculations on binary32’s and binary64’s and retrieving the result. I’ve figured out how to create a binary_float (based on this thread on stackoverflow). Here’s the code I ended up with:
Require Import BinNums BinInt ZArith Floats.
From Flocq Require Import Core ...

Discourse Bot (Apr 06 2024 at 03:19):

@slanterns posted in Https://coq.inria.fr/opam/released is down

The webpage for the package repository can no longer be opened. Is there anything wrong? Thanks!

Discourse Bot (Apr 06 2024 at 14:11):

@dragazo posted in How to simplify single-branch match expressions?

I’m working my way through the software foundations book on my own, and I’ve gotten caught on the lower_grade_lowers exercise in Basics. Specifically, I’m struggling with one sub-expression that coq refuses to simplify:
match l with
| A | _ => Grade l Natural
end

I don’t see why this expression would not simplify to simply Grade l Natural, at which point the solution becomes obvious. The only ...

Discourse Bot (Apr 10 2024 at 17:38):

@juliushamilton posted in Ologs in Coq

I am trying to work on a project where I define a formally verified model of a restaurant business. You can think of it like a model of a manufacturing process, production workflow of some kind, or organizational operation.
I really like the idea of ologs, which are category-theoretic knowledge graphs, essentially, but I am still thinking a lot about how to interpret them conceptually.
Some good...

Discourse Bot (Apr 10 2024 at 20:40):

@zepalmer (Zachary Palmer) posted in Replacing "true = false"

Hi! I’ve been learning Ltac by scribbling together a tactic that tidies things up for me. In my case, I seem to occasionally wind up with goals of the form true = false \/ P that I would like to simplify to just P. In order to be robust via compositionality, though, I’d like to tell the tactic to do two things:

Whenever we see False \/ P, use right to replace it with P
Whenever we see Q \/ P,...

Last updated: Apr 20 2024 at 00:02 UTC