🗳️ Voting_period_repr.v

Proofs

See code, Gitlab , OCaml

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

Require Import TezosOfOCaml.Proto_alpha.Environment.
Require TezosOfOCaml.Proto_alpha.Voting_period_repr.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Z.
Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Compare.

Require TezosOfOCaml.Proto_alpha.Environment.Proofs.Data_encoding.

Lemma string_of_kind_inj : ∀ x y,
  Voting_period_repr.string_of_kind x = Voting_period_repr.string_of_kind y →
  x = y.
  intros x y; destruct x, y; easy.
Qed.

Lemma kind_encoding_is_valid :
  Data_encoding.Valid.t (fun _ ⇒ True) Voting_period_repr.kind_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve kind_encoding_is_valid : Data_encoding_db.

Lemma succ_kind_inj : ∀ x y,
  Voting_period_repr.succ_kind x = Voting_period_repr.succ_kind y →
  x = y.
  intros x y; destruct x, y; easy.
Qed.

Lemma succ_kind_diff : ∀ x, Voting_period_repr.succ_kind x ≠ x.
  intro x; destruct x; easy.
Qed.

Module Valid.
  Import Voting_period_repr.voting_period.

  Record t (x : Voting_period_repr.voting_period) : Prop := {
    index : Int32.Valid.t x.(index);
    start_position : Int32.Valid.t x.(start_position);
  }.
End Valid.

Module Info.
  Module Valid.
    Import Voting_period_repr.info.

    Record t (x : Voting_period_repr.info) : Prop := {
      voting_period : Valid.t x.(voting_period);
      position : Int32.Valid.t x.(position);
      remaining : Int32.Valid.t x.(remaining);
    }.
  End Valid.
End Info.

Lemma encoding_is_valid :
  Data_encoding.Valid.t Valid.t Voting_period_repr.encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve encoding_is_valid : Data_encoding_db.

Lemma info_encoding_is_valid :
  Data_encoding.Valid.t Info.Valid.t Voting_period_repr.info_encoding.
  Data_encoding.Valid.data_encoding_auto.
Qed.
#[global] Hint Resolve info_encoding_is_valid : Data_encoding_db.

Lemma compare_is_valid :
  Compare.Valid.t
    (fun _ ⇒ True)
    (fun period ⇒ period.(Voting_period_repr.voting_period.index))
    Voting_period_repr.compare.
Proof.
  apply (Compare.equality (
    let proj x := x.(Voting_period_repr.voting_period.index) in
    Compare.projection proj Compare.Int32.(Compare.S.compare)
  )); [sfirstorder|].
  eapply Compare.implies.
  { eapply Compare.projection_is_valid.
    apply Compare.int32_is_valid.
  }
  all: sfirstorder.
Qed.