• Detailed information about the format of audio data is included in all files. Audio data, in the common case, can be introspected without requiring consulting any kind of external specification. The information provided about audio data includes sampling rate, channel depth and type information, and byte ordering for formats that use components larger than a single octet.
• Ease of parsing. The binary format is designed to facilitate easy and secure parsing without requiring backtracking or unbounded storage use. A competent developer should be able to implement a full parser within a week or two of work.
• Carefully layered metadata. Consumers are not required to understand everything about the underlying audio data in order to make use of it. For example, if audio data is encoded using an unusual and/or proprietary format, consumers can still trivially extract the raw data even if they cannot necessarily understand the data.
• Extensibility. The format consists of explicitly-sized sections with a well-defined ordering. Consumers can trivially skip sections that they do not understand. Sections carry unique 64-bit identifiers; if a section has an identifier not recognized by a consumer, the consumer may skip the section. The raw bytes that comprise a section can be extracted regardless of whether or not the consumer understands them. This specification defines a number of "standard" audio data types that consumers are expected to understand, but the format also allows for declaring new self-describing audio data types.
• Practical metadata. The format provides a standard section that contains UTF-8 encoded keys and values intended to hold arbitrary metadata. Metadata that cannot be expressed as a UTF-8 string can be included as a custom section that can be skipped by consumers that do not recognize it.

Definition divisible8 (x : nat) : Prop :=
  modulo x 8 = 0.

Theorem divisiblity8Add : ∀ (x y : nat),
  divisible8 x → divisible8 y → divisible8 (x + y).
Proof.
  (* Proof omitted for brevity; see Divisible8.v for proofs. *)
Qed.

Inductive bit : Set :=
  | B0
  | B1.

Inductive octet : Set :=
  | OctExact  : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet
  | OctRemain : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet.

Fixpoint octetsBigEndianAux
  (bits   : list bit)
  (octets : list octet)
: list octet :=
  match bits with
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest) =>
    octets ++ [OctExact b7 b6 b5 b4 b3 b2 b1 b0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 b2 b1 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 b2 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: rest) =>
    octets ++ [OctRemain b7 b6 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: rest) =>
    octets ++ [OctRemain b7 B0 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | [] =>
    octets
  end.

Definition octetsBigEndian (bits : list bit) : list octet :=
  octetsBigEndianAux bits [].

Definition octetsLittleEndian (bits : list bit) : list octet :=
  rev (octetsBigEndianAux bits []).

Theorem octetsBigEndianLengthDivisibleAllExact : forall (b : list bit),
  divisible8 (length b) -> Forall octetIsExact (octetsBigEndian b).
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.

Theorem octetsLittleEndianLengthDivisibleAllExact : forall (b : list bit),
  divisible8 (length b) -> Forall octetIsExact (octetsLittleEndian b).
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.

Theorem octetsBigEndianLengthIndivisibleRemainder : forall (b : list bit),
  0 < length b mod 8 -> ∃ o, In o (octetsBigEndian b) ∧ octetIsRemainder o.
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.

Theorem octetsLittleEndianLengthIndivisibleRemainder : forall (b : list bit),
  0 < length b mod 8 -> ∃ o, In o (octetsLittleEndian b) ∧ octetIsRemainder o.
Proof.
  (* Proof omitted for brevity; see OctetOrder.v for proofs. *)
Qed.

Fixpoint intersectionPairs
  {A     : Set}
  (f     : A -> list A -> option A)
  (ea eb : list A)
: list (A * A) :=
  match ea with
  | nil => nil
  | cons a ea_rest =>
    match f a eb with
    | Some r => (a, r) :: intersectionPairs f ea_rest eb
    | None   =>           intersectionPairs f ea_rest eb
    end
  end.

Definition finds
  {A  : Set}
  (f  : A -> list A -> option A)
  (x  : A)
  (y  : A)
  (ys : list A)
: Prop :=
  f x ys = Some y <-> In y ys.

Theorem intersectionPairsIn : forall (A : Set) (ea eb : list A) efa efb f,
  (forall x y ys, finds f x y ys) ->
    In (efa, efb) (intersectionPairs f ea eb) ->
      In efa ea /\ In efb eb.
Proof.
  (* Proof omitted for brevity; see Intersection.v for proofs. *)
Qed.

Definition isNormalized (x : R) : Prop :=
  0 <= x /\ x <= 1.

Theorem isNormalizedMult : forall x y,
  isNormalized x -> isNormalized y -> isNormalized (Rmult x y).
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.

Definition between
  (x    : R)
  (low  : R)
  (high : R)
: R :=
  let n := x - low in
  let d := high - low in
    match Reqb d 0 with
    | true  => x
    | false => n / d
    end.

Theorem betweenNorm : forall x lo hi,
  lo < hi
    -> lo <= x <= hi
      -> isNormalized (between x lo hi).
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.

Definition interpolate
  (x : R)
  (y : R)
  (f : R)
: R :=
  (x * (1 - f)) + (y * f).

Lemma interpolateRange1 : forall x y f,
  x <= y
    -> isNormalized f
      -> x <= interpolate x y f <= y.
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.

Lemma interpolateRange2 : forall x y f,
  y <= x
    -> isNormalized f
      -> y <= interpolate x y f <= x.
Proof.
  (* Proof omitted for brevity; see Interpolation.v for proofs. *)
Qed.

Inductive hashValue : Set := hashValueMake {
  hvAlgorithm : hashAlgorithm;
  hvValue     : string
}.

Inductive hashAlgorithm : Set :=
  | HA_SHA256
  .

Definition descriptor := string.

Class describable (A : Set) := {
  descriptorOf : A -> descriptor
}.

([a-z][a-z0-9_-]{0,63})(\.[a-z][a-z0-9_-]{0,62}){0,15}

• Use of semantic versioning in the file format definition. The inclusion of major and minor semantic version numbers into the file format itself means that software can know, unambiguously, whether or not it can open a given file based on the contents of the file header alone.
• A strict, unambiguous, mathematical specification of the structure and semantics of the format. This means that, long after the aurantium software has died, developers of the future can write new implementations with behaviour that they know correctly handles the format.
• The inclusion of unique identifiers and version numbers into each file; once an audio map has been created, it is considered to be immutable. Editing an audio map entails creating a new version of the existing one with an incremented version number. This allows applications to specify exact, versioned dependencies on audio map files in much the same way as software development tools can specify versioned dependencies on software libraries.
• An exact and precise description of which changes are considered to be "compatible" changes, and which changes are considered to be "incompatible". This means that new versions of files cannot be released that will silently break compatibility with existing consumers; the tools around the file format will catch these mistakes before publication.

Inductive identifier : Set := identifierMake {
  idName              : string;
  idVersionMajor      : nat;
  idVersionMinor      : nat;
  idVersionMajorRange : idVersionMajor <= 4294967295;
  idVersionMinorRange : idVersionMinor <= 4294967295
}.
(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Inductive compatVersionChange : Set :=
  (** No version change is required. *)
  | CVersionChangeNone
  (** The change requires a minor version number increment. *)
  | CVersionChangeMinor
  (** The change required a major version number increment. *)
  | CVersionChangeMajor
  .

Definition compatVersionChangeMax
  (x y : compatVersionChange) 
: compatVersionChange :=
  match (x, y) with
  | (CVersionChangeMajor , _                  ) => CVersionChangeMajor
  | (_                   , CVersionChangeMajor) => CVersionChangeMajor
  | (CVersionChangeMinor , CVersionChangeNone ) => CVersionChangeMinor
  | (CVersionChangeNone  , CVersionChangeMinor) => CVersionChangeMinor
  | (CVersionChangeMinor , CVersionChangeMinor) => CVersionChangeMinor
  | (CVersionChangeNone  , CVersionChangeNone ) => CVersionChangeNone
  end.

Theorem compatVersionChangeMaxRefl : forall x,
  compatVersionChangeMax x x = x.
Proof.
  (* Proof omitted for brevity; see Compatibility.v for proofs. *)
Qed.

Theorem compatVersionChangeMaxComm : forall x y,
  compatVersionChangeMax x y = compatVersionChangeMax y x.
Proof.
  (* Proof omitted for brevity; see Compatibility.v for proofs. *)
Qed.

Theorem compatVersionChangeMaxAssoc : forall x y z,
  compatVersionChangeMax x (compatVersionChangeMax y z) = compatVersionChangeMax (compatVersionChangeMax x y) z.
Proof.
  (* Proof omitted for brevity; see Compatibility.v for proofs. *)
Qed.

• The format of the audio data, such as unsigned pulse code modulation, signed pulse code modulation, FLAC, and etc.
• The sample rate of the audio data, expressed as samples per second.
• The sample depth of the audio data, expressed as bits per sample.
• The number of channels in the audio data.
• The octet order of the audio data, assuming the sample depth is greater than 8 bits.
• The size of the audio data, expressed in octets.

• An amplitude value of -1 will be encoded as -32768.
• An amplitude value of 0 will be encoded as 0.
• An amplitude value of 1 will be encoded as 32767.

• An amplitude value of -1 will be encoded as 0.
• An amplitude value of 0 will be encoded as 32768.
• An amplitude value of 1 will be encoded as 65536.

Definition pcmIntegerEncodeSigned
  (depth     : nat)
  (amplitude : R)
: R :=
  match Rle_dec 0 amplitude with
  | left _  => Rmult amplitude ((pow 2 (depth - 1)) - 1)
  | right _ => Rmult amplitude (pow 2 (depth - 1))
  end.

Definition pcmIntegerEncodeUnsigned
  (depth     : nat)
  (amplitude : R)
: R :=
  let s : R := Rplus (Rdiv amplitude 2%R) 0.5%R in
    Rmult s (pow 2 depth).

Inductive audioFormatType : Set :=
  (** Pulse code modulation using signed values. *)
  | AFPCMLinearIntegerSigned : audioFormatType
  (** Pulse code modulation using unsigned values. *)
  | AFPCMLinearIntegerUnsigned : audioFormatType
  (** Pulse code modulation using floating point values. *)
  | AFPCMLinearFloat : audioFormatType
  (** FLAC-compressed audio. *)
  | AFFlac : audioFormatType
  (** A format not known by this specification. *)
  | AFUnknown : descriptor -> audioFormatType
  .

Inductive clip : Set := clipMake {
  (** The unique identifier for the clip. *)
  clipId : nat;
  (** The clip name, for descriptive purposes. *)
  clipName : string;
  (** The clip audio format name. *)
  clipFormat : audioFormatType;
  (** The sample rate in bits per second. *)
  clipSampleRate : nat;
  (** The clip sample depth in bits per clip. *)
  clipSampleDepth : nat;
  (** The number of channels in the clip. *)
  clipChannels : nat;
  (** The endianness of the audio data. *)
  clipEndianness : octetOrder;
  (** The hash of the audio data. *)
  clipHash : hashValue;
  (** The offset of the first octet of audio data. *)
  clipOffset : nat;
  (** The size of the audio data in octets. *)
  clipSize : nat
}.

Definition clipInvariants (c : clip) : Prop :=
     (clipId          c <= 4294967295)
  /\ (clipSampleRate  c <= 4294967295)
  /\ (clipSampleDepth c <= 4294967295)
  /\ (clipChannels    c <= 4294967295)
  /\ (clipOffset      c <= 18446744073709551615)
  /\ (clipSize        c <= 18446744073709551615)
  .

Inductive clips : Set := clipsMake {
  clipsList         : list clip;
  clipsIdSorted     : clipsListIdIsSorted clipsList;
  clipsOffsetSorted : clipsListOffsetIsSorted clipsList;
}.

Inductive clipsListIdIsSorted : list clip -> Prop :=
  | ClipIdOne  : forall s,
      clipsListIdIsSorted [s]
  | ClipIdCons : forall s0 s1 ss,
    (clipId s0) < (clipId s1) ->
      clipsListIdIsSorted (s0 :: ss) ->
        clipsListIdIsSorted (s1 :: s0 :: ss).

Inductive clipsListOffsetIsSorted : list clip -> Prop :=
  | ClipOffsetOne : forall s,
    clipsListOffsetIsSorted [s]
  | ClipOffsetCons : forall s0 s1 ss,
    ((clipOffset s1) + (clipSize s1)) < clipOffset s0 ->
      clipsListOffsetIsSorted (s0 :: ss) ->
        clipsListOffsetIsSorted (s1 :: s0 :: ss).

Lemma clipsNonEmpty : forall (s : clips),
  [] <> clipsList s.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.

Definition clipsCompatCompareFull
  (ca cb : list clip)
: list compatVersionChangeRecord :=
  let f              := (fun c cs => clipForId (clipId c) cs) in
  let removed        := clipsRemoved ca cb in
  let added          := clipsAdded ca cb in
  let changed        := intersectionPairs f ca cb in
  let removedChanges := clipsCompatCompareRemoved removed in
  let addedChanges   := clipsCompatCompareAdded added in
  let changedChanges := clipsCompatCompareChanged changed in
    removedChanges ++ addedChanges ++ changedChanges.

Definition clipsRemoved
  (ca : list clip)
  (cb : list clip)
: list clip :=
  filter (fun c =>
    match clipForId (clipId c) cb with
    | None   => false
    | Some _ => true
    end) ca.

Theorem clipsCompatCompareMajor0 : forall ca cb,
  [] <> clipsRemoved ca cb ->
    compatVersionChangeRecordsMaximum (clipsCompatCompareFull ca cb)
      = CVersionChangeMajor.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.

Definition clipsAdded
  (ca : list clip)
  (cb : list clip)
: list clip :=
  clipsRemoved cb ca.

Theorem clipsCompatCompareMinor0 : forall ca cb,
  [] = clipsRemoved ca cb ->
    [] <> clipsAdded ca cb ->
      (forall f, [] = intersectionPairs f ca cb) ->
        compatVersionChangeRecordsMaximum (clipsCompatCompareFull ca cb)
          = CVersionChangeMinor.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.

Theorem clipEqDec : forall (x y : clip),
  {x = y}+{x <> y}.
Proof.
  (* Proof omitted for brevity; see Clip.v for proofs. *)
Qed.

Definition clipCompatCompare
  (c0 c1 : clip)
: compatVersionChangeRecord :=
  match clipEqDec c0 c1 with
  | left _ => 
    CVRMake CVersionChangeNone ""
  | right _ => 
    CVRMake CVersionChangeMajor "The values of the clip were changed."
  end.

Definition clipsCompatCompareChanged
  (r : list (clip * clip))
: list compatVersionChangeRecord :=
  map (fun p => clipCompatCompare (fst p) (snd p)) r.

Inductive keyAssignment : Set := {
  (** The unique identifier of the key assignment. *)
  kaId : nat;
  (** The lowest key value that will trigger this clip. *)
  kaValueStart : nat;
  (** The key value at which the clip plays at the normal playback rate. *)
  kaValueCenter: nat;
  (** The highest key value that will trigger this clip. *)
  kaValueEnd : nat;
  kaValueEndRange : le kaValueEnd 294967295;
  (** The key values must be ordered. *)
  kaValueStartOrder : le kaValueStart kaValueCenter;
  kaValueCenterOrder : le kaValueCenter kaValueEnd;
  (** The clip that will be triggered. *)
  kaClipId : nat;
  (** The amplitude at which this clip will be played when at the lowest key value. *)
  kaAmplitudeAtKeyStart : R;
  (** The amplitude at which this clip will be played when at the center key value. *)
  kaAmplitudeAtKeyCenter : R;
  (** The amplitude at which this clip will be played when at the highest key value. *)
  kaAmplitudeAtKeyEnd : R;
  (** The amplitude values are normalized values. *)
  kaAmplitudeAtKeyStartNormal : isNormalized kaAmplitudeAtKeyStart;
  kaAmplitudeAtKeyCenterNormal : isNormalized kaAmplitudeAtKeyCenter;
  kaAmplitudeAtKeyEndNormal : isNormalized kaAmplitudeAtKeyEnd;
  (** The velocity value at which this clip starts to be triggered. *)
  kaAtVelocityStart : R;
  (** The velocity value at which the amplitude of this clip is at maximum. *)
  kaAtVelocityCenter : R;
  (** The velocity value at which this clip stops being triggered. *)
  kaAtVelocityEnd : R;
  (** The velocity values are normalized values and are correctly ordered. *)
  kaAtVelocityStartNormal : isNormalized kaAtVelocityStart;
  kaAtVelocityCenterNormal : isNormalized kaAtVelocityCenter;
  kaAtVelocityEndNormal : isNormalized kaAtVelocityEnd;
  kaAtVelocityStartOrder : kaAtVelocityStart <= kaAtVelocityCenter;
  kaAtVelocityCenterOrder : kaAtVelocityCenter <= kaAtVelocityEnd;
  (** The amplitude at which this clip will be played when at the starting velocity value. *)
  kaAmplitudeAtVelocityStart : R;
  (** The amplitude at which this clip will be played when at the center velocity value. *)
  kaAmplitudeAtVelocityCenter : R;
  (** The amplitude at which this clip will be played when at the end velocity value. *)
  kaAmplitudeAtVelocityEnd : R;
  (** The amplitude values are normalized values. *)
  kaAmplitudeAtVelocityStartNormal : isNormalized kaAmplitudeAtVelocityStart;
  kaAmplitudeAtVelocityCenterNormal : isNormalized kaAmplitudeAtVelocityCenter;
  kaAmplitudeAtVelocityEndNormal : isNormalized kaAmplitudeAtVelocityEnd;
  (** The associated key assignment flags. *)
  kaFlags : list keyAssignmentFlag;
  kaFlagsUnique : NoDup kaFlags;
}.

Inductive keyEvaluation : Set := keyEvaluationMake {
  keyEvaluationClipId                  : nat;
  keyEvaluationVelocityAmplitude       : R;
  keyEvaluationVelocityAmplitudeNormal : isNormalized keyEvaluationVelocityAmplitude;
  keyEvaluationKeyAmplitude            : R;
  keyEvaluationKeyAmplitudeNormal      : isNormalized keyEvaluationKeyAmplitude;
  keyEvaluationRate                    : R;
  keyEvaluationRateNonNegative         : 0 <= keyEvaluationRate
}.

Definition keyAssignmentMatches
  (key        : nat)
  (velocity   : R)
  (assignment : keyAssignment)
: Prop :=
  let p0 := ((kaValueStart assignment) <= key)%nat in
  let p1 := (key <= (kaValueEnd assignment))%nat in
  let p2 := ((kaAtVelocityStart assignment) <= velocity)%R in
  let p3 := (velocity <= (kaAtVelocityEnd assignment))%R in
    p0 /\ p1 /\ p2 /\ p3.

Theorem keyAssignmentMatchesDecidable : forall k v a,
  {keyAssignmentMatches k v a}+{~keyAssignmentMatches k v a}.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Definition keyAssignmentEvaluateAmplitudeForKey
  (key        : nat)
  (assignment : keyAssignment)
: R :=
  let kLow := kaValueStart assignment in
  let kMid := kaValueCenter assignment in
  let kTop := kaValueEnd assignment in
    match Nat.compare key kMid with
    | Eq => kaAmplitudeAtKeyCenter assignment
    | Lt =>
      match lt_dec kLow kMid with
      | right _  => kaAmplitudeAtKeyCenter assignment
      | left _ =>
        let f := between (INR key) (INR kLow) (INR kMid) in
          interpolate
            (kaAmplitudeAtKeyStart assignment)
            (kaAmplitudeAtKeyCenter assignment)
            f
      end
    | Gt =>
      match lt_dec kMid kTop with
      | right _  => kaAmplitudeAtKeyCenter assignment
      | left _ =>
        let f := between (INR key) (INR kMid) (INR kTop) in
          interpolate
            (kaAmplitudeAtKeyCenter assignment)
            (kaAmplitudeAtKeyEnd assignment)
            f
      end
    end.

Theorem keyAssignmentEvaluateAmplitudeForKeyNormalized : forall k v a,
  keyAssignmentMatches k v a
    -> isNormalized (keyAssignmentEvaluateAmplitudeForKey k a).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Definition keyAssignmentEvaluateAmplitudeForVelocity
  (velocity   : R)
  (assignment : keyAssignment)
: R :=
  let kLow := kaAtVelocityStart assignment in
  let kMid := kaAtVelocityCenter assignment in
  let kTop := kaAtVelocityEnd assignment in
    match Rcompare velocity kMid with
    | Eq => kaAmplitudeAtVelocityCenter assignment
    | Lt =>
      match Rlt_dec kLow kMid with
      | left _ =>
        let f := between velocity kLow kMid in
          interpolate
            (kaAmplitudeAtVelocityStart assignment)
            (kaAmplitudeAtVelocityCenter assignment)
            f
      | right _ =>
          (kaAmplitudeAtVelocityCenter assignment)
      end
    | Gt =>
      match Rlt_dec kMid kTop with
      | left _ =>
        let f := between velocity kMid kTop in
          interpolate
            (kaAmplitudeAtVelocityCenter assignment)
            (kaAmplitudeAtVelocityEnd assignment)
            f
      | right _ =>
          (kaAmplitudeAtVelocityCenter assignment)
      end
    end.

Theorem keyAssignmentEvaluateAmplitudeForVelocityNormalized : forall k v a,
  keyAssignmentMatches k v a
    -> isNormalized (keyAssignmentEvaluateAmplitudeForVelocity v a).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Definition semitonesPitchRatio (semitones : R) : R :=
  Rpower 2.0 (Rdiv semitones 12.0).

Definition keyAssignmentEvaluateRate
  (key        : nat)
  (assignment : keyAssignment)
: R :=
  match (in_dec keyAssignmentFlagEqDec FlagUnpitched (kaFlags assignment)) with
  | left _  => 1.0
  | right _ =>
    let kLow := kaValueStart assignment in
    let kMid := kaValueCenter assignment in
      match Nat.compare key kMid with
      | Eq => 1
      | Lt =>
        let delta := minus kMid key in
          semitonesPitchRatio (-(INR delta))
      | Gt =>
        let delta := minus key kMid in
          semitonesPitchRatio (INR delta)
      end
  end.

Theorem keyAssignmentEvaluateRateNonNegative : forall k v a,
  keyAssignmentMatches k v a
    -> Rle 0 (keyAssignmentEvaluateRate k a).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Definition keyAssignmentEvaluateFull
  (key        : nat)
  (velocity   : R)
  (assignment : keyAssignment)
: option keyEvaluation :=
  match keyAssignmentMatchesDecidable key velocity assignment with
  | right _ => None
  | left p  =>
    let clip  := kaClipId assignment in
    let ampV  := keyAssignmentEvaluateAmplitudeForVelocity velocity assignment in
    let ampVP := keyAssignmentEvaluateAmplitudeForVelocityNormalized _ _ _ p in
    let ampK  := keyAssignmentEvaluateAmplitudeForKey key assignment in
    let ampKP := keyAssignmentEvaluateAmplitudeForKeyNormalized _ _ _ p in
    let rate  := keyAssignmentEvaluateRate key assignment in
    let rateP := keyAssignmentEvaluateRateNonNegative _ _ _ p in
      Some (keyEvaluationMake clip ampV ampVP ampK ampKP rate rateP)
  end.

Inductive keyAssignments : Set := {
  kasList       : list keyAssignment;
  kasListSorted : keyAssignmentListIsSorted kasList
}.

Inductive keyAssignmentListIsSorted : list keyAssignment -> Prop :=
  | kaListNone : keyAssignmentListIsSorted []
  | kaListOne : forall s, keyAssignmentListIsSorted [s]
  | kaListCons : forall s0 s1 s,
    lt (kaId s0) (kaId s1) ->
      keyAssignmentListIsSorted (s0 :: s) ->
        keyAssignmentListIsSorted (s1 :: s0 :: s).

Fixpoint keyAssignmentForId
  (i  : nat)
  (ka : list keyAssignment)
: option keyAssignment :=
  match ka with
  | nil         => None
  | cons a rest =>
    match Nat.eq_dec (kaId a) i with
    | left _  => Some a
    | right _ => keyAssignmentForId i rest
    end
  end.

Definition keyAssignmentsCompatCompareFull
  (ka kb : list keyAssignment)
: list compatVersionChangeRecord :=
  let f              := (fun k ks => keyAssignmentForId (kaId k) ks) in
  let removed        := keyAssignmentsRemoved ka kb in
  let added          := keyAssignmentsAdded ka kb in
  let changed        := intersectionPairs f ka kb in
  let removedChanges := keyAssignmentsCompatCompareRemoved removed in
  let addedChanges   := keyAssignmentsCompatCompareAdded added kb in
  let changedChanges := keyAssignmentsCompatCompareChanged changed in
    removedChanges ++ addedChanges ++ changedChanges.

Fixpoint keyAssignmentsRemoved
  (ka : list keyAssignment)
  (kb : list keyAssignment)
: list keyAssignment :=
  match ka with
  | nil => []
  | cons a rest =>
    match keyAssignmentForId (kaId a) kb with
    | None   => cons a (keyAssignmentsRemoved rest kb)
    | Some _ => keyAssignmentsRemoved rest kb
    end
  end.

Theorem keyAssignmentsCompatCompareMajor0 : forall ka kb,
  [] <> keyAssignmentsRemoved ka kb ->
    compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
      = CVersionChangeMajor.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Definition keyAssignmentsOverlap (x y : keyAssignment) : Prop :=
  let x1 := kaValueStart x in
  let x2 := kaValueEnd x in
  let y1 := kaValueStart y in
  let y2 := kaValueEnd y in
    ge x2 y1 /\ ge y2 x1.

Theorem keyAssignmentsOverlapReflexive : forall x,
  keyAssignmentsOverlap x x.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Theorem keyAssignmentsOverlapCommutative : forall x y,
  keyAssignmentsOverlap x y -> keyAssignmentsOverlap y x.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Theorem keyAssignmentsOverlapDecidable : forall x y,
  {keyAssignmentsOverlap x y}+{~keyAssignmentsOverlap x y}.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Definition keyAssignmentsOverlapping
  (k  : keyAssignment)
  (ka : list keyAssignment)
: list keyAssignment :=
  filter (fun j =>
    match keyAssignmentsOverlapDecidable k j with
    | left _ =>
      match Nat.eq_dec (kaId k) (kaId j) with
      | left _  => false
      | right _ => true
      end
    | right _ => false
    end) ka.

Theorem keyAssignmentsOverlappingNotSelf : forall k ka,
  ~In k (keyAssignmentsOverlapping k ka).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Theorem keyAssignmentsOverlappingFind0 : forall k ka p,
  (In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p))
    -> In p (keyAssignmentsOverlapping k ka).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Theorem keyAssignmentsOverlappingFind1 : forall k ka p,
  In p (keyAssignmentsOverlapping k ka) ->
    In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Theorem keyAssignmentsOverlappingFind : forall k ka p,
  (In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p))
    <-> In p (keyAssignmentsOverlapping k ka).
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Definition keyAssignmentsAdded
  (ka : list keyAssignment)
  (kb : list keyAssignment)
: list keyAssignment :=
  keyAssignmentsRemoved kb ka.

Definition keyAssignmentsCompatCompareAdd
  (k  : keyAssignment)
  (ka : list keyAssignment)
: compatVersionChangeRecord :=
  match keyAssignmentsOverlapping k ka with
  | nil => CVRMake CVersionChangeMinor "A key assignment was added."
  | _   => CVRMake CVersionChangeMajor "A key assignment was added that overlaps with an existing assignment."
  end.

Theorem keyAssignmentsCompatCompareMajor1 : forall ka kb k,
  [] = keyAssignmentsRemoved ka kb ->
    (forall f, [] = keyAssignmentsCompatCompareChanged (intersectionPairs f ka kb)) ->
      In k (keyAssignmentsAdded ka kb) ->
        [] <> (keyAssignmentsOverlapping k kb) ->
        compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
          = CVersionChangeMajor.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Theorem keyAssignmentsCompatCompareMinor0 : forall ka kb,
  [] = keyAssignmentsRemoved ka kb ->
    (forall f, [] = keyAssignmentsCompatCompareChanged (intersectionPairs f ka kb)) ->
      [] <> (keyAssignmentsAdded ka kb) ->
        Forall (fun j => [] = keyAssignmentsOverlapping j kb) (keyAssignmentsAdded ka kb) ->
          compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
           = CVersionChangeMinor.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Definition keyAssignmentValuesEq (x y : keyAssignment) : Prop :=
     (kaId x)                        = (kaId y)
  /\ (kaValueStart x)                = (kaValueStart y)
  /\ (kaValueCenter x)               = (kaValueCenter y)
  /\ (kaValueEnd x)                  = (kaValueEnd y)
  /\ (kaClipId x)                    = (kaClipId y)
  /\ (kaAmplitudeAtKeyStart x)       = (kaAmplitudeAtKeyStart y)
  /\ (kaAmplitudeAtKeyCenter x)      = (kaAmplitudeAtKeyCenter y)
  /\ (kaAmplitudeAtKeyEnd x)         = (kaAmplitudeAtKeyEnd y)
  /\ (kaAtVelocityStart x)           = (kaAtVelocityStart y)
  /\ (kaAtVelocityCenter x)          = (kaAtVelocityCenter y)
  /\ (kaAtVelocityEnd x)             = (kaAtVelocityEnd y)
  /\ (kaAmplitudeAtVelocityStart x)  = (kaAmplitudeAtVelocityStart y)
  /\ (kaAmplitudeAtVelocityCenter x) = (kaAmplitudeAtVelocityCenter y)
  /\ (kaAmplitudeAtVelocityEnd x)    = (kaAmplitudeAtVelocityEnd y)
  /\ (kaFlags x)                     = (kaFlags y)
.

Theorem keyAssignmentValuesEqDec
  (x y : keyAssignment)
: {keyAssignmentValuesEq x y}+{~keyAssignmentValuesEq x y}.
Proof.
  (* Proof omitted for brevity; see KeyMapping.v for proofs. *)
Qed.

Definition keyAssignmentCompatCompare
  (k0 k1 : keyAssignment)
: compatVersionChangeRecord :=
  match keyAssignmentValuesEqDec k0 k1 with
  | left _ => 
    CVRMake CVersionChangeNone ""
  | right _ => 
    CVRMake CVersionChangeMajor "The values of the key assignment were changed."
  end.

Definition keyAssignmentsCompatCompareChanged
  (r : list (keyAssignment * keyAssignment))
: list compatVersionChangeRecord :=
  map (fun p => keyAssignmentCompatCompare (fst p) (snd p)) r.

Definition keyAssignmentReferencesClip
  (k : keyAssignment)
  (s : clip)
: Prop :=
  (kaClipId k) = (clipId s).

Definition keyAssignmentReferencesExists
  (k : keyAssignment)
  (s : clips)
: Prop :=
  exists p, keyAssignmentReferencesClip k p /\ In p (clipsList s).

Definition keyAssignmentsReferences
  (k : keyAssignments)
  (s : clips)
: Prop :=
  forall p, In p (kasList k) -> keyAssignmentReferencesExists p s.

Definition clipsReferenced
  (k  : keyAssignments)
  (ss : clips)
: Prop :=
  Forall (fun s => exists a, keyAssignmentReferencesClip a s /\ In s (clipsList ss)) (clipsList ss).

Inductive audioMap : Set := {
  amIdentifier               : identifier;
  amClips                    : clips;
  amKeyAssignments           : keyAssignments;
  amKeyAssignmentsReferences : keyAssignmentsReferences amKeyAssignments amClips;
  amClipsReferenced          : clipsReferenced amKeyAssignments amClips;
}.

Inductive metadataValue : Set := MetadataValue {
  mKey   : string;
  mValue : string
}.

Inductive metadata : Set := Metadata {
  mValues : list metadataValue
}.

Inductive binaryExp : Set :=
    (** A 32-bit unsigned integer. *)
    | BiU32     : nat -> binaryExp
    (** A 64-bit unsigned integer. *)
    | BiU64     : nat -> binaryExp
    (** A 64-bit IEEE754 binary64 value. *)
    | BiF64     : R -> binaryExp
    (** A sequence of bytes. *)
    | BiBytes   : list byte -> binaryExp
    (** A sequence of bytes describing UTF-8 encoded text. *)
    | BiUTF8    : list byte -> binaryExp
    (** An array of binary expressions. *)
    | BiArray   : list binaryExp -> binaryExp
    (** A section of reserved space. *)
    | BiReserve : nat -> binaryExp
    (** A record with named binary expression members. *)
    | BiRecord  : list (string * binaryExp) -> binaryExp.

Fixpoint binarySize (b : binaryExp) : nat :=
  match b with
  | BiU32 _     => 4
  | BiU64 _     => 8
  | BiF64 _     => 8
  | BiBytes s   => 4 + asMultipleOf4 (length s)
  | BiUTF8 s    => 4 + asMultipleOf4 (length s)
  | BiArray f   => 4 + fold_right plus 0 (map binarySize f)
  | BiReserve s => asMultipleOf4 s
  | BiRecord f  => fold_right plus 0 (map (compose binarySize snd) f)
  end.

Definition asMultipleOf (size q : nat) (Hnz : 0 ≠ q) : nat :=
  let r := size / q in
    match Nat.ltb_spec0 r q with
    | ReflectT _ _ => (r + 1) * q
    | ReflectF _ _ => r * q
    end.

Theorem binarySizeMultiple4 : forall b, binarySize (b) mod 4 = 0.
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.

Definition binarySizePadded16 (b : binaryExp) : nat :=
  asMultipleOf16 (binarySize b).

Definition asMultipleOf4 (size : nat) : nat :=
  asMultipleOf size 4 p0not4.

Inductive streamE : Set :=
  (** A 64-bit IEEE754 binary64 value. *)
  | Vf64 : R -> streamE
  (** A 64-bit unsigned integer. *)
  | Vu64 : nat -> streamE
  (** A 32-bit unsigned integer. *)
  | Vu32 : nat -> streamE
  (** An 8-bit unsigned integer. *)
  | Vu8  : nat -> streamE.

Fixpoint binaryEval (b : binaryExp) : list streamE :=
  match b with
  | BiU32 k     => [Vu32 k]
  | BiU64 k     => [Vu64 k]
  | BiF64 k     => [Vf64 k]
  | BiBytes s   => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4)
  | BiUTF8 s    => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4)
  | BiArray f   => (Vu32 (length f)) :: concat (map binaryEval f)
  | BiReserve s => repeat (Vu8 0) (asMultipleOf4 s)
  | BiRecord f  => concat (map (compose binaryEval snd) f)
  end.

Definition binaryEvalPaddedBytes
  (b     : list byte)
  (align : nat)
  (Hneq  : 0 <> align)
: list streamE :=
  let vremaining := length b mod align in
    match vremaining with
    | 0 => map u8byte b
    | _ => map u8byte (b ++ repeat x00 (align - vremaining))
    end.

• s is empty.
• s consists of a single IEEE754 binary64 value.
• s consists of a single 64-bit integer.
• s consists of a single 32-bit integer.
• s consists of a sequence of n 8-bit integers, where n is evenly divisible by 4.
• s is the concatenation of a well-formed stream t and a well-formed stream u.

Inductive streamWellFormed : list streamE -> Prop :=
  (** An empty stream is well-formed. *)
  | BEPEmpty  : streamWellFormed []
  (** A stream consisting of a single 64-bit float is well-formed. *)
  | BEPVf64   : forall k, streamWellFormed [Vf64 k]
  (** A stream consisting of a single 64-bit integer is well-formed. *)
  | BEPVu64   : forall k, streamWellFormed [Vu64 k]
  (** A stream consisting of a single 32-bit integer is well-formed. *)
  | BEPVu32   : forall k, streamWellFormed [Vu32 k]
  (** A stream consisting of a number of 8-bit values of a length divisible by 4 is well-formed. *)
  | BEPVu8s   : forall es, Forall streamEIsU8 es -> length (es) mod 4 = 0 -> streamWellFormed es
  (** The concatenation of two well-formed streams is well-formed. *)
  | BEPAppend : forall xs ys, streamWellFormed xs -> streamWellFormed ys -> streamWellFormed (xs ++ ys).

Theorem binaryEvalStreamsWellFormed : forall b,
  streamWellFormed (binaryEval b).
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.

Theorem streamsWellFormedDivisible4 : forall es,
  streamWellFormed es -> streamSize es mod 4 = 0.
Proof.
  (* Proof omitted for brevity; see Binary.v for proofs. *)
Qed.

Definition binaryExpFileHeader : binaryExp :=
  BiRecord [
    ("id",           u64 0x894155520D0A1A0A);
    ("versionMajor", u32 1);
    ("versionMinor", u32 0)
  ].

Definition binaryIdentifier (i : identifier) : binaryExp :=
  BiRecord [
    ("name",         utf8 (idName i));
    ("versionMajor", u32 (idVersionMajor i));
    ("versionMinor", u32 (idVersionMinor i))
  ].

Definition binaryIdentifierSection (i : identifier) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D5F494421);
    ("size", u64 (binarySizePadded16 (binaryIdentifier i)));
    ("data", binaryIdentifier i)
  ].

Definition binaryClip (c : clip) : binaryExp :=
  BiRecord [
    ("id",          u32 (clipId c));
    ("name",        utf8 (clipName c));
    ("format",      utf8 (descriptorOf (clipFormat c)));
    ("sampleRate",  u32 (clipSampleRate c));
    ("sampleDepth", u32 (clipSampleDepth c));
    ("channels",    u32 (clipChannels c));
    ("endianness",  utf8 (descriptorOf (clipEndianness c)));
    ("hash",        binaryHash (clipHash c));
    ("offset",      u64 (clipOffset c));
    ("size",        u64 (clipSize c))
  ].

Definition binaryHash (h : hashValue) : binaryExp :=
  BiRecord [
    ("algorithm", utf8 (descriptorOf (hvAlgorithm h)));
    ("value",     utf8 (hvValue h))
  ].

Definition binaryClips (c : clips) : binaryExp :=
  BiArray (map binaryClip (clipsList c)).

Definition binaryClipsSectionData (c : clips) : binaryExp :=
  let audioDataStart  := clipOffset (clipFirst c) in
  let encClips        := binaryClips c in
  let encClipsSize    := binarySize encClips in
  let encClipsPad     := audioDataStart - encClipsSize in
  let audioDataSize   := clipAudioDataSizeTotal c in
  let audioDataSize16 := asMultipleOf16 audioDataSize in
    BiRecord [
      ("clips",     encClips);
      ("clipsPad",  BiReserve encClipsPad);
      ("clipsData", BiReserve audioDataSize16)
    ].

Definition binaryClipsSection (c : clips) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D434C4950);
    ("size", u64 (binarySizePadded16 (binaryClipsSectionData c)));
    ("data", binaryClipsSectionData c)
  ].

Definition binaryKeyAssignment (k : keyAssignment) : binaryExp :=
  BiRecord [
    ("id",                        u32 (kaId k));
    ("atKeyStart",                u32 (kaValueStart k));
    ("atKeyCenter",               u32 (kaValueCenter k));
    ("atKeyEnd",                  u32 (kaValueEnd k));
    ("clipId",                    u32 (kaClipId k));
    ("amplitudeAtKeyStart",       f64 (kaAmplitudeAtKeyStart k));
    ("amplitudeAtKeyCenter",      f64 (kaAmplitudeAtKeyCenter k));
    ("amplitudeAtKeyEnd",         f64 (kaAmplitudeAtKeyEnd k));
    ("atVelocityStart",           f64 (kaAtVelocityStart k));
    ("atVelocityCenter",          f64 (kaAtVelocityCenter k));
    ("atVelocityEnd",             f64 (kaAtVelocityEnd k));
    ("amplitudeAtVelocityStart",  f64 (kaAmplitudeAtVelocityStart k));
    ("amplitudeAtVelocityCenter", f64 (kaAmplitudeAtVelocityCenter k));
    ("amplitudeAtVelocityEnd",    f64 (kaAmplitudeAtVelocityEnd k));
    ("flags",                     binaryKeyAssignmentFlags (kaFlags k))
  ].

Definition binaryKeyAssignments (f : list keyAssignment) : binaryExp :=
  BiArray (map binaryKeyAssignment f).

Definition binaryKeyAssignmentFlag (f : keyAssignmentFlag) : binaryExp :=
  utf8 (descriptorOf f).

Definition binaryKeyAssignmentFlags (f : list keyAssignmentFlag) : binaryExp :=
  BiArray (map binaryKeyAssignmentFlag f).

Definition binaryKeyAssignmentsSection (c : list keyAssignment) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D4b455953);
    ("size", u64 (binarySizePadded16 (binaryKeyAssignments c)));
    ("data", binaryKeyAssignments c)
  ].

Definition binaryExpMetadataValue (m : metadataValue) : binaryExp :=
  BiRecord [
    ("key",   utf8 (mKey m));
    ("value", utf8 (mValue m))
  ].

Definition binaryExpMetadata (m : metadata) : binaryExp :=
  BiArray (map binaryExpMetadataValue (mValues m)).

Definition binaryExpMetadataSection (m : metadata) : binaryExp := 
  BiRecord [
    ("id",   u64 0x4155524D4D455441);
    ("size", u64 (binarySizePadded16 (binaryExpMetadata m)));
    ("data", binaryExpMetadata m)
  ].

Definition binaryEndSection : binaryExp := BiRecord [
  ("id",   u64 0x4155524D454E4421);
  ("size", u64 0)
].

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Arith.PeanoNat.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Init.Nat.
Require Import Coq.Init.Byte.
Require Import Coq.Bool.Bool.
Require Import Coq.Program.Basics.
Require Import Coq.Unicode.Utf8_core.

(** * Alignment *)

(** Return _size_ scaled such that it is a multiple of _q_. *)

Definition asMultipleOf (size q : nat) (Hnz : 0 ≠ q) : nat :=
  let r := size / q in
    match Nat.ltb_spec0 r q with
    | ReflectT _ _ => (r + 1) * q
    | ReflectF _ _ => r * q
    end.

Lemma p0not4 : 0 ≠ 4.
Proof. discriminate. Qed.

Lemma p0not16 : 0 ≠ 16.
Proof. discriminate. Qed.

(** Return _size_ scaled such that it is a multiple of 4. *)

Definition asMultipleOf4 (size : nat) : nat :=
  asMultipleOf size 4 p0not4.

(** Return _size_ scaled such that it is a multiple of 6. *)

Definition asMultipleOf16 (size : nat) : nat :=
  asMultipleOf size 16 p0not16.

(** If _n_ is a multiple of _m_, then _n mod m = 0_. *)

Lemma asMultipleOfMod : ∀ s q (Hneq : 0 ≠ q), (asMultipleOf s q Hneq) mod q = 0.
Proof.
  intros s q Hneq.
  unfold asMultipleOf.
  destruct (Nat.ltb_spec0 (s / q) q) as [Hlt|H1].
  - apply (Nat.mod_mul (s / q + 1) q (Nat.neq_sym _ _ Hneq)).
  - apply (Nat.mod_mul (s / q) q (Nat.neq_sym _ _ Hneq)).
Qed.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Lists.List.
Require Import Coq.Init.Nat.

Import ListNotations.

Require Import Aurantium.Compatibility.
Require Import Aurantium.Identifier.
Require Import Aurantium.Clip.
Require Import Aurantium.KeyMapping.

(** The key assignment _k_ references clip _s_. *)
Definition keyAssignmentReferencesClip
  (k : keyAssignment)
  (s : clip)
: Prop :=
  (kaClipId k) = (clipId s).

(** The clip referenced by _k_ exists in _s_. *)
Definition keyAssignmentReferencesExists
  (k : keyAssignment)
  (s : clips)
: Prop :=
  exists p, keyAssignmentReferencesClip k p /\ In p (clipsList s).

(** All key assignment in _k_ reference clips that exist in _s_. *)
Definition keyAssignmentsReferences
  (k : keyAssignments)
  (s : clips)
: Prop :=
  forall p, In p (kasList k) -> keyAssignmentReferencesExists p s.

(** Every clip in _ss_ has at least one reference in _k_. *)
Definition clipsReferenced
  (k  : keyAssignments)
  (ss : clips)
: Prop :=
  Forall (fun s => exists a, keyAssignmentReferencesClip a s /\ In s (clipsList ss)) (clipsList ss).

Inductive audioMap : Set := {
  amIdentifier               : identifier;
  amClips                    : clips;
  amKeyAssignments           : keyAssignments;
  amKeyAssignmentsReferences : keyAssignmentsReferences amKeyAssignments amClips;
  amClipsReferenced          : clipsReferenced amKeyAssignments amClips;
}.

Require Import Coq.Arith.PeanoNat.
Require Import Coq.Strings.String.
Require Import Coq.Lists.List.
Require Import Coq.Init.Nat.
Require Import Coq.Init.Byte.
Require Import Coq.Bool.Bool.
Require Import Coq.Reals.Reals.
Require Import Coq.Program.Basics.

Require Import Psatz.

Require Import Aurantium.Alignment.
Require Import Aurantium.Divisible8.
Require Import Aurantium.Identifier.
Require Import Aurantium.Clip.
Require Import Aurantium.Descriptor.
Require Import Aurantium.Hash.
Require Import Aurantium.OctetOrder.
Require Import Aurantium.KeyMapping.
Require Import Aurantium.AudioMap.
Require Import Aurantium.Metadata.

Import ListNotations.

Local Open Scope string_scope.

Set Mangle Names.

(** The type of stream elements. *)
Inductive streamE : Set :=
  (** A 64-bit IEEE754 binary64 value. *)
  | Vf64 : R -> streamE
  (** A 64-bit unsigned integer. *)
  | Vu64 : nat -> streamE
  (** A 32-bit unsigned integer. *)
  | Vu32 : nat -> streamE
  (** An 8-bit unsigned integer. *)
  | Vu8  : nat -> streamE.

Definition u8byte (b : byte) : streamE :=
  Vu8 (Byte.to_nat b).

Definition streamEIsU8 (e : streamE) : Prop :=
  match e with
  | Vf64 _ => False
  | Vu64 _ => False
  | Vu32 _ => False
  | Vu8  _ => True
  end.

(** A proposition that describes a well-formed stream. *)
Inductive streamWellFormed : list streamE -> Prop :=
  (** An empty stream is well-formed. *)
  | BEPEmpty  : streamWellFormed []
  (** A stream consisting of a single 64-bit float is well-formed. *)
  | BEPVf64   : forall k, streamWellFormed [Vf64 k]
  (** A stream consisting of a single 64-bit integer is well-formed. *)
  | BEPVu64   : forall k, streamWellFormed [Vu64 k]
  (** A stream consisting of a single 32-bit integer is well-formed. *)
  | BEPVu32   : forall k, streamWellFormed [Vu32 k]
  (** A stream consisting of a number of 8-bit values of a length divisible by 4 is well-formed. *)
  | BEPVu8s   : forall es, Forall streamEIsU8 es -> length (es) mod 4 = 0 -> streamWellFormed es
  (** The concatenation of two well-formed streams is well-formed. *)
  | BEPAppend : forall xs ys, streamWellFormed xs -> streamWellFormed ys -> streamWellFormed (xs ++ ys).

Definition streamElementSize (s : streamE) : nat :=
  match s with
  | Vf64 _ => 8
  | Vu64 _ => 8
  | Vu32 _ => 4
  | Vu8  _ => 1
  end.

Definition streamSize (s : list streamE) : nat :=
  fold_right plus 0 (map streamElementSize s).

Section binaryExpressions.

  Local Unset Elimination Schemes.

  (** The binary expression type. *)
  Inductive binaryExp : Set :=
    (** A 32-bit unsigned integer. *)
    | BiU32     : nat -> binaryExp
    (** A 64-bit unsigned integer. *)
    | BiU64     : nat -> binaryExp
    (** A 64-bit IEEE754 binary64 value. *)
    | BiF64     : R -> binaryExp
    (** A sequence of bytes. *)
    | BiBytes   : list byte -> binaryExp
    (** A sequence of bytes describing UTF-8 encoded text. *)
    | BiUTF8    : list byte -> binaryExp
    (** An array of binary expressions. *)
    | BiArray   : list binaryExp -> binaryExp
    (** A section of reserved space. *)
    | BiReserve : nat -> binaryExp
    (** A record with named binary expression members. *)
    | BiRecord  : list (string * binaryExp) -> binaryExp.

  Section binaryExp_rect.
    Variable P             : binaryExp -> Type.
    Variable P_list        : list binaryExp -> Type.
    Hypothesis P_nil       : P_list [].
    Hypothesis P_cons      : forall x xs, P x -> P_list xs -> P_list (x :: xs).
    Hypothesis P_BiU32     : forall x, P (BiU32 x).
    Hypothesis P_BiU64     : forall x, P (BiU64 x).
    Hypothesis P_BiF64     : forall x, P (BiF64 x).
    Hypothesis P_BiBytes   : forall bs, P (BiBytes bs).
    Hypothesis P_BiUTF8    : forall bs, P (BiUTF8 bs).
    Hypothesis P_BiArray   : forall bs, P_list bs -> P (BiArray bs).
    Hypothesis P_BiReserve : forall x, P (BiReserve x).
    Hypothesis P_BiRecord  : forall fs, P_list (map snd fs) -> P (BiRecord fs).

    Fixpoint binaryExp_rect (b : binaryExp) : P b :=
      let
        fix expForAll (xs : list binaryExp) : P_list xs :=
          match xs as rxs return (P_list rxs) with
          | []        => @P_nil
          | (y :: ys) => @P_cons y ys (binaryExp_rect y) (expForAll ys)
          end
      in let
        fix forAllSnd (fs : list (string * binaryExp)) : P_list (map snd fs) :=
          match fs as rf return P_list (map snd rf) with
          | []             => @P_nil
          | ((_, y) :: ys) => @P_cons y (map snd ys) (binaryExp_rect y) (forAllSnd ys)
          end
      in
        match b with
        | BiU32 c     => P_BiU32 c
        | BiU64 c     => P_BiU64 c
        | BiF64 c     => P_BiF64 c
        | BiBytes bs  => P_BiBytes bs
        | BiUTF8 bs   => P_BiUTF8 bs
        | BiArray es  => P_BiArray es (expForAll es)
        | BiReserve c => P_BiReserve c
        | BiRecord fs => P_BiRecord fs (forAllSnd fs)
        end.

  End binaryExp_rect.

  Section binaryExp_ind.
    Variable P             : binaryExp -> Prop.
    Hypothesis P_BiU32     : forall x, P (BiU32 x).
    Hypothesis P_BiU64     : forall x, P (BiU64 x).
    Hypothesis P_BiF64     : forall x, P (BiF64 x).
    Hypothesis P_BiBytes   : forall bs, P (BiBytes bs).
    Hypothesis P_BiUTF8    : forall bs, P (BiUTF8 bs).
    Hypothesis P_BiArray   : forall bs, Forall P bs -> P (BiArray bs).
    Hypothesis P_BiReserve : forall x, P (BiReserve x).
    Hypothesis P_BiRecord  : forall fs, Forall P (map snd fs) -> P (BiRecord fs).

    Definition binaryExp_ind (b : binaryExp) : P b :=
      binaryExp_rect
        P
        (Forall P)
        (Forall_nil P)
        (Forall_cons (P:=P)) 
        P_BiU32
        P_BiU64
        P_BiF64
        P_BiBytes
        P_BiUTF8
        P_BiArray
        P_BiReserve
        P_BiRecord
        b.

  End binaryExp_ind.
End binaryExpressions.

(** The size of a binary expression in octets. *)
Fixpoint binarySize (b : binaryExp) : nat :=
  match b with
  | BiU32 _     => 4
  | BiU64 _     => 8
  | BiF64 _     => 8
  | BiBytes s   => 4 + asMultipleOf4 (length s)
  | BiUTF8 s    => 4 + asMultipleOf4 (length s)
  | BiArray f   => 4 + fold_right plus 0 (map binarySize f)
  | BiReserve s => asMultipleOf4 s
  | BiRecord f  => fold_right plus 0 (map (compose binarySize snd) f)
  end.

Definition binaryEvalPaddedBytes
  (b     : list byte)
  (align : nat)
  (Hneq  : 0 <> align)
: list streamE :=
  let vremaining := length b mod align in
    match vremaining with
    | 0 => map u8byte b
    | _ => map u8byte (b ++ repeat x00 (align - vremaining))
    end.

(** The binary evaluation function; produces a stream from an expression. *)
Fixpoint binaryEval (b : binaryExp) : list streamE :=
  match b with
  | BiU32 k     => [Vu32 k]
  | BiU64 k     => [Vu64 k]
  | BiF64 k     => [Vf64 k]
  | BiBytes s   => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4)
  | BiUTF8 s    => (Vu32 (length s)) :: (binaryEvalPaddedBytes s 4 p0not4)
  | BiArray f   => (Vu32 (length f)) :: concat (map binaryEval f)
  | BiReserve s => repeat (Vu8 0) (asMultipleOf4 s)
  | BiRecord f  => concat (map (compose binaryEval snd) f)
  end.

Definition binarySizePadded16 (b : binaryExp) : nat :=
  asMultipleOf16 (binarySize b).

Definition utf8 (s : string) : binaryExp :=
  BiUTF8 (list_byte_of_string s).

Definition u32 := BiU32.
Definition u64 := BiU64.
Definition f64 := BiF64.

(** The file header. *)
Definition binaryExpFileHeader : binaryExp :=
  BiRecord [
    ("id",           u64 0x894155520D0A1A0A);
    ("versionMajor", u32 1);
    ("versionMinor", u32 0)
  ].

(** The binary encoding of an identifier. *)
Definition binaryIdentifier (i : identifier) : binaryExp :=
  BiRecord [
    ("name",         utf8 (idName i));
    ("versionMajor", u32 (idVersionMajor i));
    ("versionMinor", u32 (idVersionMinor i))
  ].

(** The AURM_ID! section. *)
Definition binaryIdentifierSection (i : identifier) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D5F494421);
    ("size", u64 (binarySizePadded16 (binaryIdentifier i)));
    ("data", binaryIdentifier i)
  ].

(** The AURMEND! section. *)
Definition binaryEndSection : binaryExp := BiRecord [
  ("id",   u64 0x4155524D454E4421);
  ("size", u64 0)
].

(** The binary encoding of a hash. *)
Definition binaryHash (h : hashValue) : binaryExp :=
  BiRecord [
    ("algorithm", utf8 (descriptorOf (hvAlgorithm h)));
    ("value",     utf8 (hvValue h))
  ].

(** The binary encoding of a clip. *)
Definition binaryClip (c : clip) : binaryExp :=
  BiRecord [
    ("id",          u32 (clipId c));
    ("name",        utf8 (clipName c));
    ("format",      utf8 (descriptorOf (clipFormat c)));
    ("sampleRate",  u32 (clipSampleRate c));
    ("sampleDepth", u32 (clipSampleDepth c));
    ("channels",    u32 (clipChannels c));
    ("endianness",  utf8 (descriptorOf (clipEndianness c)));
    ("hash",        binaryHash (clipHash c));
    ("offset",      u64 (clipOffset c));
    ("size",        u64 (clipSize c))
  ].

(** The binary encoding of an array of clips. *)
Definition binaryClips (c : clips) : binaryExp :=
  BiArray (map binaryClip (clipsList c)).

(** The AURMCLIP section. *)
Definition binaryClipsSectionData (c : clips) : binaryExp :=
  let audioDataStart  := clipOffset (clipFirst c) in
  let encClips        := binaryClips c in
  let encClipsSize    := binarySize encClips in
  let encClipsPad     := audioDataStart - encClipsSize in
  let audioDataSize   := clipAudioDataSizeTotal c in
  let audioDataSize16 := asMultipleOf16 audioDataSize in
    BiRecord [
      ("clips",     encClips);
      ("clipsPad",  BiReserve encClipsPad);
      ("clipsData", BiReserve audioDataSize16)
    ].

Definition binaryClipsSection (c : clips) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D434C4950);
    ("size", u64 (binarySizePadded16 (binaryClipsSectionData c)));
    ("data", binaryClipsSectionData c)
  ].

Definition binaryKeyAssignmentFlag (f : keyAssignmentFlag) : binaryExp :=
  utf8 (descriptorOf f).

Definition binaryKeyAssignmentFlags (f : list keyAssignmentFlag) : binaryExp :=
  BiArray (map binaryKeyAssignmentFlag f).

Definition binaryKeyAssignment (k : keyAssignment) : binaryExp :=
  BiRecord [
    ("id",                        u32 (kaId k));
    ("atKeyStart",                u32 (kaValueStart k));
    ("atKeyCenter",               u32 (kaValueCenter k));
    ("atKeyEnd",                  u32 (kaValueEnd k));
    ("clipId",                    u32 (kaClipId k));
    ("amplitudeAtKeyStart",       f64 (kaAmplitudeAtKeyStart k));
    ("amplitudeAtKeyCenter",      f64 (kaAmplitudeAtKeyCenter k));
    ("amplitudeAtKeyEnd",         f64 (kaAmplitudeAtKeyEnd k));
    ("atVelocityStart",           f64 (kaAtVelocityStart k));
    ("atVelocityCenter",          f64 (kaAtVelocityCenter k));
    ("atVelocityEnd",             f64 (kaAtVelocityEnd k));
    ("amplitudeAtVelocityStart",  f64 (kaAmplitudeAtVelocityStart k));
    ("amplitudeAtVelocityCenter", f64 (kaAmplitudeAtVelocityCenter k));
    ("amplitudeAtVelocityEnd",    f64 (kaAmplitudeAtVelocityEnd k));
    ("flags",                     binaryKeyAssignmentFlags (kaFlags k))
  ].

Definition binaryKeyAssignments (f : list keyAssignment) : binaryExp :=
  BiArray (map binaryKeyAssignment f).

(** The AURMKEYS section. *)
Definition binaryKeyAssignmentsSection (c : list keyAssignment) : binaryExp :=
  BiRecord [
    ("id",   u64 0x4155524D4b455953);
    ("size", u64 (binarySizePadded16 (binaryKeyAssignments c)));
    ("data", binaryKeyAssignments c)
  ].

Definition binaryExpMetadataValue (m : metadataValue) : binaryExp :=
  BiRecord [
    ("key",   utf8 (mKey m));
    ("value", utf8 (mValue m))
  ].

Definition binaryExpMetadata (m : metadata) : binaryExp :=
  BiArray (map binaryExpMetadataValue (mValues m)).

(** The AURMMETA section. *)
Definition binaryExpMetadataSection (m : metadata) : binaryExp := 
  BiRecord [
    ("id",   u64 0x4155524D4D455441);
    ("size", u64 (binarySizePadded16 (binaryExpMetadata m)));
    ("data", binaryExpMetadata m)
  ].

(** An example audio map file as a binary expression. *)
Example binaryExampleFile (m : audioMap) : binaryExp :=
  BiRecord [
    ("file",  binaryExpFileHeader);
    ("id",    binaryIdentifierSection (amIdentifier m));
    ("clips", binaryClipsSection (amClips m));
    ("keys",  binaryKeyAssignmentsSection (kasList (amKeyAssignments m)));
    ("end",   binaryEndSection)
  ].

Lemma fold_right_add_cons : forall x xs,
  x + fold_right plus 0 xs = fold_right plus 0 (x :: xs).
Proof. reflexivity. Qed.

Lemma forall_map_binarySize : forall es,
  Forall (fun b : binaryExp => binarySize b mod 4 = 0) es
    <-> Forall (fun n => n mod 4 = 0) (map binarySize es).
Proof.
  intros es.
  induction es.
  constructor.
  - rewrite Forall_map.
    intros H. trivial.
  - rewrite Forall_map.
    intros H. trivial.
  - rewrite Forall_map.
    constructor.
    intros H; trivial.
    intros H; trivial.
Qed.

(** The size of a binary expression is always divisible by 4. *)
Theorem binarySizeMultiple4 : forall b, binarySize (b) mod 4 = 0.
Proof.
  intros b.
  induction b as [Hbu32|Hbu64|Hbf64|Hbbyte|Hbutf|xs HFA|Hbuns|xs HFF] using binaryExp_ind.
  (* U32 values are of size 4 *)
  - reflexivity.
  (* U64 values are of size 8 *)
  - reflexivity.
  (* F64 values are of size 8 *)
  - reflexivity.

  (* Byte array values are rounded up to a multiple of 4 and prefixed with 4 *)
  - unfold binarySize.
    unfold asMultipleOf4.
    remember (asMultipleOf (Datatypes.length Hbbyte) 4 p0not4) as size eqn:Heqsize.
    rewrite Nat.add_comm.
    rewrite <- (Nat.add_mod_idemp_l size 4 4 (Nat.neq_sym _ _ p0not4)).
    assert (size mod 4 = 0) as Hm0. {
      rewrite Heqsize.
      apply (asMultipleOfMod (Datatypes.length Hbbyte) 4 (p0not4)).
    }
    rewrite Hm0.
    reflexivity.

  (* UTF-8 values are rounded up to a multiple of 4 and prefixed with 4 *)
  - unfold binarySize.
    unfold asMultipleOf4.
    remember (asMultipleOf (Datatypes.length Hbutf) 4 p0not4) as size eqn:Heqsize.
    rewrite Nat.add_comm.
    rewrite <- (Nat.add_mod_idemp_l size 4 4 (Nat.neq_sym _ _ p0not4)).
    assert (size mod 4 = 0) as Hm0. {
      rewrite Heqsize.
      apply (asMultipleOfMod (Datatypes.length Hbutf) 4 (p0not4)).
    }
    rewrite Hm0.
    reflexivity.

  (* Each element of an array is a multiple of 4, so the entire array is too. *)
  - unfold binarySize.
    fold binarySize.
    induction xs as [|y ys HforAllInd].
    -- reflexivity.
    -- assert (fold_right add 0 (map binarySize (y :: ys)) mod 4 = 0) as HfoldEq. {
         apply (@divisibilityNFoldPlus 4 (map binarySize (y :: ys))).
         discriminate.
         rewrite <- forall_map_binarySize.
         exact HFA.
       }
       rewrite map_cons.
       rewrite map_cons in HfoldEq.
       assert (4 mod 4 = 0) as H4mod40 by (reflexivity).
       assert (0 <> 4) as H0n4 by (discriminate).
       apply (divisiblityNAdd 4 (fold_right add 0 (binarySize y :: map binarySize ys)) 4 H0n4 H4mod40 HfoldEq).

  (* Unspecified values are rounded up. *)
  - unfold binarySize.
    unfold asMultipleOf4.
    rewrite asMultipleOfMod.
    reflexivity.

  (* Each element of an record is a multiple of 4, so the entire record is too. *)
  - unfold binarySize.
    fold binarySize.
    induction xs as [|y ys HforAllInd].
    -- reflexivity.
    -- rewrite map_cons.
       rewrite map_cons in HFF.
       rewrite <- fold_right_add_cons.
       apply divisiblityNAdd.
       discriminate.
       apply (Forall_inv HFF).
       apply HforAllInd.
       apply (Forall_inv_tail HFF).
Qed.

Lemma sub_0_lt_ymx : forall x y,
  0 <= x -> x < y -> 0 < y - x.
Proof.
  intros x y Hle Hlt.
  destruct x as [|a].
  - rewrite Nat.sub_0_r.
    exact Hlt.
  - rewrite <- Nat.lt_add_lt_sub_l.
    rewrite Nat.add_0_r.
    exact Hlt.
Qed.

Lemma mod_sub : forall x m,
  0 < m -> 0 < m - (x mod m) <= m.
Proof.
  intros x m Hlt.
  constructor.
  - assert (0 <= x mod m < m) as HmRange. {
      apply Nat.mod_bound_pos.
      apply Nat.le_0_l.
      exact Hlt.
    }
    destruct HmRange as [HA HB].
    remember (x mod m) as y.
    apply (sub_0_lt_ymx y m HA HB).
  - assert (x mod m < m) as HmRange. {
      apply Nat.mod_upper_bound.
      apply Nat.neq_sym.
      apply Nat.lt_neq.
      exact Hlt.
    }
    apply Nat.le_sub_l.
Qed.

Lemma mod_opposition : forall x a,
  0 <> a -> x mod a + (a - x mod a) = a.
Proof.
  intros x a Hnz.
  assert (x mod a < a) as Hxma. {
    apply (Nat.mod_upper_bound).
    apply Nat.neq_sym.
    exact Hnz.
  }
  remember (x mod a) as y eqn:Heqy.
  lia.
Qed.

Theorem binaryEvalPaddedBytesAligned : forall bs a (Hnz : 0 <> a),
  length (binaryEvalPaddedBytes bs a Hnz) mod a = 0.
Proof.
  intros bs a Hnz.
  unfold binaryEvalPaddedBytes.
  destruct (Datatypes.length bs mod a) eqn:Hlen.
  - rewrite map_length.
    exact Hlen.
  - rewrite map_length.
    rewrite app_length.
    rewrite repeat_length.
    rewrite <- Hlen.
    remember (Datatypes.length bs) as x.
    rewrite <- (Nat.add_mod_idemp_l x (a - x mod a) a).
    assert ((x mod a + (a - x mod a)) = a) as Heqa. {
      rewrite (mod_opposition x a Hnz).
      reflexivity.
    }
    rewrite Heqa.
    apply Nat.mod_same.
    apply Nat.neq_sym; exact Hnz.
    apply Nat.neq_sym; exact Hnz.
Qed.

Lemma repeat_eq : forall (A : Type) (P : A -> Prop) (n : nat) (x : A),
  Forall (eq x) (repeat x n).
Proof.
  intros A P n x.
  induction n as [|m Hm].
  - constructor.
  - simpl.
    constructor.
    reflexivity.
    exact Hm.
Qed.

Lemma Forall_implies : forall (A : Type) (P : A -> Prop) (Q : A -> Prop) (xs : list A) (H : forall x, P x -> Q x),
  Forall P xs -> Forall Q xs.
Proof.
  intros A P Q xs Ht HforAll.
  induction HforAll as [|y ys Hpy HfaP HfaQ].
  - constructor.
  - constructor.
    apply (Ht y Hpy).
    exact HfaQ.
Qed.

Theorem binaryEvalPaddedBytesU8 : forall bs a (Hnz : 0 <> a),
  Forall streamEIsU8 (binaryEvalPaddedBytes bs a Hnz).
Proof.
  intros bs a Hnz.
  unfold binaryEvalPaddedBytes.
  destruct (Datatypes.length bs mod a) as [|HB].
  - rewrite Forall_map.
    induction bs as [|r rs Hrs].
    -- constructor.
    -- constructor.
       reflexivity.
       exact Hrs.
  - rewrite map_app.
    assert (Forall streamEIsU8 (map u8byte bs)) as Hmap. {
      rewrite Forall_map.
      induction bs as [|r rs Hrs].
      - constructor.
      - constructor.
        reflexivity.
        exact Hrs.
    }
    assert (Forall streamEIsU8 (map u8byte (repeat "000"%byte (a - S HB)))) as HmapR. {
      rewrite Forall_map.
      assert (Forall (eq "000"%byte) (repeat "000"%byte (a - S HB))) as Hfeq
        by (apply (repeat_eq byte (fun _ : byte => True) (a - S HB) "000"%byte)).
      simpl.
      apply (@Forall_implies byte (eq "000"%byte) (fun _ : byte => True) (repeat "000"%byte (a - S HB))). {
        intros. exact I.
      }
      exact Hfeq.
    }
    apply Forall_app.
    constructor.
    exact Hmap.
    exact HmapR.
Qed.

Lemma app_cons : forall (A : Type) (x : A) (xs : list A),
  x :: xs = app (cons x nil) xs.
Proof.
  intros A x xs.
  reflexivity.
Qed.

(** Streams produced by the _binaryEval_ function are well-formed. *)
Theorem binaryEvalStreamsWellFormed : forall b,
  streamWellFormed (binaryEval b).
Proof.
  intros b.
  induction b as [a0|a1|a2|a3|a4|a5 Hfa|a6|a7 Hfa].
  (* U32 *)
  - apply BEPVu32.
  (* U64 *)
  - apply BEPVu64.
  (* F64 *)
  - apply BEPVf64.
  (* Bytes *)
  - unfold binaryEval.
    rewrite app_cons.
    apply BEPAppend.
    apply BEPVu32.
    assert (length (binaryEvalPaddedBytes a3 4 p0not4) mod 4 = 0) as Hlm
      by (apply (binaryEvalPaddedBytesAligned)).
    apply BEPVu8s.
    apply binaryEvalPaddedBytesU8.
    exact Hlm.
  (* UTF-8 *)
  - unfold binaryEval.
    rewrite app_cons.
    apply BEPAppend.
    apply BEPVu32.
    assert (length (binaryEvalPaddedBytes a4 4 p0not4) mod 4 = 0) as Hlm
      by (apply (binaryEvalPaddedBytesAligned)).
    assert (Forall streamEIsU8 (binaryEvalPaddedBytes a4 4 p0not4)) as Hu8
      by (apply (binaryEvalPaddedBytesU8)).
    apply (BEPVu8s _ Hu8 Hlm).
  (* Array *)
  - simpl.
    rewrite app_cons.
    apply BEPAppend.
    apply BEPVu32.
    induction a5 as [|q qs IHqs].
    -- constructor.
    -- assert (streamWellFormed (concat (map binaryEval qs))) as HqsWF
         by (apply (IHqs (Forall_inv_tail Hfa))).
       assert (streamWellFormed (binaryEval q)) as HqWF
         by (apply (Forall_inv Hfa)).
       simpl.
       apply BEPAppend.
       exact HqWF.
       exact HqsWF.
  (* Reserve *)
  - simpl.
    unfold asMultipleOf4.
    remember (asMultipleOf a6 4 p0not4) as size eqn:Heqsize.
    assert (size mod 4 = 0) as Heqm. {
      rewrite Heqsize.
      apply (asMultipleOfMod).
    }
    assert ((compose Vu8 Byte.to_nat) "000"%byte = (Vu8 0)) as HbyteEq by reflexivity.
    apply BEPVu8s.
    assert (Forall (eq (Vu8 0)) (repeat (Vu8 0) size)) as Hfeq
      by (apply (@repeat_eq streamE streamEIsU8 size (Vu8 0))).
    apply (@Forall_implies streamE (eq (Vu8 0)) streamEIsU8 (repeat (Vu8 0) size)). {
      intros x Hxeq.
      unfold streamEIsU8.
      rewrite <- Hxeq.
      exact I.
    }
    exact Hfeq.
    rewrite repeat_length.
    exact Heqm.
  (* Record *)
  - simpl.
    induction a7 as [|q qs IHqs].
    -- constructor.
    -- assert (Forall (fun b : binaryExp => streamWellFormed (binaryEval b)) (map snd qs)) as Hfqs. {
         apply (@Forall_inv_tail binaryExp (fun b : binaryExp => streamWellFormed (binaryEval b)) (snd q) (map snd qs)). {
           assert ((map snd (q :: qs)) = (snd q :: map snd qs)) as Hmc by reflexivity.
           rewrite <- Hmc.
           exact Hfa.
         }
       }
       assert (streamWellFormed (concat (map (compose binaryEval snd) qs))) as Hconqs by (apply (IHqs Hfqs)).
       rewrite map_cons.
       rewrite concat_cons.
       apply BEPAppend.
       rewrite map_cons in Hfa.
       apply (Forall_inv Hfa).
       exact Hconqs.
Qed.

Lemma fold_right_1_length : forall xs,
  Forall (eq 1) xs -> fold_right add 0 xs = length xs.
Proof.
  intros xs Hfa.
  induction xs as [|y ys IHxs].
  - reflexivity.
  - rewrite <- fold_right_add_cons.
    assert (length (y :: ys) = 1 + length (ys)) as HlenYs by reflexivity.
    rewrite HlenYs.
    assert (1 = y) as Hy1 by (apply (Forall_inv Hfa)).
    rewrite <- Hy1.
    f_equal.
    apply IHxs.
    apply (Forall_inv_tail Hfa).
Qed.

Theorem fold_right_add_app : forall xs ys,
  fold_right add 0 xs + fold_right add 0 ys = fold_right add 0 (xs ++ ys).
Proof.
  intros xs ys.
  rewrite fold_right_app.
  generalize dependent ys.
  induction xs as [|q qs IHqs].
  - reflexivity.
  - intros ys.
    simpl.
    rewrite <- (IHqs ys).
    rewrite Nat.add_assoc.
    reflexivity.
Qed.

Theorem streamSizeApp : forall xs ys,
  streamSize xs + streamSize ys = streamSize (xs ++ ys).
Proof.
  intros xs ys.
  unfold streamSize.
  rewrite map_app.
  rewrite fold_right_add_app.
  reflexivity.
Qed.

(** All well-formed streams have a size divisible by 4. *)
Theorem streamsWellFormedDivisible4 : forall es,
  streamWellFormed es -> streamSize es mod 4 = 0.
Proof.
  intros es Hwf.
  induction Hwf as [|H1|H2|H3|es Hfa Hsize|xs ys Hxswf Hxsize Hyswf Hysize].
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - reflexivity.
  - unfold streamSize.
    assert (Forall (fun e => 1 = streamElementSize e) es) as HFaSize. {
      apply (@Forall_implies streamE streamEIsU8 (fun e : streamE => 1 = streamElementSize e) es). {
        intros x His.
        destruct x as [f64|u64|u32|u8].
        - contradiction.
        - contradiction.
        - contradiction.
        - reflexivity.
      }
      exact Hfa.
    }
    assert (Forall (eq 1) (map streamElementSize es)) as Hall1. {
      apply (@Forall_map _ _ _ _ es).
      exact HFaSize.
    }
    assert (fold_right add 0 (map streamElementSize es) = length es) as HlenEq. {
      assert (length es = length (map streamElementSize es)) as HmapLen. {
        rewrite map_length.
        reflexivity.
      }
      rewrite HmapLen.
      apply (fold_right_1_length (map streamElementSize es) Hall1).
    }
    rewrite HlenEq.
    exact Hsize.
  - rewrite <- streamSizeApp.
    apply divisiblityNAdd.
    discriminate.
    exact Hxsize.
    exact Hysize.
Qed.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Lists.List.
Require Import Coq.Init.Nat.
Require Import Coq.Reals.Reals.
Require Import Psatz.

Import ListNotations.

Set Mangle Names.

Require Import Aurantium.Descriptor.
Require Import Aurantium.OctetOrder.
Require Import Aurantium.Compatibility.
Require Import Aurantium.Intersection.
Require Import Aurantium.Hash.

(** The known audio formats. *)
Inductive audioFormatType : Set :=
  (** Pulse code modulation using signed values. *)
  | AFPCMLinearIntegerSigned : audioFormatType
  (** Pulse code modulation using unsigned values. *)
  | AFPCMLinearIntegerUnsigned : audioFormatType
  (** Pulse code modulation using floating point values. *)
  | AFPCMLinearFloat : audioFormatType
  (** FLAC-compressed audio. *)
  | AFFlac : audioFormatType
  (** A format not known by this specification. *)
  | AFUnknown : descriptor -> audioFormatType
  .

Theorem audioFormatTypeEqDec : forall (x y : audioFormatType),
  {x = y}+{x <> y}.
Proof.
  intros x y.
  destruct x; (destruct y; decide equality; apply string_dec).
Qed.

Local Open Scope char_scope.
Local Open Scope string_scope.

Definition audioFormatDescribe (f : audioFormatType) : descriptor :=
  match f with
  | AFPCMLinearIntegerSigned   => "com.io7m.aurantium.pcm_linear_integer_signed"
  | AFPCMLinearIntegerUnsigned => "com.io7m.aurantium.pcm_linear_integer_unsigned"
  | AFPCMLinearFloat           => "com.io7m.aurantium.pcm_linear_float"
  | AFFlac                     => "com.io7m.aurantium.flac"
  | AFUnknown d                => d
  end.

#[export]
Instance audioFormatDescribable : describable audioFormatType := {
  descriptorOf c := audioFormatDescribe c
}.

(** A description of a single audio clip. *)
Inductive clip : Set := clipMake {
  (** The unique identifier for the clip. *)
  clipId : nat;
  (** The clip name, for descriptive purposes. *)
  clipName : string;
  (** The clip audio format name. *)
  clipFormat : audioFormatType;
  (** The sample rate in bits per second. *)
  clipSampleRate : nat;
  (** The clip sample depth in bits per clip. *)
  clipSampleDepth : nat;
  (** The number of channels in the clip. *)
  clipChannels : nat;
  (** The endianness of the audio data. *)
  clipEndianness : octetOrder;
  (** The hash of the audio data. *)
  clipHash : hashValue;
  (** The offset of the first octet of audio data. *)
  clipOffset : nat;
  (** The size of the audio data in octets. *)
  clipSize : nat
}.

Definition clipInvariants (c : clip) : Prop :=
     (clipId          c <= 4294967295)
  /\ (clipSampleRate  c <= 4294967295)
  /\ (clipSampleDepth c <= 4294967295)
  /\ (clipChannels    c <= 4294967295)
  /\ (clipOffset      c <= 18446744073709551615)
  /\ (clipSize        c <= 18446744073709551615)
  .

Theorem clipEqDec : forall (x y : clip),
  {x = y}+{x <> y}.
Proof.
  intros x y.
  destruct x; (
    destruct y; (
      try decide equality;
      try apply string_dec;
      try decide equality;
      try apply string_dec;
      try apply hashValueEqDec
    )
  ).
  apply hashAlgorithmEqDec.
Qed.

Inductive clipsListIdIsSorted : list clip -> Prop :=
  | ClipIdOne  : forall s,
      clipsListIdIsSorted [s]
  | ClipIdCons : forall s0 s1 ss,
    (clipId s0) < (clipId s1) ->
      clipsListIdIsSorted (s0 :: ss) ->
        clipsListIdIsSorted (s1 :: s0 :: ss).

Inductive clipsListOffsetIsSorted : list clip -> Prop :=
  | ClipOffsetOne : forall s,
    clipsListOffsetIsSorted [s]
  | ClipOffsetCons : forall s0 s1 ss,
    ((clipOffset s1) + (clipSize s1)) < clipOffset s0 ->
      clipsListOffsetIsSorted (s0 :: ss) ->
        clipsListOffsetIsSorted (s1 :: s0 :: ss).

Inductive clips : Set := clipsMake {
  clipsList         : list clip;
  clipsIdSorted     : clipsListIdIsSorted clipsList;
  clipsOffsetSorted : clipsListOffsetIsSorted clipsList;
}.

Lemma clipsNonEmpty : forall (s : clips),
  [] <> clipsList s.
Proof.
  intros s.
  destruct (clipsIdSorted s); discriminate.
Qed.

Definition clipFirst : forall (s : clips), clip.
Proof.
  intro s.
  pose proof (clipsNonEmpty s) as H_ne.
  destruct (clipsList s) eqn:Hs.
  - contradiction.
  - intuition.
Qed.

(** Find the clip with the given ID. *)
Fixpoint clipForId
  (i  : nat)
  (ca : list clip)
: option clip :=
  match ca with
  | nil         => None
  | cons a rest =>
    match Nat.eq_dec (clipId a) i with
    | left _  => Some a
    | right _ => clipForId i rest
    end
  end.

(** Determine all the elements of _ca_ that are not in _cb_. *)
Definition clipsRemoved
  (ca : list clip)
  (cb : list clip)
: list clip :=
  filter (fun c =>
    match clipForId (clipId c) cb with
    | None   => false
    | Some _ => true
    end) ca.

(** Determine all the elements of _cb_ that are not in _ca_. *)
Definition clipsAdded
  (ca : list clip)
  (cb : list clip)
: list clip :=
  clipsRemoved cb ca.

Definition clipsCompatCompareRemoved
  (r : list clip)
: list compatVersionChangeRecord :=
  map (fun a => CVRMake CVersionChangeMajor "A clip was removed.") r.

Lemma clipsCompatCompareRemovedForall : forall r,
  Forall (fun a => cvrChange a = CVersionChangeMajor)
    (clipsCompatCompareRemoved r).
Proof.
  intros r.
  apply Forall_map.
  induction r as [|y ys]; intuition.
Qed.

Definition clipsCompatCompareAdded
  (r : list clip)
: list compatVersionChangeRecord :=
  map (fun a => CVRMake CVersionChangeMinor "A clip was added.") r.

Lemma clipsCompatCompareAddedForall : forall r,
  [] <> r ->
    Forall (fun a => cvrChange a = CVersionChangeMinor)
      (clipsCompatCompareAdded r).
Proof.
  intros r Hneq.
  apply Forall_map.
  induction r as [|y ys IHy]. {
    contradict Hneq; reflexivity.
  } {
    constructor.
    reflexivity.
    destruct ys as [|z zs]. {
      constructor.
    } {
      apply IHy.
      discriminate.
    }
  }
Qed.

(** The rules that define the version number increments required for
    a pair of clips. *)
Definition clipCompatCompare
  (c0 c1 : clip)
: compatVersionChangeRecord :=
  match clipEqDec c0 c1 with
  | left _ => 
    CVRMake CVersionChangeNone ""
  | right _ => 
    CVRMake CVersionChangeMajor "The values of the clip were changed."
  end.

Definition clipsCompatCompareChanged
  (r : list (clip * clip))
: list compatVersionChangeRecord :=
  map (fun p => clipCompatCompare (fst p) (snd p)) r.

Definition clipsCompatCompareFull
  (ca cb : list clip)
: list compatVersionChangeRecord :=
  let f              := (fun c cs => clipForId (clipId c) cs) in
  let removed        := clipsRemoved ca cb in
  let added          := clipsAdded ca cb in
  let changed        := intersectionPairs f ca cb in
  let removedChanges := clipsCompatCompareRemoved removed in
  let addedChanges   := clipsCompatCompareAdded added in
  let changedChanges := clipsCompatCompareChanged changed in
    removedChanges ++ addedChanges ++ changedChanges.

(** If there's a non-empty list of removed clips, a major version change is required. *)
Theorem clipsCompatCompareMajor0 : forall ca cb,
  [] <> clipsRemoved ca cb ->
    compatVersionChangeRecordsMaximum (clipsCompatCompareFull ca cb)
      = CVersionChangeMajor.
Proof.
  intros ca cb H_ne.
  unfold clipsCompatCompareFull.
  apply compatVersionChangesMaximumCorrect0.
  apply in_map_iff.
  destruct (clipsRemoved ca cb) as [|y ys]. {
    contradict H_ne; reflexivity.
  } {
    simpl.
    exists {| cvrChange := CVersionChangeMajor; cvrReason := "A clip was removed." |}.
    intuition.
  }
Qed.

(** Adding a clip is a minor change. *)
Theorem clipsCompatCompareMinor0 : forall ca cb,
  [] = clipsRemoved ca cb ->
    [] <> clipsAdded ca cb ->
      (forall f, [] = intersectionPairs f ca cb) ->
        compatVersionChangeRecordsMaximum (clipsCompatCompareFull ca cb)
          = CVersionChangeMinor.
Proof.
  intros ca cb Hrm Hadd Hint.
  unfold clipsCompatCompareFull.
  rewrite <- Hrm.
  rewrite <- Hint.
  simpl.
  rewrite app_nil_r.
  clear Hrm.
  clear Hint.

  destruct (clipsAdded ca cb) as [|y ys]. {
    contradict Hadd; reflexivity.
  } {
    unfold compatVersionChangeRecordsMaximum.
    simpl.

    (* We can show that either one of the arguments _must_ be equal to Minor
       and the other to something minor or less. *)
    rewrite (
      compatVersionChangeMaxMinorInv
        CVersionChangeMinor
          (compatVersionChangesMaximum
            (map (fun r : compatVersionChangeRecord => cvrChange r)
               (clipsCompatCompareAdded ys)))
    ).

    unfold clipsCompatCompareAdded.
    rewrite map_map.
    simpl.

    (* We can prove that all elements map to a minor change. *)
    assert (
      Forall
        (fun c => c = CVersionChangeMinor) 
        (map (fun x : clip => CVersionChangeMinor) ys)
    ) as Hfa1. {
      rewrite Forall_map.
      rewrite Forall_forall.
      reflexivity.
    }

    apply CVMMinorLeft.
    constructor. {
      reflexivity.
    } {
      clear Hadd.
      induction (map (fun _ : clip => CVersionChangeMinor) ys) as [|z zs IHz]. {
        right; reflexivity.
      } {
        left.
        pose proof (Forall_inv Hfa1) as Hfb0.
        pose proof (Forall_inv_tail Hfa1) as Hfb1.
        simpl.
        rewrite Hfb0.
        destruct (IHz Hfb1) as [H0|H1]. {
          rewrite H0.
          reflexivity.
        } {
          rewrite H1.
          reflexivity.
        }
      }
    }
  }
Qed.

Fixpoint clipAudioDataSizeTotalAux (c : list clip) : nat :=
  match c with
  | []        => 0
  | (x :: []) => (clipOffset x) + (clipSize x)
  | (x :: xs) => clipAudioDataSizeTotalAux xs
  end.

Definition clipAudioDataSizeTotal (c : clips) : nat :=
  clipAudioDataSizeTotalAux (clipsList c).

Local Open Scope R_scope.

Unset Mangle Names.

Definition pcmIntegerEncodeSigned
  (depth     : nat)
  (amplitude : R)
: R :=
  match Rle_dec 0 amplitude with
  | left _  => Rmult amplitude ((pow 2 (depth - 1)) - 1)
  | right _ => Rmult amplitude (pow 2 (depth - 1))
  end.

Remark pcmIntegerEncodeSigned16_Low : pcmIntegerEncodeSigned 16 (-1) = -32768.
Proof.
  unfold pcmIntegerEncodeSigned.
  destruct (Rle_dec 0 (-1)) as [HL|HR]. {
    contradict HL.
    lra.
  } {
    assert (sub 16 1 = 15%nat) as H0 by lia.
    rewrite H0.
    assert (2 ^ 15 = 32768) as H1 by lra.
    rewrite H1.
    lra.
  }
Qed.

Remark pcmIntegerEncodeSigned16_Mid : pcmIntegerEncodeSigned 16 0 = 0.
Proof.
  unfold pcmIntegerEncodeSigned.
  destruct (Rle_dec 0 0) as [HL|HR]. {
    lra.
  } {
    contradict HR; lra.
  }
Qed.

Remark pcmIntegerEncodeSigned16_High : pcmIntegerEncodeSigned 16 1 = 32767.
Proof.
  unfold pcmIntegerEncodeSigned.
  destruct (Rle_dec 0 1) as [HL|HR]. {
    assert (sub 16 1 = 15%nat) as H0 by lia.
    rewrite H0.
    assert (2 ^ 15 - 1 = 32767) as H1 by lra.
    rewrite H1.
    lra.
  } {
    contradict HR; lra.
  }
Qed.

Definition pcmIntegerEncodeUnsigned
  (depth     : nat)
  (amplitude : R)
: R :=
  let s : R := Rplus (Rdiv amplitude 2%R) 0.5%R in
    Rmult s (pow 2 depth).

Remark pcmIntegerEncodeUnsigned16_Low : pcmIntegerEncodeUnsigned 16 (-1) = 0.
Proof.
  unfold pcmIntegerEncodeUnsigned.
  lra.
Qed.

Remark pcmIntegerEncodeUnsigned16_Mid : pcmIntegerEncodeUnsigned 16 0 = 32768.
Proof.
  unfold pcmIntegerEncodeUnsigned.
  lra.
Qed.

Remark pcmIntegerEncodeUnsigned16_High : pcmIntegerEncodeUnsigned 16 1 = 65536.
Proof.
  unfold pcmIntegerEncodeUnsigned.
  lra.
Qed.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Lists.List.
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.

Local Open Scope string_scope.
Local Open Scope char_scope.

(** * Compatibility *)

(** The version number change required for a given comparison. *)
Inductive compatVersionChange : Set :=
  (** No version change is required. *)
  | CVersionChangeNone
  (** The change requires a minor version number increment. *)
  | CVersionChangeMinor
  (** The change required a major version number increment. *)
  | CVersionChangeMajor
  .

(** Change value equality decidable. *)
Theorem compatVersionChangeEqDec : forall (x y : compatVersionChange),
  {x = y}+{~x = y}.
Proof. decide equality. Qed.

(** A record of a change, and a reason why the change was at the given level. *)
Record compatVersionChangeRecord : Set := CVRMake {
  cvrChange : compatVersionChange;
  cvrReason : string
}.

(** The maximum compatibility change required from two version changes. *)
Definition compatVersionChangeMax
  (x y : compatVersionChange) 
: compatVersionChange :=
  match (x, y) with
  | (CVersionChangeMajor , _                  ) => CVersionChangeMajor
  | (_                   , CVersionChangeMajor) => CVersionChangeMajor
  | (CVersionChangeMinor , CVersionChangeNone ) => CVersionChangeMinor
  | (CVersionChangeNone  , CVersionChangeMinor) => CVersionChangeMinor
  | (CVersionChangeMinor , CVersionChangeMinor) => CVersionChangeMinor
  | (CVersionChangeNone  , CVersionChangeNone ) => CVersionChangeNone
  end.

(** The maximum function is reflexive. *)
Theorem compatVersionChangeMaxRefl : forall x,
  compatVersionChangeMax x x = x.
Proof.
  intros x.
  destruct x; auto.
Qed.

(** The maximum function is commutative. *)
Theorem compatVersionChangeMaxComm : forall x y,
  compatVersionChangeMax x y = compatVersionChangeMax y x.
Proof.
  intros x y.
  destruct x; auto.
  destruct y; auto.
Qed.

(** The maximum function is associative. *)
Theorem compatVersionChangeMaxAssoc : forall x y z,
  compatVersionChangeMax x (compatVersionChangeMax y z) = compatVersionChangeMax (compatVersionChangeMax x y) z.
Proof.
  intros x y.
  destruct x; (destruct y; destruct z; auto).
Qed.

Theorem compatVersionChangeMaxInv : forall x y,
  compatVersionChangeMax x y = CVersionChangeMajor
    <-> (x = CVersionChangeMajor) \/ (y = CVersionChangeMajor).
Proof.
  intros x y.
  constructor. {
    intros Hmax.
    destruct x. {
      destruct y.
      contradict Hmax; discriminate.
      contradict Hmax; discriminate.
      right; reflexivity.
    } {
      destruct y.
      contradict Hmax; discriminate.
      contradict Hmax; discriminate.
      right; reflexivity.
    } {
      destruct y.
      left; reflexivity.
      left; reflexivity.
      left; reflexivity.
    }
  } {
    intros Hmax.
    destruct x. {
      destruct Hmax as [HL|HR].
      contradict HL; discriminate.
      destruct y.
      contradict HR; discriminate.
      contradict HR; discriminate.
      reflexivity.
    } {
      destruct Hmax as [HL|HR].
      contradict HL; discriminate.
      destruct y.
      contradict HR; discriminate.
      contradict HR; discriminate.
      reflexivity.
    } {
      destruct Hmax as [HL|HR].
      destruct y.
      reflexivity.
      reflexivity.
      reflexivity.
      reflexivity.
    }
  }
Qed.

Inductive compatVersionMaxMinor : compatVersionChange -> compatVersionChange -> Prop :=
  | CVMMinorLeft : forall x y,
    x = CVersionChangeMinor /\ (y = CVersionChangeMinor \/ y = CVersionChangeNone) ->
      compatVersionMaxMinor x y
  | CVMMinorRight : forall x y,
    (x = CVersionChangeMinor \/ x = CVersionChangeNone) /\ y = CVersionChangeMinor ->
      compatVersionMaxMinor x y.

Theorem compatVersionChangeMaxMinorInv : forall x y,
  compatVersionChangeMax x y = CVersionChangeMinor
    <-> compatVersionMaxMinor x y.
Proof.
  intros x y.
  constructor. {
    intros Hmax.
    destruct x. {
      destruct y.
      contradict Hmax; discriminate.
      apply CVMMinorRight; intuition.
      contradict Hmax; discriminate.
    } {
      destruct y.
      apply CVMMinorLeft; intuition.
      apply CVMMinorLeft; intuition.
      contradict Hmax; discriminate.
    } {
      destruct y.
      contradict Hmax; discriminate.
      contradict Hmax; discriminate.
      contradict Hmax; discriminate.
    }
  } {
    intros Hmax.
    destruct Hmax as [p q [Hp Hq]|p q [Hp Hq]]. {
      subst p.
      destruct Hq. {
        subst q. reflexivity.
      } {
        subst q. reflexivity.
      }
    } {
      subst q.
      destruct Hp. {
        subst p. reflexivity.
      } {
        subst p. reflexivity.
      }
    }
  }
Qed.

Fixpoint compatVersionChangesMaximum
  (rs : list compatVersionChange)
: compatVersionChange :=
  match rs with
  | nil       => CVersionChangeNone
  | cons x xs => compatVersionChangeMax x (compatVersionChangesMaximum xs)
  end.

Theorem compatVersionChangesMaximumCorrect0 : forall cs,
  In CVersionChangeMajor cs ->
    compatVersionChangesMaximum cs = CVersionChangeMajor.
Proof.
  induction cs as [|x xs]. {
    intros Hin.
    inversion Hin.
  } {
    intros Hin.
    destruct (in_inv Hin) as [HL|HR]. {
      subst x.
      simpl.
      reflexivity.
    } {
      pose proof (IHxs HR) as Hr.
      simpl.
      rewrite Hr.
      rewrite compatVersionChangeMaxComm.
      reflexivity.
    }
  }
Qed.

Theorem compatVersionChangesMaximumCorrect1 : forall cs,
  ~In CVersionChangeMajor cs ->
    compatVersionChangesMaximum cs <> CVersionChangeMajor.
Proof.
  intros cs.
  induction cs as [|x xs]. {
    intros Hnil.
    discriminate.
  } {
    intros Hnin.
    rewrite not_in_cons in Hnin.
    inversion Hnin as [HL HR].
    pose proof (IHxs HR) as Hind.
    simpl.
    destruct x. {
      destruct (compatVersionChangesMaximum xs). {
        discriminate.
      } {
        discriminate.
      } {
        contradict Hind.
        reflexivity.
      }
    } {
      destruct (compatVersionChangesMaximum xs). {
        discriminate.
      } {
        discriminate.
      } {
        contradict Hind.
        reflexivity.
      }
    } {
      contradict HL.
      reflexivity.
    }
  }
Qed.

Theorem compatVersionChangesMaximumCorrect2 : forall cs,
  ~In CVersionChangeMajor cs ->
    In CVersionChangeMinor cs ->
      compatVersionChangesMaximum cs = CVersionChangeMinor.
Proof.
  induction cs as [|x xs]. {
    intros Hnin Hin.
    inversion Hin.
  } {
    intros Hnin Hin.
    destruct (in_inv Hin) as [HL|HR]. {
      subst x.
      simpl.
      rewrite not_in_cons in Hnin.
      inversion Hnin as [HnL HnR].
      pose proof (compatVersionChangesMaximumCorrect1 _ HnR) as Hne.
      destruct (compatVersionChangesMaximum xs). {
        reflexivity.
      } {
        reflexivity.
      } {
        contradict Hne.
        reflexivity.
      }
    } {
      rewrite not_in_cons in Hnin.
      inversion Hnin as [HnL HnR].
      pose proof (IHxs HnR HR) as Hr.
      simpl.
      rewrite Hr.
      destruct x. {
        reflexivity.
      } {
        reflexivity.
      } {
        contradict HnL.
        reflexivity.
      }
    }
  }
Qed.

Theorem compatVersionChangesMaximumCorrect3 : forall cs,
  ~In CVersionChangeMajor cs ->
    ~In CVersionChangeMinor cs ->
      compatVersionChangesMaximum cs = CVersionChangeNone.
Proof.
  induction cs as [|x xs]. {
    intros Hnin0 Hnin1.
    reflexivity.
  } {
    intros Hnin0 Hnin1.
    simpl.
    rewrite not_in_cons in Hnin0.
    destruct Hnin0 as [HL0 HR0].
    rewrite not_in_cons in Hnin1.
    destruct Hnin1 as [HL1 HR1].
    rewrite (IHxs HR0 HR1).
    destruct x. {
      reflexivity.
    } {
      contradict HL1; reflexivity.
    } {
      contradict HL0; reflexivity.
    }
  }
Qed.

Definition compatVersionChangeRecordsMaximum
  (rs : list compatVersionChangeRecord)
: compatVersionChange :=
  compatVersionChangesMaximum (map (fun r => cvrChange r) rs).

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.

(** A descriptor string. *)
Definition descriptor := string.

(** The class of objects that can be described by descriptor strings. *)
Class describable (A : Set) := {
  descriptorOf : A -> descriptor
}.

Definition descriptorEqDec : forall (x y : descriptor),
  {x = y}+{x <> y}.
Proof.
  apply string_dec.
Qed.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.PArith.PArith.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Init.Nat.
Require Import Coq.Lists.List.
Require Import Coq.Unicode.Utf8_core.

(* Set Mangle Names. *)

(** The property of _x_ being divisible by 8. *)

Definition divisible8 (x : nat) : Prop :=
  modulo x 8 = 0.

(** If _x_ and _y_ are divisible by _z_, then _x + y_ is also divisible by _z_. *)

Theorem divisiblityNAdd : ∀ (x y z : nat),
  0 ≠ z → x mod z = 0 → y mod z = 0 → (x + y) mod z = 0.
Proof.
  intros x y z Hz Hx Hy.
  destruct y as [|y].
    (* If y = 0, then this matches one of our assumptions already. *)
    rewrite Nat.add_0_r; exact Hx.
    (* Otherwise, the following property always holds given that the divisor is ≠ 0. *)
    assert ((x mod z + S y) mod z = (x + S y) mod z) as Heq.
      apply (Nat.add_mod_idemp_l x (S y) z).
      apply (Nat.neq_sym 0 z Hz).
    (* x mod z = 0 *)
    rewrite Hx in Heq.
    (* 0 + S y = S y *)
    rewrite Nat.add_0_l in Heq.
    rewrite <- Heq.
    exact Hy.
Qed.

(** Divisibility is preserved over addition. *)

Theorem divisibilityNFoldPlus : ∀ z xs,
  0 ≠ z →
    Forall (λ n, n mod z = 0) xs →
      (fold_right plus 0 xs) mod z = 0.
Proof.
  intros z xs Hnz HforAll.
  induction xs as [|y ys].
  - apply (Nat.mod_0_l z (Nat.neq_sym 0 z Hnz)).
  - assert (fold_right add 0 (y :: ys) = y + fold_right add 0 ys) as Hfoldeq by reflexivity.
    rewrite Hfoldeq.
    assert (fold_right add 0 ys mod z = 0) as Hfoldeq2. {
      apply IHys.
      apply (@Forall_inv_tail nat (λ n : nat, n mod z = 0) y ys HforAll).
    }
    rewrite divisiblityNAdd.
    reflexivity.
    exact Hnz.
    apply (@Forall_inv nat (λ n : nat, n mod z = 0) y ys HforAll).
    exact Hfoldeq2.
Qed.

(** Divisibility is preserved over addition. *)

Theorem divisiblity8Add : ∀ (x y : nat),
  divisible8 x → divisible8 y → divisible8 (x + y).
Proof.
  intros x y Hx Hy.
  unfold divisible8 in *.
  apply divisiblityNAdd.
  discriminate.
  trivial.
  trivial.
Qed.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.

Require Import Aurantium.Descriptor.

Local Open Scope string_scope.

Inductive hashAlgorithm : Set :=
  | HA_SHA256
  .

Theorem hashAlgorithmEqDec : forall (x y : hashAlgorithm),
  {x = y}+{x <> y}.
Proof.
  intros x.
  destruct x;
    (destruct y;
      try decide equality
    ).
Qed.

Definition hashAlgorithmDescribe (f : hashAlgorithm) : descriptor :=
  match f with
  | HA_SHA256   => "com.io7m.aurantium.sha2_256"
  end.

#[export]
Instance hashAlgorithmDescribable : describable hashAlgorithm := {
  descriptorOf h := hashAlgorithmDescribe h
}.

Inductive hashValue : Set := hashValueMake {
  hvAlgorithm : hashAlgorithm;
  hvValue     : string
}.

Theorem hashValueEqDec : forall (x y : hashValue),
  {x = y}+{x <> y}.
Proof.
  intros x.
  destruct x;
    (destruct y;
      try decide equality;
      try apply string_dec;
      try decide equality
    ).
Qed.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.

Local Open Scope string_scope.
Local Open Scope char_scope.

Inductive identifier : Set := identifierMake {
  idName              : string;
  idVersionMajor      : nat;
  idVersionMinor      : nat;
  idVersionMajorRange : idVersionMajor <= 4294967295;
  idVersionMinorRange : idVersionMinor <= 4294967295
}.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Reals.Reals.
Require Import Coq.Reals.ROrderedType.
Require Import Psatz.

(* Set Mangle Names. *)

Local Open Scope R_scope.

(** A real number is normalized if it is in the range _[0, 1]_ *)
Definition isNormalized (x : R) : Prop :=
  0 <= x /\ x <= 1.

(** Normalization is preserved over multiplication. *)
Theorem isNormalizedMult : forall x y,
  isNormalized x -> isNormalized y -> isNormalized (Rmult x y).
Proof.
  intros x y [Hx0 Hx1] [Hy0 Hy1].
  unfold isNormalized.
  split.
  apply Rmult_le_pos.
  exact Hx0.
  exact Hy0.
  pose proof (Rmult_le_compat _ _ _ _ Hx0 Hy0 Hx1 Hy1) as Hcomp.
  assert (1 * 1 = 1) as Hobvious by apply (Rmult_1_r 1).
  rewrite <- Hobvious.
  exact Hcomp.
Qed.

(** Two real numbers that do not compare as equal according to
    a boolean comparison are not equal. *)
Lemma Reqb_neq : forall x y,
  Reqb x y = false -> x <> y.
Proof.
  intros x y Heqb.
  unfold not.
  intro Heq.
  rewrite Heq in Heqb.
  assert (Reqb y y = true) as Hbt. {
    rewrite Reqb_eq.
    reflexivity.
  }
  rewrite Heqb in Hbt.
  inversion Hbt.
Qed.

(** A supporting lemma that proves LTE ordering over division. *)
Lemma Rdiv_scale_0 : forall x y z,
  0 <= x
    -> 0 < z
      -> 0 < y
        -> x <= y <= z
          -> x / z <= x / y.
Proof.
  intros x y z H0x H0z H0y [Hxy Hyz].
  unfold Rdiv.
  assert (x * / z = / z * x) as H0 by apply Rmult_comm.
  assert (x * / y = / y * x) as H1 by apply Rmult_comm.
  rewrite H0; clear H0.
  rewrite H1; clear H1.
  apply Rmult_le_compat_r.
  apply H0x.
  apply Rle_Rinv.
  exact H0y.
  exact H0z.
  exact Hyz.
Qed.

(** A supporting lemma that proves LTE ordering over division. *)
Lemma Rdiv_le_1 : forall x y,
  0 <= x <= y ->
    0 < y ->
      x / y <= 1.
Proof.
  intros x y [H0x Hxy] H0y.
  unfold Rdiv.
  destruct (Rle_lt_or_eq_dec _ _ H0x) as [Hlt|Heq]. {
    assert (x / y <= x / x) as Hsc. {
      apply (Rdiv_scale_0 x x y H0x H0y Hlt).
      intuition.
    }
    unfold Rdiv in Hsc.
    rewrite <- Rinv_r_sym in Hsc.
    exact Hsc.
    unfold not.
    intro Hcontra.
    rewrite Hcontra in Hlt.
    pose proof (Rlt_irrefl 0) as Hcontra2.
    contradiction.
  } {
    rewrite <- Heq.
    rewrite Rmult_0_l.
    intuition.
  }
Qed.

(** 
  The _between_ function returns the amount by which _x_ is
  "between" _y_ and _z_. If the function returns 1, _x = z_.
  If the function returns 0, _x = y_. If the function returns
  0.5, _x_ is exactly halfway between _y_ and _z_.

  If _low = high_, the function returns _x_ unchanged. Arguably,
  a silly question yields a silly answer.
*)

Definition between
  (x    : R)
  (low  : R)
  (high : R)
: R :=
  let n := x - low in
  let d := high - low in
    match Reqb d 0 with
    | true  => x
    | false => n / d
    end.

(** The _between_ function should yield normalized results. *)
Theorem betweenNorm : forall x lo hi,
  lo < hi
    -> lo <= x <= hi
      -> isNormalized (between x lo hi).
Proof.
  intros x lo hi Hlohi [Hlox Hxhi].
  unfold isNormalized.
  unfold between.
  destruct (Reqb (hi - lo) 0) eqn:Heqb. {
    rewrite R_as_OT.eqb_eq in Heqb.
    pose proof (Rlt_Rminus _ _ Hlohi) as Hlt.
    pose proof (Rlt_not_eq _ _ Hlt) as Hneq.
    symmetry in Heqb.
    contradiction.
  } {
    pose proof (Reqb_neq _ _ Heqb) as Heq.
    clear Heqb.
    assert ((x - lo) <= (hi - lo)) as Hrle by lra.
    destruct (Rtotal_order (hi - lo) 0) as [Hlt0|[Hfalse|Hgt0]]. {
      pose proof (Rminus_lt _ _ Hlt0) as Hcontra.
      pose proof (Rlt_asym _ _ Hcontra) as Hfalse.
      contradiction.
    } {
      contradiction.
    } {
      pose proof (Rgt_lt _ _ Hgt0) as H0lt.
      assert (0 <= x - lo) as H0le by lra.
      constructor. {
        apply (Rle_mult_inv_pos _ _ H0le H0lt).
      } {
        assert (0 <= x - lo <= hi - lo) as Hmx by lra.
        apply (Rdiv_le_1 (x-lo) (hi-lo) Hmx H0lt).
      }
    }
  }
Qed.

(** Linearly interpolate between _x_ and _y_ by the (normalized)
    factor _f_. *)
Definition interpolate
  (x : R)
  (y : R)
  (f : R)
: R :=
  (x * (1 - f)) + (y * f).

(** If the interpolation factor is normalized, then _interpolate_
    always returns a value in _[x, y]_. *)
Lemma interpolateRange1 : forall x y f,
  x <= y
    -> isNormalized f
      -> x <= interpolate x y f <= y.
Proof.
  intros x y f Hxy [Hnf0 Hnf1].

  unfold interpolate.
  constructor. {
    replace x with (x * (1 - f) + x * f) at 1 by lra.
    eapply Rplus_le_compat. {
      apply Rle_refl.
    } {
      apply Rmult_le_compat_r.
      exact Hnf0.
      exact Hxy.
    }
  } {
    replace y with (y * (1 - f) + y * f) at 2 by lra.
    eapply Rplus_le_compat. {
      apply Rmult_le_compat_r.
      lra.
      exact Hxy.
    } {
      apply Rmult_le_compat_r.
      exact Hnf0.
      apply Rle_refl.
    }
  }
Qed.

(** If the interpolation factor is normalized, then _interpolate_
    always returns a value in _[x, y]_. *)
Lemma interpolateRange2 : forall x y f,
  y <= x
    -> isNormalized f
      -> y <= interpolate x y f <= x.
Proof.
  intros x y f Hyx [Hnf0 Hnf1].

  unfold interpolate.
  constructor. {
    replace y with (y * (1 - f) + y * f) at 1 by lra.
    eapply Rplus_le_compat. {
      apply Rmult_le_compat_r.
      lra.
      exact Hyx.
    } {
      apply Rmult_le_compat_r.
      exact Hnf0.
      apply Rle_refl.
    }
  } {
    replace x with (x * (1 - f) + x * f) at 2 by lra.
    eapply Rplus_le_compat. {
      apply Rle_refl.
    } {
      apply Rmult_le_compat_r.
      exact Hnf0.
      exact Hyx.
    }
  }
Qed.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Lists.List.

(** Return the set of elements that are in both _ea_ and _eb_, according to the 
    find function _f_. *)
Fixpoint intersectionPairs
  {A     : Set}
  (f     : A -> list A -> option A)
  (ea eb : list A)
: list (A * A) :=
  match ea with
  | nil => nil
  | cons a ea_rest =>
    match f a eb with
    | Some r => (a, r) :: intersectionPairs f ea_rest eb
    | None   =>           intersectionPairs f ea_rest eb
    end
  end.

(** The description of a "find" function; if _f_ applied to _x_ yields _y_,
    then _y_ must have been in _ys_. *)
Definition finds
  {A  : Set}
  (f  : A -> list A -> option A)
  (x  : A)
  (y  : A)
  (ys : list A)
: Prop :=
  f x ys = Some y <-> In y ys.

(** A proof of correctness for the _intersectionPairs_ function. *)
Theorem intersectionPairsIn : forall (A : Set) (ea eb : list A) efa efb f,
  (forall x y ys, finds f x y ys) ->
    In (efa, efb) (intersectionPairs f ea eb) ->
      In efa ea /\ In efb eb.
Proof.
  intros A ea.
  induction ea as [|a ea_rest]. {
    intros eb efa efb f Hfind Hin.
    inversion Hin.
  } {
    intros eb efa efb f Hfind Hin.
    simpl in Hin.
    destruct (f a eb) eqn:Haf. {
      destruct (in_inv Hin) as [Hin0|Hin1]. {
        assert (a = efa) by congruence.
        assert (a0 = efb) by congruence.
        subst a.
        subst a0.
        constructor.
        constructor; reflexivity.
        unfold finds in Hfind.
        rewrite (Hfind efa efb eb) in Haf.
        exact Haf.
      } {
        pose proof (IHea_rest eb efa efb f Hfind Hin1) as H0.
        intuition.
      }
    } {
      pose proof (IHea_rest eb efa efb f Hfind Hin) as H0.
      intuition.
    } 
  }
Qed.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Lists.List.
Require Import Coq.Init.Nat.
Require Import Coq.Arith.Peano_dec.
Require Import Coq.Arith.PeanoNat.
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Reals.Reals.
Require Import Coq.Reals.ROrderedType.

Require Import Psatz.

Require Import Aurantium.Compatibility.
Require Import Aurantium.Intersection.
Require Import Aurantium.Interpolation.
Require Import Aurantium.Descriptor.

Local Open Scope R_scope.
Local Open Scope string_scope.

Import ListNotations.

(* Set Mangle Names. *)

(** The type of key assignment flags.*)
Inductive keyAssignmentFlag : Set :=
  (** The key assignment should treat the clip as unpitched. *)
  | FlagUnpitched : keyAssignmentFlag.

Definition keyAssignmentFlagDescribe (f : keyAssignmentFlag) : descriptor :=
  match f with
  | FlagUnpitched   => "com.io7m.aurantium.unpitched"
  end.

#[export]
Instance keyAssignmentFlagDescribable : describable keyAssignmentFlag := {
  descriptorOf f := keyAssignmentFlagDescribe f
}.

(** Key assignment equality is decidable. *)
Theorem keyAssignmentFlagEqDec
  (x y : keyAssignmentFlag)
: {x = y}+{~x = y}.
Proof. decide equality. Qed.

(** 
  A key assignment assigns a clip to a range of keys, and describes
  the amplitude of the clip based on the velocity of the incoming
  note, and the position of the key within the key range. 

  A clip that should not vary in amplitude can simply assign a
  value of 1.0 for all values.
*)

Inductive keyAssignment : Set := {
  (** The unique identifier of the key assignment. *)
  kaId : nat;
  (** The lowest key value that will trigger this clip. *)
  kaValueStart : nat;
  (** The key value at which the clip plays at the normal playback rate. *)
  kaValueCenter: nat;
  (** The highest key value that will trigger this clip. *)
  kaValueEnd : nat;
  kaValueEndRange : le kaValueEnd 294967295;
  (** The key values must be ordered. *)
  kaValueStartOrder : le kaValueStart kaValueCenter;
  kaValueCenterOrder : le kaValueCenter kaValueEnd;
  (** The clip that will be triggered. *)
  kaClipId : nat;
  (** The amplitude at which this clip will be played when at the lowest key value. *)
  kaAmplitudeAtKeyStart : R;
  (** The amplitude at which this clip will be played when at the center key value. *)
  kaAmplitudeAtKeyCenter : R;
  (** The amplitude at which this clip will be played when at the highest key value. *)
  kaAmplitudeAtKeyEnd : R;
  (** The amplitude values are normalized values. *)
  kaAmplitudeAtKeyStartNormal : isNormalized kaAmplitudeAtKeyStart;
  kaAmplitudeAtKeyCenterNormal : isNormalized kaAmplitudeAtKeyCenter;
  kaAmplitudeAtKeyEndNormal : isNormalized kaAmplitudeAtKeyEnd;
  (** The velocity value at which this clip starts to be triggered. *)
  kaAtVelocityStart : R;
  (** The velocity value at which the amplitude of this clip is at maximum. *)
  kaAtVelocityCenter : R;
  (** The velocity value at which this clip stops being triggered. *)
  kaAtVelocityEnd : R;
  (** The velocity values are normalized values and are correctly ordered. *)
  kaAtVelocityStartNormal : isNormalized kaAtVelocityStart;
  kaAtVelocityCenterNormal : isNormalized kaAtVelocityCenter;
  kaAtVelocityEndNormal : isNormalized kaAtVelocityEnd;
  kaAtVelocityStartOrder : kaAtVelocityStart <= kaAtVelocityCenter;
  kaAtVelocityCenterOrder : kaAtVelocityCenter <= kaAtVelocityEnd;
  (** The amplitude at which this clip will be played when at the starting velocity value. *)
  kaAmplitudeAtVelocityStart : R;
  (** The amplitude at which this clip will be played when at the center velocity value. *)
  kaAmplitudeAtVelocityCenter : R;
  (** The amplitude at which this clip will be played when at the end velocity value. *)
  kaAmplitudeAtVelocityEnd : R;
  (** The amplitude values are normalized values. *)
  kaAmplitudeAtVelocityStartNormal : isNormalized kaAmplitudeAtVelocityStart;
  kaAmplitudeAtVelocityCenterNormal : isNormalized kaAmplitudeAtVelocityCenter;
  kaAmplitudeAtVelocityEndNormal : isNormalized kaAmplitudeAtVelocityEnd;
  (** The associated key assignment flags. *)
  kaFlags : list keyAssignmentFlag;
  kaFlagsUnique : NoDup kaFlags;
}.

(** The values that make two key assignments "equal". *)
Definition keyAssignmentValuesEq (x y : keyAssignment) : Prop :=
     (kaId x)                        = (kaId y)
  /\ (kaValueStart x)                = (kaValueStart y)
  /\ (kaValueCenter x)               = (kaValueCenter y)
  /\ (kaValueEnd x)                  = (kaValueEnd y)
  /\ (kaClipId x)                    = (kaClipId y)
  /\ (kaAmplitudeAtKeyStart x)       = (kaAmplitudeAtKeyStart y)
  /\ (kaAmplitudeAtKeyCenter x)      = (kaAmplitudeAtKeyCenter y)
  /\ (kaAmplitudeAtKeyEnd x)         = (kaAmplitudeAtKeyEnd y)
  /\ (kaAtVelocityStart x)           = (kaAtVelocityStart y)
  /\ (kaAtVelocityCenter x)          = (kaAtVelocityCenter y)
  /\ (kaAtVelocityEnd x)             = (kaAtVelocityEnd y)
  /\ (kaAmplitudeAtVelocityStart x)  = (kaAmplitudeAtVelocityStart y)
  /\ (kaAmplitudeAtVelocityCenter x) = (kaAmplitudeAtVelocityCenter y)
  /\ (kaAmplitudeAtVelocityEnd x)    = (kaAmplitudeAtVelocityEnd y)
  /\ (kaFlags x)                     = (kaFlags y)
.

(** The proposition that describes how two key assignments can overlap. *)
Definition keyAssignmentsOverlap (x y : keyAssignment) : Prop :=
  let x1 := kaValueStart x in
  let x2 := kaValueEnd x in
  let y1 := kaValueStart y in
  let y2 := kaValueEnd y in
    ge x2 y1 /\ ge y2 x1.

(** Overlapping is reflexive. An object always overlaps itself. *)
Theorem keyAssignmentsOverlapReflexive : forall x,
  keyAssignmentsOverlap x x.
Proof.
  intros x.
  unfold keyAssignmentsOverlap.
  unfold ge.
  pose proof (kaValueStartOrder x) as H0.
  pose proof (kaValueCenterOrder x) as H1.
  intuition.
Qed.

(** Overlapping is commutative. *)
Theorem keyAssignmentsOverlapCommutative : forall x y,
  keyAssignmentsOverlap x y -> keyAssignmentsOverlap y x.
Proof.
  intros x y.
  unfold keyAssignmentsOverlap.
  unfold ge.
  pose proof (kaValueStartOrder x) as H0.
  pose proof (kaValueCenterOrder x) as H1.
  pose proof (kaValueStartOrder y) as H2.
  pose proof (kaValueCenterOrder y) as H3.
  intuition.
Qed.

Lemma nat_le_dec : forall n m,
  {le n m}+{~le n m}.
Proof.
  intros n m.
  destruct (Compare.le_dec n m) as [HL0|HR0]. {
    intuition.
  } {
    destruct (Nat.eq_dec n m); intuition.
  }
Qed.

(** Determining overlap is decidable. *)
Theorem keyAssignmentsOverlapDecidable : forall x y,
  {keyAssignmentsOverlap x y}+{~keyAssignmentsOverlap x y}.
Proof.
  intros x y.
  unfold keyAssignmentsOverlap.
  unfold ge.
  pose proof (kaValueStartOrder x) as H0.
  pose proof (kaValueCenterOrder x) as H1.
  pose proof (kaValueStartOrder y) as H2.
  pose proof (kaValueCenterOrder y) as H3.
  destruct (nat_le_dec (kaValueStart y) (kaValueEnd x)) as [HL0|HR0].
  destruct (nat_le_dec (kaValueStart x) (kaValueEnd y)) as [HL1|HR1].
  intuition.
  right; intuition.
  right; intuition.
Qed.

(** Determine the list of key assignments that overlap _k_ (but that are not _k_). *)
Definition keyAssignmentsOverlapping
  (k  : keyAssignment)
  (ka : list keyAssignment)
: list keyAssignment :=
  filter (fun j =>
    match keyAssignmentsOverlapDecidable k j with
    | left _ =>
      match Nat.eq_dec (kaId k) (kaId j) with
      | left _  => false
      | right _ => true
      end
    | right _ => false
    end) ka.

(** The _keyAssignmentsOverlapping_ function never returns _k_. *)
Theorem keyAssignmentsOverlappingNotSelf : forall k ka,
  ~In k (keyAssignmentsOverlapping k ka).
Proof.
  intros k ka.
  unfold keyAssignmentsOverlapping.
  rewrite filter_In.
  destruct (keyAssignmentsOverlapDecidable k k) as [HodT|HodF]. {
    destruct (Nat.eq_dec (kaId k) (kaId k)) as [HeT|HeF]. {
      intuition.
    } {
      contradict HeF. reflexivity.
    }
  } {
    contradict HodF.
    apply keyAssignmentsOverlapReflexive.
  }
Qed.

(** The _keyAssignmentsOverlapping_ function finds overlapping assignments. *)
Theorem keyAssignmentsOverlappingFind0 : forall k ka p,
  (In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p))
    -> In p (keyAssignmentsOverlapping k ka).
Proof.
  intros k ka p [HinP [Hover Hneq]].
  unfold keyAssignmentsOverlapping.
  rewrite filter_In.
  destruct (keyAssignmentsOverlapDecidable k p) as [HodT|HodF]. {
    destruct (Nat.eq_dec (kaId k) (kaId p)) as [HeT|HeF]. {
      intuition.
    } {
      intuition.
    }
  } {
    contradiction.
  }
Qed.

(** The _keyAssignmentsOverlapping_ function finds overlapping assignments. *)
Theorem keyAssignmentsOverlappingFind1 : forall k ka p,
  In p (keyAssignmentsOverlapping k ka) ->
    In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p).
Proof.
  intros k ka p HinP.
  unfold keyAssignmentsOverlapping in HinP.
  rewrite filter_In in HinP.
  destruct (keyAssignmentsOverlapDecidable k p) as [HodT|HodF]. {
    destruct (Nat.eq_dec (kaId k) (kaId p)) as [HeT|HeF]. {
      intuition.
    } {
      intuition.
    }
  } {
    destruct HinP as [HL HR].
    contradict HR.
    discriminate.
  }
Qed.

(** The _keyAssignmentsOverlapping_ function finds overlapping assignments. *)
Theorem keyAssignmentsOverlappingFind : forall k ka p,
  (In p ka /\ keyAssignmentsOverlap k p /\ (kaId k) <> (kaId p))
    <-> In p (keyAssignmentsOverlapping k ka).
Proof.
  constructor.
  apply keyAssignmentsOverlappingFind0.
  apply keyAssignmentsOverlappingFind1.
Qed.

(** Whether two key assignments are "equal" is decidable. *)
Theorem keyAssignmentValuesEqDec
  (x y : keyAssignment)
: {keyAssignmentValuesEq x y}+{~keyAssignmentValuesEq x y}.
Proof.
  unfold keyAssignmentValuesEq.
  destruct (Nat.eq_dec (kaId x) (kaId y)).
  destruct (Nat.eq_dec (kaValueStart x) (kaValueStart y)).
  destruct (Nat.eq_dec (kaValueCenter x) (kaValueCenter y)).
  destruct (Nat.eq_dec (kaValueEnd x) (kaValueEnd y)).
  destruct (Nat.eq_dec (kaClipId x) (kaClipId y)).
  destruct (Req_dec (kaAmplitudeAtKeyStart x) (kaAmplitudeAtKeyStart y)).
  destruct (Req_dec (kaAmplitudeAtKeyCenter x) (kaAmplitudeAtKeyCenter y)).
  destruct (Req_dec (kaAmplitudeAtKeyEnd x) (kaAmplitudeAtKeyEnd y)).
  destruct (Req_dec (kaAtVelocityStart x) (kaAtVelocityStart y)).
  destruct (Req_dec (kaAtVelocityCenter x) (kaAtVelocityCenter y)).
  destruct (Req_dec (kaAtVelocityEnd x) (kaAtVelocityEnd y)).
  destruct (Req_dec (kaAmplitudeAtVelocityStart x) (kaAmplitudeAtVelocityStart y)).
  destruct (Req_dec (kaAmplitudeAtVelocityCenter x) (kaAmplitudeAtVelocityCenter y)).
  destruct (Req_dec (kaAmplitudeAtVelocityEnd x) (kaAmplitudeAtVelocityEnd y)).
  destruct (list_eq_dec keyAssignmentFlagEqDec (kaFlags x) (kaFlags y)).
  left; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
  right; intuition.
Qed.

(** The property that states the conditions under which a key assignment 
    matches a key and velocity. *)
Definition keyAssignmentMatches
  (key        : nat)
  (velocity   : R)
  (assignment : keyAssignment)
: Prop :=
  let p0 := ((kaValueStart assignment) <= key)%nat in
  let p1 := (key <= (kaValueEnd assignment))%nat in
  let p2 := ((kaAtVelocityStart assignment) <= velocity)%R in
  let p3 := (velocity <= (kaAtVelocityEnd assignment))%R in
    p0 /\ p1 /\ p2 /\ p3.

(** Whether or not a key assignment matches is decidable. *)
Theorem keyAssignmentMatchesDecidable : forall k v a,
  {keyAssignmentMatches k v a}+{~keyAssignmentMatches k v a}.
Proof.
  intros k v a.
  destruct (le_dec (kaValueStart a) k) as [H0L|H0R]. {
    destruct (le_dec k (kaValueEnd a)) as [H1L|H1R]. {
      destruct (Rle_dec (kaAtVelocityStart a) v) as [H2L|H2R]. {
        destruct (Rle_dec v (kaAtVelocityEnd a)) as [H3L|H3R]. {
          left. constructor; auto.
        } {
          right.
          unfold not; intro Hcontra; inversion Hcontra.
          intuition.
        }
      } {
        right.
        unfold not; intro Hcontra; inversion Hcontra.
        intuition.
      }
    } {
      right.
      unfold not; intro Hcontra; inversion Hcontra.
      intuition.
    }
  } {
    right.
    unfold not; intro Hcontra; inversion Hcontra.
    intuition.
  }
Qed.

(** 
  The result of evaluating a single key assignment. 

  When a key is evaluated, a playback rate is returned which is then used by
  applications to speed up or slow down clip playback in order to affect the
  perceived pitch.

  Evaluation also returns a pair of amplitude values. One amplitude is based
  upon the velocity of the original note; this change in amplitude can be used
  by audio map authors to allow instruments to vary their timbre based on how
  soft or hard a note is hit. The other amplitude is based on the key; this
  change in amplitude can be used by audio map authors to allow instruments
  to vary their timbre based on the pitches of notes.

  Normally, applications will multiply these two amplitude values to produce
  a final normalized amplitude.
*)

Inductive keyEvaluation : Set := keyEvaluationMake {
  keyEvaluationClipId                  : nat;
  keyEvaluationVelocityAmplitude       : R;
  keyEvaluationVelocityAmplitudeNormal : isNormalized keyEvaluationVelocityAmplitude;
  keyEvaluationKeyAmplitude            : R;
  keyEvaluationKeyAmplitudeNormal      : isNormalized keyEvaluationKeyAmplitude;
  keyEvaluationRate                    : R;
  keyEvaluationRateNonNegative         : 0 <= keyEvaluationRate
}.

(** Evaluate the amplitude of the given key assignment based on 
    the velocity. *)

Definition keyAssignmentEvaluateAmplitudeForVelocity
  (velocity   : R)
  (assignment : keyAssignment)
: R :=
  let kLow := kaAtVelocityStart assignment in
  let kMid := kaAtVelocityCenter assignment in
  let kTop := kaAtVelocityEnd assignment in
    match Rcompare velocity kMid with
    | Eq => kaAmplitudeAtVelocityCenter assignment
    | Lt =>
      match Rlt_dec kLow kMid with
      | left _ =>
        let f := between velocity kLow kMid in
          interpolate
            (kaAmplitudeAtVelocityStart assignment)
            (kaAmplitudeAtVelocityCenter assignment)
            f
      | right _ =>
          (kaAmplitudeAtVelocityCenter assignment)
      end
    | Gt =>
      match Rlt_dec kMid kTop with
      | left _ =>
        let f := between velocity kMid kTop in
          interpolate
            (kaAmplitudeAtVelocityCenter assignment)
            (kaAmplitudeAtVelocityEnd assignment)
            f
      | right _ =>
          (kaAmplitudeAtVelocityCenter assignment)
      end
    end.

(** Either _x <= y_ or _y <= x_. *)
Lemma Rle_or : forall x y,
  x <= y \/ y <= x.
Proof.
  intros x y.
  destruct (Rle_lt_dec x y) as [HL|HR]. {
    left; exact HL.
  } {
    right; apply Rlt_le; exact HR.
  }
Qed.

(**
  The amplitude returned by evaluating a key assignment based on
  velocity is always normalized.
*)
Theorem keyAssignmentEvaluateAmplitudeForVelocityNormalized : forall k v a,
  keyAssignmentMatches k v a
    -> isNormalized (keyAssignmentEvaluateAmplitudeForVelocity v a).
Proof.
  intros k v a [Hm0 [Hm1 [Hm2 Hm3]]].
  unfold isNormalized.

  unfold keyAssignmentEvaluateAmplitudeForVelocity.
  destruct (Rcompare_spec v (kaAtVelocityCenter a)) as [H0|H1|H2]. {
    (* v = center *)
    destruct (kaAmplitudeAtVelocityCenterNormal a) as [Hk0 Hk1].
    lra.
  } {
    (* v < center *)
    destruct (kaAmplitudeAtVelocityStartNormal a) as [Hk0 Hk1].
    destruct (kaAmplitudeAtVelocityCenterNormal a) as [Hk2 Hk3].
    remember (kaAtVelocityStart a) as kVs.
    remember (kaAtVelocityCenter a) as kVc.
    remember (kaAmplitudeAtVelocityStart a) as kAVs.
    remember (kaAmplitudeAtVelocityCenter a) as kAVc.

    remember (between v kVs kVc) as f.
    assert (kVs <= kVc) as Hscle by lra.

    destruct (Rle_or kAVs kAVc) as [HL|HR]. {
      destruct (Rlt_dec kVs kVc) as [Hlt|Hnlt]. {
        assert (isNormalized f) as Hnormf. {
          rewrite Heqf.
          apply (betweenNorm v kVs kVc Hlt).
          lra.
        }
        pose proof (interpolateRange1 kAVs kAVc f HL Hnormf).
        lra.
      } {
        lra.
      }
    } {
      destruct (Rlt_dec kVs kVc) as [Hlt|Hnlt]. {
        assert (isNormalized f) as Hnormf. {
          rewrite Heqf.
          apply (betweenNorm v kVs kVc Hlt).
          lra.
        }
        pose proof (interpolateRange2 _ _ _ HR Hnormf).
        lra.
      } {
        lra.
      }
    }
  } {
    (* center < v *)
    destruct (kaAmplitudeAtVelocityCenterNormal a) as [Hk0 Hk1].
    destruct (kaAmplitudeAtVelocityEndNormal a) as [Hk2 Hk3].
    remember (kaAtVelocityCenter a) as kVc.
    remember (kaAtVelocityEnd a) as kVe.
    remember (kaAmplitudeAtVelocityCenter a) as kAVc.
    remember (kaAmplitudeAtVelocityEnd a) as kAVe.

    remember (between v kVc kVe) as f.
    assert (kVc <= kVe) as Hcele by lra.

    destruct (Rle_or kAVc kAVe) as [HL|HR]. {
      destruct (Rlt_dec kVc kVe) as [Hlt|Hnlt]. {
        assert (isNormalized f) as Hnormf. {
          rewrite Heqf.
          apply (betweenNorm v kVc kVe Hlt).
          lra.
        }
        pose proof (interpolateRange1 kAVc kAVe f HL Hnormf).
        lra.
      } {
        lra.
      }
    } {
      destruct (Rlt_dec kVc kVe) as [Hlt|Hnlt]. {
        assert (isNormalized f) as Hnormf. {
          rewrite Heqf.
          apply (betweenNorm v kVc kVe Hlt).
          lra.
        }
        pose proof (interpolateRange2 _ _ _ HR Hnormf).
        lra.
      } {
        lra.
      }
    }
  }
Qed.

(** Evaluate the amplitude of the given key assignment based on 
    the key. *)
Definition keyAssignmentEvaluateAmplitudeForKey
  (key        : nat)
  (assignment : keyAssignment)
: R :=
  let kLow := kaValueStart assignment in
  let kMid := kaValueCenter assignment in
  let kTop := kaValueEnd assignment in
    match Nat.compare key kMid with
    | Eq => kaAmplitudeAtKeyCenter assignment
    | Lt =>
      match lt_dec kLow kMid with
      | right _  => kaAmplitudeAtKeyCenter assignment
      | left _ =>
        let f := between (INR key) (INR kLow) (INR kMid) in
          interpolate
            (kaAmplitudeAtKeyStart assignment)
            (kaAmplitudeAtKeyCenter assignment)
            f
      end
    | Gt =>
      match lt_dec kMid kTop with
      | right _  => kaAmplitudeAtKeyCenter assignment
      | left _ =>
        let f := between (INR key) (INR kMid) (INR kTop) in
          interpolate
            (kaAmplitudeAtKeyCenter assignment)
            (kaAmplitudeAtKeyEnd assignment)
            f
      end
    end.

(**
  The amplitude returned by evaluating a key assignment based on
  key is always normalized.
*)
Theorem keyAssignmentEvaluateAmplitudeForKeyNormalized : forall k v a,
  keyAssignmentMatches k v a
    -> isNormalized (keyAssignmentEvaluateAmplitudeForKey k a).
Proof.
  intros k v a [Hm0 [Hm1 [Hm2 Hm3]]].
  unfold isNormalized.

  unfold keyAssignmentEvaluateAmplitudeForKey.
  destruct (Nat.compare_spec k (kaValueCenter a)) as [Heq|Hlt|Hgt]. {
    destruct (kaAmplitudeAtKeyCenterNormal a).
    lra.
  } {
    (* k < center *)
    (* Abbreviations to make the proof context readable. *)
    remember (kaValueStart a) as ks.
    remember (kaValueCenter a) as kc.
    remember (kaAmplitudeAtKeyStart a) as kAKs.
    remember (kaAmplitudeAtKeyCenter a) as kAKc.
    remember (INR k) as rk.
    remember (INR ks) as rks.
    remember (INR kc) as rkc.
    remember (between rk rks rkc) as f.

    (* If the starting key is < the center key... *)
    destruct (lt_dec ks kc) as [Hklt|Hknlt]. {
      assert (isNormalized f) as Hnorm. {
        rewrite Heqf.
        rewrite Heqrk.
        rewrite Heqrks.
        rewrite Heqrkc.
        apply betweenNorm.
        apply lt_INR.
        exact Hklt.
        pose proof (kaValueStartOrder a) as Hso.
        split.
        apply le_INR.
        exact Hm0.
        apply le_INR.
        apply Nat.lt_le_incl.
        exact Hlt.
      }

      pose proof (kaAmplitudeAtKeyCenterNormal a) as HKACN.
      rewrite <- HeqkAKc in HKACN.
      destruct HKACN as [HKACN0 HKACN1].

      pose proof (kaAmplitudeAtKeyStartNormal a) as HKASN.
      rewrite <- HeqkAKs in HKASN.
      destruct HKASN as [HKASN0 HKASN1].

      (* Is the starting key amplitude <= the center key amplitude? *)
      destruct (Rle_or kAKs kAKc) as [Hle0|Hle1]. {
         pose proof (interpolateRange1 _ _ _ Hle0 Hnorm) as Hint0.
         lra.
      } {
         pose proof (interpolateRange2 _ _ _ Hle1 Hnorm) as Hint0.
         lra.
      }
    } {
      (* The starting key = the center key. *)
      pose proof (kaAmplitudeAtKeyCenterNormal a) as HKACN.
      rewrite <- HeqkAKc in HKACN.
      destruct HKACN as [HKACN0 HKACN1].
      lra.
    }
  } {
    (* center < k *)
    (* Abbreviations to make the proof context readable. *)
    remember (kaValueCenter a) as kc.
    remember (kaValueEnd a) as ke.
    remember (kaAmplitudeAtKeyCenter a) as kAKc.
    remember (kaAmplitudeAtKeyEnd a) as kAKe.
    remember (INR k) as rk.
    remember (INR kc) as rkc.
    remember (INR ke) as rke.
    remember (between rk rkc rke) as f.

    (* If the center key is < the end key... *)
    destruct (lt_dec kc ke) as [Hklt|Hknlt]. {
      assert (isNormalized f) as Hnorm. {
        rewrite Heqf.
        rewrite Heqrk.
        rewrite Heqrkc.
        rewrite Heqrke.
        apply betweenNorm.
        apply lt_INR.
        exact Hklt.
        pose proof (kaValueCenterOrder a) as Hso.
        split.
        apply le_INR.
        apply Nat.lt_le_incl.
        exact Hgt.
        apply le_INR.
        exact Hm1.
      }

      pose proof (kaAmplitudeAtKeyCenterNormal a) as HKACN.
      rewrite <- HeqkAKc in HKACN.
      destruct HKACN as [HKACN0 HKACN1].

      pose proof (kaAmplitudeAtKeyEndNormal a) as HKAEN.
      rewrite <- HeqkAKe in HKAEN.
      destruct HKAEN as [HKAEN0 HKAEN1].

      (* Is the starting key amplitude <= the center key amplitude? *)
      destruct (Rle_or kAKc kAKe) as [Hle0|Hle1]. {
         pose proof (interpolateRange1 _ _ _ Hle0 Hnorm) as Hint0.
         lra.
      } {
         pose proof (interpolateRange2 _ _ _ Hle1 Hnorm) as Hint0.
         lra.
      }
    } {
      (* The center key = the end key. *)
      pose proof (kaAmplitudeAtKeyCenterNormal a) as HKACN.
      rewrite <- HeqkAKc in HKACN.
      destruct HKACN as [HKACN0 HKACN1].
      lra.
    }
  }
Qed.

(** A small proof to check that Coq's Rpower really means x ^ y. *)
Lemma powCheck : Rpower 2.0 4.0 = 16.0.
Proof.
  assert (2.0 = INR 2%nat) as H2 by (simpl; lra).
  assert (4.0 = INR 4%nat) as H4 by (simpl; lra).
  assert (16.0 = INR 16%nat) as H16 by (simpl; lra).
  rewrite H2.
  rewrite H4.
  rewrite H16.
  rewrite Rpower_pow.
  simpl; lra.
  simpl; lra.
Qed.

(** Determine the pitch ratio for a change in frequency of a given number
    of semitones. *)

Definition semitonesPitchRatio (semitones : R) : R :=
  Rpower 2.0 (Rdiv semitones 12.0).

(** The pitch ratio is always non-negative. *)

Lemma semitonesPitchRatioNonNegative : forall s,
  Rle 0 (semitonesPitchRatio s).
Proof.
  intros s.
  unfold semitonesPitchRatio.
  unfold Rpower.
  remember (s / 12.0 * ln 2.0) as x.
  pose proof (exp_pos x) as Hp.
  lra.
Qed.

(** Evaluate the playback rate of the given key assignment based on 
    the key. *)

Definition keyAssignmentEvaluateRate
  (key        : nat)
  (assignment : keyAssignment)
: R :=
  match (in_dec keyAssignmentFlagEqDec FlagUnpitched (kaFlags assignment)) with
  | left _  => 1.0
  | right _ =>
    let kLow := kaValueStart assignment in
    let kMid := kaValueCenter assignment in
      match Nat.compare key kMid with
      | Eq => 1
      | Lt =>
        let delta := minus kMid key in
          semitonesPitchRatio (-(INR delta))
      | Gt =>
        let delta := minus key kMid in
          semitonesPitchRatio (INR delta)
      end
  end.

(** The playback rate returned by evaluating a key assignment
    is always non-negative. *)

Theorem keyAssignmentEvaluateRateNonNegative : forall k v a,
  keyAssignmentMatches k v a
    -> Rle 0 (keyAssignmentEvaluateRate k a).
Proof.
  intros k v a [Hm0 [Hm1 [Hm2 Hm3]]].

  unfold keyAssignmentEvaluateRate.
  destruct (in_dec keyAssignmentFlagEqDec FlagUnpitched (kaFlags a)) as [Hin|Hnin]. {
    lra.
  } {
    destruct (Nat.compare_spec k (kaValueCenter a)) as [Heq|Hlt|Hgt]. {
      intuition.
    } {
      apply semitonesPitchRatioNonNegative.
    } {
      apply semitonesPitchRatioNonNegative.
    }
  }
Qed.

(** Fully evaluate a key assignment. *)

Definition keyAssignmentEvaluateFull
  (key        : nat)
  (velocity   : R)
  (assignment : keyAssignment)
: option keyEvaluation :=
  match keyAssignmentMatchesDecidable key velocity assignment with
  | right _ => None
  | left p  =>
    let clip  := kaClipId assignment in
    let ampV  := keyAssignmentEvaluateAmplitudeForVelocity velocity assignment in
    let ampVP := keyAssignmentEvaluateAmplitudeForVelocityNormalized _ _ _ p in
    let ampK  := keyAssignmentEvaluateAmplitudeForKey key assignment in
    let ampKP := keyAssignmentEvaluateAmplitudeForKeyNormalized _ _ _ p in
    let rate  := keyAssignmentEvaluateRate key assignment in
    let rateP := keyAssignmentEvaluateRateNonNegative _ _ _ p in
      Some (keyEvaluationMake clip ampV ampVP ampK ampKP rate rateP)
  end.

(** A proposition stating that the list of key assignments is sorted. *)

Inductive keyAssignmentListIsSorted : list keyAssignment -> Prop :=
  | kaListNone : keyAssignmentListIsSorted []
  | kaListOne : forall s, keyAssignmentListIsSorted [s]
  | kaListCons : forall s0 s1 s,
    lt (kaId s0) (kaId s1) ->
      keyAssignmentListIsSorted (s0 :: s) ->
        keyAssignmentListIsSorted (s1 :: s0 :: s).

(** The tail of a sorted list is still sorted. *)

Theorem keyAssignmentListIsSortedTail : forall x xs,
  keyAssignmentListIsSorted (x :: xs) ->
    keyAssignmentListIsSorted xs.
Proof.
  intros x xs Hcons.
  inversion Hcons.
  constructor.
  auto.
Qed.

(** A set of key assignments. *)

Inductive keyAssignments : Set := {
  kasList       : list keyAssignment;
  kasListSorted : keyAssignmentListIsSorted kasList
}.

(** Evaluate all key assignments that match the given key and velocity. *)

Fixpoint keyAssignmentsEvaluateFull
  (key         : nat)
  (velocity    : R)
  (assignments : list keyAssignment)
: list keyEvaluation :=
  match assignments with
  | nil         => []
  | cons a rest =>
    match keyAssignmentEvaluateFull key velocity a with
    | None   => keyAssignmentsEvaluateFull key velocity rest
    | Some r => cons r (keyAssignmentsEvaluateFull key velocity rest)
    end
  end.

(** The rules that define the version number increments required for
    a pair of key assignments. *)

Definition keyAssignmentCompatCompare
  (k0 k1 : keyAssignment)
: compatVersionChangeRecord :=
  match keyAssignmentValuesEqDec k0 k1 with
  | left _ => 
    CVRMake CVersionChangeNone ""
  | right _ => 
    CVRMake CVersionChangeMajor "The values of the key assignment were changed."
  end.

(** Find the key assignment with the given ID. *)

Fixpoint keyAssignmentForId
  (i  : nat)
  (ka : list keyAssignment)
: option keyAssignment :=
  match ka with
  | nil         => None
  | cons a rest =>
    match Nat.eq_dec (kaId a) i with
    | left _  => Some a
    | right _ => keyAssignmentForId i rest
    end
  end.

Theorem keyAssignmentForIdIn : forall ks i k,
  keyAssignmentListIsSorted ks ->
    Some k = keyAssignmentForId i ks ->
      In k ks.
Proof.
  intros ks.
  induction ks as [|x xs]. {
    intros i k Hsort Hfalse.
    inversion Hfalse.
  } {
    intros i k Hsort Hsome.
    simpl in Hsome.
    destruct (Nat.eq_dec (kaId x) i). {
      assert (k = x) by congruence.
      subst k.
      constructor; reflexivity.
    } {
      pose proof (keyAssignmentListIsSortedTail _ _ Hsort) as HsT.
      pose proof (IHxs i k HsT Hsome) as Hind.
      apply in_cons.
      exact Hind.
    }
  }
Qed.

Theorem keyAssignmentForIdMatches : forall ks i k,
  keyAssignmentListIsSorted ks ->
    Some k = keyAssignmentForId i ks ->
      kaId k = i.
Proof.
  intros ks.
  induction ks as [|x xs]. {
    intros i k Hsort Hfalse.
    inversion Hfalse.
  } {
    intros i k Hsort Hsome.
    simpl in Hsome.
    destruct (Nat.eq_dec (kaId x) i). {
      assert (k = x) by congruence.
      subst k.
      intuition.
    } {
      pose proof (keyAssignmentListIsSortedTail _ _ Hsort) as HsT.
      pose proof (IHxs i k HsT Hsome) as Hind.
      exact Hind.
    }
  }
Qed.

Lemma keyAssignmentIdNeq : forall k0 k1,
  kaId k0 <> kaId k1 ->
    k0 <> k1.
Proof.
  intros k0 k1 Hneq.
  inversion k0.
  inversion k1.
  intuition.
  subst k0.
  apply Hneq.
  reflexivity.
Qed.

Theorem keyAssignmentForIdInNot : forall ks i k,
  keyAssignmentListIsSorted ks ->
    kaId k = i ->
      None = keyAssignmentForId i ks ->
        ~In k ks.
Proof.
  intros ks.
  induction ks as [|x xs]. {
    intros i k Hsort Heq Hnone.
    intuition.
  } {
    intros i k Hsort Heq Hnone.
    simpl in Hnone.
    subst i.
    destruct (Nat.eq_dec (kaId x) (kaId k)). {
      inversion Hnone.
    } {
      pose proof (keyAssignmentListIsSortedTail _ _ Hsort) as HsT.
      pose proof (IHxs (kaId k) k HsT eq_refl Hnone) as Hind.
      rewrite not_in_cons.
      constructor.
      apply keyAssignmentIdNeq.
      intuition.
      exact Hind.
    }
  }
Qed.

(** Determine all the elements of _ka_ that are not in _kb_. *)

Fixpoint keyAssignmentsRemoved
  (ka : list keyAssignment)
  (kb : list keyAssignment)
: list keyAssignment :=
  match ka with
  | nil => []
  | cons a rest =>
    match keyAssignmentForId (kaId a) kb with
    | None   => cons a (keyAssignmentsRemoved rest kb)
    | Some _ => keyAssignmentsRemoved rest kb
    end
  end.

(** If _k_ is in the list of removed elements, then _k_ must have
    been in _ka_. *)

Theorem keyAssignmentsRemovedIn : forall ka kb k,
  In k (keyAssignmentsRemoved ka kb) -> In k ka.
Proof.
  intros ka.
  induction ka as [|a rest]. {
    intros kb k Hin0.
    inversion Hin0.
  } {
    intros kb k Hin0.
    simpl in Hin0.
    destruct (keyAssignmentForId (kaId a) kb) eqn:Hm. {
      pose proof (IHrest kb k Hin0) as H0.
      apply in_cons.
      exact H0.
    } {
      destruct Hin0 as [HL|HR]. {
        subst a.
        constructor; reflexivity.
      } {
        pose proof (IHrest kb k HR) as H0.
        apply in_cons.
        exact H0.
      }
    }
  }
Qed.

(** If _k_ is in the list of removed elements, then _k_ must not have
    been in _kb_. *)

Theorem keyAssignmentsRemovedInNot : forall ka kb k,
  keyAssignmentListIsSorted kb ->
    In k (keyAssignmentsRemoved ka kb) ->
      ~In k kb.
Proof.
  intros ka.
  induction ka as [|a rest]. {
    intros kb k Hsort Hin0.
    inversion Hin0.
  } {
    intros kb k Hsort Hin0.
    simpl in Hin0.
    destruct (keyAssignmentForId (kaId a) kb) eqn:Hm. {
      apply IHrest.
      exact Hsort.
      exact Hin0.
    } {
      destruct Hin0 as [HL|HR]. {
        subst a.
        apply (keyAssignmentForIdInNot kb (kaId k) k Hsort eq_refl (eq_sym Hm)).
      } {
        apply IHrest.
        exact Hsort.
        exact HR.
      }
    }
  }
Qed.

(** Determine all the elements of _kb_ that are not in _ka_. *)
Definition keyAssignmentsAdded
  (ka : list keyAssignment)
  (kb : list keyAssignment)
: list keyAssignment :=
  keyAssignmentsRemoved kb ka.

(** If _k_ is in the list of added elements, then _k_ must have
    been in _kb_. *)

Theorem keyAssignmentsAddedIn : forall kb ka k,
  In k (keyAssignmentsAdded ka kb) -> In k kb.
Proof.
  unfold keyAssignmentsAdded.
  apply keyAssignmentsRemovedIn.
Qed.

(** If _k_ is in the list of added elements, then _k_ must not have
    been in _ka_. *)

Theorem keyAssignmentsAddedInNot : forall ka kb k,
  keyAssignmentListIsSorted ka ->
    In k (keyAssignmentsAdded ka kb) ->
      ~In k ka.
Proof.
  intros ka.
  unfold keyAssignmentsAdded.
  intros kb k Hsort Hin.
  apply (keyAssignmentsRemovedInNot _ _ _ Hsort Hin).
Qed.

Definition keyAssignmentsCompatCompareRemoved
  (r : list keyAssignment)
: list compatVersionChangeRecord :=
  map (fun a => CVRMake CVersionChangeMajor "A key assignment was removed.") r.

Lemma keyAssignmentsCompatCompareRemovedForall : forall r,
  Forall (fun a => cvrChange a = CVersionChangeMajor)
    (keyAssignmentsCompatCompareRemoved r).
Proof.
  intros r.
  apply Forall_map.
  induction r as [|y ys]. {
    constructor.
  } {
    simpl.
    constructor. reflexivity.
    apply IHys.
  }
Qed.

Definition keyAssignmentsCompatCompareAdd
  (k  : keyAssignment)
  (ka : list keyAssignment)
: compatVersionChangeRecord :=
  match keyAssignmentsOverlapping k ka with
  | nil => CVRMake CVersionChangeMinor "A key assignment was added."
  | _   => CVRMake CVersionChangeMajor "A key assignment was added that overlaps with an existing assignment."
  end.

Definition keyAssignmentsCompatCompareAdded
  (added : list keyAssignment)
  (ka    : list keyAssignment)
: list compatVersionChangeRecord :=
  map (fun a => keyAssignmentsCompatCompareAdd a ka) added.

Definition keyAssignmentsCompatCompareChanged
  (r : list (keyAssignment * keyAssignment))
: list compatVersionChangeRecord :=
  map (fun p => keyAssignmentCompatCompare (fst p) (snd p)) r.

Definition keyAssignmentsCompatCompareFull
  (ka kb : list keyAssignment)
: list compatVersionChangeRecord :=
  let f              := (fun k ks => keyAssignmentForId (kaId k) ks) in
  let removed        := keyAssignmentsRemoved ka kb in
  let added          := keyAssignmentsAdded ka kb in
  let changed        := intersectionPairs f ka kb in
  let removedChanges := keyAssignmentsCompatCompareRemoved removed in
  let addedChanges   := keyAssignmentsCompatCompareAdded added kb in
  let changedChanges := keyAssignmentsCompatCompareChanged changed in
    removedChanges ++ addedChanges ++ changedChanges.

(** If there's a non-empty list of removed elements, a major version change is required. *)
Theorem keyAssignmentsCompatCompareMajor0 : forall ka kb,
  [] <> keyAssignmentsRemoved ka kb ->
    compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
      = CVersionChangeMajor.
Proof.
  intros ka kb H_ne.
  unfold keyAssignmentsCompatCompareFull.
  apply compatVersionChangesMaximumCorrect0.
  apply in_map_iff.
  destruct (keyAssignmentsRemoved ka kb) as [|y ys]. {
    contradict H_ne; reflexivity.
  } {
    simpl.
    exists {| cvrChange := CVersionChangeMajor; cvrReason := "A key assignment was removed." |}.
    intuition.
  }
Qed.

(** Adding an overlapping key assignment is a major change. *)
Theorem keyAssignmentsCompatCompareMajor1 : forall ka kb k,
  [] = keyAssignmentsRemoved ka kb ->
    (forall f, [] = keyAssignmentsCompatCompareChanged (intersectionPairs f ka kb)) ->
      In k (keyAssignmentsAdded ka kb) ->
        [] <> (keyAssignmentsOverlapping k kb) ->
        compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
          = CVersionChangeMajor.
Proof.
  intros ka kb k Hrm Hch Hin Hover.
  unfold keyAssignmentsCompatCompareFull.
  rewrite <- Hrm.
  rewrite <- Hch.
  simpl.
  rewrite app_nil_r.

  destruct (keyAssignmentsAdded ka kb) as [|y ys]. {
    inversion Hin.
  } {
    simpl.
    destruct (in_inv Hin) as [HL|HR]. {
      subst k.
      unfold keyAssignmentsCompatCompareAdd.
      destruct (keyAssignmentsOverlapping y kb). {
        contradict Hover. reflexivity.
      } {
        unfold compatVersionChangeRecordsMaximum.
        simpl.
        reflexivity.
      }
    } {
      unfold keyAssignmentsCompatCompareAdded.
      unfold compatVersionChangeRecordsMaximum.
      simpl.

      (* We can show that either one of the arguments _must_ be equal to Major. *)
      rewrite (
        compatVersionChangeMaxInv
          (cvrChange (keyAssignmentsCompatCompareAdd y kb))
          (compatVersionChangesMaximum
            (map (fun r : compatVersionChangeRecord => cvrChange r) 
              (map (fun a : keyAssignment => keyAssignmentsCompatCompareAdd a kb) ys)))
      ).

      (* And we know that the right argument _must_ be Major, because k is in
         that part of the list. *)
      right.

      (* We can rewrite the nested maps to something less complicated. *)
      rewrite map_map.

      (* We can prove that k evaluates to a Major change. *)
      assert (
        cvrChange (keyAssignmentsCompatCompareAdd k kb) = CVersionChangeMajor
      ) as Hkmajor. {
        unfold keyAssignmentsCompatCompareAdd.
        destruct (keyAssignmentsOverlapping k kb). {
          contradict Hover; reflexivity.
        } {
          reflexivity.
        }
      }

      (* And we can prove that the result of evaluating k is in the list. *)
      pose proof (
        in_map 
          (fun x : keyAssignment => cvrChange (keyAssignmentsCompatCompareAdd x kb)) 
          ys k HR
      ) as HinM.
      simpl in HinM.
      rewrite Hkmajor in HinM.

      (* We have a lemma that tells us that if anything in the list is Major,
         then the result is Major. *)
      apply compatVersionChangesMaximumCorrect0.
      exact HinM.
    }
  }
Qed.

(** Adding a non-overlapping key assignment is a minor change. *)
Theorem keyAssignmentsCompatCompareMinor0 : forall ka kb,
  [] = keyAssignmentsRemoved ka kb ->
    (forall f, [] = keyAssignmentsCompatCompareChanged (intersectionPairs f ka kb)) ->
      [] <> (keyAssignmentsAdded ka kb) ->
        Forall (fun j => [] = keyAssignmentsOverlapping j kb) (keyAssignmentsAdded ka kb) ->
          compatVersionChangeRecordsMaximum (keyAssignmentsCompatCompareFull ka kb)
           = CVersionChangeMinor.
Proof.
  intros ka kb Heq0 Heq1 Hneq0 Hfa.
  unfold keyAssignmentsCompatCompareFull.
  rewrite <- Heq0.
  rewrite <- Heq1.
  simpl.
  rewrite app_nil_r.

  destruct (keyAssignmentsAdded ka kb) as [|y ys]. {
    contradict Hneq0; reflexivity.
  } {
    simpl.
    pose proof (Forall_inv Hfa) as Hfa0.
    simpl in Hfa0.
    unfold keyAssignmentsCompatCompareAdd.
    destruct (keyAssignmentsOverlapping y kb). {
      unfold compatVersionChangeRecordsMaximum.
      simpl.

      (* We can show that either one of the arguments _must_ be equal to Minor
         and the other to something minor or less. *)
      rewrite (
        compatVersionChangeMaxMinorInv
          CVersionChangeMinor
            (compatVersionChangesMaximum
              (map (fun r : compatVersionChangeRecord => cvrChange r)
                 (keyAssignmentsCompatCompareAdded ys kb)))
      ).

      unfold keyAssignmentsCompatCompareAdded.
      rewrite map_map.

      (* We can prove that y evaluates to a Major change. *)
      assert (
        cvrChange (keyAssignmentsCompatCompareAdd y kb) = CVersionChangeMinor
      ) as Hkminor. {
        unfold keyAssignmentsCompatCompareAdd.
        destruct (keyAssignmentsOverlapping y kb) eqn:Hover. {
          reflexivity.
        } {
          contradict Hover.
          pose proof (Forall_inv Hfa) as Hfa1.
          simpl in Hfa1.
          rewrite <- Hfa1.
          discriminate.
        }
      }

      (* We can prove that all elements map to a minor change. *)
      assert (
        Forall
          (fun k => k = CVersionChangeMinor) 
          (map (fun x : keyAssignment => 
            cvrChange (keyAssignmentsCompatCompareAdd x kb)) ys)
      ) as Hfa1. {
        rewrite Forall_map.
        rewrite Forall_forall.
        pose proof (Forall_inv_tail Hfa) as Hfat.

        intros j Hj.
        unfold keyAssignmentsCompatCompareAdd.
        rewrite Forall_forall in Hfat.
        rewrite <- (Hfat j Hj).
        reflexivity.
      }

      apply CVMMinorLeft.
      constructor. {
        reflexivity.
      } {
        clear Hneq0.
        clear Hfa.
        clear Hfa0.
        clear Hkminor.
        induction (map (fun x : keyAssignment => cvrChange (keyAssignmentsCompatCompareAdd x kb)) ys) as [|z zs]. {
          right; reflexivity.
        } {
          left.
          pose proof (Forall_inv Hfa1) as Hfb0.
          pose proof (Forall_inv_tail Hfa1) as Hfb1.
          simpl.
          rewrite Hfb0.

          destruct (IHzs Hfb1) as [H0|H1]. {
            rewrite H0.
            reflexivity.
          } {
            rewrite H1.
            reflexivity.
          }
        }
      }
    }
    contradict Hfa0.
    discriminate.
  }
Qed.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.
Require Import Coq.Lists.List.
Require Import Coq.Unicode.Utf8_core.

Local Open Scope string_scope.

Import ListNotations.

Inductive metadataValue : Set := MetadataValue {
  mKey   : string;
  mValue : string
}.

Inductive metadata : Set := Metadata {
  mValues : list metadataValue
}.

Require Import Coq.Arith.PeanoNat.
Require Import Coq.Lists.List.
Require Import Coq.Unicode.Utf8_core.

Require Import Aurantium.Divisible8.
Require Import Aurantium.Descriptor.

Import ListNotations.

Inductive octetOrder : Set :=
  | OctetOrderBig
  | OctetOrderLittle.

Inductive bit : Set :=
  | B0
  | B1.

Inductive octet : Set :=
  | OctExact  : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet
  | OctRemain : bit -> bit -> bit -> bit -> bit -> bit -> bit -> bit -> octet.

Definition octetIsRemainder (o : octet): Prop :=
  match o with
  | OctExact  _ _ _ _ _ _ _ _ => False
  | OctRemain _ _ _ _ _ _ _ _ => True
  end.

Definition octetIsExact (o : octet): Prop :=
  match o with
  | OctExact  _ _ _ _ _ _ _ _ => True
  | OctRemain _ _ _ _ _ _ _ _ => False
  end.

Lemma octetIsRemainderNotExact : forall (o : octet), octetIsRemainder o -> ¬octetIsExact o.
Proof.
  intros o Hrem Hfalse.
  destruct o; contradiction.
Qed.

Lemma octetIsExactNotRemainder : forall (o : octet), octetIsExact o -> ¬octetIsRemainder o.
Proof.
  intros o Hrem Hfalse.
  destruct o; contradiction.
Qed.

Inductive bitsOctetsHasRemainder : list octet -> Prop :=
  | BOHasRemainder : forall (prefix : list octet) (o : octet),
    Forall octetIsExact prefix ->
      octetIsRemainder o ->
        bitsOctetsHasRemainder (prefix ++ o :: []).

Fixpoint octetsBigEndianAux
  (bits   : list bit)
  (octets : list octet)
: list octet :=
  match bits with
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest) =>
    octets ++ [OctExact b7 b6 b5 b4 b3 b2 b1 b0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 b2 b1 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 b2 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: b3 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 b3 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: b4 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 b4 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: b5 :: rest) =>
    octets ++ [OctRemain b7 b6 b5 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: b6 :: rest) =>
    octets ++ [OctRemain b7 b6 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | (b7 :: rest) =>
    octets ++ [OctRemain b7 B0 B0 B0 B0 B0 B0 B0] ++ octetsBigEndianAux rest []
  | [] =>
    octets
  end.

Definition octetsBigEndian (bits : list bit) : list octet :=
  octetsBigEndianAux bits [].

Definition octetsLittleEndian (bits : list bit) : list octet :=
  rev (octetsBigEndianAux bits []).

Definition listInduction8 :
  forall (A : Type),
  forall (P : list A -> Prop),
  P [] ->
  (forall (b0                      : A), P (b0 :: [])) ->
  (forall (b1 b0                   : A), P (b1 :: b0 :: [])) ->
  (forall (b2 b1 b0                : A), P (b2 :: b1 :: b0 :: [])) ->
  (forall (b3 b2 b1 b0             : A), P (b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b4 b3 b2 b1 b0          : A), P (b4 :: b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b5 b4 b3 b2 b1 b0       : A), P (b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b6 b5 b4 b3 b2 b1 b0    : A), P (b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: [])) ->
  (forall (b7 b6 b5 b4 b3 b2 b1 b0 : A) (rest : list A), P rest -> P (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: rest)) ->
  forall (L : list A), P L :=
  λ A P P0 P1 P2 P3 P4 P5 P6 P7 P8,
  fix f (l : list A) :=
    match l with
    | []                                                     => P0
    | x0 :: []                                               => P1 x0
    | (x0 :: x1 :: [])                                       => P2 x0 x1
    | (x0 :: x1 :: x2 :: [])                                 => P3 x0 x1 x2
    | (x0 :: x1 :: x2 :: x3 :: [])                           => P4 x0 x1 x2 x3
    | (x0 :: x1 :: x2 :: x3 :: x4 :: [])                     => P5 x0 x1 x2 x3 x4
    | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: [])               => P6 x0 x1 x2 x3 x4 x5
    | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: [])         => P7 x0 x1 x2 x3 x4 x5 x6
    | (x0 :: x1 :: x2 :: x3 :: x4 :: x5 :: x6 :: x7 :: rest) => P8 x0 x1 x2 x3 x4 x5 x6 x7 rest (f rest)
    end.

Lemma app_non_empty : forall (A : Type) (xs : list A) (y : A),
  xs ++ [y] <> [].
Proof.
  intros A xs y.
  unfold not.
  destruct xs as [|z zs].
    intros Hfalse; inversion Hfalse.
    intros Hfalse; inversion Hfalse.
Qed.

Lemma app_list_implies_eq : forall (A : Type) (x y : A) (xs : list A),
  xs ++ [x] = [y] -> xs = [] ∧ x = y.
Proof.
  intros A x y xs Happ.
  induction xs as [|z zs] eqn:Hxe.
  - constructor. reflexivity.
    rewrite (app_nil_l [x]) in Happ.
    injection Happ as Heq; exact Heq.
  - inversion Happ.
    assert (zs ++ [x] <> []) by (apply app_non_empty).
    contradiction.
Qed.

Lemma p8notZ : 8 <> 0.
Proof. discriminate. Qed.

Lemma list_mod8_0 : forall (A : Type) (xs : list A) (n7 n6 n5 n4 n3 n2 n1 n0 : A),
  divisible8 (length xs) -> divisible8 (length (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs)).
Proof.
  intros A xs n7 n6 n5 n4 n3 n2 n1 n0 Hlen8.
  unfold divisible8 in *.
  assert (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs
       = (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: []) ++ xs) as HlistEq
          by reflexivity.
  rewrite HlistEq.
  rewrite app_length.
  assert (length [n7; n6; n5; n4; n3; n2; n1; n0] = 8) as Hprefix8 by reflexivity.
  rewrite Hprefix8.
  rewrite <- (Nat.add_mod_idemp_l 8 (length xs) 8 p8notZ).
  rewrite (Nat.mod_same 8 p8notZ).
  rewrite (Nat.add_0_l).
  exact Hlen8.
Qed.

Lemma list_mod8_1 : forall (A : Type) (xs : list A) (n7 n6 n5 n4 n3 n2 n1 n0 : A),
  divisible8 (length (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs)) -> divisible8 (length xs).
Proof.
  intros A xs n7 n6 n5 n4 n3 n2 n1 n0 Hlen8.
  unfold divisible8 in *.
  assert (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs
       = (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: []) ++ xs) as HlistEq
          by reflexivity.
  rewrite HlistEq in Hlen8.
  rewrite app_length in Hlen8.
  assert (length [n7; n6; n5; n4; n3; n2; n1; n0] = 8) as Hprefix8 by reflexivity.
  rewrite Hprefix8 in Hlen8.
  rewrite <- (Nat.add_mod_idemp_l 8 (length xs) 8 p8notZ) in Hlen8.
  rewrite (Nat.mod_same 8 p8notZ) in Hlen8.
  rewrite (Nat.add_0_l) in Hlen8.
  exact Hlen8.
Qed.

Theorem list_mod8 : forall (A : Type) (xs : list A) (n7 n6 n5 n4 n3 n2 n1 n0 : A),
  divisible8 (length xs) <-> divisible8 (length (n7 :: n6 :: n5 :: n4 :: n3 :: n2 :: n1 :: n0 :: xs)).
Proof.
  intros A xs n7 n6 n5 n4 n3 n2 n1 n0.
  constructor.
  - apply list_mod8_0.
  - apply list_mod8_1.
Qed.

Theorem octetsBigEndianLengthDivisibleAllExact : forall (b : list bit),
  divisible8 (length b) -> Forall octetIsExact (octetsBigEndian b).
Proof.
  intros b Hlen8.
  unfold octetsBigEndian.
  induction b using listInduction8.
  - constructor.
  - inversion Hlen8.
  - inversion Hlen8.
  - inversion Hlen8.
  - inversion Hlen8.
  - inversion Hlen8.
  - inversion Hlen8.
  - inversion Hlen8.
  - simpl.
    rewrite <- list_mod8 in Hlen8.
    assert (Forall octetIsExact (octetsBigEndianAux b []))   as HallExact by (apply (IHb Hlen8)).
    assert (octetIsExact (OctExact b7 b6 b5 b4 b3 b2 b1 b0)) as Hexact    by constructor.
    apply (@Forall_cons octet octetIsExact (OctExact b7 b6 b5 b4 b3 b2 b1 b0) (octetsBigEndianAux b []) Hexact HallExact).
Qed.

Theorem octetsLittleEndianLengthDivisibleAllExact : forall (b : list bit),
  divisible8 (length b) -> Forall octetIsExact (octetsLittleEndian b).
Proof.
  intros b Hlen8.
  apply (Forall_rev (octetsBigEndianLengthDivisibleAllExact b Hlen8)).
Qed.

Theorem octetsBigEndianLengthDivisibleNoRemainder : forall (b : list bit),
  Forall octetIsExact (octetsBigEndian b) -> ¬ bitsOctetsHasRemainder (octetsBigEndian b).
Proof.
  intros b HallExact.
  unfold octetsBigEndian.
  intro Hfalse.
  inversion Hfalse as [prefix o HprefixAllExact HoIsRemainder HprefixEq].
  unfold octetsBigEndian in HallExact.
  (* We know that everything in the list is exact. *)
  (* We can show that o must be in this list according to HprefixEq. *)
  assert (In o (octetsBigEndianAux b [])) as HoInB. {
    assert (In o (prefix ++ [o])) as HoInPrefix by (apply (in_elt o prefix [])).
    rewrite HprefixEq in HoInPrefix.
    exact HoInPrefix.
  }
  (* And because o is in the list, it must be exact. *)
  assert (octetIsExact o) as HoIsExact. {
    rewrite Forall_forall in HallExact.
    apply (HallExact o HoInB).
  }
  (* There is a contradiction; o cannot be both exact and a remainder. *)
  apply (octetIsExactNotRemainder o HoIsExact HoIsRemainder).
Qed.

Lemma mod_8_lt_0 : forall (m : nat),
  0 < m mod 8 -> 0 < (m + 8) mod 8.
Proof.
  intros m Hlt.
  rewrite (Nat.add_mod m 8 8).
  rewrite (Nat.mod_same).
  rewrite (Nat.add_0_r).
  rewrite (Nat.mod_mod).
  exact Hlt.
  discriminate.
  discriminate.
  discriminate.
Qed.

Lemma mod_8_lt_1 : forall (m : nat),
  0 < (m + 8) mod 8 -> 0 < m mod 8.
Proof.
  intros m Hlt.
  rewrite (Nat.add_mod m 8 8) in Hlt.
  rewrite (Nat.mod_same)      in Hlt.
  rewrite (Nat.add_0_r)       in Hlt.
  rewrite (Nat.mod_mod)       in Hlt.
  exact Hlt.
  discriminate.
  discriminate.
  discriminate.
Qed.

Lemma mod_8_lt : forall (m : nat),
  0 < (m + 8) mod 8 <-> 0 < m mod 8.
Proof.
  constructor.
  apply mod_8_lt_1.
  apply mod_8_lt_0.
Qed.

Theorem octetsBigEndianLengthIndivisibleRemainder : forall (b : list bit),
  0 < length b mod 8 -> ∃ o, In o (octetsBigEndian b) ∧ octetIsRemainder o.
Proof.
  intros b Hlength.
  induction b using listInduction8.
  - inversion Hlength.
  - exists (OctRemain b0 B0 B0 B0 B0 B0 B0 B0).
    constructor.
    left. reflexivity.
    constructor.
  - exists (OctRemain b1 b0 B0 B0 B0 B0 B0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - exists (OctRemain b2 b1 b0 B0 B0 B0 B0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - exists (OctRemain b3 b2 b1 b0 B0 B0 B0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - exists (OctRemain b4 b3 b2 b1 b0 B0 B0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - exists (OctRemain b5 b4 b3 b2 b1 b0 B0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - exists (OctRemain b6 b5 b4 b3 b2 b1 b0 B0).
    constructor.
    left.
    constructor.
    constructor.
  - assert (0 < length b mod 8) as Hlt. {
      assert (length (b7 :: b6 :: b5 :: b4 :: b3 :: b2 :: b1 :: b0 :: b) = length b + 8) as Heq
        by (rewrite Nat.add_comm; reflexivity).
      rewrite Heq in Hlength.
      rewrite <- (mod_8_lt (length b)).
      exact Hlength.
    }
    assert (∃ o : octet, In o (octetsBigEndian b) ∧ octetIsRemainder o) as HEx
      by (apply (IHb Hlt)).
    destruct HEx as [ox [HoxIn HoxRem]].
    simpl.
    exists ox.
    constructor.
    right.
    exact HoxIn.
    exact HoxRem.
Qed.

Theorem octetsLittleEndianLengthIndivisibleRemainder : forall (b : list bit),
  0 < length b mod 8 -> ∃ o, In o (octetsLittleEndian b) ∧ octetIsRemainder o.
Proof.
  unfold octetsLittleEndian.
  intros b Hlen.
  assert (∃ o, In o (octetsBigEndian b) ∧ octetIsRemainder o) as Hexists
    by (apply (octetsBigEndianLengthIndivisibleRemainder b Hlen)).
  destruct Hexists as [ox [HoxIn HoxRem]].
  exists ox.
  rewrite <- (in_rev (octetsBigEndianAux b [])).
  constructor.
  exact HoxIn.
  exact HoxRem.
Qed.

Require Import Coq.Strings.String.

Local Open Scope string_scope.

Definition octetOrderDescribe (b : octetOrder) : descriptor :=
  match b with
  | OctetOrderBig    => "com.io7m.aurantium.endian_big"
  | OctetOrderLittle => "com.io7m.aurantium.endian_little"
  end.

#[export]
Instance octetOrderDescribable : describable octetOrder := {
  descriptorOf f := octetOrderDescribe f
}.

(*
 * Copyright © 2023 Mark Raynsford <code@io7m.com> https://www.io7m.com
 *
 * Permission to use, copy, modify, and/or distribute this software for any
 * purpose with or without fee is hereby granted, provided that the above
 * copyright notice and this permission notice appear in all copies.
 *
 * THE SOFTWARE IS PROVIDED "AS IS" AND THE AUTHOR DISCLAIMS ALL WARRANTIES
 * WITH REGARD TO THIS SOFTWARE INCLUDING ALL IMPLIED WARRANTIES OF
 * MERCHANTABILITY AND FITNESS. IN NO EVENT SHALL THE AUTHOR BE LIABLE FOR ANY
 * SPECIAL, DIRECT, INDIRECT, OR CONSEQUENTIAL DAMAGES OR ANY DAMAGES
 * WHATSOEVER RESULTING FROM LOSS OF USE, DATA OR PROFITS, WHETHER IN AN
 * ACTION OF CONTRACT, NEGLIGENCE OR OTHER TORTIOUS ACTION, ARISING OUT OF OR
 * IN CONNECTION WITH THE USE OR PERFORMANCE OF THIS SOFTWARE.
 *)

Require Import Coq.Arith.PeanoNat.
Require Import Coq.Strings.String.
Require Import Coq.Strings.Ascii.

Local Open Scope string_scope.
Local Open Scope char_scope.

Set Mangle Names.

Definition digitOfNat (n : nat) : ascii :=
  match n with
  | 0 => "0"
  | 1 => "1"
  | 2 => "2"
  | 3 => "3"
  | 4 => "4"
  | 5 => "5"
  | 6 => "6"
  | 7 => "7"
  | 8 => "8"
  | _ => "9"
  end.

Fixpoint stringOfNatAux (time n : nat) (acc : string) : string :=
  let acc' := String (digitOfNat (n mod 10)) acc in
  match time with
  | 0 => acc'
  | S time' =>
    match n / 10 with
    | 0 => acc'
    | n' => stringOfNatAux time' n' acc'
    end
  end.

Definition stringOfNat (n : nat) : string :=
  stringOfNatAux n n "".