/machines/1RB0LD_1RC0RA_1RD1RF_1LA0LE_1RE1LD_0RB---/rocq/dv.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
(* Arithmetic layer for the per-step invariant J (round 1 start; standalone, no TM). *)
Require Import Arith Lia List Bool.
Import ListNotations.

Definition tri : Type := (nat * nat * bool)%type.
Definition bv (d : bool) : nat := if d then 1 else 0.

(** binary value of the digits, first pair least significant *)
Fixpoint dv (P : list tri) : nat :=
  match P with
  | [] => 0
  | (_,_,d) :: P' => bv d + 2 * dv P'
  end.

Definition touch (x : tri) : tri := let '(p,q,d) := x in (S p, pred q, negb d).
Definition dig (x : tri) : bool := let '(_,_,d) := x in d.

Lemma dv_lt P : dv P < 2 ^ length P.
Proof.
  induction P as [|[[p q] d] P IH]; cbn [dv length]; [cbn; lia|].
  rewrite Nat.pow_succ_r'. destruct d; cbn [bv]; lia.
Qed.

(** a decrement: Z all 0 (become 1), borrow digit 1 -> 0 *)
Lemma dv_dec Z x x' R : Forall (fun y => dig y = false) Z -> dig x = true -> dig x' = false ->
  dv (map touch Z ++ x' :: R) + 1 = dv (Z ++ x :: R).
Proof.
  intros HZ Hx Hx'. induction Z as [|[[p q] d] Z IH]; cbn [map app dv touch].
  - destruct x as [[p q] d], x' as [[p' q'] d']. cbn in Hx, Hx' |- *. subst. cbn. lia.
  - inversion HZ as [|? ? Hd HZ']; subst. cbn in Hd. subst d. cbn [negb bv].
    specialize (IH HZ'). lia.
Qed.

(** a merge at the borrow pair: the fused pair carries the next pair's digit *)
Lemma dv_merge Z x y y' R : Forall (fun y => dig y = false) Z -> dig x = true -> dig y' = dig y ->
  dv (map touch Z ++ y' :: R) + 1 + 2 ^ length Z * dv (y :: R) = dv (Z ++ x :: y :: R).
Proof.
  intros HZ Hx Hy. induction Z as [|[[p q] d] Z IH]; cbn [map app dv length touch].
  - destruct x as [[p q] d], y as [[p1 q1] d1], y' as [[p2 q2] d2]. cbn in Hx, Hy |- *. subst. cbn. lia.
  - inversion HZ as [|? ? Hd HZ']; subst. cbn in Hd. subst d. cbn [negb bv].
    specialize (IH HZ'). rewrite Nat.pow_succ_r'. cbn [dv] in IH |- *. nia.
Qed.

Lemma dv_ones n : dv (repeat (0, 0, true) n) = 2 ^ n - 1.
Proof.
  induction n as [|n IH]; cbn [repeat dv]; [reflexivity|].
  rewrite Nat.pow_succ_r'. pose proof (Nat.pow_nonzero 2 n). cbn [bv]. lia.
Qed.

(** every suffix satisfies Pr *)
Fixpoint AllSuf (Pr : list tri -> Prop) (P : list tri) : Prop :=
  match P with
  | [] => True
  | _ :: P' => Pr P /\ AllSuf Pr P'
  end.

Lemma AllSuf_app Pr Z R : AllSuf Pr (Z ++ R) -> AllSuf Pr R.
Proof. induction Z as [|x Z IH]; cbn; [auto | intros [_ H]; auto]. Qed.