形式言語理論2.10.1の定義2.14, 2.15, 命題2.10, 2.11のCoqによる証明

2.10.1.v

Require Import Relations Setoid Morphisms.
Require Import ssreflect seq fintype.

Section Automaton.

Variable char : finType.
Definition word := seq char.

Definition RightInvariant (R : relation word) : Prop :=
  equiv word R /\ forall (x y : word), R x y -> forall z : word, R (x++z) (y++z).

Variable L : word -> Prop.

Definition R_L (x y : word) : Prop := forall z : word, L (x++z) <-> L (y++z).

Lemma R_L_refl : Relation_Definitions.reflexive _ R_L.
Proof.
  move => x //.
Qed.

Lemma R_L_trans : Relation_Definitions.transitive _ R_L.
Proof.
  move => x y z Hxy Hyz w.
  split.
  by move /Hxy/Hyz.
  by move /Hyz/Hxy.
Qed.

Lemma R_L_symm : Relation_Definitions.symmetric _ R_L.
Proof.
  move => x y Hxy z.
  by split;move /Hxy.
Qed.

Lemma R_L_equiv : equiv word R_L.
Proof.
  split.
  exact R_L_refl.
  split.
  exact R_L_trans.
  exact R_L_symm.
Qed.

Lemma R_L_RightInvariant : RightInvariant R_L.
Proof.
  split.
  exact R_L_equiv.
  move => x y H z w.
  rewrite -2!catA.
  exact (H (z++w)).
Qed.

Add Parametric Relation : word R_L
  reflexivity proved by R_L_refl
  symmetry proved by R_L_symm
  transitivity proved by R_L_trans as L_setoid.

Section DeterministicAutomaton.

Record da : Type := {
  da_state :> Type;
  da_q0 : da_state;
  da_fin : da_state -> Prop;
  da_trans : da_state -> char -> da_state
}.

Fixpoint da_run (A : da) (x : A) (w : word) : seq A :=
match w with
  nil => [::]
 |a :: w' => da_trans A x a :: da_run A (da_trans A x a) w'
end.

Definition da_accept (A : da) (x : A) (w : word) := da_fin A (last x (da_run A x w)).

(*
Fixpoint da_accept (A : da) (x : A) (w : word) :=
match w with
  nil => da_fin A x
  | c::w' => da_accept A (da_trans A x c) w'
end.
*)

Definition da_lang (A : da) (w : word) : Prop := da_accept A (da_q0 A) w.

Definition delta (w : word) (c : char) : word := w ++ cons c nil.
Definition q0 : seq char := nil.
Definition fin (w : word) : Prop := L w.

Add Parametric Morphism : 
  delta with signature (R_L ==> eq ==> R_L) as delta_mor.
Proof.
  move => x y H c z.
  rewrite /delta -2!catA.
  exact (H ([:: c] ++ z)).
Qed.

Add Parametric Morphism : 
  fin with signature (R_L ==> iff) as fin_mor.
Proof.
  move => x y H.
  rewrite /fin.
  move : (H nil).
  by rewrite 2!cats0.
Qed.

End DeterministicAutomaton.

Definition M_L : da := {|
  da_state := word;
  da_q0 := q0;
  da_fin := fin;
  da_trans := delta
|}.

Lemma lemma1 : forall (w q:word), last q (da_run M_L q w) = q ++ w.
Proof.
  elim => [|a w IHw] q.
  by rewrite /da_run /last cats0.
  move => //=.
  by rewrite IHw /delta -catA.
Qed.
  

Goal forall w : word, da_lang M_L w <-> L w.
Proof.
  move => w.
  rewrite /da_lang /da_accept lemma1 => //=.
Qed.

End Automaton.