What are /r/dependent_types' favorite Products & Services?

From 3.5 billion Reddit comments

Besides CPDT, a huge change document-wise is Software Foundations, Benjamin Pierce online book on proofs (in Coq) and programming languages theory (in Coq). It's excellent, and it is aimed at beginners -- unlike CPDT which is a great book, but rather for people that already know Coq or at least want to go deep into the more difficult stuff. You cannot advertise Coq to students without mentioning it.

Changes in Coq since 2008. I would say adding eta-equality on functions in the definitional equality was a big change. At a smaller level, bullets definitely had an influence on how people write the usual tactic script (or SSReflect if you use that -- and the Feit-Thompson theorem is an achievement you may want to talk about).

There are exciting things in the development version of Coq, or planned to land before the next release: universe polymorphism, parallel checking of completed proofs, and the new tactics engine (which is more of an internal change that will allow for new developments in the future).

The credits section of the Coq manual is a fascinating read that will let you know everything about new features in the core distribution from whichever version you're interested in.

Set Printing Universes is your friend here. The 8.5 beta (or the trunk version) of Coq will print the universe in the error message if it's needed to distinguish otherwise equal-looking Type's.

Alternatively, you can use the polymorphic universes support added in 8.5. I assume that your nat type is defined something like

Definition nat := forall (X:Type), (X -> X) -> X -> X.

You might try

Polymorphic Definition nat := forall (X:Type), (X -> X) -> X -> X.

Then, your exp definition works for me. You might need to use Polymorphic with the exp definition to use it later :P

Or, do Set Universe Polymorphism at the top of your file, which will make all definitions polymorphic in the universe. You can use Monomorphic Definition (or Lemma, etc. for other 'definition' keywords) to restore monomorphism for one definition.

More info in Universe Polymorphism chapter of the 8.5beta reference manual.

You may want to have a look at Martin Escardo's ordinals in TT.

One possible (different) fix for your approach to work would be to use Impredicative Sets. Or give up Church encodings entirely because they're so darn inefficient anyways.

If it is your intention to actually prove software correctness then the choice of the tool will likely matter more than the choice of the underlying formalism (which in all cases will be some variant of type theory, unless you go in the direction of those first-order logic-based tools, of which I know very little).

For example, you could have a look at F* (https://www.fstar-lang.org) or Coq (https://coq.inria.fr), both of which are real working tools. Pick whichever you find more intuitive.

Isabelle isn't dependently typed. (Specifically, its type system is essentially ML + type classes.) Since you're posting here, this might matter. But if not, you might like its Isar proof language.

Note that Coq also has something similar, though it doesn't seem to be used very much.

We don't have these definitional equalities any longer. They were previously obtained from what we called the regularity condition. However there was a problem with this, in the sense that regularity was not preserved by the algorithm for composition in the universe, which was found by Dan Licata. For details see:

https://groups.google.com/d/msg/homotopytypetheory/oXQe5u_Mmtk/3HEDk5g5uq4J

So now one has to prove the above equality by hand.

It seems that your comment contains 1 or more links that are hard to tap for mobile users. I will extend those so they're easier for our sausage fingers to click!

Here is link number 1 - Previous text "Go"

^Please ^PM ^/u/eganwall ^with ^issues ^or ^feedback! ^| ^Delete

There's been quite a few winter / spring / summer schools around Coq in France (mostly in the South-East region, one in Paris).

One of them is actually about to start. They are usually announced a long while in advance on the relevant mailing lists (TYPES as shown above but also coq-club I'd expect).

Unfortunately, trading anything for Bitcoin with anonymous counterparties may not be legal in the country where you reside, due to anti-money-laundering laws and anti-terrorism laws. Although these warnings were issued by the central bank of India, I can't see how they are any less applicable to e.g. the UK or US, to be honest.

I was trying things out and I got this output:

(thm : (x : (P : ∗¹) → (A⇧¹ → A⇧¹ → P) → P) → (y : (P : ∗¹) → (A⇧¹ → A⇧¹ → P) → P) → ((P₁ : ∗¹) → (P₁ : ∗¹) → (P : P₁ → P₁ → ∗) → (₁ : A⇧¹ → A⇧¹ → P₁) → (₁ : A⇧¹ → A⇧¹ → P₁) → ((₁ : A⇧¹) → (₁ : A⇧¹) → A!!%² ₁ _₁ → (₁ : A⇧¹) → (₁ : A⇧¹) → A!!%² _₁ _₁ → P (₁ ₁ _₁) (₁ _₁ _₁)) → P (x P₁ _₁) (y P₁ _₁)) → A!!%² (f⇧¹ x) (f⇧¹ y)) × ∗₁

It seems to be using the same names for different things? Is that a bug or am I misreading something?

Those are mostly reasonable, and I've most certainly seen people make similar changes to avoid using hypothesis names, but unfortunately I don't have too many tips myself. I'll comment a tiny bit, but otherwise 100% of the things I said before apply still.

Your unfld ltac does the same thing (or rather, less than) as try unfold es, so I would absolutely not create it.

Your map-length ltac could be replaced with rewrite hints: http://adam.chlipala.net/cpdt/html/LogicProg.html (find Rewrite Hints on the page). You'll want to learn about hint dbs, if you have not done so already. In fact: there is already such a db, list in https://coq.inria.fr/distrib/current/stdlib/Coq.Lists.List.html . autorewrite in * with list should be enough here.