Teaching Divisibility and Binomials with Coq ; Enseigner divisibilité et binomiaux avec Coq
In: https://inria.hal.science/hal-04550762 ; RR-9547, Inria. 2024, pp.13, 2024
Online
report
Zugriff:
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.
Titel: |
Teaching Divisibility and Binomials with Coq ; Enseigner divisibilité et binomiaux avec Coq
|
---|---|
Autor/in / Beteiligte Person: | Boldo, Sylvie ; Clément, François ; Hamelin, David ; Mayero, Micaela ; Rousselin, Pierre ; Formally Verified Programs, Certified Tools and Numerical Computations (TOCCATA) ; Inria Saclay - Ile de France ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria)-Laboratoire Méthodes Formelles (LMF) ; Institut National de Recherche en Informatique et en Automatique (Inria)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay)-CentraleSupélec-Université Paris-Saclay-Centre National de la Recherche Scientifique (CNRS)-Ecole Normale Supérieure Paris-Saclay (ENS Paris Saclay) ; Simulation for the Environment: Reliable and Efficient Numerical Algorithms (SERENA) ; Inria de Paris ; Institut National de Recherche en Informatique et en Automatique (Inria)-Institut National de Recherche en Informatique et en Automatique (Inria) ; Centre d'Enseignement et de Recherche en Mathématiques et Calcul Scientifique (CERMICS) ; École des Ponts ParisTech (ENPC) ; Laboratoire d'Informatique de Paris-Nord (LIPN) ; Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord ; Laboratoire Analyse, Géométrie et Applications (LAGA) ; Université Paris 8 Vincennes-Saint-Denis (UP8)-Centre National de la Recherche Scientifique (CNRS)-Université Sorbonne Paris Nord ; Défi Inria LiberAbaci ; Inria ; European Project: ERC-2018-SYG-810367,EMC2 |
Link: | |
Zeitschrift: | https://inria.hal.science/hal-04550762 ; RR-9547, Inria. 2024, pp.13, 2024 |
Veröffentlichung: | HAL CCSD, 2024 |
Medientyp: | report |
Schlagwort: |
|
Sonstiges: |
|