From Stdlib Require Import List Program Lia ConstructiveEpsilon Arith Classes.Morphisms.
From mathcomp Require Import zify.
From Equations Require Import Equations.
Require Import extra_principles Util continuity_zoo_Prop partial embed_nat Common.
Import EmbedNatNotations PartialTactics ListNotations.
Set Bullet Behavior "Strict Subproofs".
Section PartialZoo.
Context `{Partiality : partiality}.
Definition neighborhood_fun (A R : Type) := list A -> part (option R).
Definition neighborhood_for [A R : Type] (gamma : neighborhood_fun A R) (F : (nat -> part A) -> part R) :=
forall (f : nat -> part A),
equiv (F f) (mu_opt (fun n => bind (fold_part_list (tabulate f 0 n)) gamma)).
Definition neighborhood_cont [A R : Type] (F : (nat -> part A) -> part R) : Prop :=
exists (gamma : neighborhood_fun A R), neighborhood_for gamma F.
Definition well_founded_neighborhood [A R : Type] (gamma : neighborhood_fun A R) : Prop :=
(forall (l l' : list A), ter (gamma (l' ++ l)) -> ter (gamma l)) /\
forall (r : R) (l l' : list A), gamma l =! Some r -> gamma (l' ++ l) =! Some r.
Definition well_founded_neighborhood_for [A R : Type] (gamma : neighborhood_fun A R) (F : (nat -> part A) -> part R) :=
well_founded_neighborhood gamma /\ neighborhood_for gamma F.
Definition well_founded_neighborhood_cont [A R : Type] (F : (nat -> part A) -> part R) : Prop :=
exists (gamma : neighborhood_fun A R), well_founded_neighborhood_for gamma F.
Definition strict_neighborhood [A R : Type] (gamma : neighborhood_fun A R) : Prop :=
forall (l : list A), ter (gamma l) <-> exists (r : R) (l' : list A), gamma (l' ++ l) =! Some r.
Definition strict_well_founded_neighborhood_for [A R : Type] (gamma : neighborhood_fun A R) (F : (nat -> part A) -> part R) :=
strict_neighborhood gamma /\ well_founded_neighborhood_for gamma F.
Definition strict_well_founded_neighborhood_cont [A R : Type] (F : (nat -> part A) -> part R) : Prop :=
exists (gamma : neighborhood_fun A R), strict_well_founded_neighborhood_for gamma F.
Definition make_well_founded [A R : Type] (gamma : neighborhood_fun A R) : neighborhood_fun A R :=
fun l => mu_opt (fun n => if n <=? length l then bind (gamma (rev (firstn n (rev l)))) (fun o => ret (match o with
| Some r => Some (Some r)
| None => None
end)) else ret (Some None)).
Lemma make_well_founded_preserves_neighborhood [A R : Type] (gamma : neighborhood_fun A R) :
forall (F : (nat -> part A) -> part R), neighborhood_for gamma F ->
neighborhood_for (make_well_founded gamma) F.
Proof.
intros F HF f r.
specialize (HF f r).
rewrite HF.
split.
- intros (n & Hn & Hn')%mu_opt_hasvalue.
apply mu_opt_hasvalue.
exists n.
split.
+ simpl_assms.
rewrite bind_hasvalue_given; eauto.
unfold make_well_founded.
apply mu_opt_hasvalue.
assert (n = length x) as -> by (eapply fold_part_list_tabulate_length; eauto).
exists (length x).
rewrite leb_correct, <- length_rev, firstn_all, rev_involutive; eauto.
split; psimpl.
intros k Hk.
rewrite leb_correct; eauto with arith.
rewrite length_rev in Hk.
specialize (Hn' k Hk).
simpl_assms.
rewrite <- tabulate_add with (n := k), fold_part_list_app in H; eauto with arith.
rewrite bind_hasvalue_given in H; eauto.
simpl_assms.
apply fold_part_list_tabulate_length in H1 as ->.
rewrite rev_app_distr, <- firstn_app_l.
2: rewrite length_rev; eauto.
rewrite <- length_rev, firstn_all, rev_involutive.
psimpl.
+ intros k Hk.
pose proof (Hn' k Hk) as (l & Hl & Hl')%bind_hasvalue.
rewrite bind_hasvalue_given; eauto.
unfold make_well_founded.
apply mu_opt_hasvalue.
assert (k = length l) as -> by (eapply fold_part_list_tabulate_length; eauto).
exists (S (length l)).
rewrite leb_correct_conv; eauto.
split; psimpl.
intros m Hm.
rewrite leb_correct; eauto with arith.
rewrite <- tabulate_add with (n := m), fold_part_list_app in Hl; eauto with arith.
simpl_assms.
assert (m = length x0) as -> by (eapply fold_part_list_tabulate_length; eauto).
rewrite rev_app_distr, <- length_rev, <- firstn_app_l, firstn_all, rev_involutive; eauto.
specialize (Hn' (length x0) ltac:(lia)).
rewrite bind_hasvalue_given in Hn'; psimpl.
- intros (n & (l & Hr & (m & Hm & Hm')%mu_opt_hasvalue)%bind_hasvalue & Hn')%mu_opt_hasvalue.
destruct (m <=? length l) eqn:E.
2: psimpl.
apply leb_complete in E.
apply mu_opt_hasvalue.
exists m.
simpl_assms.
destruct x as [r'|]; inversion H2; subst.
assert (n = length l) as -> by (eapply fold_part_list_tabulate_length; eauto).
rewrite <- tabulate_add with (n := m), fold_part_list_app in Hr; eauto with arith.
simpl_assms.
assert (m = length x) as -> by (eapply fold_part_list_tabulate_length; eauto).
rewrite bind_hasvalue_given; eauto.
rewrite rev_app_distr, <- length_rev, <- firstn_app_l, firstn_all, rev_involutive in H; eauto.
split.
1: psimpl.
intros k Hk.
specialize (Hm' k Hk).
rewrite leb_correct in Hm'; eauto with arith.
simpl_assms.
destruct x1; inversion H7; subst.
rewrite <- tabulate_add with (n := k), fold_part_list_app in H0; eauto with arith.
simpl_assms.
assert (k = length x1) as -> by (eapply fold_part_list_tabulate_length; eauto).
rewrite app_assoc, rev_app_distr, <- length_rev, <- firstn_app_l, firstn_all, rev_involutive in H3; eauto with arith.
psimpl.
Qed.
Lemma make_well_founded_is_monotonic [A R : Type] (gamma : neighborhood_fun A R) :
forall (r : R) (l l' : list A), make_well_founded gamma l =! Some r -> make_well_founded gamma (l' ++ l) =! Some r.
Proof.
intros r l l' (n & Hn & Hn')%mu_opt_hasvalue.
unfold make_well_founded in *.
apply mu_opt_hasvalue.
destruct (n <=? length l) eqn:E; simpl_assms.
apply leb_complete in E.
destruct x; inversion H2; subst.
exists n.
rewrite length_app, leb_correct; try lia.
rewrite rev_app_distr, <- firstn_app_l.
2: now rewrite length_rev.
split.
1: psimpl.
intros k Hk.
specialize (Hn' k ltac:(eauto with arith)).
rewrite leb_correct in Hn'; eauto with arith.
rewrite leb_correct, <- firstn_app_l; try rewrite length_rev; try lia.
eauto.
Qed.
Lemma make_well_founded_is_well_founded [A R : Type] (gamma : neighborhood_fun A R) :
well_founded_neighborhood (make_well_founded gamma).
Proof.
split.
2:apply make_well_founded_is_monotonic.
intros l l' (o & (n & Hn & Hn')%mu_opt_hasvalue).
destruct (n <=? length l) eqn:E.
- apply leb_complete in E.
rewrite length_app, rev_app_distr in *.
rewrite leb_correct in Hn; try lia.
exists o.
apply mu_opt_hasvalue.
exists n.
rewrite leb_correct; eauto.
rewrite <- firstn_app_l in Hn.
2: rewrite length_rev; eauto.
split.
1: eauto.
intros k Hk.
specialize (Hn' k Hk).
rewrite <- firstn_app_l in Hn'.
2: rewrite length_rev.
rewrite leb_correct.
rewrite leb_correct in Hn'.
apply Hn'.
all: lia.
- apply leb_complete_conv in E.
exists None.
apply mu_opt_hasvalue.
exists (S (length l)).
rewrite leb_correct_conv; eauto with arith.
split.
1: psimpl.
intros k Hk.
rewrite leb_correct; eauto with arith.
specialize (Hn' k ltac:(lia)).
rewrite length_app, rev_app_distr, leb_correct, <- firstn_app_l in Hn'.
2: rewrite length_rev.
eauto.
all: lia.
Qed.
Lemma neighborhood_cont_is_well_founded_neighborhood_cont [A R : Type] (F : (nat -> part A) -> part R) :
neighborhood_cont F -> well_founded_neighborhood_cont F.
Proof.
intros (gamma & Hgamma).
exists (make_well_founded gamma).
split.
- apply make_well_founded_is_well_founded.
- apply make_well_founded_preserves_neighborhood; eauto.
Qed.
Definition enumerable (A : Type) :=
exists (f : nat -> A), forall (a : A), exists (n : nat), f n = a.
Fixpoint tuple (A : Type) (n : nat) : Type :=
match n with
| O => unit
| S n => A * tuple A n
end.
Fixpoint enumerate_tuple [A : Type] (f : nat -> A) (n : nat) : nat -> tuple A n :=
match n return nat -> tuple A n with
| O => fun _ => ()
| S n => fun k => let '(n', m) := unembed k in (f n', enumerate_tuple f n m)
end.
Lemma enumerable_tuple {A : Type} {n : nat} :
enumerable A -> enumerable (tuple A n).
Proof.
intros (f & Hf).
exists (enumerate_tuple f n).
induction n as [|n IHn].
- intros (); exists 0; eauto.
- intros (a, t).
specialize (Hf a) as (n' & Hn).
specialize (IHn t) as (m & Hm).
exists (embed (n', m)).
simpl.
rewrite embedP.
subst; auto.
Qed.
Fixpoint tuple_to_list [A : Type] [n : nat] : tuple A n -> list A :=
match n return tuple A n -> list A with
| O => fun '() => nil
| S n => fun '(a, t) => a :: tuple_to_list t
end.
Lemma enumerable_list [A : Type] :
enumerable A -> enumerable (list A).
Proof.
intros HA.
pose proof HA as (f & Hf).
set (e n :=
let (len, m) := unembed n in
tuple_to_list (enumerate_tuple f len m)
).
exists e.
intros l.
induction l as [|a l IHl].
- exists 0; auto.
- destruct IHl as (m' & Hm).
unfold e in Hm |- *.
destruct (unembed m') as (len & m) eqn:E.
specialize (Hf a) as (n' & Hn).
exists (embed (S len, embed (n', m))).
rewrite embedP.
simpl.
rewrite embedP.
subst; auto.
Qed.
Definition neighborhood_fun_strictify [A R : Type] (gamma : neighborhood_fun A R) :
(nat -> list A) -> neighborhood_fun A R :=
fun e l => bind (mu_tot (fun k => let (n, m) := unembed k in
match seval (gamma (e n ++ l)) m with
| Some (Some _) => true
| _ => false
end))
(fun _ => gamma l).
Lemma neighborhood_fun_strictify_ter [A R : Type] (F : (nat -> part A) -> part R)
(gamma : neighborhood_fun A R) : forall (e : nat -> list A),
(forall (l : list A), exists (n : nat), e n = l) -> neighborhood_for gamma F -> well_founded_neighborhood gamma ->
forall (l : list A),
ter (neighborhood_fun_strictify gamma e l) <->
exists (r : R) (l' : list A), gamma (l' ++ l) =! Some r.
Proof.
intros e HA Hgamma Hwf l.
split.
- intros (o & Ho).
unfold neighborhood_fun_strictify in Ho.
psimpl.
apply mu_tot_hasvalue in H as (Hl & _).
destruct (unembed x) as (n & m).
destruct (seval (gamma (e n ++ l)) m) as [[r|]|] eqn:E; try now inversion Hl.
exists r, (e n).
eapply seval_hasvalue; eauto.
- intros (r & l' & Hr).
unfold neighborhood_fun_strictify.
assert (ter (gamma l)). {
destruct Hwf as (Hwf1 & _).
eapply Hwf1; eexists; eauto.
}
eapply bind_ter'; eauto.
destruct (HA l') as (n & Hn); subst.
apply seval_hasvalue in Hr as (m & Hm).
apply mu_tot_ter with (n := embed (n, m)).
rewrite embedP.
rewrite Hm; reflexivity.
Qed.
Lemma neighborhood_fun_strictify_hasvalue_some [A R : Type] (F : (nat -> part A) -> part R)
(gamma : neighborhood_fun A R) : forall (e : nat -> list A),
(forall (l : list A), exists (n : nat), e n = l) ->
forall (l : list A) (r : R), gamma l =! Some r ->
neighborhood_fun_strictify gamma e l =! Some r.
Proof.
intros e He l r Hr.
unfold neighborhood_fun_strictify.
eenough (ter (mu_tot _)) as (? & ?) by psimpl.
specialize (He nil) as (n & Hn).
apply seval_hasvalue in Hr as (m & Hm).
change l with (nil ++ l) in Hm.
apply mu_tot_ter with (embed (n, m)).
now rewrite embedP, Hn, Hm.
Qed.
Lemma neighborhood_fun_strictify_hasvalue_none [A R : Type] (F : (nat -> part A) -> part R)
(gamma : neighborhood_fun A R) : forall (e : nat -> list A),
(forall (l : list A), exists (n : nat), e n = l) -> neighborhood_for gamma F ->
forall (l : list A), gamma l =! None -> ter (neighborhood_fun_strictify gamma e l) ->
neighborhood_fun_strictify gamma e l =! None.
Proof.
intros e He Hgamma l Hl Hl'.
destruct Hl' as ([r|] & Hr); eauto.
unfold neighborhood_fun_strictify in Hr.
simpl_assms.
assert (None = Some r) as [=] by (eapply hasvalue_det; eauto).
Qed.
Lemma neighborhood_fun_strictify_strict [A R : Type] (F : (nat -> part A) -> part R)
(gamma : neighborhood_fun A R) : forall (e : nat -> list A),
(forall (l : list A), exists (n : nat), e n = l) -> neighborhood_for gamma F -> well_founded_neighborhood gamma ->
strict_neighborhood (neighborhood_fun_strictify gamma e).
Proof.
intros e He Hgamma Hwf l.
repeat rewrite neighborhood_fun_strictify_ter; eauto.
split; intros (r & l' & Hr).
- eapply neighborhood_fun_strictify_hasvalue_some in Hr; eauto.
- assert (Hter : ter (neighborhood_fun_strictify gamma e (l' ++ l))) by (eexists; eauto).
eapply neighborhood_fun_strictify_ter in Hter as (r' & l'' & Hr'); eauto.
exists r', (l'' ++ l').
now rewrite app_assoc in Hr'.
Qed.
Definition neighborhood_fun_strictify_wf [A R : Type] (gamma : neighborhood_fun A R) :
forall (e : nat -> list A),
(forall (l : list A), exists (n : nat), e n = l) -> well_founded_neighborhood gamma ->
well_founded_neighborhood (neighborhood_fun_strictify gamma e).
Proof.
intros e HA (Hwf1 & Hwf2).
split.
- intros l l' (r & Hr).
unfold neighborhood_fun_strictify in *.
psimpl.
eapply bind_ter'.
2: intros _ _; eapply Hwf1; eexists; eauto.
eapply mu_tot_hasvalue in H as (H & _).
destruct (unembed x) as (n & m).
destruct (HA (e n ++ l')) as (n' & Hn').
eapply mu_tot_ter with (n := embed (n', m)).
rewrite embedP, Hn', <- app_assoc.
eauto.
- intros r l l' Hr.
unfold neighborhood_fun_strictify in *.
eapply bind_hasvalue in Hr as (? & ? & ?).
eenough (ter (mu_tot _)) as (? & ?) by psimpl.
destruct (HA nil) as (n & Hn).
assert (Hr : gamma (e n ++ l' ++ l) =! Some r) by (rewrite Hn; simpl; eauto).
apply seval_hasvalue in Hr as (m & Hm).
eapply mu_tot_ter with (n := embed (n, m)).
rewrite embedP.
rewrite Hm; reflexivity.
Qed.
Lemma strictify_preserves_neighborhood [A R : Type] (gamma : neighborhood_fun A R) :
forall (e : nat -> list A), (forall (l : list A), exists (n : nat), e n = l) ->
forall (F : (nat -> part A) -> part R), neighborhood_for gamma F -> well_founded_neighborhood gamma ->
neighborhood_for (neighborhood_fun_strictify gamma e) F.
Proof.
intros e He F Hgamma Hwf f r.
rewrite (Hgamma f r).
do 2 rewrite mu_opt_hasvalue.
split.
- intros (n & Hn & Hn').
exists n.
simpl_assms.
rewrite bind_hasvalue_given; eauto.
split.
1: apply neighborhood_fun_strictify_hasvalue_some; eauto.
intros k Hk.
specialize (Hn' k Hk).
simpl_assms.
rewrite bind_hasvalue_given; eauto.
eapply neighborhood_fun_strictify_hasvalue_none; eauto.
eapply neighborhood_fun_strictify_ter; eauto.
rewrite <- tabulate_add with (n := k), fold_part_list_app in H; eauto with arith.
rewrite bind_hasvalue_given in H; eauto.
psimpl.
- intros (n & Hn & Hn').
exists n.
unfold neighborhood_fun_strictify in Hn.
simpl_assms.
split.
1: psimpl.
intros k Hk.
specialize (Hn' k Hk).
unfold neighborhood_fun_strictify in Hn'.
psimpl.
Qed.
Lemma enumerable_to_strictify_neighborhood_cont [A R : Type] : enumerable (list A) ->
forall (F : (nat -> part A) -> part R), neighborhood_cont F ->
strict_well_founded_neighborhood_cont F.
Proof.
intros (e & He) F (gamma & Hwf & Hgamma)%neighborhood_cont_is_well_founded_neighborhood_cont.
exists (neighborhood_fun_strictify gamma e).
split.
2: split.
- eapply neighborhood_fun_strictify_strict; eauto.
- eapply neighborhood_fun_strictify_wf; eauto.
- eapply strictify_preserves_neighborhood; eauto.
Qed.
Lemma well_founded_neighborhood_hasvalue [A R : Type] (gamma : neighborhood_fun A R)
(f : nat -> part A) (r : R) (n : nat) :
well_founded_neighborhood gamma ->
bind (fold_part_list (tabulate f 0 n)) gamma =! Some r ->
mu_opt (fun n => bind (fold_part_list (tabulate f 0 n)) gamma) =! r.
Proof.
intros (Hwf1 & Hwf2) Hr.
induction n as [|n IHn]. 1:{
apply mu_opt_hasvalue.
exists 0.
split; psimpl.
}
rewrite tabulate_succ', fold_part_list_app in Hr; eauto with arith.
cbn in Hr.
simpl_assms.
destruct (Hwf1 x0 [x2] ltac:(eexists; eauto)) as ([r'|] & Hr').
1: {
assert (Some r = Some r') as [=] by (eapply hasvalue_det; eauto).
subst; eapply IHn; psimpl.
}
apply mu_opt_hasvalue.
exists (S n).
rewrite tabulate_succ', fold_part_list_app; eauto with arith.
cbn; split.
1: psimpl.
intros k Hk.
inversion Hk; subst.
1: psimpl.
rewrite <- tabulate_add with (n := k), fold_part_list_app in H; eauto with arith.
psimpl.
destruct (Hwf1 _ _ ltac:(eexists; eapply Hr')) as ([r'|] & Hr''); eauto.
assert (None = Some r') as [=] by (eapply hasvalue_det; eauto).
Qed.
#[projections(primitive)]
Record sigma1_tree (A : Type) := mkSigma1Tree {
ptree_branch : (nat -> part A) -> Prop;
ptree_path : list A -> Prop;
F : (nat -> part A) -> part unit;
gamma : neighborhood_fun A unit;
Hgamma : strict_well_founded_neighborhood_for gamma F;
Hptree_branch : reflectspfn ptree_branch F;
Hptree_path : reflectspfn ptree_path (fun l => bind (gamma l) (fun _ => ret ()));
}.
Arguments ptree_branch {_}.
Arguments ptree_path {_}.
Arguments F {_}.
Arguments gamma {_}.
Arguments Hgamma {_}.
Arguments Hptree_branch {_}.
Arguments Hptree_path {_}.
Lemma ptree_branch_extend [A : Type] (T : sigma1_tree A) :
forall (f : nat -> part A), T.(ptree_branch) f ->
forall (l : list A), extend l f -> T.(ptree_path) l.
Proof.
intros f Hf l Hl.
apply Hptree_branch in Hf.
apply Hptree_path.
rewrite extend_fold_part in Hl.
destruct Hf as (r & Hr).
destruct T.(Hgamma) as (_ & (Hwf1 & Hwf2) & Hgamma).
specialize (Hgamma f r).
apply Hgamma in Hr as (n & Hn & Hn')%mu_opt_hasvalue.
enough (ter (T.(gamma) l)) as (? & ?) by (eexists; psimpl).
destruct (Nat.le_ge_cases n (length l)) as [Hnl | Hnl].
- erewrite <- tabulate_add, fold_part_list_app in Hl; try (eassumption || lia).
psimpl.
assert (x1 = x) by (eapply hasvalue_det; eauto); subst.
eexists; psimpl.
- simpl_assms.
erewrite <- tabulate_add with (n := length l), fold_part_list_app in H; try (eassumption || lia).
psimpl.
assert (x0 = l) by (eapply hasvalue_det; eauto); subst.
assert (ter (T.(gamma) l)) as (? & ?) by (eapply Hwf1; eexists; eauto).
eexists; psimpl.
Qed.
Lemma ptree_restrict [A : Type] (T : sigma1_tree A) :
forall (l l' : list A), T.(ptree_path) (l' ++ l) -> T.(ptree_path) l.
Proof.
intros l l' Hl.
apply T.(Hptree_path) in Hl.
apply T.(Hptree_path).
enough (ter (T.(gamma) l)) as (? & ?) by (eexists; psimpl).
destruct Hl.
psimpl.
destruct T.(Hgamma) as (_ & (Hwf & _) & _).
eapply Hwf.
eexists.
psimpl.
Qed.
Inductive brouwer_op (A R : Type) (T : sigma1_tree A) (gamma : neighborhood_fun A R) : forall (l : list A), T.(ptree_path) l -> Prop :=
| BOp : forall (l : list A) (Hl : T.(ptree_path) l),
(exists (r : R), gamma l =! Some r) \/ (gamma l =! None /\ forall (a : A) (Hal : T.(ptree_path) (a :: l)),
brouwer_op A R T gamma (a :: l) Hal) -> brouwer_op A R T gamma l Hl.
Arguments BOp [_ _]%_type {_%_type _ _}.
Fixpoint brouwer_op_ind' (A R : Type) (T : sigma1_tree A) (gamma : neighborhood_fun A R)
(Ar : forall (l : list A), T.(ptree_path) l -> Prop)
(HBOp : forall (l : list A) (Hl : T.(ptree_path) l),
(exists (r : R), gamma l =! Some r) \/ (gamma l =! None /\
(forall (a : A) (Hal : T.(ptree_path) (a :: l)), brouwer_op A R T gamma (a :: l) Hal) /\
(forall (a : A) (Hal : T.(ptree_path) (a :: l)), Ar (a :: l) Hal)
)
-> Ar l Hl) :
forall (l : list A) (Hl : T.(ptree_path) l), brouwer_op A R T gamma l Hl -> Ar l Hl.
Proof.
intros l Hl b.
specialize (brouwer_op_ind' A R T gamma Ar HBOp).
destruct b as [l Hl Hb].
apply (HBOp l Hl).
destruct Hb as [(r & Hr) | (Hgamma & Hb)].
- left; eexists; eauto.
- right; repeat (split; auto).
Qed.
Lemma neighborhood_for_squash [A R : Type] :
forall (F : (nat -> part A) -> part R) (gamma : neighborhood_fun A R),
neighborhood_for gamma F -> neighborhood_for (fun l => bind (gamma l) (fun o => ret match o with
| Some _ => Some ()
| _ => None
end)) (fun f => bind (F f) (fun _ => ret ())).
Proof.
intros F gamma Hgamma.
intros f (); split; specialize (Hgamma f).
- intros Hr.
apply bind_hasvalue in Hr as (? & ? & ?).
apply Hgamma in H as (n & Hn & Hn')%mu_opt_hasvalue.
apply mu_opt_hasvalue.
exists n.
split.
1: psimpl.
intros k Hk.
specialize (Hn' k Hk).
psimpl.
- intros (n & Hn & Hn')%mu_opt_hasvalue.
repeat (apply bind_hasvalue in Hn as (? & ? & Hn)).
rewrite <- ret_hasvalue_iff in Hn.
destruct x0; inversion Hn.
psimpl.
apply Hgamma.
apply mu_opt_hasvalue; exists n.
split.
1: psimpl.
intros k Hk.
specialize (Hn' k Hk); psimpl.
destruct x1; now inversion H5.
Qed.
Lemma well_founded_neighborhood_for_squash [A R : Type] :
forall (F : (nat -> part A) -> part R) (gamma : neighborhood_fun A R),
well_founded_neighborhood_for gamma F -> well_founded_neighborhood_for (fun l => bind (gamma l) (fun o => ret match o with
| Some _ => Some ()
| _ => None
end)) (fun f => bind (F f) (fun _ => ret ())).
Proof.
intros F gamma ((Hwf1 & Hwf2) & Hgamma).
split.
2: apply neighborhood_for_squash; eauto.
split.
- intros l l' (r & Hr).
psimpl.
destruct (Hwf1 l l' ltac:(eexists; eauto)).
eexists; psimpl.
- intros () l l' Hr.
apply bind_hasvalue in Hr as (? & ? & ?).
destruct x; psimpl.
Qed.
Lemma strict_well_founded_neighborhood_for_squash [A R : Type] :
forall (F : (nat -> part A) -> part R) (gamma : neighborhood_fun A R),
strict_well_founded_neighborhood_for gamma F -> strict_well_founded_neighborhood_for (fun l => bind (gamma l) (fun o => ret match o with
| Some _ => Some ()
| _ => None
end)) (fun f => bind (F f) (fun _ => ret ())).
Proof.
intros F gamma (Hstrict & Hgamma).
split.
2: apply well_founded_neighborhood_for_squash; eauto.
intros l.
eassert (ter (bind (gamma l) _) <-> ter (gamma l)) as ->
by (split; intros (? & ?); simpl_assms; eexists; psimpl).
etransitivity.
1:apply Hstrict.
split; intros (? & ? & ?); psimpl.
destruct x1; inversion H2; eauto.
Qed.
Definition termination_tree [A R : Type] (F : (nat -> part A) -> part R) (gamma : neighborhood_fun A R) :
strict_well_founded_neighborhood_for gamma F -> sigma1_tree A.
Proof.
intros Hgamma.
set (ptree_branch f := ter (F f)).
set (ptree_path l := ter (gamma l)).
apply mkSigma1Tree with (ptree_branch := ptree_branch) (ptree_path := ptree_path)
(F := fun f => bind (F f) (fun _ => ret ()))
(gamma := fun l => bind (gamma l) (fun o => ret match o with
| Some _ => Some ()
| _ => None
end)).
- now apply strict_well_founded_neighborhood_for_squash.
- unfold reflectspfn, ptree_branch.
intros f; split; intros (r & Hr); psimpl; eexists; psimpl.
- unfold reflectspfn, ptree_path.
intros f; split; intros (r & Hr); psimpl; eexists; psimpl.
Defined.
Definition brouwer_op_for [A R : Type] (gamma : neighborhood_fun A R) (F : (nat -> part A) -> part R) (Hgamma : strict_well_founded_neighborhood_for gamma F) :=
forall (Hnil : (termination_tree F gamma Hgamma).(ptree_path) nil), brouwer_op A R (termination_tree F gamma Hgamma) gamma nil Hnil.
Definition brouwer_operation_cont [A R : Type] (F : (nat -> part A) -> part R) :=
exists (gamma : neighborhood_fun A R)
(Hgamma : strict_well_founded_neighborhood_for gamma F), brouwer_op_for gamma F Hgamma.
Lemma brouwer_op_to_strict_well_founded_neighborhood [A R : Type] (F : (nat -> part A) -> part R) :
brouwer_operation_cont F -> strict_well_founded_neighborhood_cont F.
Proof.
intros (? & ? & ?); eexists; eauto.
Qed.
Lemma brouwer_op_to_neighborhood [A R : Type] (F : (nat -> part A) -> part R) :
brouwer_operation_cont F -> neighborhood_cont F.
Proof.
intros (? & (? & ? & ?) & ?); eexists; eauto.
Qed.
Definition neighborhood_canonical [A R : Type] (gamma : neighborhood_fun A R) : (nat -> part A) -> part R :=
fun f => mu_opt (fun n => bind (fold_part_list (tabulate f 0 n)) gamma).
Lemma neighborhood_canonical_correct [A R : Type] (gamma : neighborhood_fun A R) :
neighborhood_for gamma (neighborhood_canonical gamma).
Proof.
intros f r; eauto.
Qed.
Lemma permutes_quantifier_strict_well_founded_brouwer_operation [A R : Type] :
(forall (F : (nat -> part A) -> part R), strict_well_founded_neighborhood_cont F -> brouwer_operation_cont F) ->
forall (F : (nat -> part A) -> part R) (gamma : neighborhood_fun A R)
(Hgamma : strict_well_founded_neighborhood_for gamma F), brouwer_op_for gamma F Hgamma.
Proof.
intros Hcont F gamma (Hstrict & (Hwf1 & Hwf2) & Hgamma).
set (F' := neighborhood_canonical gamma).
assert (Hgamma' : strict_well_founded_neighborhood_for gamma F')
by repeat (eauto using neighborhood_canonical_correct; split).
specialize (Hcont F' ltac:(eexists; eauto)) as (xi & (Hstrict' & Hwf' & Hxi') & Hxi).
assert (Htrans : forall (r : R) (l : list A), xi l =! Some r -> exists (n : nat), gamma (rev (firstn n (rev l))) =! Some r). {
intros r l Hr.
clear Hxi.
set (f := nth_undef (rev l)).
assert (Hr' : F' f =! r). {
eapply Hxi', well_founded_neighborhood_hasvalue; eauto.
eapply bind_hasvalue_given; eauto.
eapply fold_tab_nth_undef.
rewrite firstn_all, rev_involutive.
eauto.
}
unfold F' in Hr'.
apply mu_opt_hasvalue in Hr' as (n & Hn & Hn').
exists n.
psimpl.
now apply fold_tab_nth_undef in H as (_ & ->).
}
assert (Htrans' : forall (l : list A), ter (gamma l) -> ter (xi l)). {
intros l (r & l' & Hr)%Hstrict.
set (f' := nth_undef (rev (l' ++ l))).
assert (F' f' =! r). {
destruct Hgamma' as (_ & Hgamma').
eapply Hgamma', well_founded_neighborhood_hasvalue; eauto.
1: split; eauto.
psimpl.
apply fold_tab_nth_undef.
rewrite firstn_all, rev_involutive.
eauto.
}
apply Hstrict'.
apply Hxi' in H as (m & Hm & Hm')%mu_opt_hasvalue.
psimpl.
apply fold_tab_nth_undef in H as (Hm & ->).
setoid_rewrite <- rev_firstn_rev with (n := m).
eexists r, _.
destruct Hwf'; eauto.
}
intros Hnil.
cbn in *.
specialize (Hxi (Htrans' _ Hnil)).
induction Hxi as [l Hl [(r & Hr) | (Hr & Hhered & Hind)]] using brouwer_op_ind'.
- apply Htrans in Hr as (n & Hr).
constructor; left; eauto.
exists r.
setoid_rewrite <- rev_firstn_rev.
eauto.
- destruct Hnil as ([|] & ?); constructor; [left | right; split ]; eauto.
intros a Hal.
apply Hind.
cbn in *.
eauto.
Qed.
Lemma all_strict_well_founded_neighborhood_are_brouwer_op_transfer [A R : Type] :
inhabited R ->
(forall (F : (nat -> part A) -> part R),
strict_well_founded_neighborhood_cont F -> brouwer_operation_cont F) ->
(forall (F : (nat -> part A) -> part unit),
strict_well_founded_neighborhood_cont F -> brouwer_operation_cont F).
Proof.
intros [r] HR F (gamma & Hstrict & Hwf & Hgamma).
set (F' := fun f => bind (F f) (fun _ => ret r)).
assert (HF' : strict_well_founded_neighborhood_cont F'). {
exists (fun l => bind (gamma l) (fun o => ret (match o with
| Some _ => Some r
| None => None
end))).
assert (Hter : forall l, ter (gamma l) <->
ter (bind (gamma l) (fun o => ret (match o with
| Some _ => Some r
| None => None
end))))
by (intros; split; intros (? & ?); simpl_assms; eexists; psimpl).
split.
1: {
intros l.
rewrite <- Hter.
eassert ((exists r' l',
bind (gamma (l' ++ l)) (fun o => ret match o with
| Some _ => Some r
| None => None
end) =! Some r') <-> exists r' l', gamma (l' ++ l) =! Some r'
)
as ->
by (split; intros (r' & l' & Hr'); psimpl;
destruct x; inversion H2; psimpl).
apply Hstrict.
}
eassert (Hwf_bis : well_founded_neighborhood _).
2: split; try eassumption.
1: {
destruct Hwf as (Hwf1 & Hwf2).
split.
- intros l l'.
do 2 rewrite <- Hter; eauto.
- intros r' l l'.
intros; simpl_assms.
destruct x; inversion H2; psimpl.
}
intros f r'.
unfold F'.
rewrite (Hgamma f).
split.
- intros (o & (n & Hn & Hn')%mu_opt_hasvalue & ?)%bind_hasvalue.
eapply well_founded_neighborhood_hasvalue; eauto.
psimpl.
- intros (n & Hn & Hn')%mu_opt_hasvalue.
simpl_assms.
destruct x0; inversion H3; subst.
rewrite bind_hasvalue_given with (a := u).
1:psimpl.
eapply well_founded_neighborhood_hasvalue; psimpl.
}
destruct (HR F' HF') as (xi' & Hxi' & Hbop').
set (xi := fun l => bind (xi' l) (fun o => ret (match o with
| Some _ => Some ()
| None => None
end))).
assert (Hxi : strict_well_founded_neighborhood_for xi F). {
destruct Hxi' as (Hstrict' & Hwf' & Hxi').
assert (Hter : forall l, ter (xi' l) <-> ter (xi l))
by (intros; unfold xi; split; intros (? & ?); simpl_assms; eexists; psimpl).
split.
1: {
intros l.
rewrite <- Hter.
eassert ((exists r' l', xi (l' ++ l) =! Some r')
<-> exists r' l', xi' (l' ++ l) =! Some r'
)
as ->
by (unfold xi; split; intros (r' & l' & Hr'); psimpl;
destruct x; inversion H2; psimpl).
eauto.
}
assert (Hwf_bis : well_founded_neighborhood xi). {
destruct Hwf' as (Hwf1' & Hwf2').
split.
- intros l l'.
do 2 rewrite <- Hter; eauto.
- intros () l l' Hl.
unfold xi in *.
simpl_assms.
destruct x; inversion H2.
psimpl.
}
split.
1: eauto.
intros f ().
split.
- intros Hr.
assert (F' f =! r) by (unfold F'; psimpl).
apply Hxi', mu_opt_hasvalue in H as (n & Hn & Hn').
eapply well_founded_neighborhood_hasvalue; eauto.
unfold xi.
psimpl.
- intros (n & Hn & Hn')%mu_opt_hasvalue.
assert (exists r', bind (fold_part_list (tabulate f 0 n)) xi' =! Some r')
as (? & ?). (unfold xi in *; simpl_assms; destruct x0; psimpl).
eapply well_founded_neighborhood_hasvalue, Hxi' in H; eauto.
unfold F' in *; psimpl.
destruct x0; eauto.
}
exists xi, Hxi.
assert (Htrans : forall l, ter (xi l) -> ter (xi' l))
by (intros l (? & ?); unfold xi in *; simpl_assms; eexists; psimpl).
intros Hnil.
specialize (Hbop' (Htrans _ Hnil)).
induction Hbop' as [l Hl [(r' & Hr') | (Hr & Hhered & Hind) ]] using brouwer_op_ind'.
- constructor.
left; exists (); unfold xi; psimpl.
- constructor.
right; split.
1: unfold xi; psimpl.
intros a Hal.
apply (Hind a (Htrans _ Hal) Hal).
Qed.
Definition pbarred [A : Type] (T : sigma1_tree A) (P : list A -> Prop) :=
forall (f : nat -> part A),
T.(ptree_branch) f -> exists (n : nat) (la : list A),
fold_part_list (tabulate f 0 n) =! la /\ P la.
Inductive hereditarily_pbarred [A : Type] (T : sigma1_tree A) (P : list A -> Prop) : forall (l : list A), T.(ptree_path) l -> Prop :=
| Hpbar : forall (l : list A) (Hl : T.(ptree_path) l),
P l \/ (~ P l /\ forall (a : A) (Hal : T.(ptree_path) (a :: l)), hereditarily_pbarred T P (a :: l) Hal)
-> hereditarily_pbarred T P l Hl.
Fixpoint hereditarily_pbarred_ind' [A : Type] (T : sigma1_tree A) (P : list A -> Prop) (Q : forall (l : list A), T.(ptree_path) l -> Prop) :
(forall (l : list A) (Hl : T.(ptree_path) l),
P l \/ (~ P l /\
(forall (a : A) (Hal : T.(ptree_path) (a :: l)), hereditarily_pbarred T P (a :: l) Hal) /\
(forall (a : A) (Hal : T.(ptree_path) (a :: l)), Q (a :: l) Hal)) -> Q l Hl) ->
forall (l : list A) (Hl : T.(ptree_path) l), hereditarily_pbarred T P l Hl -> Q l Hl.
Proof.
specialize (hereditarily_pbarred_ind' A T P Q).
intros Hind l Hl t.
destruct t as [l Hl [Ht | Ht]].
- apply Hind.
left.
auto.
- apply Hind.
right.
destruct Ht.
auto.
Qed.
Definition pBIT (A : Type) :=
forall (T : sigma1_tree A) (P : list A -> Prop),
(forall (l : list A), T.(ptree_path) l -> {P l} + {~P l}) ->
(forall (l l' : list A), P l -> P (l' ++ l)) ->
pbarred T P -> forall (Hnil : T.(ptree_path) nil), hereditarily_pbarred T P nil Hnil.
Definition bar_to_neighborhood_fun [A : Type] (T : sigma1_tree A) (P : list A -> Prop)
(Hdec : forall (l : list A), T.(ptree_path) l -> {P l} + {~P l}) :
neighborhood_fun A unit.
Proof.
refine (fun l => bind (proof_ter (T.(gamma) l))
(fun Hl => ret (if Hdec l _ then eval Hl else None))).
apply T.(Hptree_path).
destruct Hl as (? & ?); eexists; psimpl.
Defined.
Lemma bar_to_well_founded_neighborhood_fun [A : Type] (T : sigma1_tree A) (P : list A -> Prop)
(Hdec : forall (l : list A), T.(ptree_path) l -> {P l} + {~P l})
(Hmono : forall (l l' : list A), P l -> P (l' ++ l)) :
well_founded_neighborhood (bar_to_neighborhood_fun T P Hdec).
Proof.
destruct T.(Hgamma) as (? & (Hwf1 & Hwf2) & ?); eauto.
split.
- intros l l' (o & Ho).
unfold bar_to_neighborhood_fun in *.
simpl_assms.
eenough (ter (proof_ter (T.(gamma) l))) as (? & ?)
by (eexists; rewrite bind_hasvalue_given; psimpl).
apply proof_ter_spec; eauto.
- intros r l l' Hr.
unfold bar_to_neighborhood_fun in *.
simpl_assms.
destruct (Hdec _ _); inversion H4.
assert (ter (proof_ter (T.(gamma) (l' ++ l)))) as (? & ?). {
apply proof_ter_spec.
exists (Some r).
apply Hwf2.
rewrite <- H3; apply eval_hasvalue.
}
rewrite bind_hasvalue_given; eauto.
destruct (Hdec _ _) as [HP | HP]; eauto.
2: contradict HP; eauto.
enough (eval x0 = eval x) as -> by psimpl.
eapply hasvalue_det.
+ apply eval_hasvalue.
+ rewrite H3.
eapply Hwf2.
rewrite <- H3.
apply eval_hasvalue.
Qed.
Lemma bar_to_neighborhood [A : Type] (T : sigma1_tree A) (P : list A -> Prop)
(Hbar : pbarred T P) (Hdec : forall l, T.(ptree_path) l -> {P l} + {~P l})
(Hmono : forall l l', P l -> P (l' ++ l)) :
neighborhood_for (bar_to_neighborhood_fun T _ Hdec) T.(F).
Proof.
destruct T.(Hgamma) as (Hstrict & (Hwf1 & Hwf2) & Hgamma).
intros f ().
specialize (Hbar f).
split.
- intros (n & (l & Hl & Hr)%bind_hasvalue & Hn')%Hgamma%mu_opt_hasvalue.
assert (Hf : T.(ptree_branch) f). {
apply T.(Hptree_branch).
eexists.
eapply Hgamma, well_founded_neighborhood_hasvalue.
1:split; eauto.
psimpl.
}
specialize (Hbar Hf) as (n' & l' & Hl' & HPr).
destruct (Nat.le_ge_cases n n') as [Hnn' | Hnn'].
+ eapply well_founded_neighborhood_hasvalue.
1:eapply bar_to_well_founded_neighborhood_fun; eauto.
rewrite bind_hasvalue_given with (a := l'); eauto.
rewrite <- tabulate_add with (n := n), fold_part_list_app in Hl'; try lia.
rewrite bind_hasvalue_given in Hl'; eauto.
apply bind_hasvalue in Hl' as (l2 & ? & Hl'%ret_hasvalue_iff); subst.
assert (ter (proof_ter (T.(gamma) (l2 ++ l)))) as (? & ?). {
apply proof_ter_spec.
eexists.
eapply Hwf2.
eauto.
}
unfold bar_to_neighborhood_fun.
rewrite bind_hasvalue_given; eauto.
apply ret_hasvalue_iff.
destruct (Hdec (l2 ++ l)); try contradiction.
eapply hasvalue_det.
1: apply eval_hasvalue.
eauto.
+ eapply well_founded_neighborhood_hasvalue.
1:eapply bar_to_well_founded_neighborhood_fun; eauto.
rewrite bind_hasvalue_given with (a := l); eauto.
rewrite <- tabulate_add with (n := n'), fold_part_list_app in Hl; try lia.
rewrite bind_hasvalue_given in Hl; eauto.
apply bind_hasvalue in Hl as (l2 & ? & Hl%ret_hasvalue_iff); subst.
assert (ter (proof_ter (T.(gamma) (l2 ++ l')))) as (? & ?)
by (apply proof_ter_spec; eexists; eauto).
unfold bar_to_neighborhood_fun.
rewrite bind_hasvalue_given; eauto.
apply ret_hasvalue_iff.
apply Hmono with (l' := l2) in HPr.
destruct (Hdec (l2 ++ l')) as [_ | ?]; try contradiction.
eapply hasvalue_det; eauto.
apply eval_hasvalue.
- intros (n & (l & Hl & (Hter & Hter' & Hr%ret_hasvalue_iff)%bind_hasvalue)%bind_hasvalue & Hn')%mu_opt_hasvalue.
destruct (Hdec l) as [HPr | _]; try discriminate.
apply Hgamma.
eapply well_founded_neighborhood_hasvalue.
1: split; eauto.
psimpl.
rewrite <- Hr.
apply eval_hasvalue.
Qed.
Lemma monotone_bar_extend_true [A : Type] (T : sigma1_tree A) (P : list A -> Prop)
(Hbar : pbarred T P) (Hmono : forall l l', P l -> P (l' ++ l)) :
forall (l : list A), T.(ptree_path) l -> exists (l' : list A), P (l' ++ l).
Proof.
intros l Hl.
apply T.(Hptree_path) in Hl.
destruct Hl; psimpl.
assert (ter (T.(gamma) l)) by (eexists; eauto).
rename H0 into Hl.
clear x0 H H1.
destruct T.(Hgamma) as (Hstrict & Hwf & Hgamma).
apply Hstrict in Hl as (() & l' & Hl).
assert (Hl' : bind (fold_part_list (tabulate (nth_undef (rev (l' ++ l))) 0 (length (rev (l' ++ l))))) T.(gamma) =! Some ()). {
psimpl.
apply fold_tab_nth_undef.
rewrite firstn_all, rev_involutive; eauto.
}
apply well_founded_neighborhood_hasvalue, Hgamma in Hl'; eauto.
assert (Hl1' : T.(ptree_branch) (nth_undef (rev (l' ++ l)))). {
apply T.(Hptree_branch).
eexists; eauto.
}
specialize (Hbar (nth_undef (rev (l' ++ l))) Hl1') as (n & la & Hla' & Hla).
apply fold_tab_nth_undef in Hla' as (Hn & ->).
eapply Hmono in Hla.
rewrite rev_firstn_rev in Hla.
eauto.
Qed.
Lemma bar_to_strict_well_founded_neighborhood [A : Type] (T : sigma1_tree A) (P : list A -> Prop)
(Hbar : pbarred T P) (Hdec : forall l, T.(ptree_path) l -> {P l} + {~P l})
(Hmono : forall l l', P l -> P (l' ++ l)) :
strict_well_founded_neighborhood_for (bar_to_neighborhood_fun T _ Hdec) T.(F).
Proof.
split.
2: {
split.
- apply bar_to_well_founded_neighborhood_fun; eauto.
- apply bar_to_neighborhood; eauto.
}
intros l.
destruct T.(Hgamma) as (Hstrict & Hwf & Hgamma).
split.
- intros (o & Ho).
exists ().
destruct o as [()|].
1:exists nil; eauto.
unfold bar_to_neighborhood_fun in Ho.
simpl_assms.
clear H H2.
apply Hstrict in x as (() & l' & Hl').
assert (exists l'', P (l'' ++ l' ++ l)) as (l'' & Hl''). {
eapply monotone_bar_extend_true; eauto.
apply Hptree_path; eexists; psimpl.
}
exists (l'' ++ l').
rewrite <- app_assoc.
unfold bar_to_neighborhood_fun.
destruct Hwf as (_ & Hwf2).
apply Hwf2 with (l' := l'') in Hl'.
eassert (ter (proof_ter _)) as (? & ?) by (apply proof_ter_spec; eexists; eauto).
rewrite bind_hasvalue_given; eauto.
destruct (Hdec _ _); psimpl.
eapply ret_hasvalue_iff, hasvalue_det; eauto.
eapply eval_hasvalue.
- intros (() & l' & Hr).
unfold bar_to_neighborhood_fun in *.
simpl_assms; clear H2.
eenough (ter (proof_ter _)) as (? & ?)
by (eexists; rewrite bind_hasvalue_given; psimpl).
apply proof_ter_spec.
destruct Hwf; eauto.
Qed.
Lemma neighborhood_to_brouwer_op_pbit [A : Type] :
(forall (F : (nat -> part A) -> part unit) (gamma : neighborhood_fun A unit)
(Hgamma : strict_well_founded_neighborhood_for gamma F), brouwer_op_for gamma F Hgamma) ->
pBIT A.
Proof.
intros Hcont.
intros T P Hdec Hmono Hbar Hnil.
epose (gamma := bar_to_neighborhood_fun T _ Hdec).
assert (Hgamma : strict_well_founded_neighborhood_for gamma T.(F))
by (eapply bar_to_strict_well_founded_neighborhood; eauto).
assert (Hpath1 : forall l, T.(ptree_path) l -> (termination_tree T.(F) gamma Hgamma).(ptree_path) l). {
intros l Hl.
apply Hptree_path in Hl.
cbn.
destruct Hl.
psimpl.
unfold gamma, bar_to_neighborhood_fun.
eapply bind_ter'.
- apply proof_ter_spec.
eexists; eauto.
- intros ? ?.
eexists; psimpl.
}
specialize (Hcont T.(F) gamma Hgamma (Hpath1 _ Hnil)).
induction Hcont as [l Hl [(() & Hr)|(Hr & Hop & Hind)]] using brouwer_op_ind'; constructor.
- left.
unfold gamma, bar_to_neighborhood_fun in Hr.
psimpl.
destruct (Hdec l _); eauto.
discriminate.
- unfold gamma, bar_to_neighborhood_fun in Hr.
psimpl.
destruct (Hdec l _); eauto.
Qed.
Lemma pbit_neighborhood_to_brouwer_op [A R : Type] :
pBIT A -> (forall (gamma : neighborhood_fun A R) (F : (nat -> part A) -> part R)
(Hgamma : strict_well_founded_neighborhood_for gamma F), brouwer_op_for gamma F Hgamma).
Proof.
intros HBI.
intros gamma F Hgamma Hnil.
set (P l := exists (r : R), gamma l =! Some r).
assert (Hdec : forall l, (termination_tree F gamma Hgamma).(ptree_path) l -> {P l} + {~P l}). {
intros l Hl.
apply Hptree_path in Hl.
simpl in Hl.
assert (Hter : ter (gamma l)) by (destruct Hl; psimpl; eexists; psimpl).
destruct (eval Hter) as [o|] eqn:E.
- left.
eexists.
rewrite <- E.
apply eval_hasvalue.
- right.
intros Hc.
destruct Hc as (r & Hr).
enough (None = Some r) by discriminate.
eapply hasvalue_det; eauto.
rewrite <- E; apply eval_hasvalue.
}
assert (Hmono : forall l l', P l -> P (l' ++ l)). {
intros l l' (r & Hr).
exists r.
destruct Hgamma as (? & (? & Hwf2) & ?).
eauto.
}
assert (Hbar : pbarred (termination_tree F gamma Hgamma) P). {
intros f Hf.
apply Hptree_branch in Hf as (() & Hr).
simpl in Hr.
apply bind_hasvalue in Hr as (r & Hr & _).
destruct Hgamma as (? & (Hwf1 & Hwf2) & Hgamma).
apply Hgamma in Hr as (n & (l & Hl & Hr)%bind_hasvalue & Hn')%mu_opt_hasvalue.
exists n, l.
split; eauto.
eexists; eauto.
}
specialize (HBI (termination_tree F gamma Hgamma) P Hdec Hmono Hbar Hnil) as Hind.
induction Hind as [l Hl [HPr | (HPr & Hind & IHl)]] using hereditarily_pbarred_ind';
constructor; auto.
simpl in *.
destruct Hl as ([o|] & Hl); eauto.
Qed.
Theorem pbit_neighborhood_cont_to_brouwer_cont [A R : Type] :
enumerable (list A) -> inhabited R ->
pBIT A <-> forall (F : (nat -> part A) -> part R),
neighborhood_cont F -> brouwer_operation_cont F.
Proof.
intros HLA HR.
split.
- intros HA F HF.
apply enumerable_to_strictify_neighborhood_cont in HF as (gamma & Hgamma); auto.
exists gamma, Hgamma.
apply pbit_neighborhood_to_brouwer_op; auto.
- intros Hcont.
apply neighborhood_to_brouwer_op_pbit.
intros F gamma Hgamma.
apply permutes_quantifier_strict_well_founded_brouwer_operation.
eapply all_strict_well_founded_neighborhood_are_brouwer_op_transfer; eauto.
clear F gamma Hgamma.
intros F (gamma & Hstrict & Hwf & Hgamma).
apply Hcont.
eexists; eauto.
Qed.
Theorem pbit_neighborhood_cont_to_brouwer_cont_nat :
pBIT nat <-> forall (F : (nat -> part nat) -> part nat),
neighborhood_cont F -> brouwer_operation_cont F.
Proof.
apply pbit_neighborhood_cont_to_brouwer_cont.
2: repeat constructor.
apply enumerable_list.
exists id.
intros; eauto.
Qed.
End PartialZoo.
From mathcomp Require Import zify.
From Equations Require Import Equations.
Require Import extra_principles Util continuity_zoo_Prop partial embed_nat Common.
Import EmbedNatNotations PartialTactics ListNotations.
Set Bullet Behavior "Strict Subproofs".
Section PartialZoo.
Context `{Partiality : partiality}.
Definition neighborhood_fun (A R : Type) := list A -> part (option R).
Definition neighborhood_for [A R : Type] (gamma : neighborhood_fun A R) (F : (nat -> part A) -> part R) :=
forall (f : nat -> part A),
equiv (F f) (mu_opt (fun n => bind (fold_part_list (tabulate f 0 n)) gamma)).
Definition neighborhood_cont [A R : Type] (F : (nat -> part A) -> part R) : Prop :=
exists (gamma : neighborhood_fun A R), neighborhood_for gamma F.
Definition well_founded_neighborhood [A R : Type] (gamma : neighborhood_fun A R) : Prop :=
(forall (l l' : list A), ter (gamma (l' ++ l)) -> ter (gamma l)) /\
forall (r : R) (l l' : list A), gamma l =! Some r -> gamma (l' ++ l) =! Some r.
Definition well_founded_neighborhood_for [A R : Type] (gamma : neighborhood_fun A R) (F : (nat -> part A) -> part R) :=
well_founded_neighborhood gamma /\ neighborhood_for gamma F.
Definition well_founded_neighborhood_cont [A R : Type] (F : (nat -> part A) -> part R) : Prop :=
exists (gamma : neighborhood_fun A R), well_founded_neighborhood_for gamma F.
Definition strict_neighborhood [A R : Type] (gamma : neighborhood_fun A R) : Prop :=
forall (l : list A), ter (gamma l) <-> exists (r : R) (l' : list A), gamma (l' ++ l) =! Some r.
Definition strict_well_founded_neighborhood_for [A R : Type] (gamma : neighborhood_fun A R) (F : (nat -> part A) -> part R) :=
strict_neighborhood gamma /\ well_founded_neighborhood_for gamma F.
Definition strict_well_founded_neighborhood_cont [A R : Type] (F : (nat -> part A) -> part R) : Prop :=
exists (gamma : neighborhood_fun A R), strict_well_founded_neighborhood_for gamma F.
Definition make_well_founded [A R : Type] (gamma : neighborhood_fun A R) : neighborhood_fun A R :=
fun l => mu_opt (fun n => if n <=? length l then bind (gamma (rev (firstn n (rev l)))) (fun o => ret (match o with
| Some r => Some (Some r)
| None => None
end)) else ret (Some None)).
Lemma make_well_founded_preserves_neighborhood [A R : Type] (gamma : neighborhood_fun A R) :
forall (F : (nat -> part A) -> part R), neighborhood_for gamma F ->
neighborhood_for (make_well_founded gamma) F.
Proof.
intros F HF f r.
specialize (HF f r).
rewrite HF.
split.
- intros (n & Hn & Hn')%mu_opt_hasvalue.
apply mu_opt_hasvalue.
exists n.
split.
+ simpl_assms.
rewrite bind_hasvalue_given; eauto.
unfold make_well_founded.
apply mu_opt_hasvalue.
assert (n = length x) as -> by (eapply fold_part_list_tabulate_length; eauto).
exists (length x).
rewrite leb_correct, <- length_rev, firstn_all, rev_involutive; eauto.
split; psimpl.
intros k Hk.
rewrite leb_correct; eauto with arith.
rewrite length_rev in Hk.
specialize (Hn' k Hk).
simpl_assms.
rewrite <- tabulate_add with (n := k), fold_part_list_app in H; eauto with arith.
rewrite bind_hasvalue_given in H; eauto.
simpl_assms.
apply fold_part_list_tabulate_length in H1 as ->.
rewrite rev_app_distr, <- firstn_app_l.
2: rewrite length_rev; eauto.
rewrite <- length_rev, firstn_all, rev_involutive.
psimpl.
+ intros k Hk.
pose proof (Hn' k Hk) as (l & Hl & Hl')%bind_hasvalue.
rewrite bind_hasvalue_given; eauto.
unfold make_well_founded.
apply mu_opt_hasvalue.
assert (k = length l) as -> by (eapply fold_part_list_tabulate_length; eauto).
exists (S (length l)).
rewrite leb_correct_conv; eauto.
split; psimpl.
intros m Hm.
rewrite leb_correct; eauto with arith.
rewrite <- tabulate_add with (n := m), fold_part_list_app in Hl; eauto with arith.
simpl_assms.
assert (m = length x0) as -> by (eapply fold_part_list_tabulate_length; eauto).
rewrite rev_app_distr, <- length_rev, <- firstn_app_l, firstn_all, rev_involutive; eauto.
specialize (Hn' (length x0) ltac:(lia)).
rewrite bind_hasvalue_given in Hn'; psimpl.
- intros (n & (l & Hr & (m & Hm & Hm')%mu_opt_hasvalue)%bind_hasvalue & Hn')%mu_opt_hasvalue.
destruct (m <=? length l) eqn:E.
2: psimpl.
apply leb_complete in E.
apply mu_opt_hasvalue.
exists m.
simpl_assms.
destruct x as [r'|]; inversion H2; subst.
assert (n = length l) as -> by (eapply fold_part_list_tabulate_length; eauto).
rewrite <- tabulate_add with (n := m), fold_part_list_app in Hr; eauto with arith.
simpl_assms.
assert (m = length x) as -> by (eapply fold_part_list_tabulate_length; eauto).
rewrite bind_hasvalue_given; eauto.
rewrite rev_app_distr, <- length_rev, <- firstn_app_l, firstn_all, rev_involutive in H; eauto.
split.
1: psimpl.
intros k Hk.
specialize (Hm' k Hk).
rewrite leb_correct in Hm'; eauto with arith.
simpl_assms.
destruct x1; inversion H7; subst.
rewrite <- tabulate_add with (n := k), fold_part_list_app in H0; eauto with arith.
simpl_assms.
assert (k = length x1) as -> by (eapply fold_part_list_tabulate_length; eauto).
rewrite app_assoc, rev_app_distr, <- length_rev, <- firstn_app_l, firstn_all, rev_involutive in H3; eauto with arith.
psimpl.
Qed.
Lemma make_well_founded_is_monotonic [A R : Type] (gamma : neighborhood_fun A R) :
forall (r : R) (l l' : list A), make_well_founded gamma l =! Some r -> make_well_founded gamma (l' ++ l) =! Some r.
Proof.
intros r l l' (n & Hn & Hn')%mu_opt_hasvalue.
unfold make_well_founded in *.
apply mu_opt_hasvalue.
destruct (n <=? length l) eqn:E; simpl_assms.
apply leb_complete in E.
destruct x; inversion H2; subst.
exists n.
rewrite length_app, leb_correct; try lia.
rewrite rev_app_distr, <- firstn_app_l.
2: now rewrite length_rev.
split.
1: psimpl.
intros k Hk.
specialize (Hn' k ltac:(eauto with arith)).
rewrite leb_correct in Hn'; eauto with arith.
rewrite leb_correct, <- firstn_app_l; try rewrite length_rev; try lia.
eauto.
Qed.
Lemma make_well_founded_is_well_founded [A R : Type] (gamma : neighborhood_fun A R) :
well_founded_neighborhood (make_well_founded gamma).
Proof.
split.
2:apply make_well_founded_is_monotonic.
intros l l' (o & (n & Hn & Hn')%mu_opt_hasvalue).
destruct (n <=? length l) eqn:E.
- apply leb_complete in E.
rewrite length_app, rev_app_distr in *.
rewrite leb_correct in Hn; try lia.
exists o.
apply mu_opt_hasvalue.
exists n.
rewrite leb_correct; eauto.
rewrite <- firstn_app_l in Hn.
2: rewrite length_rev; eauto.
split.
1: eauto.
intros k Hk.
specialize (Hn' k Hk).
rewrite <- firstn_app_l in Hn'.
2: rewrite length_rev.
rewrite leb_correct.
rewrite leb_correct in Hn'.
apply Hn'.
all: lia.
- apply leb_complete_conv in E.
exists None.
apply mu_opt_hasvalue.
exists (S (length l)).
rewrite leb_correct_conv; eauto with arith.
split.
1: psimpl.
intros k Hk.
rewrite leb_correct; eauto with arith.
specialize (Hn' k ltac:(lia)).
rewrite length_app, rev_app_distr, leb_correct, <- firstn_app_l in Hn'.
2: rewrite length_rev.
eauto.
all: lia.
Qed.
Lemma neighborhood_cont_is_well_founded_neighborhood_cont [A R : Type] (F : (nat -> part A) -> part R) :
neighborhood_cont F -> well_founded_neighborhood_cont F.
Proof.
intros (gamma & Hgamma).
exists (make_well_founded gamma).
split.
- apply make_well_founded_is_well_founded.
- apply make_well_founded_preserves_neighborhood; eauto.
Qed.
Definition enumerable (A : Type) :=
exists (f : nat -> A), forall (a : A), exists (n : nat), f n = a.
Fixpoint tuple (A : Type) (n : nat) : Type :=
match n with
| O => unit
| S n => A * tuple A n
end.
Fixpoint enumerate_tuple [A : Type] (f : nat -> A) (n : nat) : nat -> tuple A n :=
match n return nat -> tuple A n with
| O => fun _ => ()
| S n => fun k => let '(n', m) := unembed k in (f n', enumerate_tuple f n m)
end.
Lemma enumerable_tuple {A : Type} {n : nat} :
enumerable A -> enumerable (tuple A n).
Proof.
intros (f & Hf).
exists (enumerate_tuple f n).
induction n as [|n IHn].
- intros (); exists 0; eauto.
- intros (a, t).
specialize (Hf a) as (n' & Hn).
specialize (IHn t) as (m & Hm).
exists (embed (n', m)).
simpl.
rewrite embedP.
subst; auto.
Qed.
Fixpoint tuple_to_list [A : Type] [n : nat] : tuple A n -> list A :=
match n return tuple A n -> list A with
| O => fun '() => nil
| S n => fun '(a, t) => a :: tuple_to_list t
end.
Lemma enumerable_list [A : Type] :
enumerable A -> enumerable (list A).
Proof.
intros HA.
pose proof HA as (f & Hf).
set (e n :=
let (len, m) := unembed n in
tuple_to_list (enumerate_tuple f len m)
).
exists e.
intros l.
induction l as [|a l IHl].
- exists 0; auto.
- destruct IHl as (m' & Hm).
unfold e in Hm |- *.
destruct (unembed m') as (len & m) eqn:E.
specialize (Hf a) as (n' & Hn).
exists (embed (S len, embed (n', m))).
rewrite embedP.
simpl.
rewrite embedP.
subst; auto.
Qed.
Definition neighborhood_fun_strictify [A R : Type] (gamma : neighborhood_fun A R) :
(nat -> list A) -> neighborhood_fun A R :=
fun e l => bind (mu_tot (fun k => let (n, m) := unembed k in
match seval (gamma (e n ++ l)) m with
| Some (Some _) => true
| _ => false
end))
(fun _ => gamma l).
Lemma neighborhood_fun_strictify_ter [A R : Type] (F : (nat -> part A) -> part R)
(gamma : neighborhood_fun A R) : forall (e : nat -> list A),
(forall (l : list A), exists (n : nat), e n = l) -> neighborhood_for gamma F -> well_founded_neighborhood gamma ->
forall (l : list A),
ter (neighborhood_fun_strictify gamma e l) <->
exists (r : R) (l' : list A), gamma (l' ++ l) =! Some r.
Proof.
intros e HA Hgamma Hwf l.
split.
- intros (o & Ho).
unfold neighborhood_fun_strictify in Ho.
psimpl.
apply mu_tot_hasvalue in H as (Hl & _).
destruct (unembed x) as (n & m).
destruct (seval (gamma (e n ++ l)) m) as [[r|]|] eqn:E; try now inversion Hl.
exists r, (e n).
eapply seval_hasvalue; eauto.
- intros (r & l' & Hr).
unfold neighborhood_fun_strictify.
assert (ter (gamma l)). {
destruct Hwf as (Hwf1 & _).
eapply Hwf1; eexists; eauto.
}
eapply bind_ter'; eauto.
destruct (HA l') as (n & Hn); subst.
apply seval_hasvalue in Hr as (m & Hm).
apply mu_tot_ter with (n := embed (n, m)).
rewrite embedP.
rewrite Hm; reflexivity.
Qed.
Lemma neighborhood_fun_strictify_hasvalue_some [A R : Type] (F : (nat -> part A) -> part R)
(gamma : neighborhood_fun A R) : forall (e : nat -> list A),
(forall (l : list A), exists (n : nat), e n = l) ->
forall (l : list A) (r : R), gamma l =! Some r ->
neighborhood_fun_strictify gamma e l =! Some r.
Proof.
intros e He l r Hr.
unfold neighborhood_fun_strictify.
eenough (ter (mu_tot _)) as (? & ?) by psimpl.
specialize (He nil) as (n & Hn).
apply seval_hasvalue in Hr as (m & Hm).
change l with (nil ++ l) in Hm.
apply mu_tot_ter with (embed (n, m)).
now rewrite embedP, Hn, Hm.
Qed.
Lemma neighborhood_fun_strictify_hasvalue_none [A R : Type] (F : (nat -> part A) -> part R)
(gamma : neighborhood_fun A R) : forall (e : nat -> list A),
(forall (l : list A), exists (n : nat), e n = l) -> neighborhood_for gamma F ->
forall (l : list A), gamma l =! None -> ter (neighborhood_fun_strictify gamma e l) ->
neighborhood_fun_strictify gamma e l =! None.
Proof.
intros e He Hgamma l Hl Hl'.
destruct Hl' as ([r|] & Hr); eauto.
unfold neighborhood_fun_strictify in Hr.
simpl_assms.
assert (None = Some r) as [=] by (eapply hasvalue_det; eauto).
Qed.
Lemma neighborhood_fun_strictify_strict [A R : Type] (F : (nat -> part A) -> part R)
(gamma : neighborhood_fun A R) : forall (e : nat -> list A),
(forall (l : list A), exists (n : nat), e n = l) -> neighborhood_for gamma F -> well_founded_neighborhood gamma ->
strict_neighborhood (neighborhood_fun_strictify gamma e).
Proof.
intros e He Hgamma Hwf l.
repeat rewrite neighborhood_fun_strictify_ter; eauto.
split; intros (r & l' & Hr).
- eapply neighborhood_fun_strictify_hasvalue_some in Hr; eauto.
- assert (Hter : ter (neighborhood_fun_strictify gamma e (l' ++ l))) by (eexists; eauto).
eapply neighborhood_fun_strictify_ter in Hter as (r' & l'' & Hr'); eauto.
exists r', (l'' ++ l').
now rewrite app_assoc in Hr'.
Qed.
Definition neighborhood_fun_strictify_wf [A R : Type] (gamma : neighborhood_fun A R) :
forall (e : nat -> list A),
(forall (l : list A), exists (n : nat), e n = l) -> well_founded_neighborhood gamma ->
well_founded_neighborhood (neighborhood_fun_strictify gamma e).
Proof.
intros e HA (Hwf1 & Hwf2).
split.
- intros l l' (r & Hr).
unfold neighborhood_fun_strictify in *.
psimpl.
eapply bind_ter'.
2: intros _ _; eapply Hwf1; eexists; eauto.
eapply mu_tot_hasvalue in H as (H & _).
destruct (unembed x) as (n & m).
destruct (HA (e n ++ l')) as (n' & Hn').
eapply mu_tot_ter with (n := embed (n', m)).
rewrite embedP, Hn', <- app_assoc.
eauto.
- intros r l l' Hr.
unfold neighborhood_fun_strictify in *.
eapply bind_hasvalue in Hr as (? & ? & ?).
eenough (ter (mu_tot _)) as (? & ?) by psimpl.
destruct (HA nil) as (n & Hn).
assert (Hr : gamma (e n ++ l' ++ l) =! Some r) by (rewrite Hn; simpl; eauto).
apply seval_hasvalue in Hr as (m & Hm).
eapply mu_tot_ter with (n := embed (n, m)).
rewrite embedP.
rewrite Hm; reflexivity.
Qed.
Lemma strictify_preserves_neighborhood [A R : Type] (gamma : neighborhood_fun A R) :
forall (e : nat -> list A), (forall (l : list A), exists (n : nat), e n = l) ->
forall (F : (nat -> part A) -> part R), neighborhood_for gamma F -> well_founded_neighborhood gamma ->
neighborhood_for (neighborhood_fun_strictify gamma e) F.
Proof.
intros e He F Hgamma Hwf f r.
rewrite (Hgamma f r).
do 2 rewrite mu_opt_hasvalue.
split.
- intros (n & Hn & Hn').
exists n.
simpl_assms.
rewrite bind_hasvalue_given; eauto.
split.
1: apply neighborhood_fun_strictify_hasvalue_some; eauto.
intros k Hk.
specialize (Hn' k Hk).
simpl_assms.
rewrite bind_hasvalue_given; eauto.
eapply neighborhood_fun_strictify_hasvalue_none; eauto.
eapply neighborhood_fun_strictify_ter; eauto.
rewrite <- tabulate_add with (n := k), fold_part_list_app in H; eauto with arith.
rewrite bind_hasvalue_given in H; eauto.
psimpl.
- intros (n & Hn & Hn').
exists n.
unfold neighborhood_fun_strictify in Hn.
simpl_assms.
split.
1: psimpl.
intros k Hk.
specialize (Hn' k Hk).
unfold neighborhood_fun_strictify in Hn'.
psimpl.
Qed.
Lemma enumerable_to_strictify_neighborhood_cont [A R : Type] : enumerable (list A) ->
forall (F : (nat -> part A) -> part R), neighborhood_cont F ->
strict_well_founded_neighborhood_cont F.
Proof.
intros (e & He) F (gamma & Hwf & Hgamma)%neighborhood_cont_is_well_founded_neighborhood_cont.
exists (neighborhood_fun_strictify gamma e).
split.
2: split.
- eapply neighborhood_fun_strictify_strict; eauto.
- eapply neighborhood_fun_strictify_wf; eauto.
- eapply strictify_preserves_neighborhood; eauto.
Qed.
Lemma well_founded_neighborhood_hasvalue [A R : Type] (gamma : neighborhood_fun A R)
(f : nat -> part A) (r : R) (n : nat) :
well_founded_neighborhood gamma ->
bind (fold_part_list (tabulate f 0 n)) gamma =! Some r ->
mu_opt (fun n => bind (fold_part_list (tabulate f 0 n)) gamma) =! r.
Proof.
intros (Hwf1 & Hwf2) Hr.
induction n as [|n IHn]. 1:{
apply mu_opt_hasvalue.
exists 0.
split; psimpl.
}
rewrite tabulate_succ', fold_part_list_app in Hr; eauto with arith.
cbn in Hr.
simpl_assms.
destruct (Hwf1 x0 [x2] ltac:(eexists; eauto)) as ([r'|] & Hr').
1: {
assert (Some r = Some r') as [=] by (eapply hasvalue_det; eauto).
subst; eapply IHn; psimpl.
}
apply mu_opt_hasvalue.
exists (S n).
rewrite tabulate_succ', fold_part_list_app; eauto with arith.
cbn; split.
1: psimpl.
intros k Hk.
inversion Hk; subst.
1: psimpl.
rewrite <- tabulate_add with (n := k), fold_part_list_app in H; eauto with arith.
psimpl.
destruct (Hwf1 _ _ ltac:(eexists; eapply Hr')) as ([r'|] & Hr''); eauto.
assert (None = Some r') as [=] by (eapply hasvalue_det; eauto).
Qed.
#[projections(primitive)]
Record sigma1_tree (A : Type) := mkSigma1Tree {
ptree_branch : (nat -> part A) -> Prop;
ptree_path : list A -> Prop;
F : (nat -> part A) -> part unit;
gamma : neighborhood_fun A unit;
Hgamma : strict_well_founded_neighborhood_for gamma F;
Hptree_branch : reflectspfn ptree_branch F;
Hptree_path : reflectspfn ptree_path (fun l => bind (gamma l) (fun _ => ret ()));
}.
Arguments ptree_branch {_}.
Arguments ptree_path {_}.
Arguments F {_}.
Arguments gamma {_}.
Arguments Hgamma {_}.
Arguments Hptree_branch {_}.
Arguments Hptree_path {_}.
Lemma ptree_branch_extend [A : Type] (T : sigma1_tree A) :
forall (f : nat -> part A), T.(ptree_branch) f ->
forall (l : list A), extend l f -> T.(ptree_path) l.
Proof.
intros f Hf l Hl.
apply Hptree_branch in Hf.
apply Hptree_path.
rewrite extend_fold_part in Hl.
destruct Hf as (r & Hr).
destruct T.(Hgamma) as (_ & (Hwf1 & Hwf2) & Hgamma).
specialize (Hgamma f r).
apply Hgamma in Hr as (n & Hn & Hn')%mu_opt_hasvalue.
enough (ter (T.(gamma) l)) as (? & ?) by (eexists; psimpl).
destruct (Nat.le_ge_cases n (length l)) as [Hnl | Hnl].
- erewrite <- tabulate_add, fold_part_list_app in Hl; try (eassumption || lia).
psimpl.
assert (x1 = x) by (eapply hasvalue_det; eauto); subst.
eexists; psimpl.
- simpl_assms.
erewrite <- tabulate_add with (n := length l), fold_part_list_app in H; try (eassumption || lia).
psimpl.
assert (x0 = l) by (eapply hasvalue_det; eauto); subst.
assert (ter (T.(gamma) l)) as (? & ?) by (eapply Hwf1; eexists; eauto).
eexists; psimpl.
Qed.
Lemma ptree_restrict [A : Type] (T : sigma1_tree A) :
forall (l l' : list A), T.(ptree_path) (l' ++ l) -> T.(ptree_path) l.
Proof.
intros l l' Hl.
apply T.(Hptree_path) in Hl.
apply T.(Hptree_path).
enough (ter (T.(gamma) l)) as (? & ?) by (eexists; psimpl).
destruct Hl.
psimpl.
destruct T.(Hgamma) as (_ & (Hwf & _) & _).
eapply Hwf.
eexists.
psimpl.
Qed.
Inductive brouwer_op (A R : Type) (T : sigma1_tree A) (gamma : neighborhood_fun A R) : forall (l : list A), T.(ptree_path) l -> Prop :=
| BOp : forall (l : list A) (Hl : T.(ptree_path) l),
(exists (r : R), gamma l =! Some r) \/ (gamma l =! None /\ forall (a : A) (Hal : T.(ptree_path) (a :: l)),
brouwer_op A R T gamma (a :: l) Hal) -> brouwer_op A R T gamma l Hl.
Arguments BOp [_ _]%_type {_%_type _ _}.
Fixpoint brouwer_op_ind' (A R : Type) (T : sigma1_tree A) (gamma : neighborhood_fun A R)
(Ar : forall (l : list A), T.(ptree_path) l -> Prop)
(HBOp : forall (l : list A) (Hl : T.(ptree_path) l),
(exists (r : R), gamma l =! Some r) \/ (gamma l =! None /\
(forall (a : A) (Hal : T.(ptree_path) (a :: l)), brouwer_op A R T gamma (a :: l) Hal) /\
(forall (a : A) (Hal : T.(ptree_path) (a :: l)), Ar (a :: l) Hal)
)
-> Ar l Hl) :
forall (l : list A) (Hl : T.(ptree_path) l), brouwer_op A R T gamma l Hl -> Ar l Hl.
Proof.
intros l Hl b.
specialize (brouwer_op_ind' A R T gamma Ar HBOp).
destruct b as [l Hl Hb].
apply (HBOp l Hl).
destruct Hb as [(r & Hr) | (Hgamma & Hb)].
- left; eexists; eauto.
- right; repeat (split; auto).
Qed.
Lemma neighborhood_for_squash [A R : Type] :
forall (F : (nat -> part A) -> part R) (gamma : neighborhood_fun A R),
neighborhood_for gamma F -> neighborhood_for (fun l => bind (gamma l) (fun o => ret match o with
| Some _ => Some ()
| _ => None
end)) (fun f => bind (F f) (fun _ => ret ())).
Proof.
intros F gamma Hgamma.
intros f (); split; specialize (Hgamma f).
- intros Hr.
apply bind_hasvalue in Hr as (? & ? & ?).
apply Hgamma in H as (n & Hn & Hn')%mu_opt_hasvalue.
apply mu_opt_hasvalue.
exists n.
split.
1: psimpl.
intros k Hk.
specialize (Hn' k Hk).
psimpl.
- intros (n & Hn & Hn')%mu_opt_hasvalue.
repeat (apply bind_hasvalue in Hn as (? & ? & Hn)).
rewrite <- ret_hasvalue_iff in Hn.
destruct x0; inversion Hn.
psimpl.
apply Hgamma.
apply mu_opt_hasvalue; exists n.
split.
1: psimpl.
intros k Hk.
specialize (Hn' k Hk); psimpl.
destruct x1; now inversion H5.
Qed.
Lemma well_founded_neighborhood_for_squash [A R : Type] :
forall (F : (nat -> part A) -> part R) (gamma : neighborhood_fun A R),
well_founded_neighborhood_for gamma F -> well_founded_neighborhood_for (fun l => bind (gamma l) (fun o => ret match o with
| Some _ => Some ()
| _ => None
end)) (fun f => bind (F f) (fun _ => ret ())).
Proof.
intros F gamma ((Hwf1 & Hwf2) & Hgamma).
split.
2: apply neighborhood_for_squash; eauto.
split.
- intros l l' (r & Hr).
psimpl.
destruct (Hwf1 l l' ltac:(eexists; eauto)).
eexists; psimpl.
- intros () l l' Hr.
apply bind_hasvalue in Hr as (? & ? & ?).
destruct x; psimpl.
Qed.
Lemma strict_well_founded_neighborhood_for_squash [A R : Type] :
forall (F : (nat -> part A) -> part R) (gamma : neighborhood_fun A R),
strict_well_founded_neighborhood_for gamma F -> strict_well_founded_neighborhood_for (fun l => bind (gamma l) (fun o => ret match o with
| Some _ => Some ()
| _ => None
end)) (fun f => bind (F f) (fun _ => ret ())).
Proof.
intros F gamma (Hstrict & Hgamma).
split.
2: apply well_founded_neighborhood_for_squash; eauto.
intros l.
eassert (ter (bind (gamma l) _) <-> ter (gamma l)) as ->
by (split; intros (? & ?); simpl_assms; eexists; psimpl).
etransitivity.
1:apply Hstrict.
split; intros (? & ? & ?); psimpl.
destruct x1; inversion H2; eauto.
Qed.
Definition termination_tree [A R : Type] (F : (nat -> part A) -> part R) (gamma : neighborhood_fun A R) :
strict_well_founded_neighborhood_for gamma F -> sigma1_tree A.
Proof.
intros Hgamma.
set (ptree_branch f := ter (F f)).
set (ptree_path l := ter (gamma l)).
apply mkSigma1Tree with (ptree_branch := ptree_branch) (ptree_path := ptree_path)
(F := fun f => bind (F f) (fun _ => ret ()))
(gamma := fun l => bind (gamma l) (fun o => ret match o with
| Some _ => Some ()
| _ => None
end)).
- now apply strict_well_founded_neighborhood_for_squash.
- unfold reflectspfn, ptree_branch.
intros f; split; intros (r & Hr); psimpl; eexists; psimpl.
- unfold reflectspfn, ptree_path.
intros f; split; intros (r & Hr); psimpl; eexists; psimpl.
Defined.
Definition brouwer_op_for [A R : Type] (gamma : neighborhood_fun A R) (F : (nat -> part A) -> part R) (Hgamma : strict_well_founded_neighborhood_for gamma F) :=
forall (Hnil : (termination_tree F gamma Hgamma).(ptree_path) nil), brouwer_op A R (termination_tree F gamma Hgamma) gamma nil Hnil.
Definition brouwer_operation_cont [A R : Type] (F : (nat -> part A) -> part R) :=
exists (gamma : neighborhood_fun A R)
(Hgamma : strict_well_founded_neighborhood_for gamma F), brouwer_op_for gamma F Hgamma.
Lemma brouwer_op_to_strict_well_founded_neighborhood [A R : Type] (F : (nat -> part A) -> part R) :
brouwer_operation_cont F -> strict_well_founded_neighborhood_cont F.
Proof.
intros (? & ? & ?); eexists; eauto.
Qed.
Lemma brouwer_op_to_neighborhood [A R : Type] (F : (nat -> part A) -> part R) :
brouwer_operation_cont F -> neighborhood_cont F.
Proof.
intros (? & (? & ? & ?) & ?); eexists; eauto.
Qed.
Definition neighborhood_canonical [A R : Type] (gamma : neighborhood_fun A R) : (nat -> part A) -> part R :=
fun f => mu_opt (fun n => bind (fold_part_list (tabulate f 0 n)) gamma).
Lemma neighborhood_canonical_correct [A R : Type] (gamma : neighborhood_fun A R) :
neighborhood_for gamma (neighborhood_canonical gamma).
Proof.
intros f r; eauto.
Qed.
Lemma permutes_quantifier_strict_well_founded_brouwer_operation [A R : Type] :
(forall (F : (nat -> part A) -> part R), strict_well_founded_neighborhood_cont F -> brouwer_operation_cont F) ->
forall (F : (nat -> part A) -> part R) (gamma : neighborhood_fun A R)
(Hgamma : strict_well_founded_neighborhood_for gamma F), brouwer_op_for gamma F Hgamma.
Proof.
intros Hcont F gamma (Hstrict & (Hwf1 & Hwf2) & Hgamma).
set (F' := neighborhood_canonical gamma).
assert (Hgamma' : strict_well_founded_neighborhood_for gamma F')
by repeat (eauto using neighborhood_canonical_correct; split).
specialize (Hcont F' ltac:(eexists; eauto)) as (xi & (Hstrict' & Hwf' & Hxi') & Hxi).
assert (Htrans : forall (r : R) (l : list A), xi l =! Some r -> exists (n : nat), gamma (rev (firstn n (rev l))) =! Some r). {
intros r l Hr.
clear Hxi.
set (f := nth_undef (rev l)).
assert (Hr' : F' f =! r). {
eapply Hxi', well_founded_neighborhood_hasvalue; eauto.
eapply bind_hasvalue_given; eauto.
eapply fold_tab_nth_undef.
rewrite firstn_all, rev_involutive.
eauto.
}
unfold F' in Hr'.
apply mu_opt_hasvalue in Hr' as (n & Hn & Hn').
exists n.
psimpl.
now apply fold_tab_nth_undef in H as (_ & ->).
}
assert (Htrans' : forall (l : list A), ter (gamma l) -> ter (xi l)). {
intros l (r & l' & Hr)%Hstrict.
set (f' := nth_undef (rev (l' ++ l))).
assert (F' f' =! r). {
destruct Hgamma' as (_ & Hgamma').
eapply Hgamma', well_founded_neighborhood_hasvalue; eauto.
1: split; eauto.
psimpl.
apply fold_tab_nth_undef.
rewrite firstn_all, rev_involutive.
eauto.
}
apply Hstrict'.
apply Hxi' in H as (m & Hm & Hm')%mu_opt_hasvalue.
psimpl.
apply fold_tab_nth_undef in H as (Hm & ->).
setoid_rewrite <- rev_firstn_rev with (n := m).
eexists r, _.
destruct Hwf'; eauto.
}
intros Hnil.
cbn in *.
specialize (Hxi (Htrans' _ Hnil)).
induction Hxi as [l Hl [(r & Hr) | (Hr & Hhered & Hind)]] using brouwer_op_ind'.
- apply Htrans in Hr as (n & Hr).
constructor; left; eauto.
exists r.
setoid_rewrite <- rev_firstn_rev.
eauto.
- destruct Hnil as ([|] & ?); constructor; [left | right; split ]; eauto.
intros a Hal.
apply Hind.
cbn in *.
eauto.
Qed.
Lemma all_strict_well_founded_neighborhood_are_brouwer_op_transfer [A R : Type] :
inhabited R ->
(forall (F : (nat -> part A) -> part R),
strict_well_founded_neighborhood_cont F -> brouwer_operation_cont F) ->
(forall (F : (nat -> part A) -> part unit),
strict_well_founded_neighborhood_cont F -> brouwer_operation_cont F).
Proof.
intros [r] HR F (gamma & Hstrict & Hwf & Hgamma).
set (F' := fun f => bind (F f) (fun _ => ret r)).
assert (HF' : strict_well_founded_neighborhood_cont F'). {
exists (fun l => bind (gamma l) (fun o => ret (match o with
| Some _ => Some r
| None => None
end))).
assert (Hter : forall l, ter (gamma l) <->
ter (bind (gamma l) (fun o => ret (match o with
| Some _ => Some r
| None => None
end))))
by (intros; split; intros (? & ?); simpl_assms; eexists; psimpl).
split.
1: {
intros l.
rewrite <- Hter.
eassert ((exists r' l',
bind (gamma (l' ++ l)) (fun o => ret match o with
| Some _ => Some r
| None => None
end) =! Some r') <-> exists r' l', gamma (l' ++ l) =! Some r'
)
as ->
by (split; intros (r' & l' & Hr'); psimpl;
destruct x; inversion H2; psimpl).
apply Hstrict.
}
eassert (Hwf_bis : well_founded_neighborhood _).
2: split; try eassumption.
1: {
destruct Hwf as (Hwf1 & Hwf2).
split.
- intros l l'.
do 2 rewrite <- Hter; eauto.
- intros r' l l'.
intros; simpl_assms.
destruct x; inversion H2; psimpl.
}
intros f r'.
unfold F'.
rewrite (Hgamma f).
split.
- intros (o & (n & Hn & Hn')%mu_opt_hasvalue & ?)%bind_hasvalue.
eapply well_founded_neighborhood_hasvalue; eauto.
psimpl.
- intros (n & Hn & Hn')%mu_opt_hasvalue.
simpl_assms.
destruct x0; inversion H3; subst.
rewrite bind_hasvalue_given with (a := u).
1:psimpl.
eapply well_founded_neighborhood_hasvalue; psimpl.
}
destruct (HR F' HF') as (xi' & Hxi' & Hbop').
set (xi := fun l => bind (xi' l) (fun o => ret (match o with
| Some _ => Some ()
| None => None
end))).
assert (Hxi : strict_well_founded_neighborhood_for xi F). {
destruct Hxi' as (Hstrict' & Hwf' & Hxi').
assert (Hter : forall l, ter (xi' l) <-> ter (xi l))
by (intros; unfold xi; split; intros (? & ?); simpl_assms; eexists; psimpl).
split.
1: {
intros l.
rewrite <- Hter.
eassert ((exists r' l', xi (l' ++ l) =! Some r')
<-> exists r' l', xi' (l' ++ l) =! Some r'
)
as ->
by (unfold xi; split; intros (r' & l' & Hr'); psimpl;
destruct x; inversion H2; psimpl).
eauto.
}
assert (Hwf_bis : well_founded_neighborhood xi). {
destruct Hwf' as (Hwf1' & Hwf2').
split.
- intros l l'.
do 2 rewrite <- Hter; eauto.
- intros () l l' Hl.
unfold xi in *.
simpl_assms.
destruct x; inversion H2.
psimpl.
}
split.
1: eauto.
intros f ().
split.
- intros Hr.
assert (F' f =! r) by (unfold F'; psimpl).
apply Hxi', mu_opt_hasvalue in H as (n & Hn & Hn').
eapply well_founded_neighborhood_hasvalue; eauto.
unfold xi.
psimpl.
- intros (n & Hn & Hn')%mu_opt_hasvalue.
assert (exists r', bind (fold_part_list (tabulate f 0 n)) xi' =! Some r')
as (? & ?). (unfold xi in *; simpl_assms; destruct x0; psimpl).
eapply well_founded_neighborhood_hasvalue, Hxi' in H; eauto.
unfold F' in *; psimpl.
destruct x0; eauto.
}
exists xi, Hxi.
assert (Htrans : forall l, ter (xi l) -> ter (xi' l))
by (intros l (? & ?); unfold xi in *; simpl_assms; eexists; psimpl).
intros Hnil.
specialize (Hbop' (Htrans _ Hnil)).
induction Hbop' as [l Hl [(r' & Hr') | (Hr & Hhered & Hind) ]] using brouwer_op_ind'.
- constructor.
left; exists (); unfold xi; psimpl.
- constructor.
right; split.
1: unfold xi; psimpl.
intros a Hal.
apply (Hind a (Htrans _ Hal) Hal).
Qed.
Definition pbarred [A : Type] (T : sigma1_tree A) (P : list A -> Prop) :=
forall (f : nat -> part A),
T.(ptree_branch) f -> exists (n : nat) (la : list A),
fold_part_list (tabulate f 0 n) =! la /\ P la.
Inductive hereditarily_pbarred [A : Type] (T : sigma1_tree A) (P : list A -> Prop) : forall (l : list A), T.(ptree_path) l -> Prop :=
| Hpbar : forall (l : list A) (Hl : T.(ptree_path) l),
P l \/ (~ P l /\ forall (a : A) (Hal : T.(ptree_path) (a :: l)), hereditarily_pbarred T P (a :: l) Hal)
-> hereditarily_pbarred T P l Hl.
Fixpoint hereditarily_pbarred_ind' [A : Type] (T : sigma1_tree A) (P : list A -> Prop) (Q : forall (l : list A), T.(ptree_path) l -> Prop) :
(forall (l : list A) (Hl : T.(ptree_path) l),
P l \/ (~ P l /\
(forall (a : A) (Hal : T.(ptree_path) (a :: l)), hereditarily_pbarred T P (a :: l) Hal) /\
(forall (a : A) (Hal : T.(ptree_path) (a :: l)), Q (a :: l) Hal)) -> Q l Hl) ->
forall (l : list A) (Hl : T.(ptree_path) l), hereditarily_pbarred T P l Hl -> Q l Hl.
Proof.
specialize (hereditarily_pbarred_ind' A T P Q).
intros Hind l Hl t.
destruct t as [l Hl [Ht | Ht]].
- apply Hind.
left.
auto.
- apply Hind.
right.
destruct Ht.
auto.
Qed.
Definition pBIT (A : Type) :=
forall (T : sigma1_tree A) (P : list A -> Prop),
(forall (l : list A), T.(ptree_path) l -> {P l} + {~P l}) ->
(forall (l l' : list A), P l -> P (l' ++ l)) ->
pbarred T P -> forall (Hnil : T.(ptree_path) nil), hereditarily_pbarred T P nil Hnil.
Definition bar_to_neighborhood_fun [A : Type] (T : sigma1_tree A) (P : list A -> Prop)
(Hdec : forall (l : list A), T.(ptree_path) l -> {P l} + {~P l}) :
neighborhood_fun A unit.
Proof.
refine (fun l => bind (proof_ter (T.(gamma) l))
(fun Hl => ret (if Hdec l _ then eval Hl else None))).
apply T.(Hptree_path).
destruct Hl as (? & ?); eexists; psimpl.
Defined.
Lemma bar_to_well_founded_neighborhood_fun [A : Type] (T : sigma1_tree A) (P : list A -> Prop)
(Hdec : forall (l : list A), T.(ptree_path) l -> {P l} + {~P l})
(Hmono : forall (l l' : list A), P l -> P (l' ++ l)) :
well_founded_neighborhood (bar_to_neighborhood_fun T P Hdec).
Proof.
destruct T.(Hgamma) as (? & (Hwf1 & Hwf2) & ?); eauto.
split.
- intros l l' (o & Ho).
unfold bar_to_neighborhood_fun in *.
simpl_assms.
eenough (ter (proof_ter (T.(gamma) l))) as (? & ?)
by (eexists; rewrite bind_hasvalue_given; psimpl).
apply proof_ter_spec; eauto.
- intros r l l' Hr.
unfold bar_to_neighborhood_fun in *.
simpl_assms.
destruct (Hdec _ _); inversion H4.
assert (ter (proof_ter (T.(gamma) (l' ++ l)))) as (? & ?). {
apply proof_ter_spec.
exists (Some r).
apply Hwf2.
rewrite <- H3; apply eval_hasvalue.
}
rewrite bind_hasvalue_given; eauto.
destruct (Hdec _ _) as [HP | HP]; eauto.
2: contradict HP; eauto.
enough (eval x0 = eval x) as -> by psimpl.
eapply hasvalue_det.
+ apply eval_hasvalue.
+ rewrite H3.
eapply Hwf2.
rewrite <- H3.
apply eval_hasvalue.
Qed.
Lemma bar_to_neighborhood [A : Type] (T : sigma1_tree A) (P : list A -> Prop)
(Hbar : pbarred T P) (Hdec : forall l, T.(ptree_path) l -> {P l} + {~P l})
(Hmono : forall l l', P l -> P (l' ++ l)) :
neighborhood_for (bar_to_neighborhood_fun T _ Hdec) T.(F).
Proof.
destruct T.(Hgamma) as (Hstrict & (Hwf1 & Hwf2) & Hgamma).
intros f ().
specialize (Hbar f).
split.
- intros (n & (l & Hl & Hr)%bind_hasvalue & Hn')%Hgamma%mu_opt_hasvalue.
assert (Hf : T.(ptree_branch) f). {
apply T.(Hptree_branch).
eexists.
eapply Hgamma, well_founded_neighborhood_hasvalue.
1:split; eauto.
psimpl.
}
specialize (Hbar Hf) as (n' & l' & Hl' & HPr).
destruct (Nat.le_ge_cases n n') as [Hnn' | Hnn'].
+ eapply well_founded_neighborhood_hasvalue.
1:eapply bar_to_well_founded_neighborhood_fun; eauto.
rewrite bind_hasvalue_given with (a := l'); eauto.
rewrite <- tabulate_add with (n := n), fold_part_list_app in Hl'; try lia.
rewrite bind_hasvalue_given in Hl'; eauto.
apply bind_hasvalue in Hl' as (l2 & ? & Hl'%ret_hasvalue_iff); subst.
assert (ter (proof_ter (T.(gamma) (l2 ++ l)))) as (? & ?). {
apply proof_ter_spec.
eexists.
eapply Hwf2.
eauto.
}
unfold bar_to_neighborhood_fun.
rewrite bind_hasvalue_given; eauto.
apply ret_hasvalue_iff.
destruct (Hdec (l2 ++ l)); try contradiction.
eapply hasvalue_det.
1: apply eval_hasvalue.
eauto.
+ eapply well_founded_neighborhood_hasvalue.
1:eapply bar_to_well_founded_neighborhood_fun; eauto.
rewrite bind_hasvalue_given with (a := l); eauto.
rewrite <- tabulate_add with (n := n'), fold_part_list_app in Hl; try lia.
rewrite bind_hasvalue_given in Hl; eauto.
apply bind_hasvalue in Hl as (l2 & ? & Hl%ret_hasvalue_iff); subst.
assert (ter (proof_ter (T.(gamma) (l2 ++ l')))) as (? & ?)
by (apply proof_ter_spec; eexists; eauto).
unfold bar_to_neighborhood_fun.
rewrite bind_hasvalue_given; eauto.
apply ret_hasvalue_iff.
apply Hmono with (l' := l2) in HPr.
destruct (Hdec (l2 ++ l')) as [_ | ?]; try contradiction.
eapply hasvalue_det; eauto.
apply eval_hasvalue.
- intros (n & (l & Hl & (Hter & Hter' & Hr%ret_hasvalue_iff)%bind_hasvalue)%bind_hasvalue & Hn')%mu_opt_hasvalue.
destruct (Hdec l) as [HPr | _]; try discriminate.
apply Hgamma.
eapply well_founded_neighborhood_hasvalue.
1: split; eauto.
psimpl.
rewrite <- Hr.
apply eval_hasvalue.
Qed.
Lemma monotone_bar_extend_true [A : Type] (T : sigma1_tree A) (P : list A -> Prop)
(Hbar : pbarred T P) (Hmono : forall l l', P l -> P (l' ++ l)) :
forall (l : list A), T.(ptree_path) l -> exists (l' : list A), P (l' ++ l).
Proof.
intros l Hl.
apply T.(Hptree_path) in Hl.
destruct Hl; psimpl.
assert (ter (T.(gamma) l)) by (eexists; eauto).
rename H0 into Hl.
clear x0 H H1.
destruct T.(Hgamma) as (Hstrict & Hwf & Hgamma).
apply Hstrict in Hl as (() & l' & Hl).
assert (Hl' : bind (fold_part_list (tabulate (nth_undef (rev (l' ++ l))) 0 (length (rev (l' ++ l))))) T.(gamma) =! Some ()). {
psimpl.
apply fold_tab_nth_undef.
rewrite firstn_all, rev_involutive; eauto.
}
apply well_founded_neighborhood_hasvalue, Hgamma in Hl'; eauto.
assert (Hl1' : T.(ptree_branch) (nth_undef (rev (l' ++ l)))). {
apply T.(Hptree_branch).
eexists; eauto.
}
specialize (Hbar (nth_undef (rev (l' ++ l))) Hl1') as (n & la & Hla' & Hla).
apply fold_tab_nth_undef in Hla' as (Hn & ->).
eapply Hmono in Hla.
rewrite rev_firstn_rev in Hla.
eauto.
Qed.
Lemma bar_to_strict_well_founded_neighborhood [A : Type] (T : sigma1_tree A) (P : list A -> Prop)
(Hbar : pbarred T P) (Hdec : forall l, T.(ptree_path) l -> {P l} + {~P l})
(Hmono : forall l l', P l -> P (l' ++ l)) :
strict_well_founded_neighborhood_for (bar_to_neighborhood_fun T _ Hdec) T.(F).
Proof.
split.
2: {
split.
- apply bar_to_well_founded_neighborhood_fun; eauto.
- apply bar_to_neighborhood; eauto.
}
intros l.
destruct T.(Hgamma) as (Hstrict & Hwf & Hgamma).
split.
- intros (o & Ho).
exists ().
destruct o as [()|].
1:exists nil; eauto.
unfold bar_to_neighborhood_fun in Ho.
simpl_assms.
clear H H2.
apply Hstrict in x as (() & l' & Hl').
assert (exists l'', P (l'' ++ l' ++ l)) as (l'' & Hl''). {
eapply monotone_bar_extend_true; eauto.
apply Hptree_path; eexists; psimpl.
}
exists (l'' ++ l').
rewrite <- app_assoc.
unfold bar_to_neighborhood_fun.
destruct Hwf as (_ & Hwf2).
apply Hwf2 with (l' := l'') in Hl'.
eassert (ter (proof_ter _)) as (? & ?) by (apply proof_ter_spec; eexists; eauto).
rewrite bind_hasvalue_given; eauto.
destruct (Hdec _ _); psimpl.
eapply ret_hasvalue_iff, hasvalue_det; eauto.
eapply eval_hasvalue.
- intros (() & l' & Hr).
unfold bar_to_neighborhood_fun in *.
simpl_assms; clear H2.
eenough (ter (proof_ter _)) as (? & ?)
by (eexists; rewrite bind_hasvalue_given; psimpl).
apply proof_ter_spec.
destruct Hwf; eauto.
Qed.
Lemma neighborhood_to_brouwer_op_pbit [A : Type] :
(forall (F : (nat -> part A) -> part unit) (gamma : neighborhood_fun A unit)
(Hgamma : strict_well_founded_neighborhood_for gamma F), brouwer_op_for gamma F Hgamma) ->
pBIT A.
Proof.
intros Hcont.
intros T P Hdec Hmono Hbar Hnil.
epose (gamma := bar_to_neighborhood_fun T _ Hdec).
assert (Hgamma : strict_well_founded_neighborhood_for gamma T.(F))
by (eapply bar_to_strict_well_founded_neighborhood; eauto).
assert (Hpath1 : forall l, T.(ptree_path) l -> (termination_tree T.(F) gamma Hgamma).(ptree_path) l). {
intros l Hl.
apply Hptree_path in Hl.
cbn.
destruct Hl.
psimpl.
unfold gamma, bar_to_neighborhood_fun.
eapply bind_ter'.
- apply proof_ter_spec.
eexists; eauto.
- intros ? ?.
eexists; psimpl.
}
specialize (Hcont T.(F) gamma Hgamma (Hpath1 _ Hnil)).
induction Hcont as [l Hl [(() & Hr)|(Hr & Hop & Hind)]] using brouwer_op_ind'; constructor.
- left.
unfold gamma, bar_to_neighborhood_fun in Hr.
psimpl.
destruct (Hdec l _); eauto.
discriminate.
- unfold gamma, bar_to_neighborhood_fun in Hr.
psimpl.
destruct (Hdec l _); eauto.
Qed.
Lemma pbit_neighborhood_to_brouwer_op [A R : Type] :
pBIT A -> (forall (gamma : neighborhood_fun A R) (F : (nat -> part A) -> part R)
(Hgamma : strict_well_founded_neighborhood_for gamma F), brouwer_op_for gamma F Hgamma).
Proof.
intros HBI.
intros gamma F Hgamma Hnil.
set (P l := exists (r : R), gamma l =! Some r).
assert (Hdec : forall l, (termination_tree F gamma Hgamma).(ptree_path) l -> {P l} + {~P l}). {
intros l Hl.
apply Hptree_path in Hl.
simpl in Hl.
assert (Hter : ter (gamma l)) by (destruct Hl; psimpl; eexists; psimpl).
destruct (eval Hter) as [o|] eqn:E.
- left.
eexists.
rewrite <- E.
apply eval_hasvalue.
- right.
intros Hc.
destruct Hc as (r & Hr).
enough (None = Some r) by discriminate.
eapply hasvalue_det; eauto.
rewrite <- E; apply eval_hasvalue.
}
assert (Hmono : forall l l', P l -> P (l' ++ l)). {
intros l l' (r & Hr).
exists r.
destruct Hgamma as (? & (? & Hwf2) & ?).
eauto.
}
assert (Hbar : pbarred (termination_tree F gamma Hgamma) P). {
intros f Hf.
apply Hptree_branch in Hf as (() & Hr).
simpl in Hr.
apply bind_hasvalue in Hr as (r & Hr & _).
destruct Hgamma as (? & (Hwf1 & Hwf2) & Hgamma).
apply Hgamma in Hr as (n & (l & Hl & Hr)%bind_hasvalue & Hn')%mu_opt_hasvalue.
exists n, l.
split; eauto.
eexists; eauto.
}
specialize (HBI (termination_tree F gamma Hgamma) P Hdec Hmono Hbar Hnil) as Hind.
induction Hind as [l Hl [HPr | (HPr & Hind & IHl)]] using hereditarily_pbarred_ind';
constructor; auto.
simpl in *.
destruct Hl as ([o|] & Hl); eauto.
Qed.
Theorem pbit_neighborhood_cont_to_brouwer_cont [A R : Type] :
enumerable (list A) -> inhabited R ->
pBIT A <-> forall (F : (nat -> part A) -> part R),
neighborhood_cont F -> brouwer_operation_cont F.
Proof.
intros HLA HR.
split.
- intros HA F HF.
apply enumerable_to_strictify_neighborhood_cont in HF as (gamma & Hgamma); auto.
exists gamma, Hgamma.
apply pbit_neighborhood_to_brouwer_op; auto.
- intros Hcont.
apply neighborhood_to_brouwer_op_pbit.
intros F gamma Hgamma.
apply permutes_quantifier_strict_well_founded_brouwer_operation.
eapply all_strict_well_founded_neighborhood_are_brouwer_op_transfer; eauto.
clear F gamma Hgamma.
intros F (gamma & Hstrict & Hwf & Hgamma).
apply Hcont.
eexists; eauto.
Qed.
Theorem pbit_neighborhood_cont_to_brouwer_cont_nat :
pBIT nat <-> forall (F : (nat -> part nat) -> part nat),
neighborhood_cont F -> brouwer_operation_cont F.
Proof.
apply pbit_neighborhood_cont_to_brouwer_cont.
2: repeat constructor.
apply enumerable_list.
exists id.
intros; eauto.
Qed.
End PartialZoo.