Commit 69e63615 authored by Robbert Krebbers's avatar Robbert Krebbers
Browse files

Bump Iris.

parent 47b09af3
Pipeline #14875 passed with stage
in 17 minutes and 53 seconds
......@@ -6,5 +6,5 @@ install: [make "install"]
remove: ["rm" "-rf" "'%{lib}%/coq/user-contrib/fri"]
depends: [
"coq" { (>= "8.7.2") | (= "dev") }
"coq-iris" { (= "dev.2019-02-06.0.4f086f68") | (= "dev") }
"coq-iris" { (= "dev.2019-02-20.0.8a8c1405") | (= "dev") }
]
From fri.algebra Require Export cmra.
From fri.algebra Require Import updates local_updates.
From stdpp Require Export collections coPset.
From stdpp Require Export sets coPset.
(** This is pretty much the same as algebra/gset, but I was not able to
generalize the construction without breaking canonical structures. *)
......
From fri.algebra Require Export cmra.
From fri.algebra Require Import updates local_updates.
From stdpp Require Export collections gmap.
From stdpp Require Export sets gmap.
Inductive gset_disj K `{Countable K} :=
| GSet : gset K gset_disj K
......
......@@ -12,8 +12,8 @@
**)
From Coq Require Import Wf_nat Omega.
From stdpp Require Export tactics base relations list collections.
From stdpp Require set.
From stdpp Require Export tactics base relations list sets.
From stdpp Require propset.
Require ClassicalEpsilon.
(** * Definitions *)
......@@ -1338,8 +1338,8 @@ Section cofair.
End erasure.
Section block.
Import stdpp.set ClassicalEpsilon.
Context (flatten: A B * (nat set nat)).
Import stdpp.propset ClassicalEpsilon.
Context (flatten: A B * (nat propset nat)).
Context (flatten_spec_step:
i a a', R1 i a a'
( l, isteps R2 l ((flatten a).1) ((flatten a').1)
......
......@@ -144,7 +144,7 @@ Section setoid_rel.
Hint Resolve rtc_rtcS : arsS.
Lemma rtcS_once x y : R x y rtcS R x y.
Proof. eauto with ars arsS. Qed.
Proof. eauto using rtc_once with arsS. Qed.
Lemma rtcS_r x y z : rtcS R x y R y z rtcS R x z.
Proof. intros. etransitivity; eauto. eapply rtcS_once; auto. Qed.
Lemma rtcS_inv x z : rtcS R x z x z y, R x y rtcS R y z.
......@@ -152,14 +152,14 @@ Section setoid_rel.
Lemma rtcS_ind_l (P : A Prop) (Hp: Proper (() ==> iff) P) (z : A)
(Prefl : P z) (Pstep : x y, R x y rtcS R y z P y P x) :
x, rtcS R x z P x.
Proof. induction 1; eauto with ars arsS. eapply Hp; eauto. Qed.
Proof. induction 1; eauto with arsS. eapply Hp; eauto. Qed.
Lemma rtcS_ind_r_weak (P : A A Prop) (Hp: Proper (() ==> () ==> iff) P)
(Prefl : x, P x x) (Pstep : x y z, rtcS R x y R y z P x y P x z) :
x z, rtcS R x z P x z.
Proof.
cut ( y z, rtcS R y z x, rtcS R x y P x y P x z).
{ eauto using rtcS_refl. }
induction 1; eauto using rtcS_r with ars arsS.
induction 1; eauto using rtcS_r with arsS.
intros x0 Hr HP; eapply Hp; try eapply HP; eauto.
Qed.
Lemma rtcS_ind_r (P : A Prop) (x : A) (Hp: Proper (() ==> iff) P)
......@@ -178,7 +178,7 @@ Section setoid_rel.
Qed.
Lemma rtcS_inv_r x z : rtcS R x z x z y, rtcS R x y R y z.
Proof.
revert z. apply rtcS_ind_r; eauto with ars arsS.
revert z. apply rtcS_ind_r; eauto with arsS.
intros y z Heq.
split.
* rewrite Heq.
......
From stdpp Require Export set.
From stdpp Require Export propset.
From fri.algebra Require Export cmra.
From fri.algebra Require Import dra.
Local Arguments valid _ _ !_ /.
......@@ -11,13 +11,13 @@ Structure stsT := STS {
state : Type;
token : Type;
prim_step : relation state;
tok : state set token;
tok : state propset token;
}.
Arguments STS {_ _} _ _.
Arguments prim_step {_} _ _.
Arguments tok {_} _.
Notation states sts := (set (state sts)).
Notation tokens sts := (set (token sts)).
Notation states sts := (propset (state sts)).
Notation tokens sts := (propset (token sts)).
(** * Theory and definitions *)
Section sts.
......@@ -45,8 +45,8 @@ Definition up_set (S : states sts) (T : tokens sts) : states sts :=
(** Tactic setup *)
Hint Resolve Step.
Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 50 (¬equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
Hint Extern 50 (¬equiv (A:=propset _) _ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
Hint Extern 50 (_ ## _) => set_solver : sts.
......@@ -58,7 +58,7 @@ Proof.
eauto with sts; set_solver.
Qed.
Global Instance framestep_proper : Proper (() ==> (=) ==> (=) ==> iff) frame_step.
Proof. move=> ?? /collection_equiv_spec [??]; split; by apply framestep_mono. Qed.
Proof. move=> ?? /set_equiv_spec [??]; split; by apply framestep_mono. Qed.
Instance closed_proper' : Proper (() ==> () ==> impl) closed.
Proof. destruct 3; constructor; intros until 0; setoid_subst; eauto. Qed.
Global Instance closed_proper : Proper (() ==> () ==> iff) closed.
......@@ -67,11 +67,11 @@ Global Instance up_preserving : Proper ((=) ==> flip (⊆) ==> (⊆)) up.
Proof.
intros s ? <- T T' HT ; apply elem_of_subseteq.
induction 1 as [|s1 s2 s3 [T1 T2]]; [constructor|].
eapply elem_of_mkSet, rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
eapply elem_of_PropSet, rtc_l; [eapply Frame_step with T1 T2|]; eauto with sts.
Qed.
Global Instance up_proper : Proper ((=) ==> () ==> ()) up.
Proof.
by move=> ??? ?? /collection_equiv_spec [??]; split; apply up_preserving.
by move=> ??? ?? /set_equiv_spec [??]; split; apply up_preserving.
Qed.
Global Instance up_set_preserving : Proper (() ==> flip () ==> ()) up_set.
Proof.
......@@ -80,7 +80,7 @@ Proof.
Qed.
Global Instance up_set_proper : Proper (() ==> () ==> ()) up_set.
Proof.
move=> S1 S2 /collection_equiv_spec [??] T1 T2 /collection_equiv_spec [??];
move=> S1 S2 /set_equiv_spec [??] T1 T2 /set_equiv_spec [??];
split; by apply up_set_preserving.
Qed.
......@@ -121,7 +121,7 @@ Proof. constructor. Qed.
Lemma subseteq_up_set S T : S up_set S T.
Proof. intros s ?; apply elem_of_bind; eauto using elem_of_up. Qed.
Lemma up_up_set s T : up s T up_set {[ s ]} T.
Proof. by rewrite /up_set collection_bind_singleton. Qed.
Proof. by rewrite /up_set set_bind_singleton. Qed.
Lemma closed_up_set S T : ( s, s S tok s ## T) closed (up_set S T) T.
Proof.
intros HS; unfold up_set; split.
......@@ -134,7 +134,7 @@ Proof.
Qed.
Lemma closed_up s T : tok s ## T closed (up s T) T.
Proof.
intros; rewrite -(collection_bind_singleton (λ s, up s T) s).
intros; rewrite -(set_bind_singleton (λ s, up s T) s).
apply closed_up_set; set_solver.
Qed.
Lemma closed_up_set_empty S : closed (up_set S ) .
......@@ -149,7 +149,7 @@ Lemma up_non_empty s T : up s T ≢ ∅.
Proof. eapply non_empty_inhabited, elem_of_up. Qed.
Lemma up_closed S T : closed S T up_set S T S.
Proof.
intros ?; apply collection_equiv_spec; split; auto using subseteq_up_set.
intros ?; apply set_equiv_spec; split; auto using subseteq_up_set.
intros s; unfold up_set; rewrite elem_of_bind; intros (s'&Hstep&?).
induction Hstep; eauto using closed_step.
Qed.
......@@ -164,8 +164,8 @@ Notation steps := (rtc step).
(* The type of bounds we can give to the state of an STS. This is the type
that we equip with an RA structure. *)
Inductive car (sts : stsT) :=
| auth : state sts set (token sts) car sts
| frag : set (state sts) set (token sts ) car sts.
| auth : state sts propset (token sts) car sts
| frag : propset (state sts) propset (token sts ) car sts.
Arguments auth {_} _ _.
Arguments frag {_} _ _.
End sts.
......@@ -212,8 +212,8 @@ Global Instance sts_step : step.Step (car sts) := λ x1 x2,
(auth s2 T2 ## y2) (x2 auth s2 T2 y2)
(tc prim_step) s1 s2.
Hint Extern 50 (equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 50 (¬equiv (A:=set _) _ _) => set_solver : sts.
Hint Extern 50 (equiv (A:=propset _) _ _) => set_solver : sts.
Hint Extern 50 (¬equiv (A:=propset _) _ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
Hint Extern 50 (_ _) => set_solver : sts.
Hint Extern 50 (_ ## _) => set_solver : sts.
......@@ -249,7 +249,7 @@ Proof.
exists s1, T1, a1, s2', T2', a2'.
split_and?; eauto.
assert (s2 = s1') by eauto using auth_disj_decomp.
subst. eauto with ars.
subst. eauto using tc_transitive.
Qed.
Instance sts_step_proper: Proper (equiv ==> equiv ==> impl) sts_step.
......@@ -428,7 +428,7 @@ Lemma sts_up_set_intersection S1 Sf Tf :
Proof.
intros Hclf. apply (anti_symm ()).
- move=>s [HS1 HSf]. split. by apply HS1. by apply subseteq_up_set.
- move=>s [HS1 [s' [/elem_of_mkSet Hsup Hs']]]. split; first done.
- move=>s [HS1 [s' [/elem_of_PropSet Hsup Hs']]]. split; first done.
eapply closed_steps, Hsup; first done. set_solver +Hs'.
Qed.
......@@ -484,7 +484,7 @@ Structure stsT := STS {
}.
Arguments STS {_} _.
Arguments prim_step {_} _ _.
Notation states sts := (set (state sts)).
Notation states sts := (propset (state sts)).
Canonical sts_notok (sts : stsT) : sts.stsT :=
sts.STS (token:=Empty_set) (@prim_step sts) (λ _, ).
......
......@@ -469,7 +469,7 @@ Section gmap.
([ map] kx m3, Φ k x).
Proof.
intros Hsub1 Hsub2 Hdom.
pose (m3 := (map_of_list (filter (λ p, p.1 dom (gset K) m1 p.1 dom (gset K) m2)
pose (m3 := (list_to_map (filter (λ p, p.1 dom (gset K) m1 p.1 dom (gset K) m2)
(map_to_list m)) : gmap K A)).
exists m3.
rewrite assoc.
......@@ -480,7 +480,7 @@ Section gmap.
assert (m3 m) as Hsub3.
{ apply map_subseteq_spec=> x a.
rewrite /m3. intros Hlook3.
apply elem_of_map_of_list_2, elem_of_list_filter in Hlook3.
apply elem_of_list_to_map_2, elem_of_list_filter in Hlook3.
rewrite elem_of_map_to_list in Hlook3 *. naive_solver.
}
apply (anti_symm ()).
......@@ -491,7 +491,7 @@ Section gmap.
rewrite ?elem_of_dom //=.
inversion 1 as (a'&Hlook3).
rewrite /m3 in Hlook3.
apply elem_of_map_of_list_2, elem_of_list_filter in Hlook3.
apply elem_of_list_to_map_2, elem_of_list_filter in Hlook3.
set_unfold. naive_solver.
** rewrite lookup_union_Some; last first.
{ apply (map_disjoint_dom (D:= gset K)). set_unfold. set_solver. }
......@@ -504,7 +504,7 @@ Section gmap.
intros Hnone2.
assert (is_Some (m3 !! x)) as (a'&Hlook').
{ rewrite /is_Some. case_eq (m3 !! x); first eauto.
rewrite /m3. intros Hnot%not_elem_of_map_of_list_2.
rewrite /m3. intros Hnot%not_elem_of_list_to_map_2.
exfalso; apply Hnot. apply elem_of_list_fmap.
exists (x, a); split; auto.
apply elem_of_list_filter. rewrite elem_of_map_to_list; split; auto.
......@@ -517,7 +517,7 @@ Section gmap.
rewrite elem_of_dom //= in Hin_3 *.
inversion 1 as (a'&Hlook3).
rewrite /m3 in Hlook3.
apply elem_of_map_of_list_2, elem_of_list_filter in Hlook3.
apply elem_of_list_to_map_2, elem_of_list_filter in Hlook3.
set_unfold. naive_solver.
Qed.
End gmap.
......@@ -104,26 +104,26 @@ Inductive prot_prim_step : relation session :=
| right_prim_step c pr tr tr' pl tl nl nr:
prot_prim_step (Session pl pr tl tr nl nr) (Session pl (pr ++ [c]) tl tr' nl (S nr)).
Definition tok (s : session) : set token :=
Definition tok (s : session) : propset token :=
{[ t | i, ((t = left_tok i) (i left_count s))
((t = right_tok i) (i right_count s))]}.
Global Arguments tok !_ /.
Canonical Structure sts := sts.STS prot_prim_step tok.
Definition up_left_tok (k: nat) : set token := {[ t | n, t = left_tok n n > k]}.
Definition up_right_tok (k: nat) : set token := {[ t | n, t = right_tok n n > k]}.
Definition up_left_tok (k: nat) : propset token := {[ t | n, t = left_tok n n > k]}.
Definition up_right_tok (k: nat) : propset token := {[ t | n, t = right_tok n n > k]}.
Definition up_left (p: list choice) (l: loc) (n: nat) : set session :=
Definition up_left (p: list choice) (l: loc) (n: nat) : propset session :=
{[ s' | left_state s' = p
left_ptr s' = l
left_count s' = n]}.
Definition up_right (p: list choice) (l: loc) (n: nat) : set session :=
Definition up_right (p: list choice) (l: loc) (n: nat) : propset session :=
{[ s' | right_state s' = p
right_ptr s' = l
right_count s' = n]}.
Definition up_exact s : set session := {[s]}.
Definition up_exact s : propset session := {[s]}.
Lemma up_left_closed p l n:
sts.closed (up_left p l n) (up_left_tok n).
......
......@@ -284,21 +284,21 @@ Section lr.
set (l := map_to_list S).
set (l1 := filter (λ p, p.1 dom (gset string) Γ1) l).
set (l2 := filter (λ p, p.1 dom (gset string) Γ2) l).
exists (map_of_list l1).
exists (map_of_list l2).
exists (list_to_map l1).
exists (list_to_map l2).
split_and!.
- rewrite /l1 /l. apply map_subseteq_spec=>x P.
intros Helem%elem_of_map_of_list_2.
intros Helem%elem_of_list_to_map_2.
by apply elem_of_list_filter in Helem as (?&?%elem_of_map_to_list).
- rewrite /l2 /l. apply map_subseteq_spec=>x P.
intros Helem%elem_of_map_of_list_2.
intros Helem%elem_of_list_to_map_2.
by apply elem_of_list_filter in Helem as (?&?%elem_of_map_to_list).
- clear -Hdom. set_unfold. rewrite /l1 /l2 /l=>x.
rewrite ?elem_of_dom.
rewrite /is_Some.
intros ((P1&Helem1)&(P2&Helem2)).
apply elem_of_map_of_list_2, elem_of_list_filter in Helem1 as (Hd1&_).
apply elem_of_map_of_list_2, elem_of_list_filter in Helem2 as (Hd2&_).
apply elem_of_list_to_map_2, elem_of_list_filter in Helem1 as (Hd1&_).
apply elem_of_list_to_map_2, elem_of_list_filter in Helem2 as (Hd2&_).
eapply Hdom. split; eauto.
- apply map_eq_iff=>x. rewrite /subst2typ lookup_fmap.
case_eq (Γ1 !! x).
......@@ -306,9 +306,9 @@ Section lr.
assert (Γ !! x = Some ty) as Hlook.
{ eapply (map_subseteq_spec Γ1); eauto. }
eapply subst2typ_inv in Hlook as (eh&ec&?); eauto.
assert ((map_of_list l1 : gmap string _) !! x
assert ((list_to_map l1 : gmap string _) !! x
= Some {| styp := ty; hval := eh; cval := ec |}) as Hlook'.
{ apply elem_of_map_of_list_1.
{ apply elem_of_list_to_map_1.
* rewrite /l1 /l. eapply NoDup_filter_fmap. apply NoDup_fst_map_to_list.
* rewrite /l1 /l. apply elem_of_list_filter. split.
** rewrite elem_of_dom; eauto.
......@@ -317,7 +317,7 @@ Section lr.
rewrite Hlook'. auto.
* intros Hnone.
rewrite Hnone.
rewrite not_elem_of_map_of_list_1; auto.
rewrite not_elem_of_list_to_map_1; auto.
rewrite /l1.
intros ((?&P)&Heq&Helem)%elem_of_list_fmap_2.
apply elem_of_list_filter in Helem as (HelemΓ1&?).
......@@ -329,9 +329,9 @@ Section lr.
assert (Γ !! x = Some ty) as Hlook.
{ eapply (map_subseteq_spec Γ2); eauto. }
eapply subst2typ_inv in Hlook as (eh&ec&?); eauto.
assert ((map_of_list l2 : gmap string _) !! x
assert ((list_to_map l2 : gmap string _) !! x
= Some {| styp := ty; hval := eh; cval := ec |}) as Hlook'.
{ apply elem_of_map_of_list_1.
{ apply elem_of_list_to_map_1.
* rewrite /l2 /l. eapply NoDup_filter_fmap. apply NoDup_fst_map_to_list.
* rewrite /l2 /l. apply elem_of_list_filter. split.
** rewrite elem_of_dom; eauto.
......@@ -340,7 +340,7 @@ Section lr.
rewrite Hlook'. auto.
* intros Hnone.
rewrite Hnone.
rewrite not_elem_of_map_of_list_1; auto.
rewrite not_elem_of_list_to_map_1; auto.
rewrite /l2.
intros ((?&P)&Heq&Helem)%elem_of_list_fmap_2.
apply elem_of_list_filter in Helem as (HelemΓ1&?).
......
......@@ -89,8 +89,8 @@ Proof.
replace (x :: lS.*1) with (((x, e) :: lS).*1); auto.
rewrite Heq. apply NoDup_fst_map_to_list. }
eapply IHlS.
* symmetry. by apply map_to_of_list.
* rewrite map_to_of_list; eauto.
* symmetry. by apply map_to_list_to_map.
* rewrite map_to_list_to_map; eauto.
Qed.
Lemma lsubst_app l1 l2 e:
......@@ -482,7 +482,7 @@ Proof.
* assert ( k, Permutation (map_to_list S) (k ++ [(x, e)])) as (k&Hperm).
{ setoid_rewrite Permutation_app_comm.
apply submseteq_Permutation.
erewrite <-(@map_to_of_list); try apply _.
erewrite <-(@map_to_list_to_map); try apply _.
* apply map_to_list_submseteq. set_unfold.
apply map_subseteq_spec.
intros x' e'.
......
......@@ -89,8 +89,8 @@ Proof.
replace (x :: lS.*1) with (((x, e) :: lS).*1); auto.
rewrite Heq. apply NoDup_fst_map_to_list. }
eapply IHlS.
* symmetry. by apply map_to_of_list.
* rewrite map_to_of_list; eauto.
* symmetry. by apply map_to_list_to_map.
* rewrite map_to_list_to_map; eauto.
Qed.
Lemma lsubst_app l1 l2 e:
......@@ -488,7 +488,7 @@ Proof.
* assert ( k, Permutation (map_to_list S) (k ++ [(x, e)])) as (k&Hperm).
{ setoid_rewrite Permutation_app_comm.
apply submseteq_Permutation.
erewrite <-(@map_to_of_list); try apply _.
erewrite <-(@map_to_list_to_map); try apply _.
* apply map_to_list_submseteq. set_unfold.
apply map_subseteq_spec.
intros x' e'.
......
......@@ -33,7 +33,7 @@ Section ticket_sts.
Inductive token := enter_tok (n: nat) | finish_tok (n: nat).
Definition tok (s: ticket_state) : set token :=
Definition tok (s: ticket_state) : propset token :=
match s with
| ticket_pre n =>
{[ t | i, (t = enter_tok i i < n) (t = finish_tok i i < n) ]}
......@@ -190,7 +190,7 @@ Section ticket_sts.
set_unfold; (done || lia).
Qed.
Definition up_tok (k: nat) : set token :=
Definition up_tok (k: nat) : propset token :=
{[ t | n, (t = enter_tok n t = finish_tok n) n k]}.
Lemma up_tok_anti n:
......
From stdpp Require Import set.
From stdpp Require Import propset.
From Coq Require Import Classical_Pred_Type.
Section compact.
......
......@@ -4,7 +4,7 @@
are not in the Coq standard library. *)
From Coq.ssr Require Import ssreflect.
From Coq Require Export Permutation.
From stdpp Require Export list set.
From stdpp Require Export list propset.
Inductive Forall4 {A B C D} (P : A B C D Prop) :
list A list B list C list D Prop :=
......
From Coq.ssr Require Export ssreflect.
From fri.prelude Require Export list compact.
From stdpp Require Export prelude mapset.
From stdpp Require Export set natmap fin_collections collections fin_maps.
From stdpp Require set.
From stdpp Require Export propset natmap fin_sets sets fin_maps.
From stdpp Require propset.
From Coq Require Classical_Pred_Type.
Lemma subseteq_union_decompose:
......@@ -37,7 +37,7 @@ Lemma natset_powerset_finite:
(A: natset), set_finite {[ B | B A ]}.
Proof.
intros A.
eapply (collection_ind (λ A, set_finite {[ B | B A]})).
eapply (set_ind (λ A, set_finite {[ B | B A]})).
* intros A' A'' Hequiv. by rewrite leibniz_equiv_iff in Hequiv * => ->.
* exists []. intros B Hin.
cut (B = ); intros; subst; first left.
......@@ -95,7 +95,7 @@ Qed.
** intros. eapply Hnin'. right. auto.
Qed.
Lemma set_finite_flatten A (X: set A) (Y: list (set A)):
Lemma set_finite_flatten A (X: propset A) (Y: list (propset A)):
( X', X' Y set_finite X')
( x, x X X', X' Y x X')
set_finite X.
......@@ -103,7 +103,7 @@ Qed.
intros Hall_fin Hin.
assert ( Xrest, set_finite Xrest
( x : A, x X x Xrest
X' : set A, X' Y x X' Xrest)) as Hin'.
X' : propset A, X' Y x X' Xrest)) as Hin'.
{
exists .
split.
......@@ -133,7 +133,7 @@ Qed.
Section compact_setoid.
Import stdpp.set Classical_Pred_Type.
Import stdpp.propset Classical_Pred_Type.
Definition set_finite_setoid `{Equiv A} {B} {H : ElemOf A B} (X : B) : Prop :=
l : list A, x : A, x X x' : A, x x' x' l.
......@@ -149,7 +149,7 @@ Section compact_setoid.
Lemma set_finite_setoid_inj `{Equiv A, Equiv A'}
{Equiv: Equivalence ((): relation A')}
(X: set A) (f: A A') (f_proper: x y, x X x y f x f y)
(X: propset A) (f: A A') (f_proper: x y, x X x y f x f y)
(f_inj: x y, x X y X f x f y x y):
set_finite_setoid (fmap f X)
set_finite_setoid X.
......@@ -262,7 +262,7 @@ Section compact_setoid.
Qed.
End compact_setoid.
Lemma union_finite_setoid `{Equiv A, Equivalence A} (X Y: set A):
Lemma union_finite_setoid `{Equiv A, Equivalence A} (X Y: propset A):
set_finite_setoid X
set_finite_setoid Y
set_finite_setoid (X Y).
......@@ -275,14 +275,14 @@ Proof.
exists x'; split; eauto. apply elem_of_app; right; auto.
Qed.
Lemma set_finite_setoid_flatten `{Equiv A, Equivalence A ()} (X: set A) (Y: list (set A)):
Lemma set_finite_setoid_flatten `{Equiv A, Equivalence A ()} (X: propset A) (Y: list (propset A)):
( X', X' Y set_finite_setoid X')
( x, x X X', X' Y x X')
set_finite_setoid X.
Proof.
intros Hall_fin Hin.
assert ( Xrest, set_finite_setoid Xrest
( x : A, x X x Xrest X' : set A, X' Y x X' Xrest)) as Hin'.
( x : A, x X x Xrest X' : propset A, X' Y x X' Xrest)) as Hin'.
{
exists .
split.
......@@ -311,13 +311,13 @@ Proof.
Qed.
Lemma set_finite_quotient (A A': Type) (f: A A')
(X: set A) (Y: set A') (f_in: x, x X f x Y)
(f_blocks: y, (X' : set A), set_finite X' x, x X f x = y x X'):
(X: propset A) (Y: propset A') (f_in: x, x X f x Y)
(f_blocks: y, (X' : propset A), set_finite X' x, x X f x = y x X'):
set_finite Y
set_finite X.
Proof.
intros (l&Hfin_in).
edestruct (exists_list_choice' l (λ y (X' : set A), set_finite X'
edestruct (exists_list_choice' l (λ y (X' : propset A), set_finite X'
( x, x X f x = y x X'))
set_finite)
as (l'&Hin_l'&Hin_l'2).
......@@ -339,14 +339,14 @@ Proof.
Qed.
Lemma set_finite_setoid_quotient `{Equiv A, Equivalence A (), Equiv A', Equivalence A ()}
(f: A A') (X: set A) (Y: set A') (f_in: x, x X f x Y)
(f_blocks: y, X' : set A, set_finite_setoid X'
(f: A A') (X: propset A) (Y: propset A') (f_in: x, x X f x Y)
(f_blocks: y, X' : propset A, set_finite_setoid X'
x, x X f x y x X'):
set_finite_setoid Y
set_finite_setoid X.
Proof.
intros (l&Hfin_in).
edestruct (exists_list_choice' l (λ y (X' : set A), set_finite_setoid X'
edestruct (exists_list_choice' l (λ y (X' : propset A), set_finite_setoid X'
( x, x X f x y x X')) set_finite_setoid)
as (l'&Hin_l'&Hin_l'2).
{ intros y Hin. edestruct (f_blocks y); eauto. }
......@@ -368,13 +368,13 @@ Proof.
Qed.
Lemma set_finite_setoid_quotient_strong `{Equiv A, Equivalence A (), Equiv A', Equivalence A ()}
(f: A option A') (X: set A) (Y: set A') (f_in: x, x X y, f x = Some y y Y)
(f_blocks: y, (X' :set A), set_finite_setoid X' x, x X f x Some y x X'):
(f: A option A') (X: propset A) (Y: propset A') (f_in: x, x X y, f x = Some y y Y)
(f_blocks: y, (X' :propset A), set_finite_setoid X' x, x X f x Some y x X'):
set_finite_setoid Y
set_finite_setoid X.
Proof.
intros (l&Hfin_in).
edestruct (exists_list_choice' l (λ y (X' : set A), set_finite_setoid X'
edestruct (exists_list_choice' l (λ y (X' : propset A), set_finite_setoid X'
( x, x X f x Some y x X'))
set_finite_setoid)
as (l'