/machines/1RB0RF_1RC0RB_1LD0RA_1LE0LD_1RB0LC_1LA---/rocq/regroup.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
Require Import ssim chain count right.
From BusyCoq Require Import Individual62.
Require Import Lia ZifyNat List Arith NArith ZArith.
Import ListNotations.

Open Scope nat_scope.

(* ===================================================================== *)
(* The regrouping after the record visit (write-up 6.2): the chain in D2 *)
(* is the same tape as a chain in U0 grouped one defect later.          *)
(* ===================================================================== *)

Definition rtop (qs : list (list N)) (z : N) : N :=
  match qs with [] => z | q :: _ => nth 0 q 0%N end.

Fixpoint rshift (qs : list (list N)) (z : N) : list (list N) :=
  match qs with
  | [] => []
  | q :: qs' => [nth 1 q 0; nth 2 q 0; nth 3 q 0; rtop qs' z]%N :: rshift qs' z
  end.

Lemma shift_len qs z : length (rshift qs z) = length qs.
Proof. induction qs; cbn; congruence. Qed.

Lemma dot4 (a b c d : N) q :
  dot [a; b; c; d] q = (a * nth 0 q 0 + b * nth 1 q 0 + c * nth 2 q 0 + d * nth 3 q 0)%N.
Proof. destruct q as [|x0 [|x1 [|x2 [|x3 q]]]]; cbn; lia. Qed.

Lemma alt_split b m k : Nat.eqb (m mod 2) 0 = true -> alt b (m + k) = alt b m ++ alt b k.
Proof.
  intros H. rewrite alt_add. unfold afterb_nat. rewrite H. reflexivity.
Qed.

Lemma ev_q nu c a : ev nu (LF c a) = N.to_nat (c + dot a nu).
Proof. reflexivity. Qed.

Lemma regroup qs : forall z X X',
  X = alt S0 1 *> (alt S0 (2 + 4 * N.to_nat z) *> X') ->
  chs (repeat D2 (length qs)) qs X =
    alt S0 1 *> (alt S0 (2 + 4 * N.to_nat (rtop qs z)) *> chs (repeat U0 (length qs)) (rshift qs z) X').
Proof.
  induction qs as [|q qs IH]; intros z X X' HX; [exact HX|].
  cbn [length repeat chs rshift rtop]. rewrite (IH z X X' HX).
  set (Y := chs (repeat U0 (length qs)) (rshift qs z) X').
  change (blk D2) with [(S0, cn 1); (S0, vt 5); (S0, vs 4); (S1, va 4); (S0, vl 0)]%N.
  change (blk U0) with [(S0, cn 3); (S0, vt 4); (S1, vs 4); (S0, va 1); (S0, vl 2)]%N.
  cbn [ev_runs]. unfold ev, vt, vs, va, vl, cn. cbn [lc lv]. rewrite !dot4. cbn [nth dot].
  set (xt := nth 0 q 0%N). set (xs := nth 1 q 0%N). set (xa := nth 2 q 0%N). set (xI := nth 3 q 0%N).
  set (tz := rtop qs z).
  assert (E1 : alt S0 (N.to_nat (5 + (4 * xt + 0 * xs + 0 * xa + 0 * xI))) = alt S0 (2 + 4 * N.to_nat xt) ++ alt S0 3).
  { replace (N.to_nat (5 + (4 * xt + 0 * xs + 0 * xa + 0 * xI))) with ((2 + 4 * N.to_nat xt) + 3) by lia.
    apply alt_split. apply Nat.eqb_eq. replace (2 + 4 * N.to_nat xt) with (2 + N.to_nat xt * 2 * 2) by lia.
    rewrite Nat.Div0.mod_add. reflexivity. }
  assert (E2 : alt S0 (N.to_nat (1 + (0 * xs + 0 * xa + 4 * xI + 0 * tz))) = alt S0 (N.to_nat (0 + (0 * xt + 0 * xs + 0 * xa + 4 * xI))) ++ alt S0 1).
  { replace (N.to_nat (1 + (0 * xs + 0 * xa + 4 * xI + 0 * tz))) with (N.to_nat (0 + (0 * xt + 0 * xs + 0 * xa + 4 * xI)) + 1) by lia.
    apply alt_split. apply Nat.eqb_eq. replace (N.to_nat (0 + (0 * xt + 0 * xs + 0 * xa + 4 * xI))) with (0 + N.to_nat xI * 2 * 2) by lia.
    rewrite Nat.Div0.mod_add. reflexivity. }
  rewrite E1, E2, !Str_app_assoc. cbn [alt Str_app app].
  replace (N.to_nat (2 + (0 * xs + 0 * xa + 0 * xI + 4 * tz))) with (2 + 4 * N.to_nat tz) by lia.
  replace (N.to_nat (4 + (4 * xs + 0 * xa + 0 * xI + 0 * tz))) with (N.to_nat (4 + (0 * xt + 4 * xs + 0 * xa + 0 * xI))) by lia.
  replace (N.to_nat (4 + (0 * xs + 4 * xa + 0 * xI + 0 * tz))) with (N.to_nat (4 + (0 * xt + 0 * xs + 4 * xa + 0 * xI))) by lia.
  reflexivity.
Qed.

(* block 1 and the left word after the left record, regrouped *)
Lemma regroup_b1 : b1s PD2 (LWs 81) = alt S0 1 *> (alt S0 (2 + 4 * N.to_nat 0) *> b1s P0 (LWs 0)).
Proof. reflexivity. Qed.