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

Lemma drop_step L Re Rs nu X' :
  reach 100000 (Rc B (L, TV 0) (Re, T0)) (Lc D ([], TV 0) (Rs, T0)) = true ->
  ev_runs nu L X' {{B}}> evR nu Re -->+ X' <{{D}} evR nu Rs.
Proof. intros H. exact (reach_spec _ _ _ H nu (fun _ => X')). Qed.

Definition W5t (t : N) : N := (18701 + 149688 * t)%N.
Definition W5s (t : N) : N := (6227 + 49896 * t)%N.
Definition W5a (t : N) : N := (2069 + 16632 * t)%N.

Lemma rec_r5_ok : reach 100000 (Rc B ([(S0, cn 1); (S0, tl1 74806 598752)], TV 0) (Re_r5, T0)) (Lc D ([], TV 0) (Rs_r0, T0)) = true.
Proof. vm_compute. reflexivity. Qed.

Lemma step_r5 t f1 deep :
  chs (repeat D2 (S (length deep))) ([W5t t; W5s t; W5a t; f1] :: deep) (b1s PD2 (LWs 81)) {{B}}> evR [t] Re_r5 -->+
  Gc (repeat U0 (S (length deep)), P0, 0) ([W5s t; W5a t; f1; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r0).
Proof.
  pose proof (regroup ([W5t t; W5s t; W5a t; f1] :: deep) 0%N _ (b1s P0 (LWs 0)) regroup_b1) as E.
  cbn [length] in E. rewrite E. clear E. cbn [rtop rshift nth Gc].
  set (X' := chs (repeat U0 (S (length deep))) ([W5s t; W5a t; f1; rtop deep 0%N] :: rshift deep 0%N) (b1s P0 (LWs 0))).
  replace (2 + 4 * N.to_nat (W5t t)) with (ev [t] (tl1 74806 598752)) by (unfold ev, W5t, tl1; cbn [lc lv dot]; lia).
  change (alt S0 1 *> (alt S0 (ev [t] (tl1 74806 598752)) *> X')) with (ev_runs [t] [(S0, cn 1); (S0, tl1 74806 598752)] X').
  apply drop_step, rec_r5_ok.
Qed.

Lemma pow_K0 k0 e : 2 <= e -> 3 ^ (k0 + 2 * e) = 3 ^ (k0 + 4) * 9 ^ (e - 2).
Proof.
  intros He. replace (k0 + 2 * e) with ((k0 + 4) + 2 * (e - 2)) by lia.
  rewrite Nat.pow_add_r, Nat.pow_mul_r. reflexivity.
Qed.

(* one record interval of class r5 *)
Lemma S_r5 e t f1 deep : 2 <= e -> 1 + 8 * N.to_nat t = 9 ^ (e - 2) -> length deep = 1 + 2 * e ->
  Gc (repeat U0 (S (length deep)), P0, 0) ([W5t t; W5s t; W5a t; f1] :: deep) (evR [t] Rs_r5) -->+
  Gc (repeat U0 (S (length deep)), P0, 0) ([W5s t; W5a t; f1; rtop deep 0%N] :: rshift deep 0%N) (evR [t] Rs_r0).
Proof.
  intros He Ht Hl.
  eapply evstep_progress_trans; [apply interval_tm; [lia | reflexivity |]|].
  - intros T ET. pose proof (prog_check_spec _ _ _ _ _ int_r5 [t]) as HP.
    assert (E3 : 3 ^ S (S (S (length deep))) = 81 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (S (1 + 2 * e)))) with (4 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    assert (E2 : 3 ^ S (S (length deep)) = 27 * 81 * (1 + 8 * N.to_nat t)).
    { rewrite Ht, Hl. replace (S (S (1 + 2 * e))) with (3 + 2 * e) by lia.
      rewrite pow_K0 by exact He. reflexivity. }
    rewrite E3 in ET. rewrite E2.
    replace T with (ev [t] (tl1 3278 26244)) by (unfold ev, tl1; cbn [lc lv dot]; lia).
    replace (81 * (27 * 81 * (1 + 8 * N.to_nat t)) - 1 - ev [t] (tl1 3278 26244)) with (ev [t] (tl1 173868 1390932))
      by (unfold ev, tl1; cbn [lc lv dot]; lia).
    exact HP.
  - eapply progress_trans; [apply record_visit; reflexivity|].
    apply step_r5.
Qed.