Définition de la fonction prédécesseur (avec pred 0 = 0) pour les nombres naturels en Lean

Question

J'apprends l'assistant de preuve Lean. Un exercice dans https://leanprover.github.io/theorem_proving_in_lean/inductive_types.html consiste à définir la fonction prédécesseur pour les nombres naturels. Quelqu'un peut-il m'aider avec ça?

Answer 1

Vous êtes probablement familier avec le modèle de correspondance de Lean ou d'un langage de programmation fonctionnelle, est donc ici une solution qui utilise ce mécanisme:

open nat 

definition pred : ℕ → ℕ 
| zero  := zero 
| (succ n) := n 

Une autre façon de le faire est d'utiliser un recursor comme ceci:

def pred (n : ℕ) : ℕ := 
    nat.rec_on n 0 (λ p _, p) 

ici, 0 est ce que nous revenons si l'argument est nul et (λ p _, p) est une fonction anonyme qui prend deux arguments: le prédécesseur (p) de n et le résultat de l'appel récursif pred p. La fonction anonyme ignore le deuxième argument et renvoie le prédécesseur.