Teaching Divisibility and Binomials with Coq - HAL Accéder directement au contenu
Rapport Année : 2024

Teaching Divisibility and Binomials with Coq

Enseigner divisibilité et binomiaux avec Coq

Résumé

The goal of this contribution is to provide worksheets in Coq for students to learn about divisibility and binomials. These basic topics are a good case study as they are widely taught in the early academic years (or before in France). We present here our technical and pedagogical choices and the numerous exercises we developed. As expected, it required additional Coq material such as other lemmas and dedicated tactics. The worksheets are freely available and flexible in several ways.
Le but de cette contribution est de fournir des feuilles d'exercices en Coq à destination des étudiants pour l'apprentissage de la divisibilité et des coefficients binomiaux. Ces domaines élémentaires sont un bon sujet d'étude car ils sont largement enseignés durant les premières années universitaires (ou avant en France). Nous présentons nos choix techniques et pédagogiques et les nombreux exercices que nous avons développés. Sans surprise, cela a nécessité des développements {\Coq} supplémentaires tels que de nouveaux lemmes et des tactiques dédiées. Les feuilles d'exercices sont en accès libre et d'un usage flexible.
Fichier principal
Vignette du fichier
RR-9547.pdf ( 709.3 Ko ) Télécharger
Origine : Fichiers produits par l'(les) auteur(s)
Loading...

Dates et versions

hal-04550762, version 1 (18-04-2024)

Licence

Paternité - CC BY 4.0

Identifiants

  • HAL Id : hal-04550762 , version 1
  • ARXIV : 2404.12676

Citer

Sylvie Boldo, François Clément, David Hamelin, Micaela Mayero, Pierre Rousselin. Teaching Divisibility and Binomials with Coq. RR-9547, Inria. 2024, pp.13. ⟨hal-04550762⟩
44 Consultations
53 Téléchargements
Dernière date de mise à jour le 12/05/2024
comment ces indicateurs sont-ils produits

Altmetric

Partager

Gmail Facebook Twitter LinkedIn Plus