What are /r/Coq's favorite Products & Services?

From 3.5 billion Reddit comments

Quoting the manual on decide equality:

> This tactic solves a goal of the form forall x y:R, {x=y}+{~x=y}, where R is an inductive type such that its constructors do not take proofs or functions as arguments, nor objects in dependent types. It solves goals of the form {x=y}+{~x=y} as well.

Previous definitions within a file can be used in subsequent proofs. To use definitions and theorems from another file, compile that file with the coqc command and then import it into your current file. Most commonly one does this with Require Import <Name>., but there are variations. See the documentation for more detail:

https://coq.inria.fr/distrib/current/refman/proof-engine/vernacular-commands.html#coq:cmd.require

For larger scale developments, you'll likely want to research the _CoqProject file format and coq_makefile command.

> How would you tackle this issue?

By writing x => x as the default case rather than _ => x. The behaviour is the same but the type is not.

As for the question about intrinsically typed vs. raw data + predicate, Coq people tend to favour the second option because the language constructs to manipulate intrinsically typed data are not very convenient. You can have a look in the manual for the extended match allowing you to write complex dependent pattern matchings. You may also want to use equations rather than writing these nasty dependent pattern-matches yourself.

The approach to "not refer to names in proof" is an interesting option. To avoid having to write match goal with ... end, a lightweight syntax to select hypotheses by type rather than by name could be very helpful -- I have observed this feature being put to good use by Isabelle users.

I was sure that there was a bugreport against Coq to request this feature, but I could not find it back. I created a new ticket to track it.

>Please use {} instead []

tells you all you need to know. Additionally, https://coq.inria.fr/refman/language/extensions/implicit-arguments.html

I think this points to the reason why that part of your proof was impossible: https://stackoverflow.com/questions/4519692/keeping-information-when-using-induction

Basically information was "lost" in the induction and so the proof became impossible. You'll want to introduce an equality with a fresh variable or try out the dependent induction tactic (which I believe essentially does the same thing but automatically).

edit: more details.

LebNotation? The comment says that this style is used in Mergesort and you can indeed see it in action there.

To add files, put 'Add LoadPath <file directory location>' at the top of the file you want to add your module too

This command will add <file directory location> to the coq load path so that it gets searched when coq runs Import commands

Next put 'Require Import <file name>' under the 'Add LoadPath ...' command

Note you can just put the full path and name of the file you want to add into a single 'Require Import' statement

here is a partial guide to coq modules: https://coq.inria.fr/tutorial/3-modules

Here is an example question that might benefit from the Gallina tag.

For the description - I'd mention something about Gallina being the object language of Coq, or maybe "if your question is about tactics, use the coq-tactic tag instead."

> Theorem: let v and w be good vectors with the same contents. Then v and w have the same length. Proof: induction on v. If v is empty, then w must also be empty. If v = (Cons a v’), then we must have that a is in w. Then w has the same contents and length as (Cons a w’). By goodness, we have that w’ and v’ have the same contents (namely, the contents of v, excluding a). Then w’ and v’ have the same length by the inductive hypothesis.

I'm not sure that this proof goes through since we don't have that w = (Cons a w').

But I think I understand your general strategy and actually it seems quite similar to the one described by the Coq MSets library where a set is a record with the underlying data type (say, a list or AVL tree) together with a predicate IsOk which says that the data type doesn't contain duplicates or in the case of AVL trees, probably some more complicated predicate.

Following: http://coq-blog.clarus.me/tutorial-a-hello-world-in-coq.html Have you correctly installed coq-io-system?

opam repo add coq-released https://coq.inria.fr/opam/released opam install coq-io-system

If you can use ssreflect's rewrite, you can chain them as explained there: https://coq.inria.fr/refman/proof-engine/ssreflect-proof-language.html#chained-rewrite-steps

Your rewrites could become rewrite !op_assoc -op_inv_l !-op_id_l in H (roughly, I'm too lazy to test).

I don't see the match. It is the point of the Arguments firstn : simpl nomatch. to make sure that firstn is not unfolded unless it can be reduced. It is documented here

The stronger lemma indeed looks more useful.

Where are you getting list_max from, or how have you defined it? It’s not in the standard library, so I guess you’ve defined it yourself; but the proof of this will depend on how you’ve defined it.

Generally, for questions like this, people can help you much more easily if you give a “minimal working example” — i.e. a stripped-down version of your file, including the necessary import statements and definitions, so that we can copy-paste that into a file and try it out ourselves, rather than having to guess all your definitions!

That said: assuming your list_max is defined by recursion on the list (or equivalently by fold-ing over the list with max), I can suggest two strategies:

1. a direct proof by induction on the list (which should work as both

2. a version formalising the “human proof” you suggest. For this, you’ll need two lemmas corresponding to the facts you use in that proof: one giving the relationship between leb and forallb, and another giving the relationship between forallb and existsb.

In general, quotient types are a bit more problematic than many other kinds of type constructions. There are two possibilities in Coq:

1. You could use setoids. A setoid is a type together with an equivalence relation, i.e., we form the quotients freely by simply carrying around the equivalence relation by which the type ought to be quotiened. There is a lot of machinery in Coq to support setoids.

2. The new and fancy way to do quotients is to use homotopy type theory. Quotients can be constructed as higher-inductive types: to quotient the type A by the equivalence relation R we introduce a new type A/R which has a constructor q : A → A/R, and for all x, y : A and all r : R x y we add a path p x y r : q x = q y (in homotopy type theory u = v is thought of as the type of paths from u to v). This constructions should remind you not of quotients, but of homotopy quotients: we are not actually identifying q x and q y, we're connecting them with a path.

The HoTT approach can be seen in the HoTT library, while the setoids are part of the Coq standard library.

This looks really nice, congratulations! Could you also comment to point towards your work on my Bug 4451 -- Feature request: light syntax to select hypotheses by type rather than by name?