/machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/rocq/Jtm.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
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
(** * The invariant J on abstract states, and one macro step (TM part) *)

Record st := mkst { sh : nat; sP : list (nat*nat*bool); sT : Tl; sph : phase; sc4 : bool }.

Definition Cf (s : st) : Q * tape := K (sh s) (sP s) (sT s).

Definition TC (ph : phase) (c4 : bool) (T : Tl) : Prop :=
  match ph with
  | E1 | E1t | LX => T = TN /\ c4 = false
  | L1 => T = TN
  | E2 | E2t => T = TA 1 /\ c4 = false
  | T0 => (exists k, T = TB k /\ 3 <= k) /\ c4 = false
  | L2 => exists t, T = TA t /\ 2 <= t
  end.

Definition J (s : st) : Prop :=
  sP s <> [] /\ TC (sph s) (sc4 s) (sT s) /\ AllI (PCx (sph s) (sc4 s) (sh s)) 1 (sP s).

Lemma split1 (P : list tri) :
  (exists Z x R, P = Z ++ x :: R /\ Forall dig0 Z /\ dig x = true) \/ Forall dig0 P.
Proof.
  induction P as [|[[p q] d] P IH]; [right; constructor|].
  destruct d.
  - left. exists (@nil (nat*nat*bool)), (p,q,true), P. auto.
  - destruct IH as [(Z & x & R & -> & HZ & Hx) | H].
    + left. exists ((p,q,false) :: Z), x, R. split; [reflexivity|].
      split; [constructor; [reflexivity|exact HZ] | exact Hx].
    + right. constructor; [reflexivity | exact H].
Qed.

Lemma Z_okL_V0 ph c4 h y : ph <> LX -> forall Z i, Forall dig0 (Z ++ [y]) ->
  AllI (PCx ph c4 h) i (Z ++ [y]) -> Forall okL Z.
Proof.
  intros Hph. induction Z as [|[[p q] d] Z IH]; intros i HZ HA; [constructor|].
  inversion HZ as [|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d.
  cbn [app AllI] in HA. destruct HA as [Hh HA]. constructor; [|eapply IH; eauto].
  cbn. split; [reflexivity|]. unfLh Hh. rewrite dv_zero in Hh by (constructor; [reflexivity | exact HZ']).
  eapply q2_V0; [exact Hh | rewrite length_app; cbn; lia | intros E; contradiction].
Qed.

Lemma lastOK_True Z : lastOK (fun _ => True) Z.
Proof. induction Z as [|[[p q] d] Z IH]; [exact I|]. destruct Z; [exact I | exact IH]. Qed.

Lemma Forall_snoc_inv (Pr : tri -> Prop) Z y : Forall Pr (Z ++ [y]) -> Forall Pr Z /\ Pr y.
Proof. intros H. apply Forall_app in H. destruct H as [H1 H2]. inversion H2. auto. Qed.

Lemma last_pc ph c4 h Z p q d : Forall dig0 (Z ++ [(p,q,d)]) -> AllI (PCx ph c4 h) 1 (Z ++ [(p,q,d)]) ->
  d = false /\ PC ph c4 h (1 + length Z) p q 0 0.
Proof.
  intros HZ HA. apply Forall_snoc_inv in HZ. destruct HZ as [_ Hd]. unfold dig0, dig in Hd. subst d.
  split; [reflexivity|]. pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hy _].
  unfLh Hy. exact Hy.
Qed.

Lemma first_pc ph c4 h p q d Z : Forall dig0 ((p,q,d) :: Z) -> AllI (PCx ph c4 h) 1 ((p,q,d) :: Z) ->
  d = false /\ PC ph c4 h 1 p q (length Z) 0 /\ Forall dig0 Z /\ AllI (PCx ph c4 h) 2 Z.
Proof.
  intros HZ [Hh HA]. inversion HZ as [|? ? Hd HZ']; subst. unfold dig0, dig in Hd. subst d.
  split; [reflexivity|]. unfLh Hh. rewrite dv_zero in Hh by (constructor; [reflexivity | exact HZ']).
  auto.
Qed.

Ltac pnc H := let H' := fresh in destruct H as (_ & _ & H' & _); unfold PN in H'; cbn - [Nat.modulo] in H'.

Lemma Jstep : forall s, J s -> exists s', Cf s -->+ Cf s' /\ J s'.
Proof.
  intros [h P T ph c4] (HP & HT & HA). unfold Cf. cbn [sh sP sT sph sc4] in *.
  destruct (split1 P) as [(Z & [[p q] d] & R & -> & HZ & Hd) | H0].
  - (* some digit is 1: a Dec-family step *)
    cbn in Hd. subst d.
    assert (HZL : Forall okL Z) by (apply (Z_okL ph c4 h Z 1 (p, q, true) R); [exact HZ | reflexivity | exact HA]).
    pose proof (AllI_app _ _ _ _ HA) as HB. cbn [AllI] in HB. destruct HB as [Hx HR].
    assert (Hx' := Hx). unfLh Hx'.
    destruct q as [|[|q]].
    + exfalso. destruct Hx' as (_ & Hq & _). lia.
    + destruct (borrow1 ph c4 h (1 + length Z) p (length R) (dv ((p, 1, true) :: R)))
        as (Hph & Hk & HL1 & HLX); [lia | cbn [dv bv]; lia | exact Hx' |].
      destruct R as [|[[p' q'] d'] R0].
      * destruct T as [|t|k].
        -- exfalso. destruct Hph as [-> | [-> | ->]].
           ++ destruct (HL1 eq_refl) as (Hn & _). cbn in Hn. lia.
           ++ destruct HT as (t & Ht & _). discriminate.
           ++ specialize (HLX eq_refl). cbn in HLX. lia.
        -- assert (ph = L2) as ->.
           { destruct Hph as [-> | [-> | ->]]; cbn in HT; try reflexivity;
               try discriminate; destruct HT; discriminate. }
           destruct HT as (t' & Ht & Ht2). injection Ht as <-.
           destruct (inv_MT c4 h Z p HZ HA) as [HA' Hlen].
           exists (mkst (4 + h) (map touch Z) (TA (p + t + 3)) L2 false). cbn [sh sP sT sph sc4]. split.
           ++ apply DecMergeTail. exact HZL.
           ++ split; [destruct Z; [cbn in Hlen; lia | discriminate]|].
              split; [exists (p + t + 3); split; [reflexivity | lia] | exact HA'].
        -- exfalso. destruct Hph as [-> | [-> | ->]]; cbn in HT;
             repeat match goal with H : _ /\ _ |- _ => destruct H | H : exists _, _ |- _ => destruct H end;
             discriminate.
      * exists (mkst (4 + h) (map touch Z ++ (p + p' + 3, q', d') :: R0) T ph c4). cbn [sh sP sT sph sc4].
        split.
        -- apply DecMerge. exact HZL.
        -- split; [destruct Z; discriminate|]. split; [exact HT|]. eapply inv_Merge; eauto.
    + exists (mkst (4 + h) (map touch Z ++ (S p, S q, false) :: R) T ph c4). cbn [sh sP sT sph sc4]. split.
      * apply Dec. exact HZL.
      * split; [destruct Z; discriminate|]. split; [exact HT|]. apply inv_Dec; assumption.
  - (* all digits 0 *)
    destruct ph.
    + (* E1: End *)
      destruct HT as [-> ->]. destruct (exists_last HP) as (Z & [[p q] d] & ->).
      destruct (last_pc _ _ _ _ _ _ _ H0 HA) as [-> Hy].
      assert (Hq : 2 <= q) by (pnc Hy; lia). destruct q as [|[|q]]; [lia|lia|].
      assert (HZL : Forall okL Z) by (eapply Z_okL_V0; [| exact H0 | exact HA]; discriminate).
      apply Forall_snoc_inv in H0. destruct H0 as [HZ _].
      exists (mkst (4 + h) (map touch Z ++ [(S p, S q, false)]) (TA 1) E2 false). cbn [sh sP sT sph sc4].
      split; [apply EndR; exact HZL|]. split; [apply snoc_nn|]. split; [split; reflexivity|].
      eapply inv_End; [left; split; reflexivity | exact HZ | exact HA].
    + (* E2: Ov *)
      destruct HT as [-> ->]. destruct P as [|[[p1 q1] d1] Z]; [congruence|].
      destruct (first_pc _ _ _ _ _ _ _ H0 HA) as (-> & Hh & HZ & HA2).
      assert (Hp1 := p1_V0 _ _ _ _ _ _ Hh ltac:(left; reflexivity)).
      destruct p1 as [|[|p1]]; [lia|lia|].
      destruct (AllI_okRO _ _ _ Z 2 HZ HA2) as [HR HO].
      assert (Hq1 : 1 <= q1) by (destruct Hh as (_ & Hq & _); exact Hq).
      destruct (lastOK_dec Z) as [HX | HX].
      * exists (mkst 2 ((h + 5, S p1, false) :: ovp q1 Z 1) TN LX false). cbn [sh sP sT sph sc4].
        split; [apply Ov; assumption|]. split; [discriminate|]. split; [split; reflexivity|].
        eapply (inv_Ov E2 LX false (fun x => x = 4)); [right; left; auto | discriminate | auto | exact HZ | exact HX | exact HA].
      * exists (mkst 2 ((h + 5, S p1, false) :: ovp q1 Z 1) TN L1 false). cbn [sh sP sT sph sc4].
        split; [apply Ov; assumption|]. split; [discriminate|]. split; [reflexivity|].
        eapply (inv_Ov E2 L1 false (fun x => x <> 4)); [left; auto | discriminate | auto | exact HZ | exact HX | exact HA].
    + (* E1t: End *)
      destruct HT as [-> ->]. destruct (exists_last HP) as (Z & [[p q] d] & ->).
      destruct (last_pc _ _ _ _ _ _ _ H0 HA) as [-> Hy].
      assert (Hq : 2 <= q) by (pnc Hy; lia). destruct q as [|[|q]]; [lia|lia|].
      assert (HZL : Forall okL Z) by (eapply Z_okL_V0; [| exact H0 | exact HA]; discriminate).
      apply Forall_snoc_inv in H0. destruct H0 as [HZ _].
      exists (mkst (4 + h) (map touch Z ++ [(S p, S q, false)]) (TA 1) E2t false). cbn [sh sP sT sph sc4].
      split; [apply EndR; exact HZL|]. split; [apply snoc_nn|]. split; [split; reflexivity|].
      eapply inv_End; [right; split; reflexivity | exact HZ | exact HA].
    + (* E2t: Ov to an L-slot after a T2 start *)
      destruct HT as [-> ->]. destruct P as [|[[p1 q1] d1] Z]; [congruence|].
      destruct (first_pc _ _ _ _ _ _ _ H0 HA) as (-> & Hh & HZ & HA2).
      assert (Hp1 := p1_V0 _ _ _ _ _ _ Hh ltac:(right; left; reflexivity)).
      destruct p1 as [|[|p1]]; [lia|lia|].
      destruct (AllI_okRO _ _ _ Z 2 HZ HA2) as [HR HO].
      assert (Hq1 : 1 <= q1) by (destruct Hh as (_ & Hq & _); exact Hq).
      exists (mkst 2 ((h + 5, S p1, false) :: ovp q1 Z 1) TN L1 true). cbn [sh sP sT sph sc4].
      split; [apply Ov; assumption|]. split; [discriminate|]. split; [reflexivity|].
      eapply (inv_Ov E2t L1 true (fun _ => True)); [right; right; left; auto | discriminate | auto | exact HZ | apply lastOK_True | exact HA].
    + (* T0: X2 *)
      destruct HT as [(k & -> & Hk) ->]. destruct (exists_last HP) as (Z & [[p q] d] & ->).
      destruct (last_pc _ _ _ _ _ _ _ H0 HA) as [-> Hy].
      assert (Hq : 2 <= q) by (pnc Hy; lia). destruct q as [|[|q]]; [lia|lia|].
      destruct k as [|k]; [lia|].
      assert (HZL : Forall okL Z) by (eapply Z_okL_V0; [| exact H0 | exact HA]; discriminate).
      apply Forall_snoc_inv in H0. destruct H0 as [HZ _].
      exists (mkst (4 + h) (map touch Z ++ [(S p, S q, false); (3, S k, true)]) TN E1t false).
      cbn [sh sP sT sph sc4].
      split; [apply X2; exact HZL|]. split; [destruct Z; discriminate|]. split; [split; reflexivity|].
      apply inv_X2; [exact HZ | lia | exact HA].
    + (* L1: EndLast *)
      cbn in HT. subst T. destruct (exists_last HP) as (Z & [[p q] d] & ->).
      destruct (last_pc _ _ _ _ _ _ _ H0 HA) as [-> Hy].
      assert (Hq : q = 1) by (pnc Hy; lia). subst q.
      assert (HZL : Forall okL Z) by (eapply Z_okL_V0; [| exact H0 | exact HA]; discriminate).
      apply Forall_snoc_inv in H0. destruct H0 as [HZ _].
      destruct (inv_EndLast c4 h Z p HZ HA) as [HA' Hlen].
      exists (mkst (4 + h) (map touch Z) (TA (p + 4)) L2 c4). cbn [sh sP sT sph sc4].
      split; [apply EndLast; exact HZL|]. split; [destruct Z; [cbn in Hlen; lia | discriminate]|].
      split; [exists (p + 4); split; [reflexivity | lia] | exact HA'].
    + (* L2: Ov *)
      destruct HT as (t & -> & Ht).
      destruct c4.
      { exfalso. destruct (exists_last HP) as (Z & [[p q] d] & ->).
        destruct (last_pc _ _ _ _ _ _ _ H0 HA) as [-> Hy]. exact (L2_c4_V0 _ _ _ _ Hy). }
      destruct P as [|[[p1 q1] d1] Z]; [congruence|].
      destruct (first_pc _ _ _ _ _ _ _ H0 HA) as (-> & Hh & HZ & HA2).
      assert (Hp1 := p1_V0 _ _ _ _ _ _ Hh ltac:(right; right; left; reflexivity)).
      destruct p1 as [|[|p1]]; [lia|lia|].
      destruct (AllI_okRO _ _ _ Z 2 HZ HA2) as [HR HO].
      assert (Hq1 : 1 <= q1) by (destruct Hh as (_ & Hq & _); exact Hq).
      exists (mkst 2 ((h + 5, S p1, false) :: ovp q1 Z t) TN E1 false). cbn [sh sP sT sph sc4].
      split; [apply Ov; assumption|]. split; [discriminate|]. split; [split; reflexivity|].
      eapply (inv_Ov L2 E1 false (fun _ => True)); [right; right; right; auto | intros _; exact Ht | intros E; congruence | exact HZ | apply lastOK_True | exact HA].
    + (* LX: X1 *)
      destruct HT as [-> ->].
      pose proof (AllI_len _ _ _ _ HP HA) as Hlen. cbn [minlen] in Hlen.
      destruct (exists_last HP) as (P1 & [[pb qb] db] & ->).
      assert (HP1 : P1 <> []) by (destruct P1; [cbn in Hlen; lia | discriminate]).
      destruct (exists_last HP1) as (P2 & [[pa qa] da] & ->).
      destruct P2 as [|[[p1 q1] d1] Z]; [cbn in Hlen; lia|].
      rewrite <- !app_assoc in H0, HA |- *. cbn [app] in H0, HA |- *.
      destruct (first_pc _ _ _ _ _ _ _ H0 HA) as (-> & Hh & HZab & HA2).
      apply Forall_app in HZab. destruct HZab as [HZ Hab].
      inversion Hab as [|? ? Hda Hab']; subst. inversion Hab' as [|? ? Hdb _]; subst.
      unfold dig0, dig in Hda, Hdb. subst da db.
      pose proof (AllI_app _ _ _ _ HA2) as HB. cbn [AllI] in HB. destruct HB as [Ha [Hb _]].
      unfLh Ha. unfLh Hb. cbn [length dv bv] in Ha, Hb.
      assert (Hqa : qa = 1) by (pnc Ha; lia). assert (Hqb : qb = 1) by (pnc Hb; lia). subst qa qb.
      assert (Hpa : 1 <= pa) by (destruct Ha as (Hp & _); exact Hp). destruct pa as [|pa]; [lia|].
      assert (Hp1 := p1_V0 _ _ _ _ _ _ Hh ltac:(right; right; right; reflexivity)).
      destruct p1 as [|[|p1]]; [lia|lia|].
      assert (HZab' : Forall dig0 (Z ++ [(S pa, 1, false); (pb, 1, false)]))
        by (apply Forall_app; split; [exact HZ | repeat constructor]).
      destruct (AllI_okRO _ _ _ _ 2 HZab' HA2) as [HR HO].
      apply Forall_app in HR. apply Forall_app in HO. destruct HR as [HR _]. destruct HO as [HO _].
      assert (Hq1 : 1 <= q1) by (destruct Hh as (_ & Hq & _); exact Hq).
      exists (mkst 2 ((h + 5, S p1, false) :: ovpX q1 Z (S pa)) (TB (pb + 3)) T0 false).
      cbn [sh sP sT sph sc4]. split; [apply X1; assumption|].
      split; [discriminate|]. split; [split; [exists (pb + 3); split; [reflexivity | lia] | reflexivity]|].
      eapply inv_X1; [exact HZ | exact HA].
Qed.

Lemma J_base : J (mkst 2 base TN E1 false).
Proof.
  unfold J, base. cbn [sh sP sT sph sc4]. split; [discriminate|]. split; [split; reflexivity|].
  cbn [AllI]. unfold PCx, Lift, PC, PN, PI. cbn. repeat split; lia.
Qed.

Lemma nonhalt : ~ halts tm c0.
Proof.
  apply multistep_nonhalt with (c' := K 2 base TN); [exact init|].
  change (K 2 base TN) with (Cf (mkst 2 base TN E1 false)).
  apply progress_nonhalt_cond with (P := J); [exact Jstep | exact J_base].
Qed.