/machines/1RB1LF_0RC0RB_0LD1LA_1LC0LE_0LA---_1LA1LF/rocq/t3_part.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
(** ** Iterates, shape lemmas *)

Inductive PAs : nat -> nat -> nat -> nat -> nat -> Prop :=
| PAs0 e o : PAs 0 e o e o
| PAsS j e o e1 o1 e2 o2 : PA e o e1 o1 -> PAs j e1 o1 e2 o2 -> PAs (S j) e o e2 o2.

Lemma PA_eq e o e' o' e2 o2 e2' o2':
  PA e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PA e2 o2 e2' o2'.
Proof. intros; subst; auto. Qed.

Lemma PF_eq e o e' o' e2 o2 e2' o2':
  PF e o e' o' -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PF e2 o2 e2' o2'.
Proof. intros; subst; auto. Qed.

Lemma PAs_eq j e o e' o' j2 e2 o2 e2' o2':
  PAs j e o e' o' -> j = j2 -> e = e2 -> o = o2 -> e' = e2' -> o' = o2' -> PAs j2 e2 o2 e2' o2'.
Proof. intros; subst; auto. Qed.

Lemma PAs_1 e o e' o': PA e o e' o' -> PAs 1 e o e' o'.
Proof. intros. econstructor; eauto. constructor. Qed.

Lemma PAs_trans j1 j2 e o e1 o1 e2 o2:
  PAs j1 e o e1 o1 -> PAs j2 e1 o1 e2 o2 -> PAs (j1+j2) e o e2 o2.
Proof.
  induction 1; intros; cbn; auto.
  econstructor; eauto.
Qed.

Lemma PAs_split j1 j2 e o e2 o2:
  PAs (j1+j2) e o e2 o2 -> exists e1 o1, PAs j1 e o e1 o1 /\ PAs j2 e1 o1 e2 o2.
Proof.
  gen e o. induction j1; intros e o H.
  - exists e, o. split; [constructor|auto].
  - cbn in H. inversion H; subst.
    destruct (IHj1 _ _ H2) as [e3 [o3 [H3 H4]]].
    exists e3, o3. split; auto. econstructor; eauto.
Qed.

Lemma PAs_dbl j e o e' o':
  PAs j e o e' o' -> PAs (2*j) (2*e) (2*o) (2*e') (2*o').
Proof.
  induction 1.
  - constructor.
  - replace (2 * S j) with (S (S (2*j))) by lia.
    econstructor. 1: apply PA0.
    econstructor. 1: apply PA1; eassumption.
    assumption.
Qed.

Lemma PAs_dbl1 j e o e' o':
  PAs (S j) e o e' o' -> PAs (2*j+1) (2*e+1) (2*o) (2*e') (2*o').
Proof.
  intros H. inversion H; subst.
  replace (2*j+1) with (S (2*j)) by lia.
  econstructor. 1: apply PA1; eassumption.
  apply PAs_dbl; assumption.
Qed.

(** ** Increments *)

Lemma INC_std N: PA N 0 (N+1) 0.
Proof.
  induction N as [N IH] using lt_wf_ind.
  destruct (Nat.Even_or_Odd N) as [[N' HN]|[N' HN]]; subst N.
  - eapply PA_eq. 1: apply (PA0 N' 0). all: lia.
  - eapply PA_eq. 1: apply (PA1 N' 0 (N'+1) 0), IH. all: lia.
Qed.

Lemma INC_stds j N: PAs j N 0 (N+j) 0.
Proof.
  gen N. induction j; intros N.
  - eapply PAs_eq. 1: apply PAs0. all: lia.
  - econstructor. 1: apply INC_std.
    eapply PAs_eq. 1: apply IHj. all: lia.
Qed.

Lemma PF_inc0 o: PF 0 o 0 (o+1).
Proof.
  induction o as [o IH] using lt_wf_ind.
  destruct (Nat.Even_or_Odd o) as [[o' Ho]|[o' Ho]]; subst o.
  - eapply PF_eq. 1: apply (PF0 0 o'). all: lia.
  - eapply PF_eq. 1: apply (PF1 0 o' 0 (o'+1)), IH. all: lia.
Qed.

Lemma Gap P: forall c E o1,
  c+1 < 2^(P+1) ->
  PA (c + 2^(P+1)*E) (2^P*(2*o1+1)) (c + 1 + 2^(P+1)*E) (2^P*(2*o1+1)).
Proof.
  induction P; intros c E o1 Hc.
  - cbn in *. eapply PA_eq. 1: apply (PA0 E (2*o1+1)). all: lia.
  - rewrite !Nat.pow_succ_r' in *.
    destruct (Nat.Even_or_Odd c) as [[c' Hc']|[c' Hc']]; subst c.
    + eapply PA_eq. 1: apply (PA0 (c' + 2^(P+1)*E) _). all: lia.
    + eapply PA_eq. 1: apply (PA1 (c' + 2^(P+1)*E) (2^P*(2*o1+1)) (c'+1+2^(P+1)*E) (2^P*(2*o1+1))), IH.
      all: lia.
Qed.

Lemma Gaps P j: forall c E o1,
  c+j < 2^(P+1) ->
  PAs j (c + 2^(P+1)*E) (2^P*(2*o1+1)) (c + j + 2^(P+1)*E) (2^P*(2*o1+1)).
Proof.
  induction j; intros c E o1 Hc.
  - eapply PAs_eq. 1: apply PAs0. all: lia.
  - econstructor. 1: apply Gap; lia.
    eapply PAs_eq. 1: apply (IHj (c+1)). all: lia.
Qed.

Lemma F_inc h: forall E o O,
  o + 1 < 2^h ->
  PF (2^h*E) (o + 2^h*O) (2^h*E) (o + 1 + 2^h*O).
Proof.
  induction h; intros E o O Ho.
  - cbn in Ho. lia.
  - rewrite !Nat.pow_succ_r' in *.
    destruct (Nat.Even_or_Odd o) as [[o' Ho']|[o' Ho']]; subst o.
    + eapply PF_eq. 1: apply (PF0 (2^h*E) (o' + 2^h*O)). all: lia.
    + eapply PF_eq. 1: apply (PF1 (2^h*E) (o' + 2^h*O) (2^h*E) (o'+1+2^h*O)), IH.
      all: lia.
Qed.

Lemma F_carry h: forall E O E' O',
  PF E O E' O' ->
  PF (2^h*E) (2^h - 1 + 2^h*O) (2^h*E') (2^h*O').
Proof.
  induction h; intros E O E' O' H.
  - cbn. eapply PF_eq. 1: apply H. all: lia.
  - rewrite !Nat.pow_succ_r' in *.
    pose proof (Nat.pow_nonzero 2 h).
    eapply PF_eq. 1: apply (PF1 (2^h*E) (2^h - 1 + 2^h*O) (2^h*E') (2^h*O')), IHh, H.
    all: lia.
Qed.