Lvc.Infra.SigR

Require Import Util DecSolve Coq.Classes.RelationClasses PartialOrder .

Set Implicit Arguments.

Definition sig_R {A} {P:AProp} (R:A A Prop) (a b: { a : A | P a}) :=
match a, b with
| exist a _, exist b _R a b
end.

Instance sig_R_refl A (P:AProp) R `{Reflexive A R} : Reflexive (@sig_R A P R).
Proof.
hnf in H.
hnf; intros [a ?]. hnf. eauto.
Qed.

Instance sig_R_sym A (P:AProp) R `{Symmetric A R} : Symmetric (@sig_R A P R).
Proof.
hnf in H.
hnf; intros [a ?] [b ?]. eapply H.
Qed.

Instance sig_R_trans A (P:A Prop) R `{Transitive A R} : Transitive (@sig_R A P R).
Proof.
hnf; intros [a ?] [b ?] [c ?]. eapply H.
Qed.

Instance sig_R_Equivalence A (P:A Prop) R `{Equivalence A R} : Equivalence (@sig_R A P R).
Proof.
econstructor.
- hnf; intros; reflexivity.
- hnf; intros; symmetry; eauto.
- hnf; intros; etransitivity; eauto.
Qed.

Instance sig_R_anti A P R Eq `{EqA:Equivalence _ Eq} `{@Antisymmetric A Eq EqA R}
: @Antisymmetric _ (@sig_R _ P Eq) _ (@sig_R _ P R).
Proof.
intros [a ?] [b ?] B C; simpl in ×. eauto.
Qed.

Instance sig_R_dec A (P:A Prop) (R:AAProp)
`{ a b, Computable (R a b)} (a b:sig P) :
Computable (sig_R R a b).
Proof.
destruct a,b; simpl; eauto.
Defined.

Instance sig_R_proj1_sig A (P:AProp) (R:A A Prop)
: Proper (@sig_R A P R ==> R) (@proj1_sig A P).
Proof.
unfold Proper, respectful.
intros [a ?] [b ?]; simpl; eauto.
Qed.

Instance proj1_sig_poLe (Dom : Type) P (H:PartialOrder Dom)
: Proper (@poLe _ (@PartialOrder_sig _ H _) ==> poLe) (@proj1_sig Dom P).
Proof.
hnf; intros. destruct x,y. simpl in ×. eauto.
Qed.

Require Import Get MoreList.

Lemma list_sig_decomp A (P:AProp)
: list { a : A | P a }
{ L : list A | n a, get L n a P a }.
Proof.
intros.
refine (exist _ (@proj1_sig A P X) _).
intros. inv_get. destruct x. eauto.
Defined.