Library ASCommon.Common
This file is the top level of most the ASCommon library. Most users should
just Require Import ASCommon.Common.
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 CBase.
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.
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.
λ 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.
countable for sigT, copied from prod_countable
#[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.
`{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.