/machines/1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF/rocq/c_strict400.v · raw
  1
  2
  3
  4
  5
  6
  7
  8
  9
 10
 11
 12
 13
 14
 15
 16
 17
 18
 19
 20
 21
 22
 23
 24
 25
 26
 27
 28
 29
 30
 31
 32
 33
 34
 35
 36
 37
 38
 39
 40
 41
 42
 43
 44
 45
 46
 47
 48
 49
 50
 51
 52
 53
 54
 55
 56
 57
 58
 59
 60
 61
 62
 63
 64
 65
 66
 67
 68
 69
 70
 71
 72
 73
 74
 75
 76
 77
 78
 79
 80
 81
 82
 83
 84
 85
 86
 87
 88
 89
 90
 91
 92
 93
 94
 95
 96
 97
 98
 99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
From BusyCoq Require Import Individual62.

Require Import ZArith Lia.
Require Import String.
Require Import List.
From BusyCoq Require Import ES_v3.

Definition tm := Eval compute in (TM_from_str "1RB1LD_0RC1RC_1LA1RE_---1LE_1RF0RC_0RB0LF").

Notation "c -->* c'" := (c -[ tm ]->* c') (at level 40).
Notation "c -->+ c'" := (c -[ tm ]->+ c') (at level 40).

Definition G : list sym :=
  [0;0;1;1;0;1;1;1;1;0;1;1;0;1;1;1;1;1;1;0;1;1;0;1;1;1;1;1;0;0;1;1;0;1;1;1;1;1;0;1;1;0;0].

Definition Kr n a b c d :=
  0inf <{{F}} G *> [1] *> [1;1]^^n *> [0] *> [1;1]^^a *> [0;1;1;0] *> [1;1]^^b
    *> [0;0;0;0;0;0] *> [1] *> [1;1]^^c *> [0;1;1;0;1;1;1;1;0;0;0;0;0;0] *> [1;1]^^d
    *> [0;1;1;0;0;1;1;0;1;1;1] *> 0inf.


Fixpoint cc_steps (n:nat) (x:cconfig) : option cconfig :=
match n with
| O => Some x
| S n0 =>
  match cconfig_step tm x with
  | Some x0 => cc_steps n0 x0
  | None => None
  end
end.

Lemma cc_steps_spec n x y:
  cc_steps n x = Some y -> cconfig_to_config x -->* cconfig_to_config y.
Proof.
  gen x.
  induction n; cbn[cc_steps]; intros x H.
  - inverts H. apply evstep_refl.
  - pose proof (cconfig_step_spec tm x) as HE.
    destruct (cconfig_step tm x) as [x0|]. 2: congruence.
    eapply evstep_step; eauto.
Qed.

Fixpoint cc_steps' (n1 n2 n3:nat) (x:cconfig) : option cconfig :=
match n1 with
| O => cc_steps n3 x
| S n1 =>
  match cc_steps n2 x with
  | Some x0 => cc_steps' n1 n2 n3 x0
  | None => None
  end
end.

Lemma cc_steps'_spec n1 n2 n3 x y:
  cc_steps' n1 n2 n3 x = Some y -> cconfig_to_config x -->* cconfig_to_config y.
Proof.
  gen x.
  induction n1; cbn[cc_steps']; intros x H.
  - exact (cc_steps_spec _ _ _ H).
  - destruct (cc_steps n2 x) as [x0|] eqn:E. 2: congruence.
    eapply evstep_trans.
    + exact (cc_steps_spec _ _ _ E).
    + apply IHn1, H.
Qed.

Definition Kr_list n a b c d : list sym :=
  G ++ [1] ++ [1;1]^^n ++ [0] ++ [1;1]^^a ++ [0;1;1;0] ++ [1;1]^^b
    ++ [0;0;0;0;0;0] ++ [1] ++ [1;1]^^c ++ [0;1;1;0;1;1;1;1;0;0;0;0;0;0] ++ [1;1]^^d
    ++ [0;1;1;0;0;1;1;0;1;1;1].

Lemma Kr_cc n a b c d:
  Kr n a b c d = cconfig_to_config ([], Kr_list n a b c d, 0, F).
Proof.
  unfold Kr, Kr_list, cconfig_to_config.
  cbn [Str_app]. rewrite !Str_app_assoc. reflexivity.
Qed.


Definition sstep (x:cconfig) : option cconfig :=
  match x with
  | (l, r, m, s) =>
    match tm (s, m) with
    | Some (o, L, s') =>
        match l with
        | [] => Some ([], o::r, 0, s')
        | h::t => Some (t, o::r, h, s')
        end
    | Some (o, R, s') =>
        match r with
        | [] => Some (o::l, [], 0, s')
        | h::t => Some (o::l, t, h, s')
        end
    | None => None
    end
  end.

Fixpoint ss_steps (n:nat) (x:cconfig) : option cconfig :=
match n with
| O => Some x
| S n0 =>
  match sstep x with
  | Some x0 => ss_steps n0 x0
  | None => None
  end
end.

Fixpoint ss_steps' (n1 n2 n3:nat) (x:cconfig) : option cconfig :=
match n1 with
| O => ss_steps n3 x
| S n1 =>
  match ss_steps n2 x with
  | Some x0 => ss_steps' n1 n2 n3 x0
  | None => None
  end
end.

Lemma t: exists y, ss_steps' 400 1000 0 ([],[],0,A) = Some y.
Proof. eexists. vm_compute. reflexivity. Time Qed.