Personnes présentes
- Frédéric Boulanger
- Thibaut Balabonski
- Safouan Taha
- Benoît Valiron
- Burkhart Wolff
- Lina Ye
(Teaching Proofs) theory
Burkhart Wolff presents an educational project to teach the proof to students in master.
The project goal is to model the translation chain of regular expressions into non-deterministic automata with epsilon edges, then to non-deterministic automata (without epsilon) and finally to deterministic automata.
First, students can use a "regexp" theory defining the abstract syntax of regular expressions and a function "L" that gives the language of expressions:
datatype 'a regexp = EmptySet ("∅")
| EmptyWord ("ε")
| Atom 'a
| Seq "'a regexp" "'a regexp" (infixl "⋅" 70)
| Sum "'a regexp" "'a regexp" (infixl "+" 65)
| Star "'a regexp" ("_⇧*" [80] 80)
fun L :: "'a regexp ⇒ 'a list set" where
"L ∅ = {}"
| "L ε = {[]}"
| "L (Atom c) = {[c]}"
| "L (x⋅y) = {u @ v | u v. u∈L x ∧ v∈L y}"
| "L (x+y) = L x ∪ L y"
| "L (x⇧*) = star (L x)" (* "star" builds inductively the concatenation closure of words in $L(x)$ *)
Burkhart also provides to its students an Automata theory defining both deterministic and non-deterministic automata together with formalization of the acceptance criterion.
(* states × transition function × Final states*)
type_synonym ('a,'s)na = "'s × ('a ⇒ 's ⇒ 's set) × ('s ⇒ bool)"
definition accepts⇩s⇩a :: "('a,'s)sa ⇒ 'a list ⇒ bool"
where ...
type_synonym ('a,'s)da = "'s × ('a ⇒ 's ⇒ 's) × ('s ⇒ bool)"
definition accepts⇩d⇩a :: "('a,'s)da ⇒ 'a list ⇒ bool"
where ...
Students have to write in Isabelle/HOL a number of simple and induction proofs (they are allowed to use sledgehammer) and to model a part of the translation function from RegExp to automata and prove it correct; the overall proof architecture was given but gaps had to be filled out. Basically, 25 sorry's and undefined's in definitions had to be replaced.
To do so, they need to prove that the regexp language and the one of the resulting automaton are both equivalent.
function regexp2na :: "'a regexp ⇒ ('a,'s)na"
where ...
theorem "w ∈ L rexp ⟷ accepts (regexp2na rexp) w"
While Christine and mine master-level Interactive Theorem Proving Course (see also for the project material) was near disaster in 2015/2016, the 2016/17 edition went amazingly well. Obviously, our material had substantially improved (in particular the lab-exercises) and we profited from stronger master-class this year...