Teaching Divisibility and Binomials with Coq Enseigner divisibilité et binomiaux avec Coq En Fr

Fiche du document

Auteurs
Type de document
Périmètre
Langue
Identifiants
Source

HAL SHS (Sciences de l’Homme et de la Société)

Relations

Ce document est lié à :
https://hal.science/hal-04725586v1

Ce document est lié à :
info:eu-repo/semantics/altIdentifier/arxiv/2404.12676

Ce document est lié à :
info:eu-repo/grantAgreement//ERC-2018-SYG-810367/EU/Extreme-scale Mathematically-based Computational Chemistry/EMC2

Collection

Archives ouvertes

Organisation

Centre pour la communication scientifique directe

Licences

http://creativecommons.org/licenses/by/ , info:eu-repo/semantics/OpenAccess

Mots-clés En Fr

Worksheet Coq Arithmetic Divisibility Binomial coefficient Feuille d'exercices Coq Arithmétique Divisibilité Coefficient binomial

Sujets proches En Fr

Gallus gallus Gallus domesticus Coq domestique Coqs Coq d'élevage

Citer ce document

Sylvie Boldo et al., « Enseigner divisibilité et binomiaux avec Coq », HAL SHS (Sciences de l’Homme et de la Société), ID : 10670/1.f27934...

Métriques

Partage / Export

Résumé En Fr

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, the numerous exercises we developed and a small experiment we conducted on two students. 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, les nombreux exercices que nous avons développés ainsi qu'une petite expérience menée sur deux étudiants. 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.

document thumbnail

Par les mêmes auteurs

Sur les mêmes sujets