Library Turing

Section Turing.

Require Import Coq.Sets.Ensembles.
Require Import Coq.Sets.Finite_sets.
Require Import Coq.Logic.Decidable.
Require Import Coq.Sets.Finite_sets_facts.

Require Import Arith.
Require Import Omega.

Require Import Classical.

Eval compute in (fst (1,2,3)).
Eval compute in (snd (1,2,3)).
Check (((1,2),3)).

Inductive ShiftDirection:Type :=
|shiftleft:ShiftDirection
|shiftright:ShiftDirection.


Inductive halftape (Gamma:Type):=
|htapeempty:halftape Gamma
|htapefirst:Gamma -> (halftape Gamma)
 -> (halftape Gamma).

Inductive tape (Gamma:Type):=
tape_intro:
(halftape Gamma) -> Gamma -> (halftape Gamma)
 -> (tape Gamma).

Definition emptytape (Gamma:Type) (blank:Gamma):=
tape_intro Gamma
(htapeempty Gamma) blank (htapeempty Gamma).

Definition tapeleft (Gamma:Type) (t:tape Gamma)
:halftape Gamma.
Defined.

Definition tapecenter (Gamma:Type) (t:tape Gamma)
:Gamma.
Defined.

Definition taperight (Gamma:Type) (t:tape Gamma)
:halftape Gamma.
Defined.

Definition tapewrite (Gamma:Type) (t:tape Gamma)
(w:Gamma):tape Gamma.
Defined.

Definition tapeshiftleft (Gamma:Type) (blank:Gamma)
(t:tape Gamma):tape Gamma.
Defined.

Definition tapeshiftright (Gamma:Type) (blank:Gamma)
(t:tape Gamma):tape Gamma.
Defined.

Definition tapeshift (Gamma:Type) (blank:Gamma)
(t:tape Gamma) (dir:ShiftDirection):=
match dir with
|shiftleft => tapeshiftleft Gamma blank t
|shiftright => tapeshiftright Gamma blank t
end.

Definition DecidableEq (U:Type):=forall (x y:U),

{x=y}+{x<>y}
.


Definition DecidableEnsemble (U:Type) (S:Ensemble U):=
forall x:U, {In U S x} + {~In U S x}.

Lemma emptydecidable: forall (U:Type),
DecidableEnsemble U (Empty_set U).

Lemma singletondecidable: forall (U:Type) (x:U),
DecidableEq U -> DecidableEnsemble U (Singleton U x).

Lemma coupledecidable: forall (U:Type) (x y:U),
DecidableEq U -> DecidableEnsemble U (Couple U x y).

Lemma uniondecidable: forall (U:Type) (A B:Ensemble U),
DecidableEnsemble U A ->
DecidableEnsemble U B ->
DecidableEnsemble U (Union U A B).

Definition step (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q)
(t:tape Gamma)
(dec:DecidableEnsemble Q F)
:Q*(tape Gamma)*bool.
Defined.


Definition step_result_q {Q} {tape} (result:Q*tape*bool):=
 let (x,_):=result in let (q,_):=x in q.
Definition step_result_t {Q} {tape} (result:Q*tape*bool):=
  let (x,_):=result in let (_,t):=x in t.
Definition step_result_h {Q} {tape} (result:Q*tape*bool):=let (_,h):=result in h.

Lemma step_dec: forall (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q)
(t:tape Gamma)
(dec:DecidableEnsemble Q F),
let result:=step Q Gamma blank delta q0 F t dec in

(In _ F (step_result_q result) /\ step_result_h result=true) \/
(~ In _ F (step_result_q result) /\ step_result_h result=false).

Fixpoint run (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (t:tape Gamma)
(dec:DecidableEnsemble Q F) (count:nat):(tape Gamma*nat):=
match count with
|0 => (t,0)
|S c => match (step Q Gamma blank delta q0 F t dec) with
 |(nq,nt,true) => (nt,count)
 |(nq,nt,false) => run Q Gamma blank delta nq F nt dec c
 end
end.

Fixpoint run_full (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (t:tape Gamma)
(dec:DecidableEnsemble Q F) (count:nat):(Q*(tape Gamma)*bool*nat):=
match count with
|0 => (q0,t,false,0)
|S c => match (step Q Gamma blank delta q0 F t dec) with
 |(nq,nt,true) => (nq,nt,true,count)
 |(nq,nt,false) => run_full Q Gamma blank delta nq F nt dec c
 end
end.


Definition run_full_result_q {Q} {tape} (result:Q*tape*bool*nat):=
 let (x,_):=result in let (y,_):=x in let (q,_):=y in q.
Definition run_full_result_t {Q} {tape} (result:Q*tape*bool*nat):=
 let (x,_):=result in let (x,_):=x in let (_,t):=x in t.
Definition run_full_result_h {Q} {tape} (result:Q*tape*bool*nat):=
 let (x,_):=result in let (_,h):=x in h.
Definition run_full_result_c {Q} {tape} (result:Q*tape*bool*nat):=
 let (_,c):=result in c.

Lemma run_full_dec: forall (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (t:tape Gamma)
(dec:DecidableEnsemble Q F) (count:nat),
let result:=run_full Q Gamma blank delta q0 F t dec (S count) in

(In _ F (run_full_result_q result) /\ run_full_result_h result=true)\/
(~ In _ F (run_full_result_q result) /\ run_full_result_h result=false /\
run_full_result_c result=0).

Lemma run_full_noncero: forall (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (t:tape Gamma)
(dec:DecidableEnsemble Q F) (count:nat),
let result:=run_full Q Gamma blank delta q0 F t dec count in
0<run_full_result_c result -> run_full_result_h result=true.

Lemma run_full_countdec: forall (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (t:tape Gamma)
(dec:DecidableEnsemble Q F) (count:nat),
run_full_result_c (run_full Q Gamma blank delta q0 F t dec count)<=count.

Lemma run_full_same: forall (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (t:tape Gamma)
(dec:DecidableEnsemble Q F) (c1 c2:nat),
let result1:=run_full Q Gamma blank delta q0 F t dec c1 in
let result2:=run_full Q Gamma blank delta q0 F t dec c2 in
(run_full_result_h result1=true /\ run_full_result_h result2=true) ->
(run_full_result_q result1=run_full_result_q result2 /\
run_full_result_t result1=run_full_result_t result2 /\
c1-run_full_result_c result1=c2-run_full_result_c result2
).


Definition runblank (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q)
(dec:DecidableEnsemble Q F) (count:nat):(tape Gamma*nat):=
run Q Gamma blank delta q0 F
  (emptytape Gamma blank) dec count.

Section examples.
Let L:=shiftleft.
Let R:=shiftright.
 Section max3step.
Inductive ex_Q:=ex_A:ex_Q|ex_B:ex_Q|ex_C:ex_Q|ex_H:ex_Q.
Let Q:=ex_Q.
Let A:=ex_A.
Let B:=ex_B.
Let C:=ex_C.
Let H:=ex_H.

Lemma ex_Qdecidable: forall (x y:Q), {x=y}+{x<>y}.

 Inductive ex_Gamma:=ex_blank:ex_Gamma|filled:ex_Gamma.
Let Gamma:=ex_Gamma.
 Let delta (q:Q) (g:Gamma):=
 match q with
 |ex_A => match g with ex_blank => (B,filled,R)
   | filled => (H,filled,R) end
 |ex_B => match g with ex_blank => (B,filled,L)
   | filled => (C,ex_blank,R) end
 |ex_C => match g with ex_blank => (C,filled,L)
   | filled => (A,filled,L) end
 |ex_H => match g with ex_blank => (H,ex_blank,R)
   | filled => (H,filled,R) end
 end.
 Check delta.
 Let F:=Singleton Q H.
 Let M:=(Q,Gamma,ex_blank,delta,A,F).
 Print M.

 Eval compute in (if true then 0 else 1).

 Eval compute in (runblank
  Q Gamma ex_blank delta A F
  (singletondecidable Q H ex_Qdecidable) 100).

 Eval compute in
  (step Q Gamma ex_blank delta A F (emptytape Gamma ex_blank)).
 End max3step.

End examples.


Fixpoint natpow (m n:nat):=
match n with
|O=>1
|S p=>m*(natpow m p)
end.
Eval compute in (natpow 2 10).

Lemma natpow_e0: forall n:nat, natpow n 0=1.

Lemma natpow_0: forall n:nat, 0<n-> natpow 0 n=0.

Definition polybound (f:nat->nat) (e:nat):=
exists n0, exists c:nat, forall n:nat, n0<=n -> f n<=c*(natpow n e).

Definition anypolybound (f:nat->nat):=exists e:nat, polybound f e.

Lemma ex_n2_bounded: polybound (fun n:nat=>n*n) 2.

Lemma nat_n_le_nm: forall m n:nat,n<=n* S m.

Lemma polybound_plus1: forall (f:nat->nat) (e:nat),
polybound f e -> polybound f (S e).

Fixpoint halftape_length (Gamma:Type) (h:halftape Gamma):=
match h with
|htapeempty=>0
|htapefirst h b=>S (halftape_length Gamma b)
end.

Definition tape_length (Gamma:Type) (t:tape Gamma):=
S(halftape_length Gamma (tapeleft Gamma t) +
halftape_length Gamma (taperight Gamma t)).


Inductive machinerecognized (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (dec:DecidableEnsemble Q F)
:Ensemble (tape Gamma):=
|recognize : forall t:tape Gamma, (exists count:nat,
0<snd (run_full Q Gamma blank delta q0 F t dec count))
->In (tape Gamma) (machinerecognized Q Gamma blank delta q0 F dec) t.

Definition machinetime (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (dec:DecidableEnsemble Q F)
(f:nat->nat):Prop:=
forall t:tape Gamma,
In _ (machinerecognized Q Gamma blank delta q0 F dec) t->
exists n:nat, n<=f (tape_length _ t) /\
0<snd (run_full Q Gamma blank delta q0 F t dec n).


Inductive class_P_recognized (Gamma:Type): Ensemble (Ensemble (tape Gamma)):=
|class_P_solvable: forall C:Ensemble(tape Gamma),
(exists Q:Type, exists blank:Gamma,
exists delta:Q->Gamma->(Q*Gamma*ShiftDirection),
exists q0:Q, exists F:Ensemble Q,
exists dec:DecidableEnsemble Q F,
exists f:nat->nat,
(machinetime Q Gamma blank delta q0 F dec f)
/\
(machinerecognized Q Gamma blank delta q0 F dec)=C
/\
anypolybound f
)
->In _ (class_P_recognized Gamma) C.

Definition machinedeciding (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (dec:DecidableEnsemble Q F):=
forall t:tape Gamma,
In _ (machinerecognized Q Gamma blank delta q0 F dec) t.

Inductive language_complement (Gamma:Type) (L:Ensemble (tape Gamma))
:Ensemble (tape Gamma):=
|language_complement_intro: forall t:tape Gamma, ~ In _ L t
 -> In _ (language_complement Gamma L) t.

Inductive class_complement (Gamma:Type) (C:Ensemble (Ensemble (tape Gamma)))
:Ensemble (Ensemble (tape Gamma)):=
|class_complement_intro:forall L:Ensemble (tape Gamma),
In _ C L -> In _ (class_complement Gamma C) (language_complement Gamma L).

Definition class_complementclosed (Gamma:Type) (C:Ensemble (Ensemble (tape Gamma))):=
C=class_complement Gamma C.

Lemma language_complement_involution: forall (Gamma:Type) (L:Ensemble (tape Gamma)),
language_complement _ (language_complement _ L)=L.

Lemma class_complement_involution: forall (Gamma:Type) (C:Ensemble(Ensemble (tape Gamma))),
class_complement _ (class_complement _ C)=C.

Theorem language_complement_inclusion: forall (Gamma:Type) (A B:Ensemble (tape Gamma)),
Included _ A B -> Included _ (language_complement _ B) (language_complement _ A).

Inductive machineaccepted (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (A:Ensemble Q)
(dec:DecidableEnsemble Q F)
:Ensemble (tape Gamma):=
|machineaccept : forall t:tape Gamma, (exists count:nat,
let result:=run_full Q Gamma blank delta q0 F t dec count in
0<snd result /\ In _ A (run_full_result_q result) )
->In (tape Gamma) (machineaccepted Q Gamma blank delta q0 F A dec) t.

Lemma accepted_is_in_complement: forall (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (A:Ensemble Q)
(dec:DecidableEnsemble Q F),
Included _
(machineaccepted Q Gamma blank delta q0 F A dec)
(language_complement _ (machineaccepted Q Gamma blank delta q0
 F (Ensembles.Complement Q A) dec)).

Theorem accepted_complement: forall (Q Gamma:Type) (blank:Gamma)
(delta:Q->Gamma->(Q*Gamma*ShiftDirection))
(q0:Q) (F:Ensemble Q) (A:Ensemble Q)
(dec:DecidableEnsemble Q F),
machinedeciding Q Gamma blank delta q0 F dec->
machineaccepted Q Gamma blank delta q0 F A dec=
language_complement _ (machineaccepted Q Gamma blank delta q0
 F (Ensembles.Complement Q A) dec).

Inductive class_P (Gamma:Type): Ensemble (Ensemble (tape Gamma)):=
|class_P_intro: forall C:Ensemble(tape Gamma),
(exists Q:Type, exists blank:Gamma,
exists delta:Q->Gamma->(Q*Gamma*ShiftDirection),
exists q0:Q, exists F:Ensemble Q, exists A:Ensemble Q,
exists dec:DecidableEnsemble Q F,
exists f:nat->nat,
(machinetime Q Gamma blank delta q0 F dec f)
/\
(machineaccepted Q Gamma blank delta q0 F A dec)=C
/\
(machinedeciding Q Gamma blank delta q0 F dec)
/\
anypolybound f
)
->In _ (class_P Gamma) C.

Theorem class_P_complementclosed: forall (Gamma:Type),
class_complementclosed _ (class_P Gamma).


End Turing.