🍃 Bytes.v

Proofs

See code, Gitlab

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.
Require Import TezosOfOCaml.Environment.V8.Proofs.String.
Require Import TezosOfOCaml.Environment.V8.Proofs.Compare.

Boolean equality on [Bytes] is reflexive.

Lemma equal_reflexive bytes : Bytes.equal bytes bytes = true.
Proof.
  unfold Bytes.equal.
  apply String.equal_is_valid ; try constructor.
Qed.

Propositional equality and [equal] are equivalent on [Bytes].

Lemma equal_is_valid : Compare.Equal.Valid.t (fun _ ⇒ True) Bytes.equal.
Proof.
  unfold Compare.Equal.Valid.t.
  intros bytes1 bytes2 _ _.
  unfold Bytes.equal.
  apply String.equal_is_valid ; try constructor.
Qed.