Built with Alectryon, running Coq+SerAPI v8.12.0+0.12.0. Coq sources are in this panel; goals and messages will appear in the other. Bubbles () indicate interactive fragments: hover for details, tap to reveal contents. Use Ctrl+↑ Ctrl+↓ to navigate, Ctrl+🖱️ to focus.

Require Import Arith.
Require Import RelationClasses.
Require Import List.
Require Import Helpers.

Set Implicit Arguments.

Disk model.

This file defines our model of a disk. We represent a disk as a list of 1KB blocks and provide functions to read and update disks, as well as theorems about these operations. In order to describe disks, we first provide a model of byte sequences.

Model of bytes.

In our lab assignments, we will model disks as consisting of blocks, which are in turn composed of bytes. Here, we define a notion of a byte array: the type of an array of n bytes will be bytes n.

There's one unusual aspect of how we model bytes: instead of defining the bytes type in Coq, we simply add it as an Axiom. This means we are not providing a Coq (Gallina) implementation of bytes, and instead we are telling Coq to assume that there exists something called bytes, and there exist other functions that manipulate bytes that we define here as well (like bytes_dec to decide if two byte arrays are equal).

When we generate executable code by extracting our Coq (Gallina) code into Haskell, we will be required to provide a Haskell implementation of any such Axiom. This correspondence is made below, using Extract Constant, and we (as developers) are responsible for making sure any axioms we state (like bsplit_bappend) are true of our Haskell implementations.

Axiom bytes : nat -> Type.

Axiom bytes_dec : forall n, EqualDec (bytes n).
Existing Instance bytes_dec.

Two "initial" byte values: an all-zero array, bytes0, and an all-ones array, bytes1. We also promise that all-zero and all-ones arrays are different, as long as there's at least one element.

Axiom bytes0 : forall n, bytes n.
Axiom bytes1 : forall n, bytes n.
Axiom bytes_differ : forall n, n > 0 -> bytes0 n <> bytes1 n.

Definition bnull : bytes 0 := bytes0 0.

Axiom bappend : forall n1 n2, bytes n1 -> bytes n2 -> bytes (n1+n2).
Axiom bsplit : forall n1 n2, bytes (n1+n2) -> bytes n1 * bytes n2.
Arguments bsplit {n1 n2} bs.

Axiom bsplit_bappend : forall n1 n2 (b1 : bytes n1) (b2 : bytes n2), bsplit (bappend b1 b2) = (b1, b2).

Fixpoint bsplit_list {n} {m} : bytes (n * m) -> list (bytes m) :=
  match n with
  | O => fun _ => nil
  | S n' => fun (bs : bytes ((S n') * m)) =>
    let (this, rest) := bsplit bs in
    this :: bsplit_list rest
  end.

Extraction Language Haskell.

Extract Constant bytes => "Data.ByteString.ByteString".
Extract Constant bytes_dec => "(\n b1 b2 -> b1 Prelude.== b2)".
Extract Constant bytes0 => "(\n -> Data.ByteString.replicate (Prelude.fromIntegral n) 0)".

Extract Constant bappend => "(\_ _ bs1 bs2 -> Data.ByteString.append bs1 bs2)".
Extract Constant bsplit => "(\n1 _ bs -> Data.ByteString.splitAt (Prelude.fromIntegral n1) bs)".

Model of blocks.

We represent blocks as a byte array of a fixed size.

We define the block size as a separate constant, blockbytes, to avoid the literal constant 1024 reducing performance of proofs.

Definition blockbytes := 1024.

Definition block := bytes blockbytes.
Definition block0 : block := bytes0 _.
Definition block1 : block := bytes1 _.

Theorem block0_block1_differ : block0 <> block1.block0 <> block1
Proof.block0 <> block1
  apply bytes_differ.blockbytes > 0
  unfold blockbytes.1024 > 0
  lia.
Qed.

Hint Resolve block0_block1_differ : core.

Mark blockbytes as opaque so that Coq doesn't expand it too eagerly.

Opaque blockbytes.

Disk as a list of blocks.

Now we can define our model of a disk: a list of blocks. A disk with zero blocks is an empty list, nil.

Definition disk := list block.

Definition empty_disk : disk := nil.

We define three main operations on disks:

diskGet d a gets the contents of an address a in disk d. It returns an option block, which is either a block value b (represented by Some b), or None if a is past the end of the disk.
diskSize returns the size of the disk, which is just the length of the list representing the disk.
diskUpd writes to a disk. Since Gallina is a functional language, we cannot update a disk "in-place", so instead diskUpd returns a new disk reflecting the write. Specifically, diskUpd d a b returns a new disk with address a updated to block value b, if a is in-bounds, or the original disk unchanged if a is out-of-bounds.

We address into disks with addr, which is simply a nat.

Definition addr := nat.

Definition diskGet (d : disk) (a : addr) : option block :=
  nth_error d a.

Definition diskSize (d : disk) : nat := length d.

Fixpoint diskUpd d (a: addr) b : disk :=
  match d with
  | nil => nil
  | db :: drest =>
    match a with
    | O => b :: drest
    | S a' => db :: diskUpd drest a' b
    end
  end.

We define another helper operation, diskShrink, which takes a disk and drops the last block. This will be helpful in the bad-block-remapping lab assignment.

Definition diskShrink (d : disk) : disk :=
  firstn (length d - 1) d.

We also define variants of diskGet and diskUpd that operate on multiple blocks at a time. These may be helpful in the logging lab assignment, but not required in any sense.

Fixpoint diskGets (d : disk) (a : addr) (count : nat) : list (option block) :=
  match count with
  | O =>
    nil
  | S count' =>
    diskGet d a :: diskGets d (a+1) count'
  end.

Fixpoint diskUpds (d : disk) (a : addr) (blocks : list block) : disk :=
  match blocks with
  | nil =>
    d
  | b :: blocks' =>
    diskUpd (diskUpds d (a+1) blocks') a b
  end.

Finally, we prove a variety of theorems about the behavior of these disk operations.

Theorems about diskGet

Theorem disk_inbounds_exists : forall a d,
    a < diskSize d ->
    exists b, diskGet d a = Some b.forall (a : nat) (d : disk),
a < diskSize d ->
exists b : block, diskGet d a = Some b
Proof.forall (a : nat) (d : disk),
a < diskSize d ->
exists b : block, diskGet d a = Some b
  unfold diskSize.forall (a : nat) (d : disk),
a < length d -> exists b : block, diskGet d a = Some b
  intros.a:nat
d:disk
H:a < length d
exists b : block, diskGet d a = Some b
  case_eq (diskGet d a); intros; eauto.a:nat
d:disk
H:a < length d
H0:diskGet d a = None
exists b : block, None = Some b
  apply nth_error_None in H0.a:nat
d:disk
H:a < length d
H0:length d <= a
exists b : block, None = Some b
  lia.
Qed.

Theorem disk_inbounds_not_none : forall a d,
    a < diskSize d ->
    diskGet d a = None ->
    False.forall (a : nat) (d : disk),
a < diskSize d -> diskGet d a = None -> False
Proof.forall (a : nat) (d : disk),
a < diskSize d -> diskGet d a = None -> False
  unfold diskSize.forall (a : nat) (d : disk),
a < length d -> diskGet d a = None -> False
  intros.a:nat
d:disk
H:a < length d
H0:diskGet d a = None
False
  apply nth_error_None in H0.a:nat
d:disk
H:a < length d
H0:length d <= a
False
  lia.
Qed.

Theorem disk_none_oob : forall a d,
    diskGet d a = None ->
    ~a < diskSize d.forall (a : addr) (d : disk),
diskGet d a = None -> ~ a < diskSize d
Proof.forall (a : addr) (d : disk),
diskGet d a = None -> ~ a < diskSize d
  intros.a:addr
d:disk
H:diskGet d a = None
~ a < diskSize d
  destruct (lt_dec a (diskSize d)); eauto.a:addr
d:disk
H:diskGet d a = None
l:a < diskSize d
~ a < diskSize d
  exfalso; eapply disk_inbounds_not_none; eauto.
Qed.

Theorem disk_oob_eq : forall d a,
    ~a < diskSize d ->
    diskGet d a = None.forall (d : disk) (a : nat),
~ a < diskSize d -> diskGet d a = None
Proof.forall (d : disk) (a : nat),
~ a < diskSize d -> diskGet d a = None
  unfold diskSize.forall (d : disk) (a : nat),
~ a < length d -> diskGet d a = None
  induction d; simpl; intros.a:nat
H:~ a < 0
diskGet nil a = None
a:block
d:list block
IHd:forall a : nat, ~ a < length d -> diskGet d a = None
a0:nat
H:~ a0 < S (length d)
diskGet (a :: d) a0 = None
  -a:nat
H:~ a < 0
diskGet nil a = None induction a; eauto.
  -a:block
d:list block
IHd:forall a : nat, ~ a < length d -> diskGet d a = None
a0:nat
H:~ a0 < S (length d)
diskGet (a :: d) a0 = None destruct a0; simpl.a:block
d:list block
IHd:forall a : nat, ~ a < length d -> diskGet d a = None
H:~ 0 < S (length d)
Some a = None
a:block
d:list block
IHd:forall a : nat, ~ a < length d -> diskGet d a = None
a0:nat
H:~ S a0 < S (length d)
diskGet d a0 = None
    +a:block
d:list block
IHd:forall a : nat, ~ a < length d -> diskGet d a = None
H:~ 0 < S (length d)
Some a = None lia.
    +a:block
d:list block
IHd:forall a : nat, ~ a < length d -> diskGet d a = None
a0:nat
H:~ S a0 < S (length d)
diskGet d a0 = None eapply IHd.a:block
d:list block
IHd:forall a : nat, ~ a < length d -> diskGet d a = None
a0:nat
H:~ S a0 < S (length d)
~ a0 < length d lia.
Qed.

(* this rule allows autorewrite to simplify maybe_eq *)
Theorem maybe_eq_None_is_True T (v:T) :
  maybe_eq None v = True.T:Type
v:T
None =?= v = True
Proof.T:Type
v:T
None =?= v = True
  reflexivity.
Qed.

Hint Rewrite maybe_eq_None_is_True : upd.

Theorem maybe_eq_None_holds T (v:T) : maybe_eq None v.T:Type
v:T
None =?= v
Proof.T:Type
v:T
None =?= v
  exact I.
Qed.

Hint Resolve maybe_eq_None_holds : core.

Theorem nth_error_ext_eq A : forall (l1 l2: list A),
    (forall a, nth_error l1 a = nth_error l2 a) ->
    l1 = l2.A:Type
forall l1 l2 : list A,
(forall a : nat, nth_error l1 a = nth_error l2 a) ->
l1 = l2
Proof.A:Type
forall l1 l2 : list A,
(forall a : nat, nth_error l1 a = nth_error l2 a) ->
l1 = l2
  induction l1; simpl; intros.A:Type
l2:list A
H:forall a : nat, nth_error nil a = nth_error l2 a
nil = l2
A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
l2:list A
H:forall a0 : nat,
nth_error (a :: l1) a0 = nth_error l2 a0
a :: l1 = l2
  -A:Type
l2:list A
H:forall a : nat, nth_error nil a = nth_error l2 a
nil = l2 destruct l2; simpl; intros; eauto.A:Type
a:A
l2:list A
H:forall a0 : nat,
nth_error nil a0 = nth_error (a :: l2) a0
nil = a :: l2
    specialize (H 0); simpl in *.A:Type
a:A
l2:list A
H:None = Some a
nil = a :: l2
    congruence.
  -A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
l2:list A
H:forall a0 : nat,
nth_error (a :: l1) a0 = nth_error l2 a0
a :: l1 = l2 destruct l2; simpl; intros.A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
H:forall a0 : nat,
nth_error (a :: l1) a0 = nth_error nil a0
a :: l1 = nil
A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
a0:A
l2:list A
H:forall a1 : nat,
nth_error (a :: l1) a1 = nth_error (a0 :: l2) a1
a :: l1 = a0 :: l2
    +A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
H:forall a0 : nat,
nth_error (a :: l1) a0 = nth_error nil a0
a :: l1 = nil specialize (H 0); simpl in *.A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
H:Some a = None
a :: l1 = nil
      congruence.
    +A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
a0:A
l2:list A
H:forall a1 : nat,
nth_error (a :: l1) a1 = nth_error (a0 :: l2) a1
a :: l1 = a0 :: l2 specialize (H 0) as H'; simpl in H'.A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
a0:A
l2:list A
H:forall a1 : nat,
nth_error (a :: l1) a1 = nth_error (a0 :: l2) a1
H':Some a = Some a0
a :: l1 = a0 :: l2
      f_equal; try congruence.A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
a0:A
l2:list A
H:forall a1 : nat,
nth_error (a :: l1) a1 = nth_error (a0 :: l2) a1
H':Some a = Some a0
l1 = l2
      eapply IHl1; intros.A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
a0:A
l2:list A
H:forall a1 : nat,
nth_error (a :: l1) a1 = nth_error (a0 :: l2) a1
H':Some a = Some a0
a1:nat
nth_error l1 a1 = nth_error l2 a1
      specialize (H (S a1)); simpl in H.A:Type
a:A
l1:list A
IHl1:forall l2 : list A,
(forall a : nat,
 nth_error l1 a = nth_error l2 a) -> 
l1 = l2
a0:A
l2:list A
a1:nat
H:nth_error l1 a1 = nth_error l2 a1
H':Some a = Some a0
nth_error l1 a1 = nth_error l2 a1
      eauto.
Qed.

Theorem nth_error_ext_inbounds_eq A : forall (l1 l2: list A),
    length l1 = length l2 ->
    (forall a, a < length l1 -> nth_error l1 a = nth_error l2 a) ->
    l1 = l2.A:Type
forall l1 l2 : list A,
length l1 = length l2 ->
(forall a : nat,
 a < length l1 -> nth_error l1 a = nth_error l2 a) ->
l1 = l2
Proof.A:Type
forall l1 l2 : list A,
length l1 = length l2 ->
(forall a : nat,
 a < length l1 -> nth_error l1 a = nth_error l2 a) ->
l1 = l2
  intros.A:Type
l1, l2:list A
H:length l1 = length l2
H0:forall a : nat,
a < length l1 -> nth_error l1 a = nth_error l2 a
l1 = l2
  apply nth_error_ext_eq; intros.A:Type
l1, l2:list A
H:length l1 = length l2
H0:forall a : nat,
a < length l1 -> nth_error l1 a = nth_error l2 a
a:nat
nth_error l1 a = nth_error l2 a
  destruct (lt_dec a (length l1)); eauto.A:Type
l1, l2:list A
H:length l1 = length l2
H0:forall a : nat,
a < length l1 -> nth_error l1 a = nth_error l2 a
a:nat
n:~ a < length l1
nth_error l1 a = nth_error l2 a
  Search nth_error.H0:
  forall a : nat,
  a < length l1 -> nth_error l1 a = nth_error l2 a
nth_error_ext_eq:
  forall [A : Type] (l1 l2 : list A),
  (forall a : nat, nth_error l1 a = nth_error l2 a) ->
  l1 = l2
nth_error_In:
  forall [A : Type] (l : list A) (n : nat) [x : A],
  nth_error l n = Some x -> In x l
In_nth_error:
  forall [A : Type] (l : list A) (x : A),
  In x l -> exists n : nat, nth_error l n = Some x
nth_error_None:
  forall [A : Type] (l : list A) (n : nat),
  nth_error l n = None <-> length l <= n
nth_error_nth:
  forall [A : Type] (l : list A) (n : nat) [x : A]
    (d : A), nth_error l n = Some x -> nth n l d = x
nth_error_Some:
  forall [A : Type] (l : list A) (n : nat),
  nth_error l n <> None <-> n < length l
nth_error_app1:
  forall [A : Type] (l l' : list A) [n : nat],
  n < length l ->
  nth_error (l ++ l') n = nth_error l n
nth_error_nth':
  forall [A : Type] (l : list A) [n : nat] (d : A),
  n < length l -> nth_error l n = Some (nth n l d)
nth_error_app2:
  forall [A : Type] (l l' : list A) [n : nat],
  length l <= n ->
  nth_error (l ++ l') n = nth_error l' (n - length l)
NoDup_nth_error:
  forall [A : Type] (l : list A),
  NoDup l <->
  (forall i j : nat,
   i < length l ->
   nth_error l i = nth_error l j -> i = j)
map_nth_error:
  forall [A B : Type] (f : A -> B) (n : nat)
    (l : list A) [d : A],
  nth_error l n = Some d ->
  nth_error (map f l) n = Some (f d)
nth_error_split:
  forall [A : Type] (l : list A) (n : nat) [a : A],
  nth_error l n = Some a ->
  exists l1 l2 : list A,
    l = l1 ++ a :: l2 /\ length l1 = n
A:Type
l1, l2:list A
H:length l1 = length l2
H0:forall a : nat,
a < length l1 -> nth_error l1 a = nth_error l2 a
a:nat
n:~ a < length l1
nth_error l1 a = nth_error l2 a
  assert (nth_error l1 a = None).A:Type
l1, l2:list A
H:length l1 = length l2
H0:forall a : nat,
a < length l1 -> nth_error l1 a = nth_error l2 a
a:nat
n:~ a < length l1
nth_error l1 a = None
A:Type
l1, l2:list A
H:length l1 = length l2
H0:forall a : nat,
a < length l1 -> nth_error l1 a = nth_error l2 a
a:nat
n:~ a < length l1
H1:nth_error l1 a = None
nth_error l1 a = nth_error l2 a
  apply nth_error_None; lia.A:Type
l1, l2:list A
H:length l1 = length l2
H0:forall a : nat,
a < length l1 -> nth_error l1 a = nth_error l2 a
a:nat
n:~ a < length l1
H1:nth_error l1 a = None
nth_error l1 a = nth_error l2 a
  assert (nth_error l2 a = None).A:Type
l1, l2:list A
H:length l1 = length l2
H0:forall a : nat,
a < length l1 -> nth_error l1 a = nth_error l2 a
a:nat
n:~ a < length l1
H1:nth_error l1 a = None
nth_error l2 a = None
A:Type
l1, l2:list A
H:length l1 = length l2
H0:forall a : nat,
a < length l1 -> nth_error l1 a = nth_error l2 a
a:nat
n:~ a < length l1
H1:nth_error l1 a = None
H2:nth_error l2 a = None
nth_error l1 a = nth_error l2 a
  apply nth_error_None; lia.A:Type
l1, l2:list A
H:length l1 = length l2
H0:forall a : nat,
a < length l1 -> nth_error l1 a = nth_error l2 a
a:nat
n:~ a < length l1
H1:nth_error l1 a = None
H2:nth_error l2 a = None
nth_error l1 a = nth_error l2 a
  congruence.
Qed.

Theorem disk_ext_eq : forall d d',
    (forall a, diskGet d a = diskGet d' a) ->
    d = d'.forall d d' : disk,
(forall a : addr, diskGet d a = diskGet d' a) ->
d = d'
Proof.forall d d' : disk,
(forall a : addr, diskGet d a = diskGet d' a) ->
d = d'
  intros.d, d':disk
H:forall a : addr, diskGet d a = diskGet d' a
d = d'
  apply nth_error_ext_eq; auto.
Qed.

Theorem disk_ext_inbounds_eq : forall d d',
    diskSize d = diskSize d' ->
    (forall a, a < diskSize d -> diskGet d a = diskGet d' a) ->
    d = d'.forall d d' : disk,
diskSize d = diskSize d' ->
(forall a : nat,
 a < diskSize d -> diskGet d a = diskGet d' a) ->
d = d'
Proof.forall d d' : disk,
diskSize d = diskSize d' ->
(forall a : nat,
 a < diskSize d -> diskGet d a = diskGet d' a) ->
d = d'
  intros.d, d':disk
H:diskSize d = diskSize d'
H0:forall a : nat,
a < diskSize d -> diskGet d a = diskGet d' a
d = d'
  apply nth_error_ext_inbounds_eq; auto.
Qed.

Theorems about diskUpd

Theorem diskUpd_eq_some : forall d a b0 b,
    diskGet d a = Some b0 ->
    diskGet (diskUpd d a b) a = Some b.forall (d : disk) (a : addr) (b0 b : block),
diskGet d a = Some b0 ->
diskGet (diskUpd d a b) a = Some b
Proof.forall (d : disk) (a : addr) (b0 b : block),
diskGet d a = Some b0 ->
diskGet (diskUpd d a b) a = Some b
  induction d; simpl; eauto.forall (a : addr) (b0 b : block),
diskGet nil a = Some b0 -> diskGet nil a = Some b
a:block
d:list block
IHd:forall (a : addr) (b0 b : block),
diskGet d a = Some b0 -> diskGet (diskUpd d a b) a = Some b
forall (a0 : addr) (b0 b : block),
diskGet (a :: d) a0 = Some b0 ->
diskGet
  match a0 with
  | 0 => b :: d
  | S a' => a :: diskUpd d a' b
  end a0 = Some b
  -forall (a : addr) (b0 b : block),
diskGet nil a = Some b0 -> diskGet nil a = Some b destruct a; simpl; intros; congruence.
  -a:block
d:list block
IHd:forall (a : addr) (b0 b : block),
diskGet d a = Some b0 -> diskGet (diskUpd d a b) a = Some b
forall (a0 : addr) (b0 b : block),
diskGet (a :: d) a0 = Some b0 ->
diskGet
  match a0 with
  | 0 => b :: d
  | S a' => a :: diskUpd d a' b
  end a0 = Some b destruct a0; simpl; intros; eauto.
Qed.

Theorem diskUpd_eq : forall d a b,
    a < diskSize d ->
    diskGet (diskUpd d a b) a = Some b.forall (d : disk) (a : nat) (b : block),
a < diskSize d -> diskGet (diskUpd d a b) a = Some b
Proof.forall (d : disk) (a : nat) (b : block),
a < diskSize d -> diskGet (diskUpd d a b) a = Some b
  intros.d:disk
a:nat
b:block
H:a < diskSize d
diskGet (diskUpd d a b) a = Some b
  apply disk_inbounds_exists in H; deex.d:disk
a:nat
b, b0:block
H:diskGet d a = Some b0
diskGet (diskUpd d a b) a = Some b
  eauto using diskUpd_eq_some.
Qed.

Theorem diskUpd_size : forall d a b,
    diskSize (diskUpd d a b) = diskSize d.forall (d : list block) (a : addr) (b : block),
diskSize (diskUpd d a b) = diskSize d
Proof.forall (d : list block) (a : addr) (b : block),
diskSize (diskUpd d a b) = diskSize d
  induction d; simpl; eauto.a:block
d:list block
IHd:forall (a : addr) (b : block), diskSize (diskUpd d a b) = diskSize d
forall (a0 : addr) (b : block),
diskSize
  match a0 with
  | 0 => b :: d
  | S a' => a :: diskUpd d a' b
  end = S (diskSize d)
  destruct a0; simpl; intros; eauto.
Qed.

Theorem diskUpd_oob_eq : forall d a b,
    ~a < diskSize d ->
    diskGet (diskUpd d a b) a = None.forall (d : disk) (a : nat) (b : block),
~ a < diskSize d -> diskGet (diskUpd d a b) a = None
Proof.forall (d : disk) (a : nat) (b : block),
~ a < diskSize d -> diskGet (diskUpd d a b) a = None
  intros.d:disk
a:nat
b:block
H:~ a < diskSize d
diskGet (diskUpd d a b) a = None
  apply disk_oob_eq.d:disk
a:nat
b:block
H:~ a < diskSize d
~ a < diskSize (diskUpd d a b)
  rewrite diskUpd_size; auto.
Qed.

Theorem diskUpd_neq : forall d a b a',
    a <> a' ->
    diskGet (diskUpd d a b) a' = diskGet d a'.forall (d : list block) (a : addr) (b : block)
  (a' : addr),
a <> a' -> diskGet (diskUpd d a b) a' = diskGet d a'
Proof.forall (d : list block) (a : addr) (b : block)
  (a' : addr),
a <> a' -> diskGet (diskUpd d a b) a' = diskGet d a'
  induction d; simpl; intros; auto.a:block
d:list block
IHd:forall (a : addr) (b : block) (a' : addr),
a <> a' -> diskGet (diskUpd d a b) a' = diskGet d a'
a0:addr
b:block
a':addr
H:a0 <> a'
diskGet
  match a0 with
  | 0 => b :: d
  | S a' => a :: diskUpd d a' b
  end a' = diskGet (a :: d) a'
  destruct a0; simpl.a:block
d:list block
IHd:forall (a : addr) (b : block) (a' : addr),
a <> a' -> diskGet (diskUpd d a b) a' = diskGet d a'
b:block
a':addr
H:0 <> a'
diskGet (b :: d) a' = diskGet (a :: d) a'
a:block
d:list block
IHd:forall (a : addr) (b : block) (a' : addr),
a <> a' -> diskGet (diskUpd d a b) a' = diskGet d a'
a0:nat
b:block
a':addr
H:S a0 <> a'
diskGet (a :: diskUpd d a0 b) a' = diskGet (a :: d) a'
  -a:block
d:list block
IHd:forall (a : addr) (b : block) (a' : addr),
a <> a' -> diskGet (diskUpd d a b) a' = diskGet d a'
b:block
a':addr
H:0 <> a'
diskGet (b :: d) a' = diskGet (a :: d) a' destruct a'; simpl; try lia; auto.
  -a:block
d:list block
IHd:forall (a : addr) (b : block) (a' : addr),
a <> a' -> diskGet (diskUpd d a b) a' = diskGet d a'
a0:nat
b:block
a':addr
H:S a0 <> a'
diskGet (a :: diskUpd d a0 b) a' = diskGet (a :: d) a' destruct a'; simpl; auto.
Qed.

Theorem diskUpd_none : forall d a b,
    diskGet d a = None ->
    diskUpd d a b = d.forall (d : disk) (a : addr) (b : block),
diskGet d a = None -> diskUpd d a b = d
Proof.forall (d : disk) (a : addr) (b : block),
diskGet d a = None -> diskUpd d a b = d
  induction d; simpl; intros; auto.a:block
d:list block
IHd:forall (a : addr) (b : block), diskGet d a = None -> diskUpd d a b = d
a0:addr
b:block
H:diskGet (a :: d) a0 = None
match a0 with
| 0 => b :: d
| S a' => a :: diskUpd d a' b
end = a :: d
  destruct a0; simpl in *; try congruence.a:block
d:list block
IHd:forall (a : addr) (b : block), diskGet d a = None -> diskUpd d a b = d
a0:nat
b:block
H:diskGet d a0 = None
a :: diskUpd d a0 b = a :: d
  rewrite IHd; eauto.
Qed.

Theorem diskUpd_same : forall d a b,
    diskGet d a = Some b ->
    diskUpd d a b = d.forall (d : disk) (a : addr) (b : block),
diskGet d a = Some b -> diskUpd d a b = d
Proof.forall (d : disk) (a : addr) (b : block),
diskGet d a = Some b -> diskUpd d a b = d
  induction d; simpl; intros; auto.a:block
d:list block
IHd:forall (a : addr) (b : block), diskGet d a = Some b -> diskUpd d a b = d
a0:addr
b:block
H:diskGet (a :: d) a0 = Some b
match a0 with
| 0 => b :: d
| S a' => a :: diskUpd d a' b
end = a :: d
  destruct a0; simpl in *.a:block
d:list block
IHd:forall (a : addr) (b : block), diskGet d a = Some b -> diskUpd d a b = d
b:block
H:Some a = Some b
b :: d = a :: d
a:block
d:list block
IHd:forall (a : addr) (b : block), diskGet d a = Some b -> diskUpd d a b = d
a0:nat
b:block
H:diskGet d a0 = Some b
a :: diskUpd d a0 b = a :: d
  -a:block
d:list block
IHd:forall (a : addr) (b : block), diskGet d a = Some b -> diskUpd d a b = d
b:block
H:Some a = Some b
b :: d = a :: d congruence.
  -a:block
d:list block
IHd:forall (a : addr) (b : block), diskGet d a = Some b -> diskUpd d a b = d
a0:nat
b:block
H:diskGet d a0 = Some b
a :: diskUpd d a0 b = a :: d rewrite IHd; eauto.
Qed.

Theorem diskUpd_twice : forall d a b b',
    diskUpd (diskUpd d a b) a b' = diskUpd d a b'.forall (d : list block) (a : addr) (b b' : block),
diskUpd (diskUpd d a b) a b' = diskUpd d a b'
Proof.forall (d : list block) (a : addr) (b b' : block),
diskUpd (diskUpd d a b) a b' = diskUpd d a b'
  induction d; simpl; intros; auto.a:block
d:list block
IHd:forall (a : addr) (b b' : block),
diskUpd (diskUpd d a b) a b' = diskUpd d a b'
a0:addr
b, b':block
diskUpd
  match a0 with
  | 0 => b :: d
  | S a' => a :: diskUpd d a' b
  end a0 b' =
match a0 with
| 0 => b' :: d
| S a' => a :: diskUpd d a' b'
end
  destruct a0; simpl in *.a:block
d:list block
IHd:forall (a : addr) (b b' : block),
diskUpd (diskUpd d a b) a b' = diskUpd d a b'
b, b':block
b' :: d = b' :: d
a:block
d:list block
IHd:forall (a : addr) (b b' : block),
diskUpd (diskUpd d a b) a b' = diskUpd d a b'
a0:nat
b, b':block
a :: diskUpd (diskUpd d a0 b) a0 b' =
a :: diskUpd d a0 b'
  -a:block
d:list block
IHd:forall (a : addr) (b b' : block),
diskUpd (diskUpd d a b) a b' = diskUpd d a b'
b, b':block
b' :: d = b' :: d congruence.
  -a:block
d:list block
IHd:forall (a : addr) (b b' : block),
diskUpd (diskUpd d a b) a b' = diskUpd d a b'
a0:nat
b, b':block
a :: diskUpd (diskUpd d a0 b) a0 b' =
a :: diskUpd d a0 b' rewrite IHd; eauto.
Qed.

Theorem diskUpd_comm : forall d a a' b b',
    a <> a' ->
    diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b.forall (d : list block) (a a' : addr) (b b' : block),
a <> a' ->
diskUpd (diskUpd d a b) a' b' =
diskUpd (diskUpd d a' b') a b
Proof.forall (d : list block) (a a' : addr) (b b' : block),
a <> a' ->
diskUpd (diskUpd d a b) a' b' =
diskUpd (diskUpd d a' b') a b
  induction d; simpl; intros; auto.a:block
d:list block
IHd:forall (a a' : addr) (b b' : block),
a <> a' -> diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b
a0, a':addr
b, b':block
H:a0 <> a'
diskUpd
  match a0 with
  | 0 => b :: d
  | S a' => a :: diskUpd d a' b
  end a' b' =
diskUpd
  match a' with
  | 0 => b' :: d
  | S a' => a :: diskUpd d a' b'
  end a0 b
  destruct a0; destruct a'; simpl in *.a:block
d:list block
IHd:forall (a a' : addr) (b b' : block),
a <> a' -> diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b
b, b':block
H:0 <> 0
b' :: d = b :: d
a:block
d:list block
IHd:forall (a a' : addr) (b b' : block),
a <> a' -> diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b
a':nat
b, b':block
H:0 <> S a'
b :: diskUpd d a' b' = b :: diskUpd d a' b'
a:block
d:list block
IHd:forall (a a' : addr) (b b' : block),
a <> a' -> diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b
a0:nat
b, b':block
H:S a0 <> 0
b' :: diskUpd d a0 b = b' :: diskUpd d a0 b
a:block
d:list block
IHd:forall (a a' : addr) (b b' : block),
a <> a' -> diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b
a0, a':nat
b, b':block
H:S a0 <> S a'
a :: diskUpd (diskUpd d a0 b) a' b' =
a :: diskUpd (diskUpd d a' b') a0 b
  -a:block
d:list block
IHd:forall (a a' : addr) (b b' : block),
a <> a' -> diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b
b, b':block
H:0 <> 0
b' :: d = b :: d lia.
  -a:block
d:list block
IHd:forall (a a' : addr) (b b' : block),
a <> a' -> diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b
a':nat
b, b':block
H:0 <> S a'
b :: diskUpd d a' b' = b :: diskUpd d a' b' congruence.
  -a:block
d:list block
IHd:forall (a a' : addr) (b b' : block),
a <> a' -> diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b
a0:nat
b, b':block
H:S a0 <> 0
b' :: diskUpd d a0 b = b' :: diskUpd d a0 b congruence.
  -a:block
d:list block
IHd:forall (a a' : addr) (b b' : block),
a <> a' -> diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b
a0, a':nat
b, b':block
H:S a0 <> S a'
a :: diskUpd (diskUpd d a0 b) a' b' =
a :: diskUpd (diskUpd d a' b') a0 b rewrite IHd; eauto.
Qed.

Theorem diskUpd_comm_lt : forall d a a' b b',
    a < a' ->
    diskUpd (diskUpd d a b) a' b' = diskUpd (diskUpd d a' b') a b.forall (d : list block) (a a' : nat) (b b' : block),
a < a' ->
diskUpd (diskUpd d a b) a' b' =
diskUpd (diskUpd d a' b') a b
Proof.forall (d : list block) (a a' : nat) (b b' : block),
a < a' ->
diskUpd (diskUpd d a b) a' b' =
diskUpd (diskUpd d a' b') a b
  intros.d:list block
a, a':nat
b, b':block
H:a < a'
diskUpd (diskUpd d a b) a' b' =
diskUpd (diskUpd d a' b') a b
  apply diskUpd_comm.d:list block
a, a':nat
b, b':block
H:a < a'
a <> a'
  lia.
Qed.

Theorem diskUpd_oob_noop : forall d a b,
    ~a < diskSize d ->
    diskUpd d a b = d.forall (d : disk) (a : nat) (b : block),
~ a < diskSize d -> diskUpd d a b = d
Proof.forall (d : disk) (a : nat) (b : block),
~ a < diskSize d -> diskUpd d a b = d
  induction d; simpl; intros; auto.a:block
d:list block
IHd:forall (a : nat) (b : block), ~ a < diskSize d -> diskUpd d a b = d
a0:nat
b:block
H:~ a0 < S (diskSize d)
match a0 with
| 0 => b :: d
| S a' => a :: diskUpd d a' b
end = a :: d
  destruct a0; simpl in *.a:block
d:list block
IHd:forall (a : nat) (b : block), ~ a < diskSize d -> diskUpd d a b = d
b:block
H:~ 0 < S (diskSize d)
b :: d = a :: d
a:block
d:list block
IHd:forall (a : nat) (b : block), ~ a < diskSize d -> diskUpd d a b = d
a0:nat
b:block
H:~ S a0 < S (diskSize d)
a :: diskUpd d a0 b = a :: d
  -a:block
d:list block
IHd:forall (a : nat) (b : block), ~ a < diskSize d -> diskUpd d a b = d
b:block
H:~ 0 < S (diskSize d)
b :: d = a :: d lia.
  -a:block
d:list block
IHd:forall (a : nat) (b : block), ~ a < diskSize d -> diskUpd d a b = d
a0:nat
b:block
H:~ S a0 < S (diskSize d)
a :: diskUpd d a0 b = a :: d rewrite IHd; auto; lia.
Qed.

Theorems about diskShrink

Theorem diskShrink_size : forall d,
    diskSize d <> 0 ->
    diskSize (diskShrink d) = diskSize d - 1.forall d : disk,
diskSize d <> 0 ->
diskSize (diskShrink d) = diskSize d - 1
Proof.forall d : disk,
diskSize d <> 0 ->
diskSize (diskShrink d) = diskSize d - 1
  unfold diskSize, diskShrink; intros.d:disk
H:length d <> 0
length (firstn (length d - 1) d) = length d - 1
  rewrite firstn_length.d:disk
H:length d <> 0
Init.Nat.min (length d - 1) (length d) = length d - 1
  rewrite min_l; lia.
Qed.

Theorem diskShrink_preserves : forall d a,
    a <> diskSize (diskShrink d) ->
    diskGet (diskShrink d) a = diskGet d a.forall (d : disk) (a : nat),
a <> diskSize (diskShrink d) ->
diskGet (diskShrink d) a = diskGet d a
Proof.forall (d : disk) (a : nat),
a <> diskSize (diskShrink d) ->
diskGet (diskShrink d) a = diskGet d a
  unfold diskShrink.forall (d : disk) (a : nat),
a <> diskSize (firstn (length d - 1) d) ->
diskGet (firstn (length d - 1) d) a = diskGet d a
  induction d; simpl; intros; auto.a:block
d:list block
IHd:forall a : nat,
a <> diskSize (firstn (length d - 1) d) ->
diskGet (firstn (length d - 1) d) a = diskGet d a
a0:nat
H:a0 <> diskSize (firstn (length d - 0) (a :: d))
diskGet (firstn (length d - 0) (a :: d)) a0 =
diskGet (a :: d) a0
  destruct d; simpl in *.a:block
IHd:forall a : nat, a <> 0 -> diskGet nil a = diskGet nil a
a0:nat
H:a0 <> 0
diskGet nil a0 = diskGet (a :: nil) a0
a, b:block
d:list block
IHd:forall a : nat,
a <> diskSize (firstn (length d - 0) (b :: d)) ->
diskGet (firstn (length d - 0) (b :: d)) a = diskGet (b :: d) a
a0:nat
H:a0 <> S (diskSize (firstn (length d) (b :: d)))
diskGet (a :: firstn (length d) (b :: d)) a0 =
diskGet (a :: b :: d) a0
  -a:block
IHd:forall a : nat, a <> 0 -> diskGet nil a = diskGet nil a
a0:nat
H:a0 <> 0
diskGet nil a0 = diskGet (a :: nil) a0 destruct a0; try lia; simpl.a:block
IHd:forall a : nat, a <> 0 -> diskGet nil a = diskGet nil a
a0:nat
H:S a0 <> 0
None = diskGet nil a0
    destruct a0; auto.
  -a, b:block
d:list block
IHd:forall a : nat,
a <> diskSize (firstn (length d - 0) (b :: d)) ->
diskGet (firstn (length d - 0) (b :: d)) a = diskGet (b :: d) a
a0:nat
H:a0 <> S (diskSize (firstn (length d) (b :: d)))
diskGet (a :: firstn (length d) (b :: d)) a0 =
diskGet (a :: b :: d) a0 destruct a0; simpl; auto.a, b:block
d:list block
IHd:forall a : nat,
a <> diskSize (firstn (length d - 0) (b :: d)) ->
diskGet (firstn (length d - 0) (b :: d)) a = diskGet (b :: d) a
a0:nat
H:S a0 <> S (diskSize (firstn (length d) (b :: d)))
diskGet (firstn (length d) (b :: d)) a0 =
diskGet (b :: d) a0
    replace (length d - 0) with (length d) in * by lia.a, b:block
d:list block
IHd:forall a : nat,
a <> diskSize (firstn (length d) (b :: d)) ->
diskGet (firstn (length d) (b :: d)) a = diskGet (b :: d) a
a0:nat
H:S a0 <> S (diskSize (firstn (length d) (b :: d)))
diskGet (firstn (length d) (b :: d)) a0 =
diskGet (b :: d) a0
    rewrite <- IHd; auto.
Qed.

Theorem diskShrink_diskUpd_last : forall d a b,
    a >= diskSize d - 1 ->
    diskShrink (diskUpd d a b) = diskShrink d.forall (d : disk) (a : nat) (b : block),
a >= diskSize d - 1 ->
diskShrink (diskUpd d a b) = diskShrink d
Proof.forall (d : disk) (a : nat) (b : block),
a >= diskSize d - 1 ->
diskShrink (diskUpd d a b) = diskShrink d
  unfold diskShrink; intros.d:disk
a:nat
b:block
H:a >= diskSize d - 1
firstn (length (diskUpd d a b) - 1) (diskUpd d a b) =
firstn (length d - 1) d
  destruct (eq_nat_dec a (diskSize d - 1)); subst.d:disk
b:block
H:diskSize d - 1 >= diskSize d - 1
firstn (length (diskUpd d (diskSize d - 1) b) - 1)
  (diskUpd d (diskSize d - 1) b) =
firstn (length d - 1) d
d:disk
a:nat
b:block
H:a >= diskSize d - 1
n:a <> diskSize d - 1
firstn (length (diskUpd d a b) - 1) (diskUpd d a b) =
firstn (length d - 1) d
  -d:disk
b:block
H:diskSize d - 1 >= diskSize d - 1
firstn (length (diskUpd d (diskSize d - 1) b) - 1)
  (diskUpd d (diskSize d - 1) b) =
firstn (length d - 1) d clear H.d:disk
b:block
firstn (length (diskUpd d (diskSize d - 1) b) - 1)
  (diskUpd d (diskSize d - 1) b) =
firstn (length d - 1) d
    rewrite diskUpd_size; unfold diskSize.d:disk
b:block
firstn (length d - 1) (diskUpd d (length d - 1) b) =
firstn (length d - 1) d
    induction d; simpl; auto.a:block
d:list block
b:block
IHd:firstn (length d - 1) (diskUpd d (length d - 1) b) = firstn (length d - 1) d
firstn (length d - 0)
  match length d - 0 with
  | 0 => b :: d
  | S a' => a :: diskUpd d a' b
  end = firstn (length d - 0) (a :: d)
    destruct d; simpl in *; auto.a, b0:block
d:list block
b:block
IHd:firstn (length d - 0)
match length d - 0 with
| 0 => b :: d
| S a' => b0 :: diskUpd d a' b
end = firstn (length d - 0) (b0 :: d)
a
:: firstn (length d)
     match length d with
     | 0 => b :: d
     | S a' => b0 :: diskUpd d a' b
     end = a :: firstn (length d) (b0 :: d)
    replace (length d - 0) with (length d) in * by lia.a, b0:block
d:list block
b:block
IHd:firstn (length d)
match length d with
| 0 => b :: d
| S a' => b0 :: diskUpd d a' b
end = firstn (length d) (b0 :: d)
a
:: firstn (length d)
     match length d with
     | 0 => b :: d
     | S a' => b0 :: diskUpd d a' b
     end = a :: firstn (length d) (b0 :: d)
    f_equal; auto.
  -d:disk
a:nat
b:block
H:a >= diskSize d - 1
n:a <> diskSize d - 1
firstn (length (diskUpd d a b) - 1) (diskUpd d a b) =
firstn (length d - 1) d rewrite diskUpd_oob_noop by lia; auto.
Qed.

Theorem diskShrink_diskUpd_notlast : forall d a b,
    a < diskSize d - 1 ->
    diskShrink (diskUpd d a b) = diskUpd (diskShrink d) a b.forall (d : disk) (a : nat) (b : block),
a < diskSize d - 1 ->
diskShrink (diskUpd d a b) =
diskUpd (diskShrink d) a b
Proof.forall (d : disk) (a : nat) (b : block),
a < diskSize d - 1 ->
diskShrink (diskUpd d a b) =
diskUpd (diskShrink d) a b
  unfold diskShrink.forall (d : disk) (a : nat) (b : block),
a < diskSize d - 1 ->
firstn (length (diskUpd d a b) - 1) (diskUpd d a b) =
diskUpd (firstn (length d - 1) d) a b
  induction d; simpl; auto; intros.a:block
d:list block
IHd:forall (a : nat) (b : block),
a < diskSize d - 1 ->
firstn (length (diskUpd d a b) - 1) (diskUpd d a b) =
diskUpd (firstn (length d - 1) d) a b
a0:nat
b:block
H:a0 < diskSize d - 0
firstn
  (length
     match a0 with
     | 0 => b :: d
     | S a' => a :: diskUpd d a' b
     end - 1)
  match a0 with
  | 0 => b :: d
  | S a' => a :: diskUpd d a' b
  end = diskUpd (firstn (length d - 0) (a :: d)) a0 b
  destruct a0; simpl; auto.a:block
d:list block
IHd:forall (a : nat) (b : block),
a < diskSize d - 1 ->
firstn (length (diskUpd d a b) - 1) (diskUpd d a b) =
diskUpd (firstn (length d - 1) d) a b
b:block
H:0 < diskSize d - 0
firstn (length d - 0) (b :: d) =
diskUpd (firstn (length d - 0) (a :: d)) 0 b
a:block
d:list block
IHd:forall (a : nat) (b : block),
a < diskSize d - 1 ->
firstn (length (diskUpd d a b) - 1) (diskUpd d a b) =
diskUpd (firstn (length d - 1) d) a b
a0:nat
b:block
H:S a0 < diskSize d - 0
firstn (length (diskUpd d a0 b) - 0)
  (a :: diskUpd d a0 b) =
diskUpd (firstn (length d - 0) (a :: d)) (S a0) b
  -a:block
d:list block
IHd:forall (a : nat) (b : block),
a < diskSize d - 1 ->
firstn (length (diskUpd d a b) - 1) (diskUpd d a b) =
diskUpd (firstn (length d - 1) d) a b
b:block
H:0 < diskSize d - 0
firstn (length d - 0) (b :: d) =
diskUpd (firstn (length d - 0) (a :: d)) 0 b destruct d; simpl; auto.
  -a:block
d:list block
IHd:forall (a : nat) (b : block),
a < diskSize d - 1 ->
firstn (length (diskUpd d a b) - 1) (diskUpd d a b) =
diskUpd (firstn (length d - 1) d) a b
a0:nat
b:block
H:S a0 < diskSize d - 0
firstn (length (diskUpd d a0 b) - 0)
  (a :: diskUpd d a0 b) =
diskUpd (firstn (length d - 0) (a :: d)) (S a0) b destruct d; simpl in *; auto.a, b0:block
d:list block
IHd:forall (a : nat) (b : block),
a < diskSize d - 0 ->
firstn
(length match a with
| 0 => b :: d
| S a' => b0 :: diskUpd d a' b
end - 1)
match a with
| 0 => b :: d
| S a' => b0 :: diskUpd d a' b
end = diskUpd (firstn (length d - 0) (b0 :: d)) a b
a0:nat
b:block
H:S a0 < S (diskSize d)
firstn
  (length
     match a0 with
     | 0 => b :: d
     | S a' => b0 :: diskUpd d a' b
     end - 0)
  (a
   :: match a0 with
      | 0 => b :: d
      | S a' => b0 :: diskUpd d a' b
      end) =
a :: diskUpd (firstn (length d) (b0 :: d)) a0 b
    replace (length d - 0) with (length d) in * by lia.a, b0:block
d:list block
IHd:forall (a : nat) (b : block),
a < diskSize d - 0 ->
firstn
(length match a with
| 0 => b :: d
| S a' => b0 :: diskUpd d a' b
end - 1)
match a with
| 0 => b :: d
| S a' => b0 :: diskUpd d a' b
end = diskUpd (firstn (length d) (b0 :: d)) a b
a0:nat
b:block
H:S a0 < S (diskSize d)
firstn
  (length
     match a0 with
     | 0 => b :: d
     | S a' => b0 :: diskUpd d a' b
     end - 0)
  (a
   :: match a0 with
      | 0 => b :: d
      | S a' => b0 :: diskUpd d a' b
      end) =
a :: diskUpd (firstn (length d) (b0 :: d)) a0 b
    rewrite <- IHd by lia.a, b0:block
d:list block
IHd:forall (a : nat) (b : block),
a < diskSize d - 0 ->
firstn
(length match a with
| 0 => b :: d
| S a' => b0 :: diskUpd d a' b
end - 1)
match a with
| 0 => b :: d
| S a' => b0 :: diskUpd d a' b
end = diskUpd (firstn (length d) (b0 :: d)) a b
a0:nat
b:block
H:S a0 < S (diskSize d)
firstn
  (length
     match a0 with
     | 0 => b :: d
     | S a' => b0 :: diskUpd d a' b
     end - 0)
  (a
   :: match a0 with
      | 0 => b :: d
      | S a' => b0 :: diskUpd d a' b
      end) =
a
:: firstn
     (length
        match a0 with
        | 0 => b :: d
        | S a' => b0 :: diskUpd d a' b
        end - 1)
     match a0 with
     | 0 => b :: d
     | S a' => b0 :: diskUpd d a' b
     end
    destruct a0; simpl; try rewrite diskUpd_size; unfold diskSize;
      replace (length d - 0) with (length d) by lia; auto.
Qed.

Hint Rewrite diskUpd_size : disk_size.
Hint Rewrite diskShrink_size using solve [ auto || lia ] : disk_size.

Theorems about diskUpds

Theorem diskUpds_neq : forall blocks d a a',
  a' < a \/ a' >= a + length blocks ->
  diskGet (diskUpds d a blocks) a' = diskGet d a'.forall (blocks : list block) (d : disk) (a a' : nat),
a' < a \/ a' >= a + length blocks ->
diskGet (diskUpds d a blocks) a' = diskGet d a'
Proof.forall (blocks : list block) (d : disk) (a a' : nat),
a' < a \/ a' >= a + length blocks ->
diskGet (diskUpds d a blocks) a' = diskGet d a'
  induction blocks; simpl; auto; intros.a:block
blocks:list block
IHblocks:forall (d : disk) (a a' : nat),
a' < a \/ a' >= a + length blocks ->
diskGet (diskUpds d a blocks) a' =
diskGet d a'
d:disk
a0, a':nat
H:a' < a0 \/ a' >= a0 + S (length blocks)
diskGet (diskUpd (diskUpds d (a0 + 1) blocks) a0 a) a' =
diskGet d a'
  rewrite diskUpd_neq by lia.a:block
blocks:list block
IHblocks:forall (d : disk) (a a' : nat),
a' < a \/ a' >= a + length blocks ->
diskGet (diskUpds d a blocks) a' =
diskGet d a'
d:disk
a0, a':nat
H:a' < a0 \/ a' >= a0 + S (length blocks)
diskGet (diskUpds d (a0 + 1) blocks) a' = diskGet d a'
  rewrite IHblocks; auto.a:block
blocks:list block
IHblocks:forall (d : disk) (a a' : nat),
a' < a \/ a' >= a + length blocks ->
diskGet (diskUpds d a blocks) a' =
diskGet d a'
d:disk
a0, a':nat
H:a' < a0 \/ a' >= a0 + S (length blocks)
a' < a0 + 1 \/ a' >= a0 + 1 + length blocks
  lia.
Qed.

Theorem diskUpds_size : forall blocks d a,
    diskSize (diskUpds d a blocks) = diskSize d.forall (blocks : list block) (d : disk) (a : addr),
diskSize (diskUpds d a blocks) = diskSize d
Proof.forall (blocks : list block) (d : disk) (a : addr),
diskSize (diskUpds d a blocks) = diskSize d
  induction blocks; simpl; eauto; intros.a:block
blocks:list block
IHblocks:forall (d : disk) (a : addr),
diskSize (diskUpds d a blocks) = diskSize d
d:disk
a0:addr
diskSize (diskUpd (diskUpds d (a0 + 1) blocks) a0 a) =
diskSize d
  rewrite diskUpd_size; auto.
Qed.

Theorem diskUpds_diskUpd_comm : forall blocks d a a' b,
  a' < a \/ a' >= a + length blocks ->
  diskUpd (diskUpds d a blocks) a' b = diskUpds (diskUpd d a' b) a blocks.forall (blocks : list block) (d : disk) (a a' : nat)
  (b : block),
a' < a \/ a' >= a + length blocks ->
diskUpd (diskUpds d a blocks) a' b =
diskUpds (diskUpd d a' b) a blocks
Proof.forall (blocks : list block) (d : disk) (a a' : nat)
  (b : block),
a' < a \/ a' >= a + length blocks ->
diskUpd (diskUpds d a blocks) a' b =
diskUpds (diskUpd d a' b) a blocks
  induction blocks; simpl; auto; intros.a:block
blocks:list block
IHblocks:forall (d : disk) (a a' : nat) (b : block),
a' < a \/ a' >= a + length blocks ->
diskUpd (diskUpds d a blocks) a' b =
diskUpds (diskUpd d a' b) a blocks
d:disk
a0, a':nat
b:block
H:a' < a0 \/ a' >= a0 + S (length blocks)
diskUpd (diskUpd (diskUpds d (a0 + 1) blocks) a0 a) a'
  b =
diskUpd (diskUpds (diskUpd d a' b) (a0 + 1) blocks) a0
  a
  rewrite diskUpd_comm by lia.a:block
blocks:list block
IHblocks:forall (d : disk) (a a' : nat) (b : block),
a' < a \/ a' >= a + length blocks ->
diskUpd (diskUpds d a blocks) a' b =
diskUpds (diskUpd d a' b) a blocks
d:disk
a0, a':nat
b:block
H:a' < a0 \/ a' >= a0 + S (length blocks)
diskUpd (diskUpd (diskUpds d (a0 + 1) blocks) a' b) a0
  a =
diskUpd (diskUpds (diskUpd d a' b) (a0 + 1) blocks) a0
  a
  rewrite IHblocks; auto.a:block
blocks:list block
IHblocks:forall (d : disk) (a a' : nat) (b : block),
a' < a \/ a' >= a + length blocks ->
diskUpd (diskUpds d a blocks) a' b =
diskUpds (diskUpd d a' b) a blocks
d:disk
a0, a':nat
b:block
H:a' < a0 \/ a' >= a0 + S (length blocks)
a' < a0 + 1 \/ a' >= a0 + 1 + length blocks
  lia.
Qed.

Theorem diskUpds_diskUpd_after : forall blocks d a b,
  diskUpd (diskUpds d a blocks) (a + length blocks) b =
  diskUpds d a (blocks ++ (b :: nil)).forall (blocks : list block) (d : disk) (a : addr)
  (b : block),
diskUpd (diskUpds d a blocks) (a + length blocks) b =
diskUpds d a (blocks ++ b :: nil)
Proof.forall (blocks : list block) (d : disk) (a : addr)
  (b : block),
diskUpd (diskUpds d a blocks) (a + length blocks) b =
diskUpds d a (blocks ++ b :: nil)
  induction blocks; simpl; auto; intros.d:disk
a:addr
b:block
diskUpd d (a + 0) b = diskUpd d a b
a:block
blocks:list block
IHblocks:forall (d : disk) (a : addr) (b : block),
diskUpd (diskUpds d a blocks)
  (a + length blocks) b =
diskUpds d a (blocks ++ b :: nil)
d:disk
a0:addr
b:block
diskUpd (diskUpd (diskUpds d (a0 + 1) blocks) a0 a)
  (a0 + S (length blocks)) b =
diskUpd (diskUpds d (a0 + 1) (blocks ++ b :: nil)) a0
  a
  -d:disk
a:addr
b:block
diskUpd d (a + 0) b = diskUpd d a b replace (a + 0) with a; auto.
  -a:block
blocks:list block
IHblocks:forall (d : disk) (a : addr) (b : block),
diskUpd (diskUpds d a blocks)
  (a + length blocks) b =
diskUpds d a (blocks ++ b :: nil)
d:disk
a0:addr
b:block
diskUpd (diskUpd (diskUpds d (a0 + 1) blocks) a0 a)
  (a0 + S (length blocks)) b =
diskUpd (diskUpds d (a0 + 1) (blocks ++ b :: nil)) a0
  a rewrite diskUpd_comm by lia.a:block
blocks:list block
IHblocks:forall (d : disk) (a : addr) (b : block),
diskUpd (diskUpds d a blocks)
  (a + length blocks) b =
diskUpds d a (blocks ++ b :: nil)
d:disk
a0:addr
b:block
diskUpd
  (diskUpd (diskUpds d (a0 + 1) blocks)
     (a0 + S (length blocks)) b) a0 a =
diskUpd (diskUpds d (a0 + 1) (blocks ++ b :: nil)) a0
  a
    rewrite <- IHblocks.a:block
blocks:list block
IHblocks:forall (d : disk) (a : addr) (b : block),
diskUpd (diskUpds d a blocks)
  (a + length blocks) b =
diskUpds d a (blocks ++ b :: nil)
d:disk
a0:addr
b:block
diskUpd
  (diskUpd (diskUpds d (a0 + 1) blocks)
     (a0 + S (length blocks)) b) a0 a =
diskUpd
  (diskUpd (diskUpds d (a0 + 1) blocks)
     (a0 + 1 + length blocks) b) a0 a
    replace (a0 + S (length blocks)) with (a0 + 1 + length blocks) by lia.a:block
blocks:list block
IHblocks:forall (d : disk) (a : addr) (b : block),
diskUpd (diskUpds d a blocks)
  (a + length blocks) b =
diskUpds d a (blocks ++ b :: nil)
d:disk
a0:addr
b:block
diskUpd
  (diskUpd (diskUpds d (a0 + 1) blocks)
     (a0 + 1 + length blocks) b) a0 a =
diskUpd
  (diskUpd (diskUpds d (a0 + 1) blocks)
     (a0 + 1 + length blocks) b) a0 a
    reflexivity.
Qed.

Theorem diskUpds_diskUpd_before : forall blocks d a b,
  diskUpd (diskUpds d (a + 1) blocks) a b =
  diskUpds d a (b :: blocks).forall (blocks : list block) (d : disk) (a : nat)
  (b : block),
diskUpd (diskUpds d (a + 1) blocks) a b =
diskUpds d a (b :: blocks)
Proof.forall (blocks : list block) (d : disk) (a : nat)
  (b : block),
diskUpd (diskUpds d (a + 1) blocks) a b =
diskUpds d a (b :: blocks)
  reflexivity.
Qed.

Theorems about diskGets

Theorem diskGets_first : forall count d a,
  diskGets d a (count+1) = diskGet d a :: diskGets d (a+1) count.forall (count : nat) (d : disk) (a : addr),
diskGets d a (count + 1) =
diskGet d a :: diskGets d (a + 1) count
Proof.forall (count : nat) (d : disk) (a : addr),
diskGets d a (count + 1) =
diskGet d a :: diskGets d (a + 1) count
  intros.count:nat
d:disk
a:addr
diskGets d a (count + 1) =
diskGet d a :: diskGets d (a + 1) count
  replace (count+1) with (S count) by lia.count:nat
d:disk
a:addr
diskGets d a (S count) =
diskGet d a :: diskGets d (a + 1) count
  reflexivity.
Qed.

Theorem diskGets_last : forall count d a,
  diskGets d a (count+1) = diskGets d a count ++ (diskGet d (a+count) :: nil).forall (count : nat) (d : disk) (a : addr),
diskGets d a (count + 1) =
diskGets d a count ++ diskGet d (a + count) :: nil
Proof.forall (count : nat) (d : disk) (a : addr),
diskGets d a (count + 1) =
diskGets d a count ++ diskGet d (a + count) :: nil
  induction count; simpl; intros.d:disk
a:addr
diskGet d a :: nil = diskGet d (a + 0) :: nil
count:nat
IHcount:forall (d : disk) (a : addr),
diskGets d a (count + 1) =
diskGets d a count ++
diskGet d (a + count) :: nil
d:disk
a:addr
diskGet d a :: diskGets d (a + 1) (count + 1) =
diskGet d a
:: diskGets d (a + 1) count ++
   diskGet d (a + S count) :: nil
  -d:disk
a:addr
diskGet d a :: nil = diskGet d (a + 0) :: nil replace (a+0) with a by lia; auto.
  -count:nat
IHcount:forall (d : disk) (a : addr),
diskGets d a (count + 1) =
diskGets d a count ++
diskGet d (a + count) :: nil
d:disk
a:addr
diskGet d a :: diskGets d (a + 1) (count + 1) =
diskGet d a
:: diskGets d (a + 1) count ++
   diskGet d (a + S count) :: nil rewrite IHcount.count:nat
IHcount:forall (d : disk) (a : addr),
diskGets d a (count + 1) =
diskGets d a count ++
diskGet d (a + count) :: nil
d:disk
a:addr
diskGet d a
:: diskGets d (a + 1) count ++
   diskGet d (a + 1 + count) :: nil =
diskGet d a
:: diskGets d (a + 1) count ++
   diskGet d (a + S count) :: nil
    replace (a+1+count) with (a+S count) by lia; auto.
Qed.

Theorem diskGets_app : forall count0 count1 d a,
  diskGets d a (count0+count1) = diskGets d a count0 ++ diskGets d (a+count0) count1.forall (count0 count1 : nat) (d : disk) (a : addr),
diskGets d a (count0 + count1) =
diskGets d a count0 ++ diskGets d (a + count0) count1
Proof.forall (count0 count1 : nat) (d : disk) (a : addr),
diskGets d a (count0 + count1) =
diskGets d a count0 ++ diskGets d (a + count0) count1
  induction count0; simpl; auto; intros.count0:nat
IHcount0:forall (count1 : nat) (d : disk) (a : addr),
diskGets d a (count0 + count1) =
diskGets d a count0 ++
diskGets d (a + count0) count1
count1:nat
d:disk
a:addr
diskGet d a :: diskGets d (a + 1) (count0 + count1) =
diskGet d a
:: diskGets d (a + 1) count0 ++
   diskGets d (a + S count0) count1
  rewrite IHcount0.count0:nat
IHcount0:forall (count1 : nat) (d : disk) (a : addr),
diskGets d a (count0 + count1) =
diskGets d a count0 ++
diskGets d (a + count0) count1
count1:nat
d:disk
a:addr
diskGet d a
:: diskGets d (a + 1) count0 ++
   diskGets d (a + 1 + count0) count1 =
diskGet d a
:: diskGets d (a + 1) count0 ++
   diskGets d (a + S count0) count1
  replace (a+1+count0) with (a+S count0) by lia.count0:nat
IHcount0:forall (count1 : nat) (d : disk) (a : addr),
diskGets d a (count0 + count1) =
diskGets d a count0 ++
diskGets d (a + count0) count1
count1:nat
d:disk
a:addr
diskGet d a
:: diskGets d (a + 1) count0 ++
   diskGets d (a + S count0) count1 =
diskGet d a
:: diskGets d (a + 1) count0 ++
   diskGets d (a + S count0) count1
  auto.
Qed.

Theorem diskGets_length : forall d a count,
    length (diskGets d a count) = count.forall (d : disk) (a : addr) (count : nat),
length (diskGets d a count) = count
Proof.forall (d : disk) (a : addr) (count : nat),
length (diskGets d a count) = count
  intros.d:disk
a:addr
count:nat
length (diskGets d a count) = count
  revert a.d:disk
count:nat
forall a : addr, length (diskGets d a count) = count
  induction count; simpl; auto.
Qed.

Theorem diskGets_index : forall d a count i,
    i < count ->
    nth_error (diskGets d a count) i = Some (diskGet d (a+i)).forall (d : disk) (a : addr) (count i : nat),
i < count ->
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
Proof.forall (d : disk) (a : addr) (count i : nat),
i < count ->
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
  intros.d:disk
a:addr
count, i:nat
H:i < count
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
  generalize dependent i.d:disk
a:addr
count:nat
forall i : nat,
i < count ->
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
  revert a.d:disk
count:nat
forall (a : addr) (i : nat),
i < count ->
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
  induction count; simpl; intros.d:disk
a:addr
i:nat
H:i < 0
nth_error nil i = Some (diskGet d (a + i))
d:disk
count:nat
IHcount:forall (a : addr) (i : nat),
i < count ->
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
a:addr
i:nat
H:i < S count
nth_error (diskGet d a :: diskGets d (a + 1) count) i =
Some (diskGet d (a + i))
  -d:disk
a:addr
i:nat
H:i < 0
nth_error nil i = Some (diskGet d (a + i)) lia.
  -d:disk
count:nat
IHcount:forall (a : addr) (i : nat),
i < count ->
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
a:addr
i:nat
H:i < S count
nth_error (diskGet d a :: diskGets d (a + 1) count) i =
Some (diskGet d (a + i)) destruct i; simpl.d:disk
count:nat
IHcount:forall (a : addr) (i : nat),
i < count ->
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
a:addr
H:0 < S count
Some (diskGet d a) = Some (diskGet d (a + 0))
d:disk
count:nat
IHcount:forall (a : addr) (i : nat),
i < count ->
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
a:addr
i:nat
H:S i < S count
nth_error (diskGets d (a + 1) count) i =
Some (diskGet d (a + S i))
    replace (a+0) with a by lia; auto.d:disk
count:nat
IHcount:forall (a : addr) (i : nat),
i < count ->
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
a:addr
i:nat
H:S i < S count
nth_error (diskGets d (a + 1) count) i =
Some (diskGet d (a + S i))
    rewrite IHcount by lia.d:disk
count:nat
IHcount:forall (a : addr) (i : nat),
i < count ->
nth_error (diskGets d a count) i =
Some (diskGet d (a + i))
a:addr
i:nat
H:S i < S count
Some (diskGet d (a + 1 + i)) =
Some (diskGet d (a + S i))
    replace (a+1+i) with (a+S i) by lia; auto.
Qed.

Hint Rewrite diskGets_length : disk_size.
Section diskGets_proof.
Hint Rewrite nth_error_app1 using (autorewrite with disk_size in *; lia) : upd.
Hint Rewrite nth_error_app2 using (autorewrite with disk_size in *; lia) : upd.
Hint Rewrite diskGets_index using lia : upd.

Theorem diskGets_app_disk : forall d1 d2 a count,
    count >= length d1-a ->
    a < length d1 ->
    diskGets (d1 ++ d2) a count =
    diskGets d1 a (length d1 - a) ++ diskGets d2 0 (count - (length d1-a)).forall (d1 d2 : list block) (a count : nat),
count >= length d1 - a ->
a < length d1 ->
diskGets (d1 ++ d2) a count =
diskGets d1 a (length d1 - a) ++
diskGets d2 0 (count - (length d1 - a))
Proof.forall (d1 d2 : list block) (a count : nat),
count >= length d1 - a ->
a < length d1 ->
diskGets (d1 ++ d2) a count =
diskGets d1 a (length d1 - a) ++
diskGets d2 0 (count - (length d1 - a))
  intros.d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
diskGets (d1 ++ d2) a count =
diskGets d1 a (length d1 - a) ++
diskGets d2 0 (count - (length d1 - a))
  apply nth_error_ext_inbounds_eq.d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
length (diskGets (d1 ++ d2) a count) =
length
  (diskGets d1 a (length d1 - a) ++
   diskGets d2 0 (count - (length d1 - a)))
d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
forall a0 : nat,
a0 < length (diskGets (d1 ++ d2) a count) ->
nth_error (diskGets (d1 ++ d2) a count) a0 =
nth_error
  (diskGets d1 a (length d1 - a) ++
   diskGets d2 0 (count - (length d1 - a))) a0
  {d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
length (diskGets (d1 ++ d2) a count) =
length
  (diskGets d1 a (length d1 - a) ++
   diskGets d2 0 (count - (length d1 - a))) repeat rewrite ?diskGets_length, ?app_length.d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
count = length d1 - a + (count - (length d1 - a))
    lia. }d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
forall a0 : nat,
a0 < length (diskGets (d1 ++ d2) a count) ->
nth_error (diskGets (d1 ++ d2) a count) a0 =
nth_error
  (diskGets d1 a (length d1 - a) ++
   diskGets d2 0 (count - (length d1 - a))) a0
  intros i **.d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
i:nat
H1:i < length (diskGets (d1 ++ d2) a count)
nth_error (diskGets (d1 ++ d2) a count) i =
nth_error
  (diskGets d1 a (length d1 - a) ++
   diskGets d2 0 (count - (length d1 - a))) i
  autorewrite with disk_size upd in *.d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
i:nat
H1:i < count
nth_error (diskGets (d1 ++ d2) a count) i =
nth_error
  (diskGets d1 a (length d1 - a) ++
   diskGets d2 0 (count - (length d1 - a))) i
  rewrite diskGets_index by lia.d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
i:nat
H1:i < count
Some (diskGet (d1 ++ d2) (a + i)) =
nth_error
  (diskGets d1 a (length d1 - a) ++
   diskGets d2 0 (count - (length d1 - a))) i
  destruct (lt_dec i (length d1 - a));
    unfold diskGet;
    autorewrite with disk_size upd in *.d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
i:nat
H1:i < count
l:i < length d1 - a
Some (nth_error d1 (a + i)) =
Some (diskGet d1 (a + i))
d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
i:nat
H1:i < count
n:~ i < length d1 - a
Some (nth_error d2 (a + i - length d1)) =
Some (diskGet d2 (0 + (i - (length d1 - a))))
  -d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
i:nat
H1:i < count
l:i < length d1 - a
Some (nth_error d1 (a + i)) =
Some (diskGet d1 (a + i)) auto.
  -d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
i:nat
H1:i < count
n:~ i < length d1 - a
Some (nth_error d2 (a + i - length d1)) =
Some (diskGet d2 (0 + (i - (length d1 - a)))) unfold diskGet.d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
i:nat
H1:i < count
n:~ i < length d1 - a
Some (nth_error d2 (a + i - length d1)) =
Some (nth_error d2 (0 + (i - (length d1 - a))))
    do 2 f_equal.d1, d2:list block
a, count:nat
H:count >= length d1 - a
H0:a < length d1
i:nat
H1:i < count
n:~ i < length d1 - a
a + i - length d1 = 0 + (i - (length d1 - a))
    lia.
Qed.
End diskGets_proof.

Theorem diskGets_append_one : forall d1 a x count,
    a < length d1 ->
    a + count = S (length d1) ->
    diskGets (d1 ++ x::nil) a count =
    diskGets d1 a (length d1 - a) ++ (Some x::nil).forall (d1 : list block) (a : nat) (x : block)
  (count : nat),
a < length d1 ->
a + count = S (length d1) ->
diskGets (d1 ++ x :: nil) a count =
diskGets d1 a (length d1 - a) ++ Some x :: nil
Proof.forall (d1 : list block) (a : nat) (x : block)
  (count : nat),
a < length d1 ->
a + count = S (length d1) ->
diskGets (d1 ++ x :: nil) a count =
diskGets d1 a (length d1 - a) ++ Some x :: nil
  intros.d1:list block
a:nat
x:block
count:nat
H:a < length d1
H0:a + count = S (length d1)
diskGets (d1 ++ x :: nil) a count =
diskGets d1 a (length d1 - a) ++ Some x :: nil
  rewrite diskGets_app_disk by lia.d1:list block
a:nat
x:block
count:nat
H:a < length d1
H0:a + count = S (length d1)
diskGets d1 a (length d1 - a) ++
diskGets (x :: nil) 0 (count - (length d1 - a)) =
diskGets d1 a (length d1 - a) ++ Some x :: nil
  replace (count - (length d1 - a)) with 1 by lia; simpl; auto.
Qed.

Theorem diskUpd_diskGets_neq : forall count d a a0 v0,
  (a0 < a \/ a0 > a + count) ->
  diskGets (diskUpd d a0 v0) a count = diskGets d a count.forall (count : nat) (d : list block) (a a0 : nat)
  (v0 : block),
a0 < a \/ a0 > a + count ->
diskGets (diskUpd d a0 v0) a count =
diskGets d a count
Proof.forall (count : nat) (d : list block) (a a0 : nat)
  (v0 : block),
a0 < a \/ a0 > a + count ->
diskGets (diskUpd d a0 v0) a count =
diskGets d a count
  induction count; simpl; intros; auto.count:nat
IHcount:forall (d : list block) 
  (a a0 : nat) (v0 : block),
a0 < a \/ a0 > a + count ->
diskGets (diskUpd d a0 v0) a count =
diskGets d a count
d:list block
a, a0:nat
v0:block
H:a0 < a \/ a0 > a + S count
diskGet (diskUpd d a0 v0) a
:: diskGets (diskUpd d a0 v0) (a + 1) count =
diskGet d a :: diskGets d (a + 1) count
  rewrite diskUpd_neq by lia.count:nat
IHcount:forall (d : list block) 
  (a a0 : nat) (v0 : block),
a0 < a \/ a0 > a + count ->
diskGets (diskUpd d a0 v0) a count =
diskGets d a count
d:list block
a, a0:nat
v0:block
H:a0 < a \/ a0 > a + S count
diskGet d a
:: diskGets (diskUpd d a0 v0) (a + 1) count =
diskGet d a :: diskGets d (a + 1) count
  rewrite IHcount by lia.count:nat
IHcount:forall (d : list block) 
  (a a0 : nat) (v0 : block),
a0 < a \/ a0 > a + count ->
diskGets (diskUpd d a0 v0) a count =
diskGets d a count
d:list block
a, a0:nat
v0:block
H:a0 < a \/ a0 > a + S count
diskGet d a :: diskGets d (a + 1) count =
diskGet d a :: diskGets d (a + 1) count
  auto.
Qed.

Theorem diskUpds_diskGets_neq : forall count d a a0 vs,
  (a0 + length vs < a \/ a0 >= a + count) ->
  diskGets (diskUpds d a0 vs) a count = diskGets d a count.forall (count : nat) (d : disk) (a a0 : nat)
  (vs : list block),
a0 + length vs < a \/ a0 >= a + count ->
diskGets (diskUpds d a0 vs) a count =
diskGets d a count
Proof.forall (count : nat) (d : disk) (a a0 : nat)
  (vs : list block),
a0 + length vs < a \/ a0 >= a + count ->
diskGets (diskUpds d a0 vs) a count =
diskGets d a count
  induction count; simpl; intros; auto.count:nat
IHcount:forall (d : disk) (a a0 : nat)
  (vs : list block),
a0 + length vs < a \/ a0 >= a + count ->
diskGets (diskUpds d a0 vs) a count =
diskGets d a count
d:disk
a, a0:nat
vs:list block
H:a0 + length vs < a \/ a0 >= a + S count
diskGet (diskUpds d a0 vs) a
:: diskGets (diskUpds d a0 vs) (a + 1) count =
diskGet d a :: diskGets d (a + 1) count
  rewrite diskUpds_neq by lia.count:nat
IHcount:forall (d : disk) (a a0 : nat)
  (vs : list block),
a0 + length vs < a \/ a0 >= a + count ->
diskGets (diskUpds d a0 vs) a count =
diskGets d a count
d:disk
a, a0:nat
vs:list block
H:a0 + length vs < a \/ a0 >= a + S count
diskGet d a
:: diskGets (diskUpds d a0 vs) (a + 1) count =
diskGet d a :: diskGets d (a + 1) count
  rewrite IHcount by lia.count:nat
IHcount:forall (d : disk) (a a0 : nat)
  (vs : list block),
a0 + length vs < a \/ a0 >= a + count ->
diskGets (diskUpds d a0 vs) a count =
diskGets d a count
d:disk
a, a0:nat
vs:list block
H:a0 + length vs < a \/ a0 >= a + S count
diskGet d a :: diskGets d (a + 1) count =
diskGet d a :: diskGets d (a + 1) count
  auto.
Qed.

Theorem diskUpds_diskGets_eq : forall vs d a,
  a + length vs <= diskSize d ->
  diskGets (diskUpds d a vs) a (length vs) = map Some vs.forall (vs : list block) (d : disk) (a : nat),
a + length vs <= diskSize d ->
diskGets (diskUpds d a vs) a (length vs) = map Some vs
Proof.forall (vs : list block) (d : disk) (a : nat),
a + length vs <= diskSize d ->
diskGets (diskUpds d a vs) a (length vs) = map Some vs
  induction vs; simpl; intros; auto.a:block
vs:list block
IHvs:forall (d : disk) (a : nat),
a + length vs <= diskSize d ->
diskGets (diskUpds d a vs) a (length vs) =
map Some vs
d:disk
a0:nat
H:a0 + S (length vs) <= diskSize d
diskGet (diskUpd (diskUpds d (a0 + 1) vs) a0 a) a0
:: diskGets (diskUpd (diskUpds d (a0 + 1) vs) a0 a)
     (a0 + 1) (length vs) = Some a :: map Some vs
  rewrite diskUpd_eq.a:block
vs:list block
IHvs:forall (d : disk) (a : nat),
a + length vs <= diskSize d ->
diskGets (diskUpds d a vs) a (length vs) =
map Some vs
d:disk
a0:nat
H:a0 + S (length vs) <= diskSize d
Some a
:: diskGets (diskUpd (diskUpds d (a0 + 1) vs) a0 a)
     (a0 + 1) (length vs) = 
Some a :: map Some vs
a:block
vs:list block
IHvs:forall (d : disk) (a : nat),
a + length vs <= diskSize d ->
diskGets (diskUpds d a vs) a (length vs) =
map Some vs
d:disk
a0:nat
H:a0 + S (length vs) <= diskSize d
a0 < diskSize (diskUpds d (a0 + 1) vs)
  -a:block
vs:list block
IHvs:forall (d : disk) (a : nat),
a + length vs <= diskSize d ->
diskGets (diskUpds d a vs) a (length vs) =
map Some vs
d:disk
a0:nat
H:a0 + S (length vs) <= diskSize d
Some a
:: diskGets (diskUpd (diskUpds d (a0 + 1) vs) a0 a)
     (a0 + 1) (length vs) = 
Some a :: map Some vs rewrite diskUpd_diskGets_neq by lia.a:block
vs:list block
IHvs:forall (d : disk) (a : nat),
a + length vs <= diskSize d ->
diskGets (diskUpds d a vs) a (length vs) =
map Some vs
d:disk
a0:nat
H:a0 + S (length vs) <= diskSize d
Some a
:: diskGets (diskUpds d (a0 + 1) vs) 
     (a0 + 1) (length vs) = 
Some a :: map Some vs
    rewrite IHvs by lia.a:block
vs:list block
IHvs:forall (d : disk) (a : nat),
a + length vs <= diskSize d ->
diskGets (diskUpds d a vs) a (length vs) =
map Some vs
d:disk
a0:nat
H:a0 + S (length vs) <= diskSize d
Some a :: map Some vs = Some a :: map Some vs
    auto.
  -a:block
vs:list block
IHvs:forall (d : disk) (a : nat),
a + length vs <= diskSize d ->
diskGets (diskUpds d a vs) a (length vs) =
map Some vs
d:disk
a0:nat
H:a0 + S (length vs) <= diskSize d
a0 < diskSize (diskUpds d (a0 + 1) vs) rewrite diskUpds_size.a:block
vs:list block
IHvs:forall (d : disk) (a : nat),
a + length vs <= diskSize d ->
diskGets (diskUpds d a vs) a (length vs) =
map Some vs
d:disk
a0:nat
H:a0 + S (length vs) <= diskSize d
a0 < diskSize d lia.
Qed.

Theorem append_size : forall d1 d2,
    diskSize (d1 ++ d2) = diskSize d1 + diskSize d2.forall d1 d2 : list block,
diskSize (d1 ++ d2) = diskSize d1 + diskSize d2
Proof.forall d1 d2 : list block,
diskSize (d1 ++ d2) = diskSize d1 + diskSize d2
  apply app_length.
Qed.

Hint Rewrite append_size : disk_size.
Hint Rewrite diskUpds_size : disk_size.

Theorem diskUpd_app1 : forall d1 d2 a v,
    a < length d1 ->
    diskUpd (d1 ++ d2) a v = diskUpd d1 a v ++ d2.forall (d1 d2 : list block) (a : nat) (v : block),
a < length d1 ->
diskUpd (d1 ++ d2) a v = diskUpd d1 a v ++ d2
Proof.forall (d1 d2 : list block) (a : nat) (v : block),
a < length d1 ->
diskUpd (d1 ++ d2) a v = diskUpd d1 a v ++ d2
  induction d1; simpl; intros.d2:list block
a:nat
v:block
H:a < 0
diskUpd d2 a v = d2
a:block
d1:list block
IHd1:forall (d2 : list block) (a : nat) (v : block),
a < length d1 ->
diskUpd (d1 ++ d2) a v = diskUpd d1 a v ++ d2
d2:list block
a0:nat
v:block
H:a0 < S (length d1)
match a0 with
| 0 => v :: d1 ++ d2
| S a' => a :: diskUpd (d1 ++ d2) a' v
end =
match a0 with
| 0 => v :: d1
| S a' => a :: diskUpd d1 a' v
end ++ d2
  -d2:list block
a:nat
v:block
H:a < 0
diskUpd d2 a v = d2 lia.
  -a:block
d1:list block
IHd1:forall (d2 : list block) (a : nat) (v : block),
a < length d1 ->
diskUpd (d1 ++ d2) a v = diskUpd d1 a v ++ d2
d2:list block
a0:nat
v:block
H:a0 < S (length d1)
match a0 with
| 0 => v :: d1 ++ d2
| S a' => a :: diskUpd (d1 ++ d2) a' v
end =
match a0 with
| 0 => v :: d1
| S a' => a :: diskUpd d1 a' v
end ++ d2 destruct a0; simpl; auto.a:block
d1:list block
IHd1:forall (d2 : list block) (a : nat) (v : block),
a < length d1 ->
diskUpd (d1 ++ d2) a v = diskUpd d1 a v ++ d2
d2:list block
a0:nat
v:block
H:S a0 < S (length d1)
a :: diskUpd (d1 ++ d2) a0 v =
a :: diskUpd d1 a0 v ++ d2
    rewrite IHd1 by lia; auto.
Qed.

Theorem diskUpd_app2 : forall d1 d2 a v,
    a >= length d1 ->
    diskUpd (d1 ++ d2) a v = d1 ++ diskUpd d2 (a - length d1) v.forall (d1 d2 : list block) (a : nat) (v : block),
a >= length d1 ->
diskUpd (d1 ++ d2) a v =
d1 ++ diskUpd d2 (a - length d1) v
Proof.forall (d1 d2 : list block) (a : nat) (v : block),
a >= length d1 ->
diskUpd (d1 ++ d2) a v =
d1 ++ diskUpd d2 (a - length d1) v
  induction d1; simpl; intros.d2:list block
a:nat
v:block
H:a >= 0
diskUpd d2 a v = diskUpd d2 (a - 0) v
a:block
d1:list block
IHd1:forall (d2 : list block) (a : nat) (v : block),
a >= length d1 ->
diskUpd (d1 ++ d2) a v =
d1 ++ diskUpd d2 (a - length d1) v
d2:list block
a0:nat
v:block
H:a0 >= S (length d1)
match a0 with
| 0 => v :: d1 ++ d2
| S a' => a :: diskUpd (d1 ++ d2) a' v
end = a :: d1 ++ diskUpd d2 (a0 - S (length d1)) v
  -d2:list block
a:nat
v:block
H:a >= 0
diskUpd d2 a v = diskUpd d2 (a - 0) v replace (a-0) with a by lia; auto.
  -a:block
d1:list block
IHd1:forall (d2 : list block) (a : nat) (v : block),
a >= length d1 ->
diskUpd (d1 ++ d2) a v =
d1 ++ diskUpd d2 (a - length d1) v
d2:list block
a0:nat
v:block
H:a0 >= S (length d1)
match a0 with
| 0 => v :: d1 ++ d2
| S a' => a :: diskUpd (d1 ++ d2) a' v
end = a :: d1 ++ diskUpd d2 (a0 - S (length d1)) v destruct a0; simpl; try lia.a:block
d1:list block
IHd1:forall (d2 : list block) (a : nat) (v : block),
a >= length d1 ->
diskUpd (d1 ++ d2) a v =
d1 ++ diskUpd d2 (a - length d1) v
d2:list block
a0:nat
v:block
H:S a0 >= S (length d1)
a :: diskUpd (d1 ++ d2) a0 v =
a :: d1 ++ diskUpd d2 (a0 - length d1) v
    rewrite IHd1 by lia; auto.
Qed.

Theorem diskUpds_app1 : forall d1 d2 n v,
    n+length v < length d1 ->
  diskUpds (d1 ++ d2) n v = diskUpds d1 n v ++ d2.forall (d1 d2 : list block) (n : nat) (v : list block),
n + length v < length d1 ->
diskUpds (d1 ++ d2) n v = diskUpds d1 n v ++ d2
Proof.forall (d1 d2 : list block) (n : nat) (v : list block),
n + length v < length d1 ->
diskUpds (d1 ++ d2) n v = diskUpds d1 n v ++ d2
  intros.d1, d2:list block
n:nat
v:list block
H:n + length v < length d1
diskUpds (d1 ++ d2) n v = diskUpds d1 n v ++ d2
  generalize dependent n.d1, d2, v:list block
forall n : nat,
n + length v < length d1 ->
diskUpds (d1 ++ d2) n v = diskUpds d1 n v ++ d2
  induction v; simpl; auto; intros.d1, d2:list block
a:block
v:list block
IHv:forall n : nat,
n + length v < length d1 -> diskUpds (d1 ++ d2) n v = diskUpds d1 n v ++ d2
n:nat
H:n + S (length v) < length d1
diskUpd (diskUpds (d1 ++ d2) (n + 1) v) n a =
diskUpd (diskUpds d1 (n + 1) v) n a ++ d2
  rewrite IHv by lia.d1, d2:list block
a:block
v:list block
IHv:forall n : nat,
n + length v < length d1 -> diskUpds (d1 ++ d2) n v = diskUpds d1 n v ++ d2
n:nat
H:n + S (length v) < length d1
diskUpd (diskUpds d1 (n + 1) v ++ d2) n a =
diskUpd (diskUpds d1 (n + 1) v) n a ++ d2
  rewrite diskUpd_app1; auto.d1, d2:list block
a:block
v:list block
IHv:forall n : nat,
n + length v < length d1 -> diskUpds (d1 ++ d2) n v = diskUpds d1 n v ++ d2
n:nat
H:n + S (length v) < length d1
n < length (diskUpds d1 (n + 1) v)
  autorewrite with disk_size.d1, d2:list block
a:block
v:list block
IHv:forall n : nat,
n + length v < length d1 -> diskUpds (d1 ++ d2) n v = diskUpds d1 n v ++ d2
n:nat
H:n + S (length v) < length d1
n < diskSize d1
  unfold diskSize; lia.
Qed.

Theorem diskUpds_app2 : forall d1 d2 n v,
  length d1 <= n ->
  diskUpds (d1 ++ d2) n v = d1 ++ diskUpds d2 (n - length d1) v.forall (d1 d2 : list block) (n : nat) (v : list block),
length d1 <= n ->
diskUpds (d1 ++ d2) n v =
d1 ++ diskUpds d2 (n - length d1) v
Proof.forall (d1 d2 : list block) (n : nat) (v : list block),
length d1 <= n ->
diskUpds (d1 ++ d2) n v =
d1 ++ diskUpds d2 (n - length d1) v
  intros.d1, d2:list block
n:nat
v:list block
H:length d1 <= n
diskUpds (d1 ++ d2) n v =
d1 ++ diskUpds d2 (n - length d1) v
  generalize dependent n.d1, d2, v:list block
forall n : nat,
length d1 <= n ->
diskUpds (d1 ++ d2) n v =
d1 ++ diskUpds d2 (n - length d1) v
  induction v; simpl; auto; intros.d1, d2:list block
a:block
v:list block
IHv:forall n : nat,
length d1 <= n ->
diskUpds (d1 ++ d2) n v = d1 ++ diskUpds d2 (n - length d1) v
n:nat
H:length d1 <= n
diskUpd (diskUpds (d1 ++ d2) (n + 1) v) n a =
d1 ++
diskUpd (diskUpds d2 (n - length d1 + 1) v)
  (n - length d1) a
  rewrite IHv by lia.d1, d2:list block
a:block
v:list block
IHv:forall n : nat,
length d1 <= n ->
diskUpds (d1 ++ d2) n v = d1 ++ diskUpds d2 (n - length d1) v
n:nat
H:length d1 <= n
diskUpd (d1 ++ diskUpds d2 (n + 1 - length d1) v) n a =
d1 ++
diskUpd (diskUpds d2 (n - length d1 + 1) v)
  (n - length d1) a
  rewrite diskUpd_app2 by lia.d1, d2:list block
a:block
v:list block
IHv:forall n : nat,
length d1 <= n ->
diskUpds (d1 ++ d2) n v = d1 ++ diskUpds d2 (n - length d1) v
n:nat
H:length d1 <= n
d1 ++
diskUpd (diskUpds d2 (n + 1 - length d1) v)
  (n - length d1) a =
d1 ++
diskUpd (diskUpds d2 (n - length d1 + 1) v)
  (n - length d1) a
  replace (n + 1 - length d1) with (n - length d1 + 1) by lia; auto.
Qed.

Theorem firstn_app_one : forall A (l: list A) n r,
    nth_error l n = Some r ->
    firstn (S n) l = firstn n l ++ r::nil.forall (A : Type) (l : list A) (n : nat) (r : A),
nth_error l n = Some r ->
firstn (S n) l = firstn n l ++ r :: nil
Proof.forall (A : Type) (l : list A) (n : nat) (r : A),
nth_error l n = Some r ->
firstn (S n) l = firstn n l ++ r :: nil
  intros.A:Type
l:list A
n:nat
r:A
H:nth_error l n = Some r
firstn (S n) l = firstn n l ++ r :: nil
  generalize dependent l.A:Type
n:nat
r:A
forall l : list A,
nth_error l n = Some r ->
firstn (S n) l = firstn n l ++ r :: nil
  induction n; destruct l; simpl in *; intros; try congruence.A:Type
n:nat
r:A
IHn:forall l : list A,
nth_error l n = Some r ->
match l with
| nil => nil
| a :: l0 => a :: firstn n l0
end = firstn n l ++ r :: nil
a:A
l:list A
H:nth_error l n = Some r
a
:: match l with
   | nil => nil
   | a :: l => a :: firstn n l
   end = a :: firstn n l ++ r :: nil
  f_equal.A:Type
n:nat
r:A
IHn:forall l : list A,
nth_error l n = Some r ->
match l with
| nil => nil
| a :: l0 => a :: firstn n l0
end = firstn n l ++ r :: nil
a:A
l:list A
H:nth_error l n = Some r
match l with
| nil => nil
| a :: l => a :: firstn n l
end = firstn n l ++ r :: nil
  rewrite IHn; auto.
Qed.

Theorem firstn_log_app_one : forall (log: list block) n r,
    diskGet log n = Some r ->
    firstn (S n) log = firstn (n) log ++ r::nil.forall (log : list block) (n : addr) (r : block),
diskGet log n = Some r ->
firstn (S n) log = firstn n log ++ r :: nil
Proof.forall (log : list block) (n : addr) (r : block),
diskGet log n = Some r ->
firstn (S n) log = firstn n log ++ r :: nil
  intros.log:list block
n:addr
r:block
H:diskGet log n = Some r
firstn (S n) log = firstn n log ++ r :: nil
  generalize dependent log.n:addr
r:block
forall log : list block,
diskGet log n = Some r ->
firstn (S n) log = firstn n log ++ r :: nil
  induction n; destruct log; simpl in *; intros; try congruence.n:nat
r:block
IHn:forall log : list block,
diskGet log n = Some r ->
match log with
| nil => nil
| a :: l => a :: firstn n l
end = firstn n log ++ r :: nil
b:block
log:list block
H:diskGet log n = Some r
b
:: match log with
   | nil => nil
   | a :: l => a :: firstn n l
   end = b :: firstn n log ++ r :: nil
  f_equal.n:nat
r:block
IHn:forall log : list block,
diskGet log n = Some r ->
match log with
| nil => nil
| a :: l => a :: firstn n l
end = firstn n log ++ r :: nil
b:block
log:list block
H:diskGet log n = Some r
match log with
| nil => nil
| a :: l => a :: firstn n l
end = firstn n log ++ r :: nil
  rewrite IHn; auto.
Qed.

We combine all of the above theorems into a hint database called "upd". This means that, when you type autorewrite with upd in some Coq proof, Coq will try to rewrite using all of the hints in that database.

The using part of the hint tells Coq that all of the side conditions associated with the rewrite must be solved using the tactic specified in the using clause. This prevents Coq from applying a rewrite rule if some side condition (like an address being out-of-bounds) cannot be immediately proven.

Ltac solve_disk_size :=
  solve [ autorewrite with disk_size; (auto || lia) ].

Hint Rewrite diskUpd_eq using solve_disk_size : upd.
Hint Rewrite disk_oob_eq using solve_disk_size : upd.
Hint Rewrite diskUpd_oob_eq using solve_disk_size : upd.
Hint Rewrite diskUpd_size : upd.
Hint Rewrite diskUpd_neq using (solve [ auto ]) : upd.
Hint Rewrite diskUpd_comm_lt using solve_disk_size : upd.
Hint Rewrite diskUpd_none using (solve [ auto ]) : upd.

Hint Rewrite diskUpd_same using (solve [ auto ]) : upd.
Hint Rewrite diskUpd_oob_noop using solve_disk_size : upd.
Hint Rewrite diskUpd_twice : upd.

Hint Rewrite diskUpds_neq using solve_disk_size : upd.
Hint Rewrite diskUpds_diskUpd_comm using solve_disk_size : upd.
Hint Rewrite diskUpds_size : upd.

Hint Rewrite diskUpd_diskGets_neq using solve_disk_size : upd.
Hint Rewrite diskUpds_diskGets_neq using solve_disk_size : upd.
Hint Rewrite diskUpds_diskGets_eq using solve_disk_size : upd.

Hint Rewrite diskShrink_size using solve_disk_size : upd.
Hint Rewrite diskShrink_preserves using solve_disk_size : upd.
Hint Rewrite diskShrink_diskUpd_last using solve_disk_size : upd.
Hint Rewrite diskShrink_diskUpd_notlast using solve_disk_size : upd.