From Hammer Require Export Tactics.
From stdpp Require Export strings.
From stdpp Require Export fin.
From stdpp Require Export pretty.
From stdpp Require Export vector.
From stdpp Require Export finite.
From stdpp Require Export relations.
From stdpp Require Export propset.
From stdpp Require Export listset.
From stdpp.bitvector Require Export bitvector tactics.

Require Import Options.
Require Export CDestruct.
Require Export CMonads.
Require Export CArith.
Require Export CBool.
Require Export CList.
Require Export CVec.
Require Export COption.
Require Export CResult.
Require Export CBitvector.
Require Export CSets.
Require Export CMaps.
Require Export CInduction.
Require Export CBase.

Definition fun_add {A B} `{EqDecision A} (k : A) (v : B) (f : A → B) :=
  λ x, if k =? x then v else f x.

Definition dfun_add `{EqDecision A} `{CTrans A B} (k : A) (v : B k) (f : ∀ a, B a) :=
  λ x, match decide (k = x) with
       | left e ⇒ ctrans e v
       | _ ⇒ f x
       end.

#[global] Program Instance sigT_countable `{Countable A} (P : A → Type)
  `{EqDecision (sigT P)}
  `{∀ a : A, EqDecision (P a)} `{∀ a : A, Countable (P a)} : Countable (sigT P)
  := {|
    encode xy := prod_encode (encode (xy.T1)) (encode (xy.T2));
    decode p :=
      x ← prod_decode_fst p ≫= decode;
      y ← prod_decode_snd p ≫= decode; Some (existT x y)
  |}.
Next Obligation.
  intros ??????? [x y]. cbn.
  rewrite prod_decode_encode_fst, prod_decode_encode_snd; cbn.
  by repeat (rewrite decode_encode; cbn).
Qed.

Definition fforallb `{Finite A} (P : A → bool) : bool :=
  forallb P (enum A).

Global Instance fforallb_unfold `{Finite A} (P : A → bool) Q:
  (∀ a : A, BoolUnfold (P a) (Q a)) →
  BoolUnfold (fforallb P) (∀ a : A, Q a).
Proof.
  tcclean.
  unfold fforallb.
  rewrite bool_unfold.
  sauto lq:on dep:on.
Qed.

Definition fexistsb `{Finite A} (P : A → bool) : bool :=
  existsb P (enum A).

Global Instance fexistsb_unfold `{Finite A} (P : A → bool) Q:
  (∀ a : A, BoolUnfold (P a) (Q a)) →
  BoolUnfold (fexistsb P) (∃ a : A, Q a).
Proof.
  tcclean.
  unfold fexistsb.
  rewrite bool_unfold.
  sauto lq:on dep:on.
Qed.

Global Instance pretty_fin (n : nat) : Pretty (fin n) :=
  (fun n ⇒ pretty (n : nat)).
Global Hint Mode Pretty ! : typeclass_instances.

Definition fin_to_N {n : nat} : fin n → N := N.of_nat ∘ fin_to_nat.
Coercion fin_to_N : fin >-> N.
Lemma fin_to_N_lt {n : nat} (i : fin n) : (i < N.of_nat n)%N.
Proof. use (fin_to_nat_lt i). unfold fin_to_N. cbn. lia. Qed.