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

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

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

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

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

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

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

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

**@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?

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

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

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

**@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?

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

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

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

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

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

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

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

**@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

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

**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 5Coq 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 ...

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

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

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

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

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

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

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

**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→SThis 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 <: (...

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

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

**@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?

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

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

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

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

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

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

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

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

...

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

**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 ?jSo, after intros i i_range. I have:

i : nat

i_r...

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

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

endf ≡ λ s, match s with

| inl a => f (inl a)

| inr b => f (inr ...

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

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

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

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

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

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

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

...

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

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

...

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

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

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

**@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 0we 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...

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

(...

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

**@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?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

**@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!

**@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 !

**@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

...

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

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

**@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?

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

**@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

...

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

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

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

**@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 [+] x2what ...

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

**@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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

...

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

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

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

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

**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 VectorCheck 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?

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

**@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 repositoriesanyone know how to fix this?

cross: How does one install a new version of Coq when ...

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

**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!

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

**@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

| [] ...

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

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

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

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

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

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

anyone else getting "page not found"?

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

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

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

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

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

**@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”

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

**@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!

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

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

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

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

...

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

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

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

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

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

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

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

**@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

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

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

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

**@zhengpushi** posted in **How to organize a Coq library?**

How to organize a Coq library?

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

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

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

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

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

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

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

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

**@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

...

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

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

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

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

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

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

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

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

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

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

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

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

**@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?

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

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

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

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

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

**@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 contentRequire Export Sample.

Require Extraction.

Require ExtrOcamlBasic.

Requir...

Last updated: Oct 04 2023 at 22:01 UTC