(* EXO mots *) Section MOTS. Variable char : Set. Variable a : char. Variable b : char. Require Import List. Definition word : Set := list char. Definition pempty (w:word) : Prop := (w = nil). Definition pchar (c:char) (w:word) : Prop := (w = c::nil). Definition pconcat (p1:word -> Prop) (p2:word -> Prop) (w : word):= (* ... *) Theorem pconcat_empty : forall p w, pconcat p pempty w -> p w. Proof. (* ... *) Qed. Inductive pstar (p:word -> Prop) : word -> Prop := (* ... *) Theorem star_concat : forall (p:word->Prop) w1 w2, p w1 -> pstar p w2 -> pstar p (app w1 w2). Proof. (* ... *) Qed. Theorem concat_star : forall (p:word->Prop) w1 w2, pstar p w1 -> p w2 -> pstar p (app w1 w2). Proof. (* ... *) Qed. Theorem star_pconcat : forall (p:word->Prop) w, pconcat (pstar p) p w -> pstar p w. (* ... *) Qed. End MOTS.