Exos Coq
Quelques tactiques de Coq,
PDF (Joe Redmon).
En plus fourni, la Coq Tactics Cheatsheet.
- TP1 : énoncé, squelette
Indications :
- Exo 1 :
intro, intros, assumption, apply hyp, destruct hyp, split, left, right unfold not
- Exo 2 :
destruct hyp with term, exists term
- Exo 3 :
specialize hyp with term, assert (hyp:formula), assert(formula), Search(eq_sym)
- TP2 : énoncé, squelette
Indications :
simpl, induction var, rewrite hyp, rewrite prop. Require Import Lia. Lemma mult_n_0:forall n, n*0=0.
- TP3 : énoncé, squelette
- TP4 : énoncé
- TP5 : énoncé
- Mini Guide Coq
- TP1 : énoncé, squelette
- TP2 : énoncé, squelette
- TP3 : énoncé, squelette
- TP4 : énoncé, squelette
L'ouvrage Logical Foundations
Les trois premiers chapitres de Logical Foundations (Benjamin Pierce et al.) de la série
Software Foundations,
traduits en français par Tom Hirschowitz.
- Les bases, squelette
- L'induction, squelette
- Les structures de données, squelette