/machines/1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC/rocq/t1.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
From BusyCoq Require Import Individual62.
Require Import ZifyNat Lia.
Require Import ZArith.
Require Import String.
From BusyCoq Require Import BinaryCounter_v2.

Open Scope list.

Definition tm := Eval compute in (TM_from_str "1RB1RA_1LC1LE_1RF1LD_1RE0LD_0LB0RA_---0RC").

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

Definition C n := BinInc [1;1] n.
Definition HF (l r : side) := l <{{E}} [1;0;1;1] *> r.

Lemma RIncG l r n:
  l <* [1;1;0;1] {{A}}> [1;1]^^n *> [0;0] *> r -->+
  l <{{E}} [1;0;1;1] *> [0;0]^^n *> [1;1] *> r.
Proof. es. Qed.

Lemma RInc n l:
  l <* [1;1;0;1] {{A}}> C n -->+ HF l (C (1+n)).
Proof.
  unfold C, HF. apply RBinInc_spec. intros. apply RIncG.
Qed.

Lemma L1 u b r:
  HF (u <* [1] <* [0;1]^^b) r -->+ u <* [0] <* [0;1]^^b <* [1;1;0;1] {{A}}> r.
Proof. unfold HF. es. Qed.

Lemma L0 u b r:
  HF (u <* [0;0;1;0] <* [0;1]^^b) r -->+ u <* [0;1;0;1] <* [0;1]^^b <* [1;1;0;1] {{A}}> r.
Proof. unfold HF. es. Qed.

Lemma L011 u r:
  HF (u <* [0;0;1;1;0;1]) r -->+ u <* [0;1;1;0;1;0] <* [1;1;0;1] {{A}}> r.
Proof. unfold HF. es. Qed.

Lemma LEat b r:
  HF (0inf <* [0;1]^^b) r -->+ 0inf <* [0;1]^^(b+2) <* [0;1;1] {{A}}> r.
Proof. unfold HF. es. Qed.

Lemma Y1C v n:
  v <* [0;1;1] {{A}}> C (n*2+1) -->+ HF (v <* [1]) (C (1+n)).
Proof.
  unfold C. rewrite BinInc_mul2add1. fold (C n).
  eapply progress_trans. 2: apply RInc.
  unfold C. es.
Qed.

Lemma Y2C v n:
  v <* [0;1;1] {{A}}> C (n*4) -->+ HF (v <* [1;1;1]) (C n).
Proof.
  unfold C. replace (n*4) with (n*2*2) by lia. rewrite !BinInc_mul2.
  unfold HF. es.
Qed.

Lemma Y3 v s r:
  v <* [0;1;1] {{A}}> [0;0] *> [1;1] *> [1;1]^^s *> [0;0] *> r -->+
  HF (v <* [1;1]) ([0;0]^^s *> [0] *> [1;1] *> r).
Proof. unfold HF. es. Qed.

Lemma Y4 v m:
  v <* [0;1;1] {{A}}> [1;1;0] *> [1;1] *> C m -->+ HF (v <* [1;0;1;1]) (C (1+m)).
Proof.
  eapply progress_trans. 2: apply RInc.
  es.
Qed.

Lemma Y1Q v r:
  v <* [0;1;1] {{A}}> [1;1] *> [0;0] *> r -->+ HF (v <* [1]) ([1;1] *> r).
Proof. unfold HF. es. Qed.

Lemma ROvf l j m:
  l <* [1;1;0;1] {{A}}> [1;1]^^j *> [0;1;1] *> C m -->+
  HF (l <* [0;1] <* [1;1]^^j <* [1]) (C (1+m)).
Proof.
  eapply progress_trans. 2: apply RInc.
  es.
Qed.