Post

Thomas🪴
@lipsum.dev

En ce moment, quand j'ai un peu de temps, j'essaie d'apprendre à coder en Lean. Un petit fil à ce sujet 🧵⬇️ …

1 repost2 likes

Thomas🪴
@lipsum.dev

Lean est un assistant de preuve : grosso modo, un langage de programmation qui permet d'écrire des raisonnements mathématiques et de vérifier leur validité — dans le même style, il y a Rocq (alias Coq). J'avais partagé un exemple de programme très simple en Lean ici bsky.app/profile/lips... …

Thomas🪴@lipsum.dev

Avec l'assistant de preuve Lean : theorem married_looks_unmarried (H1 : Looks Paul Linda) (H2 : Looks Linda John) (H3 : Married Paul) (H4 : ¬Married John) : ∃ x y : Person, Married x ∧ ¬Married y ∧ Looks x y := by by_cases h : Married Linda · exists Linda, John · exists Paul, Linda

Thomas🪴
@lipsum.dev

Pour un exemple un peu plus avancé, on peut définir une variante de quicksort : def quicksort : List Nat → List Nat | nil => nil | pivot :: rest => quicksort (rest.filter (· < pivot)) ++ [pivot] ++ quicksort (rest.filter (· ≥ pivot)) …

Thomas🪴
@lipsum.dev

Cependant, pour que cette définition soit acceptée en Lean, il faut prouver la terminaison du programme. Ceci peut se faire en démontrant que les listes passées récursivement en argument à quicksort sont de tailles strictement plus petites que celle d'entrée. …

Thomas🪴
@lipsum.dev

Par ailleurs, on aura sûrement envie de démontrer certaines propriétés de la fonction quicksort. Exemple : les listes d'entrée et de sortie contiennent les mêmes éléments comptés avec leurs multiplicités : theorem quicksort_is_permutation : (quicksort l) ~ l := … (insert proof here) … …