Follow

Proving Algebraic Datatypes are “Algebraic” in
soap.coffee/~lthms/posts/Algeb

It was fun to write, hope you enjoy reading it. I tried to spellcheck it, but tbh I wouldn’t be surprise to find mistakes… If you notice some, feel free to tell me!

@lthms dans le premier exemple en rust la notation "List a" (dans le Box) est pas correcte

@na Ahah, mais tellement x). Ça m’apprendra à essayer d’écrire du rust sans compilateur. Merci !

@lthms de rien :)

Aussi, ici : "where unit models the nil case, and α + list α models the cons case." Ça devrait être un * non ?

(déso je rapporte les erreurs que je vois une à une mais je suis sûr portable et c'est plus pratique comme ça)

@na Indeed! C’est pratique pour moi aussi, je les corrige au fur et à mesure (:

@lthms j'ai tout lu et c'était très intéressant, je suis juste triste de pas avoir le niveau en Coq pour comprendre certaines démonstrations :(( merci d'avoir écrit ça en tout cas

@na Cool ! Si tu as des questions, hésite pas du coup. (:

@lthms je pense qu'il faudrait surtout que je prenne un tuto Coq et que je m'y mette sérieusement haha, sinon je vais te poser des questions pendant deux semaines je pense

@na La première étape un peu « facile » c’est sans doute d’installer Coq/CoqIDE et de regarder pas à pas comment se découpent les preuves.

Après dans cet article, pour les garder courtes, j’ai eu tendance à les réduire au maximum donc tu verras pas forcément grand chose x).

That being said, si un jour tu te mets à Coq, je répondrais à toutes les questions que tu pourras poser, pendant deux semaine ou plus \o/ avec plaisir.

@lthms je ferais sans doute ça quand j'aurais un pc sous la main

Et merci de bien vouloir répondre à mes futures questions :)))

@lthms @na Tout pareil 😊 C'est toujours sympa de répondre à la plupart des questions Coq ☺️

@MartinShadok @lthms @na
Petite question, vous me conseillez quoi pour commencer à apprendre Coq ?
Je connais déjà OCaml, et j'ai déjà vu quelques preuves basiques en Coq.

@jin @MartinShadok @na Perso, ma ressource de base a été le Coq’art. La collection de livre Software Foundations est souvent conseillé aujourd’hui.

Une fois les bases acquises, il faut lire le manuel et lire du code pour « découvrir » les douze mille constructions de Coq et choisir celles qui te conviennent le mieux (Coq est de ces systèmes où il existe plein de manière de faire la même chose et il n'existe aucun consensus pour désigner un sous-ensemble « largement conseillé »).

@lthms ooh, you finished it! I will reserve some time for reading it tomorrow. I don't think I can catch finer points this point of the evening anymore 😁

@tuturto feel free to share your thoughts and questions!

@lthms the parts I have read so far are super good and easy enough to follow. I made a mistake and tried reading it in the late evening though, so I couldn't make it to end.

But I'm definitely going read it through with thought. This is interesting stuff!

@lthms "The associativity of sum is straightforward to prove, and should not pose a particular challenge to perspective readers; if we assume that this article is well-written, that is!" :)

I liked the article, seemed very well written and example good. I didn't understand everything, but that's probably because I'm just beginner in Coq and many of the tactics used I hadn't seen before.

I did bookmark it though. Maybe I can understand it later when I have better understanding of basics.

Sign in to participate in the conversation
Mastodon

Server run by the main developers of the project 🐘 It is not focused on any particular niche interest - everyone is welcome as long as you follow our code of conduct!