From SyntheticComputability Require Import TuringReducibility.OracleComputability.
From SyntheticComputability Require Import partial Definitions reductions Dec DecidabilityFacts.
Require Import Lia List.
From stdpp Require Import list.
Import PartialTactics.
Lemma seval_hasvalue' {partiality : partial.partiality} [A : Type] (x : part A) (a : A) n :
seval x n = Some a -> x =! a.
Proof.
intros. eapply seval_hasvalue. eauto.
Qed.
Section PT.
Context {Part : partiality} {X : Type} {Y : Type}.
Variable q : Y → Prop.
Variable p : X → Prop.
Variable F1 : Functional Y bool X ().
Variable tau1 : X → (list bool) ↛ (Y + unit).
Variable HF1 : ∀ (R : Rel Y bool) (x : X) (o : ()), F1 R x o ↔ (∃ (qs : list Y) (ans : list bool), interrogation (tau1 x) R qs ans ∧ tau1 x ans =! inr o).
Variable H1 : ∀ x : X, p x ↔ F1 (char_rel q) x ().
Variable F2 : Functional Y bool X ().
Variable tau2 : X → (list bool) ↛ (Y + unit).
Variable HF2 : ∀ (R : Rel Y bool) (x : X) (o : ()), F2 R x o ↔ (∃ (qs : list Y) (ans : list bool), interrogation (tau2 x) R qs ans ∧ tau2 x ans =! inr o).
Variable H2 : ∀ x : X, ¬ p x ↔ F2 (char_rel q) x ().
Definition get_ans B (tqs : list (bool * Y)) (ans : list bool) := (map snd (filter (fun '((b, q), a) => b = B) (zip_with pair tqs ans))).
Definition get_ans1 := get_ans true.
Definition get_ans2 := get_ans false.
Definition get_qs B (tqs : list (bool * Y)) := (map snd (filter (fun '((b, q)) => b = B) tqs)).
Definition get_qs1 := get_qs true.
Definition get_qs2 := get_qs false.
Lemma get_ans_app B t1 t2 a1 a2 :
length t1 = length a1 ->
get_ans B (t1 ++ t2) (a1 ++ a2) = get_ans B t1 a1 ++ get_ans B t2 a2.
Proof.
intros Hlen.
induction t1 in a1, Hlen |- *; destruct a1; cbn in *; try lia.
- reflexivity.
- destruct a. destruct decide.
+ cbn. f_equal. eapply IHt1. lia.
+ eapply IHt1. lia.
Qed.
Lemma get_qs_app B t1 t2 :
get_qs B (t1 ++ t2) = get_qs B t1 ++ get_qs B t2.
Proof.
induction t1.
- reflexivity.
- cbn. destruct a. destruct decide.
+ cbn. f_equal. eapply IHt1.
+ eapply IHt1.
Qed.
Definition τ := fun x '(old, n, tqs) ans =>
match old with Some q => ret (inl (None, n, tqs ++ [(false, q)], Some q))
| None =>
match seval (tau1 x (get_ans1 tqs ans)) n, seval (tau2 x (get_ans2 tqs ans)) n with
| Some (inr o), _ => ret (inr true)
| _ , Some (inr o) => ret (inr false)
| Some (inl q), Some (inl q') => ret (inl (Some q' , S n, tqs ++ [(true, q)], Some q))
| Some (inl q), _ => ret (inl (None, S n, tqs ++ [(true, q)], Some q))
| _, Some (inl q) => ret (inl (None, S n, tqs ++ [(false, q)], Some q))
| _, _ => ret (inl (None, S n, tqs, None))
end end.
Definition qs_from_tqs (tqs : list (bool * Y)) := map snd tqs.
Definition subtree (tau : list bool ↛ (Y + ())) ans l := tau (ans ++ l).
Definition subtree' {E Q A O} (tau : stree E Q A O) ans e l := tau e (ans ++ l).
Variable q_dec : forall y, q y \/ ~ q y.
Lemma q_reflect y : exists b, char_rel q y b.
Proof.
destruct (q_dec y).
exists true; eauto.
exists false; eauto.
Qed.
Variable Y_dec : eq_dec Y.
Lemma count_up_1 m tqs x ans v :
p x ->
length tqs = length ans ->
interrogation (tau2 x) (char_rel q) (get_qs2 tqs) (get_ans2 tqs ans) ->
tau1 x (get_ans1 tqs ans) =! v ->
exists tqs' ans' n',
seval (tau1 x (get_ans1 tqs ans)) n' = Some v /\
sinterrogation (subtree' (τ x) ans) (char_rel q) tqs' ans' (None,m, tqs) (None, n', tqs ++ map (pair false) tqs') /\
interrogation (subtree (tau2 x) (get_ans2 tqs ans)) (char_rel q) tqs' ans'.
Proof.
intros Hx Hlen Hi2 Hend.
eapply seval_hasvalue in Hend as [n Hend].
edestruct Wf_nat.dec_inh_nat_subset_has_unique_least_element with (P := fun n => seval (tau1 x (get_ans1 tqs ans)) n = Some v).
{ intros. clear - Y_dec. destruct seval as [ [? | []] | ]; try now clear; firstorder congruence.
all: destruct v as [ | []]; try now clear; firstorder congruence.
destruct (Y_dec y y0); try firstorder congruence.
}
{ eauto. }
clear n Hend. rename x0 into n. destruct H as [ [] ]. rename H into Hend.
clear H3.
assert (Hleast : ∀ x' : nat, x' < n -> seval (tau1 x (get_ans1 tqs ans)) x' = None).
{
intros x' Hl. destruct (seval (tau1 x (get_ans1 tqs ans)) x') as [ [ | []] | ] eqn:E.
- assert (v = inl y) as ->. { eapply hasvalue_det; eapply seval_hasvalue'; eauto. }
eapply H0 in E. lia.
- assert (v = inr ()) as ->. { eapply hasvalue_det; eapply seval_hasvalue'; eauto. }
eapply H0 in E. lia.
- reflexivity.
}
clear H0.
destruct (Nat.le_dec m n).
- revert Hi2 Hend Hlen Hleast. revert ans tqs. pattern m, n. revert m l.
eapply Nat.left_induction.
+ exact _.
+ intros. exists [], [], n. repeat eapply conj.
* eauto.
* cbn. rewrite app_nil_r. econstructor.
* econstructor.
+ intros m Hlt IH ? ? ? ? ? ?.
destruct (seval (tau2 x (get_ans2 tqs ans)) m) as [ [ | []] | ] eqn:E.
* destruct (q_reflect y) as [b Hb].
specialize (IH (ans ++ [b]) (tqs ++ [(false, y)])).
edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3).
{
unfold get_qs2. rewrite !get_qs_app.
unfold get_ans2. rewrite !get_ans_app; eauto.
cbn. destruct decide; try congruence.
cbn. econstructor. eauto. 2: eapply Hb.
eapply seval_hasvalue'; eassumption.
}
{
unfold get_ans1. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn. rewrite app_nil_r.
all: eauto.
}
{ rewrite !app_length. cbn. lia. }
{
unfold get_ans1. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn. rewrite app_nil_r.
all: eauto.
}
exists (y :: tqs'), (b :: ans'), n'. repeat eapply conj.
-- unfold get_ans1 in IH1.
rewrite get_ans_app in IH1. 2: eauto.
cbn in IH1. destruct decide; try congruence.
cbn in *. rewrite app_nil_r in IH1. eauto.
-- eapply sinterrogation_cons.
2: eauto. cbn.
rewrite app_nil_r.
assert (seval (tau1 x (get_ans1 tqs ans)) m = None) as ->.
{ eapply Hleast. lia. }
rewrite E. psimpl.
cbn. unfold subtree in *.
rewrite <- !app_assoc in IH2. cbn in *.
eapply sinterrogation_ext. 2: eassumption.
intros. unfold subtree'. cbn. now rewrite <- app_assoc.
-- eapply interrogation_cons. eapply seval_hasvalue'; eauto.
unfold subtree. rewrite app_nil_r. eassumption. eauto.
eapply interrogation_ext. 3: eauto. 2: reflexivity.
intros. unfold subtree.
unfold get_ans2. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn. now rewrite <- app_assoc.
eauto.
* edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3); eauto.
assert (~ p x). {
eapply H2.
eapply HF2. repeat eexists. 2: eapply seval_hasvalue'; eauto.
eauto.
}
tauto.
* specialize (IH ans tqs).
edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3); eauto.
exists tqs', ans', n'. repeat eapply conj.
-- eauto.
-- eapply sinterrogation_scons.
2: eauto. cbn.
rewrite app_nil_r.
assert (seval (tau1 x (get_ans1 tqs ans)) m = None) as ->.
{ eapply Hleast. lia. }
rewrite E. psimpl.
-- eauto.
- exists [], [], m. repeat eapply conj.
+ eapply seval_mono; eauto. lia.
+ cbn. rewrite app_nil_r. econstructor.
+ cbn. econstructor.
Qed.
Lemma count_up_2 m tqs x ans v :
~ p x ->
length tqs = length ans ->
interrogation (tau1 x) (char_rel q) (get_qs1 tqs) (get_ans1 tqs ans) ->
tau2 x (get_ans2 tqs ans) =! v ->
exists tqs' ans' n',
seval (tau2 x (get_ans2 tqs ans)) n' = Some v /\
sinterrogation (subtree' (τ x) ans) (char_rel q) tqs' ans' (None,m, tqs) (None, n', tqs ++ map (pair true) tqs') /\
interrogation (subtree (tau1 x) (get_ans1 tqs ans)) (char_rel q) tqs' ans'.
Proof.
intros Hx Hlen Hi2 [n Hend] % seval_hasvalue.
edestruct Wf_nat.dec_inh_nat_subset_has_unique_least_element with (P := fun n => seval (tau2 x (get_ans2 tqs ans)) n = Some v).
{ intros. clear - Y_dec. destruct seval as [ [? | []] | ]; try now clear; firstorder congruence.
all: destruct v as [ | []]; try now clear; firstorder congruence.
destruct (Y_dec y y0); try firstorder congruence.
}
{ eauto. }
clear n Hend. rename x0 into n. destruct H as [ [] ]. rename H into Hend.
clear H3.
assert (Hleast : ∀ x' : nat, x' < n -> seval (tau2 x (get_ans2 tqs ans)) x' = None).
{
intros x' Hl. destruct (seval (tau2 x (get_ans2 tqs ans)) x') as [ [ | []] | ] eqn:E.
- assert (v = inl y) as ->. { eapply hasvalue_det; eapply seval_hasvalue'; eauto. }
eapply H0 in E. lia.
- assert (v = inr ()) as ->. { eapply hasvalue_det; eapply seval_hasvalue'; eauto. }
eapply H0 in E. lia.
- reflexivity.
}
clear H0.
destruct (Nat.le_dec m n).
- revert Hi2 Hend Hlen Hleast. revert ans tqs. pattern m, n. revert m l.
eapply Nat.left_induction.
+ exact _.
+ intros. exists [], [], n. repeat eapply conj.
* eauto.
* cbn. rewrite app_nil_r. econstructor.
* econstructor.
+ intros m Hlt IH ? ? ? ? ? ?.
destruct (seval (tau1 x (get_ans1 tqs ans)) m) as [ [ | []] | ] eqn:E.
* destruct (q_reflect y) as [b Hb].
specialize (IH (ans ++ [b]) (tqs ++ [(true, y)])).
edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3).
{
unfold get_qs1. rewrite !get_qs_app.
unfold get_ans1. rewrite !get_ans_app; eauto.
cbn. destruct decide; try congruence.
cbn. econstructor. eauto.
eapply seval_hasvalue'; eauto.
eauto.
}
{
unfold get_ans2. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn.
rewrite app_nil_r; eassumption.
all: eauto.
}
{ rewrite !app_length. cbn. lia. }
{
unfold get_ans2. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn. rewrite app_nil_r.
all: eauto.
}
exists (y :: tqs'), (b :: ans'), n'. repeat eapply conj.
-- unfold get_ans2 in IH1.
rewrite get_ans_app in IH1. 2: eauto.
cbn in IH1. destruct decide; try congruence.
cbn in *. rewrite app_nil_r in IH1. eauto.
-- eapply sinterrogation_cons.
2: eauto. cbn.
rewrite app_nil_r.
rewrite E.
rewrite Hleast. 2: lia.
psimpl.
cbn. unfold subtree in *.
rewrite <- !app_assoc in IH2. cbn in *.
eapply sinterrogation_ext. 2: eassumption.
intros. unfold subtree'. cbn. now rewrite <- app_assoc.
-- eapply interrogation_cons. eapply seval_hasvalue'; eauto.
unfold subtree. rewrite app_nil_r. eassumption. eauto.
eapply interrogation_ext. 3: eauto. 2: reflexivity.
intros. unfold subtree.
unfold get_ans1. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn. now rewrite <- app_assoc.
eauto.
* edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3); eauto.
assert (p x). {
eapply H1, HF1. repeat eexists. 2: eapply seval_hasvalue'; eauto.
eauto.
}
tauto.
* specialize (IH ans tqs).
edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3); eauto.
exists tqs', ans', n'. repeat eapply conj.
-- eauto.
-- eapply sinterrogation_scons.
2: eauto. cbn.
rewrite app_nil_r.
rewrite E.
rewrite Hleast. 2: lia. psimpl.
-- eauto.
- exists [], [], m. repeat eapply conj.
+ eapply seval_mono; eauto. lia.
+ cbn. rewrite app_nil_r. econstructor.
+ cbn. econstructor.
Qed.
Lemma back:
∀ (x : X) (qs : list Y) (ans : list bool) (n : nat) (tqs : list (bool * Y)) o,
sinterrogation (τ x) (char_rel q) qs ans (None, 0, []) (o, n, tqs)
→ qs = map snd tqs
/\ length ans = length tqs
/\ match o with Some q => tau2 x (get_ans2 tqs ans) =! inl q | None => True end
∧ interrogation (tau1 x) (λ (x0 : Y) (b : bool), if b then q x0 else ¬ q x0) (get_qs1 tqs) (get_ans1 tqs ans)
∧ interrogation (tau2 x) (λ (x0 : Y) (b : bool), if b then q x0 else ¬ q x0) (get_qs2 tqs) (get_ans2 tqs ans).
Proof.
intros x qs ans n tqs o Hint.
remember (None, 0, []) as begin.
remember (o, n, tqs) as theend.
induction Hint in Heqbegin, Heqtheend, tqs, n, o |- *.
- subst. inversion Heqtheend; subst. cbn. repeat eapply conj; econstructor.
- subst. destruct e1' as [[o' n'] tqs'].
cbn in H. destruct o'; cbn in *; psimpl.
edestruct IHHint as (-> & Hlen & IH3 & IH1 & IH2); try reflexivity.
destruct seval as [ [? | []] | ] eqn:E1.
+ destruct (seval (tau2 x (get_ans2 tqs' ans)) n') as [ [? | []] | ] eqn:E2; psimpl.
+ psimpl.
+ destruct (seval (tau2 x (get_ans2 tqs' ans)) n') as [ [? | []] | ] eqn:E2; psimpl.
- subst. destruct e1' as [[o' n'] tqs'].
edestruct IHHint as (-> & Hlen & IH3 & IH1 & IH2); try reflexivity.
cbn in H. destruct o'; psimpl.
{
assert ((get_qs2 (tqs' ++ [(false, q0)])) = get_qs2 tqs' ++ [q0]) as Eqn1.
{ unfold get_qs2. rewrite get_qs_app. cbn. destruct decide; try congruence. reflexivity. }
assert ((get_qs1 (tqs' ++ [(false, q0)])) = get_qs1 tqs') as Eqn2.
{ unfold get_qs1. rewrite get_qs_app. cbn. destruct decide; try congruence. cbn. now rewrite app_nil_r. }
assert ((get_ans2 (tqs' ++ [(false, q0)]) (ans ++ [a])) = get_ans2 tqs' ans ++ [a]) as Eqn1'.
{ unfold get_ans2. rewrite get_ans_app. 2: lia.
cbn. now destruct decide; try congruence; cbn.
}
assert ((get_ans1 (tqs' ++ [(false, q0)]) (ans ++ [a])) = get_ans1 tqs' ans) as Eqn2'.
{ unfold get_ans1. rewrite get_ans_app. 2: lia.
cbn. destruct decide; try congruence; cbn. now rewrite app_nil_r.
}
repeat eapply conj.
+ now rewrite map_app; cbn.
+ rewrite !app_length; cbn. lia.
+ eauto.
+ rewrite Eqn2, Eqn2'. eauto.
+ rewrite Eqn1, Eqn1'. econstructor. eauto. 2: eapply H0.
eauto.
}
destruct seval as [ [? | []] | ] eqn:E1.
+ assert ((get_qs1 (tqs' ++ [(true, q0)])) = get_qs1 tqs' ++ [q0]) as Eqn1.
{ unfold get_qs1. rewrite get_qs_app. cbn. destruct decide; try congruence. reflexivity. }
assert ((get_qs2 (tqs' ++ [(true, q0)])) = get_qs2 tqs') as Eqn2.
{ unfold get_qs2. rewrite get_qs_app. cbn. destruct decide; try congruence. cbn. now rewrite app_nil_r. }
assert ((get_ans1 (tqs' ++ [(true, q0)]) (ans ++ [a])) = get_ans1 tqs' ans ++ [a]) as Eqn1'.
{ unfold get_ans1. rewrite get_ans_app. 2: lia.
cbn. now destruct decide; try congruence; cbn.
}
assert ((get_ans2 (tqs' ++ [(true, q0)]) (ans ++ [a])) = get_ans2 tqs' ans) as Eqn2'.
{ unfold get_ans2. rewrite get_ans_app. 2: lia.
cbn. destruct decide; try congruence; cbn. now rewrite app_nil_r.
}
destruct (seval (tau2 x (get_ans2 tqs' ans)) n') as [ [? | []] | ] eqn:E2; psimpl.
* repeat eapply conj.
-- now rewrite map_app.
-- rewrite !app_length; cbn. lia.
-- rewrite Eqn2'. eapply seval_hasvalue'; eauto.
-- rewrite Eqn1, Eqn1'. econstructor. eauto. 2: eapply H0.
eapply seval_hasvalue'; eauto.
-- rewrite Eqn2, Eqn2'. eauto.
* repeat eapply conj.
-- now rewrite map_app.
-- rewrite !app_length; cbn. lia.
-- eauto.
-- rewrite Eqn1, Eqn1'. econstructor. eauto. 2: eapply H0.
eapply seval_hasvalue'; eauto.
-- rewrite Eqn2, Eqn2'. eauto.
+ psimpl.
+ destruct (seval (tau2 x (get_ans2 tqs' ans)) n') as [ [? | []] | ] eqn:E2; psimpl.
assert ((get_qs2 (tqs' ++ [(false, q0)])) = get_qs2 tqs' ++ [q0]) as Eqn1.
{ unfold get_qs2. rewrite get_qs_app. cbn. destruct decide; try congruence. reflexivity. }
assert ((get_qs1 (tqs' ++ [(false, q0)])) = get_qs1 tqs') as Eqn2.
{ unfold get_qs1. rewrite get_qs_app. cbn. destruct decide; try congruence. cbn. now rewrite app_nil_r. }
assert ((get_ans2 (tqs' ++ [(false, q0)]) (ans ++ [a])) = get_ans2 tqs' ans ++ [a]) as Eqn1'.
{ unfold get_ans2. rewrite get_ans_app. 2: lia.
cbn. now destruct decide; try congruence; cbn.
}
assert ((get_ans1 (tqs' ++ [(false, q0)]) (ans ++ [a])) = get_ans1 tqs' ans) as Eqn2'.
{ unfold get_ans1. rewrite get_ans_app. 2: lia.
cbn. destruct decide; try congruence; cbn. now rewrite app_nil_r.
}
repeat eapply conj.
-- now rewrite map_app.
-- rewrite !app_length; cbn. lia.
-- eauto.
-- rewrite Eqn2, Eqn2'. eauto.
-- rewrite Eqn1, Eqn1'. econstructor. eauto. 2: eapply H0.
eapply seval_hasvalue'; eauto.
Qed.
Lemma get_ans_map_no b tqs ans :
get_ans b (map (pair (negb b)) tqs) ans = [].
Proof.
induction tqs in ans |- *; cbn. 1: reflexivity.
destruct ans; try reflexivity. cbn.
destruct decide. { destruct b; cbn in*; congruence. }
eauto.
Qed.
Lemma get_qs_map_no b tqs :
get_qs b (map (pair (negb b)) tqs) = [].
Proof.
induction tqs; cbn. 1: reflexivity.
destruct decide. { destruct b; cbn in*; congruence. }
eauto.
Qed.
Lemma get_qs_map_yes b tqs :
get_qs b (map (pair (b)) tqs) = tqs.
Proof.
induction tqs; cbn. 1: reflexivity.
destruct decide; try congruence. cbn. f_equal. eauto.
Qed.
Lemma get_ans_map_yes b tqs ans :
length tqs = length ans ->
get_ans b (map (pair b) tqs) ans = ans.
Proof.
induction tqs in ans |- *; cbn.
all: destruct ans; cbn in *; try lia.
1: reflexivity. intros.
destruct decide; try congruence.
cbn. f_equal.
eauto.
Qed.
Lemma main :
∀ (x : X) (b : bool), char_rel p x b ↔ (∃ (qs : list Y) (ans : list bool) e, sinterrogation (τ x) (char_rel q) qs ans (None, 0, nil) e ∧ τ x e ans =! inr b).
Proof.
intros. split. destruct b; cbn.
- intros Hx.
eapply H1 in Hx as Hx'. eapply HF1 in Hx' as (qs & ans & Hint & Hend).
enough (∃ (ans0 : list bool) m (qs0 : list (bool * Y)),
qs = get_qs1 qs0 /\
ans = get_ans1 qs0 ans0 /\
interrogation (tau2 x) (char_rel q) (get_qs2 qs0) (get_ans2 qs0 ans0) /\
sinterrogation (τ x) (char_rel q) (map snd qs0) ans0 (None, 0, []) (None, m, qs0)).
{ cbn in *. decompose [ex and] H. subst.
eapply count_up_1 in Hend as lem; eauto.
2:{ eapply sinterrogation_length in H6. rewrite map_length in H6. lia. }
destruct lem as (tqs' & ans' & n' & Hn' & IH1 & IH2).
eexists (_ ++ tqs').
eexists (_ ++ ans').
eexists (None, n', _ ++ map (pair false) tqs').
split.
eapply sinterrogation_app.
eauto. eassumption.
cbn.
unfold get_ans1. rewrite get_ans_app.
rewrite get_ans_map_no. rewrite app_nil_r.
unfold get_ans1 in *.
rewrite Hn'. psimpl.
eapply sinterrogation_length in H6.
rewrite map_length in H6. lia.
}
clear Hend. induction Hint.
+ exists []. exists 0. exists []. repeat econstructor.
+ cbn in IHHint. destruct IHHint as (ans_ & m & qs_ & -> & -> & IH1 & IH2).
eapply count_up_1 in H as lem; eauto.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. lia. }
destruct lem as (tqs' & ans' & n' & Hn' & HH1 & HH2).
rename q0 into y.
destruct (seval (tau2 x (get_ans false qs_ ans_ ++ ans')) n') as [ [ | []] | ] eqn:E2.
{
destruct (q_reflect y0) as [b Hb].
eexists (ans_ ++ ans' ++ [a;b] ).
exists (S n').
eexists (qs_ ++ map (pair false) tqs' ++ [(true, y); (false, y0)] ).
cbn. repeat eapply conj.
* unfold get_qs1. rewrite !get_qs_app.
cbn. destruct decide; try congruence.
now rewrite get_qs_map_no.
* unfold get_ans1. rewrite !get_ans_app.
2:{ rewrite map_length. eapply interrogation_length; eauto. }
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
cbn. destruct decide; try congruence.
now rewrite get_ans_map_no.
* unfold get_qs2, get_ans2.
rewrite !get_qs_app.
rewrite !get_ans_app.
rewrite get_qs_map_yes, get_ans_map_yes.
eapply interrogation_app; eauto.
eapply interrogation_app; eauto.
cbn. destruct decide; try congruence. destruct decide; try congruence. cbn.
eapply Interrogate with (qs := []) (ans := []); eauto. econstructor.
rewrite app_nil_r. eapply seval_hasvalue'; eauto.
eapply interrogation_length; eauto.
rewrite map_length. eapply interrogation_length; eauto.
eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto.
* rewrite !map_app. eapply sinterrogation_app.
eauto.
eapply sinterrogation_app.
rewrite map_map, map_id.
eauto.
cbn.
eapply sinterrogation_cons.
rewrite app_nil_r. cbn.
unfold get_ans1 in *. rewrite !get_ans_app.
rewrite get_ans_map_no. rewrite app_nil_r.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite Hn'.
unfold get_ans2. rewrite get_ans_app.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite get_ans_map_yes. 2: eapply interrogation_length; eauto.
rewrite E2. rewrite <- app_assoc. psimpl.
eapply H0.
eapply sinterrogation_cons.
cbn. psimpl. eapply Hb.
rewrite <- !app_assoc. cbn. econstructor.
}
{
enough (~ p x) by tauto.
eapply H2, HF2. repeat eexists.
2: eapply seval_hasvalue'; eauto.
eapply interrogation_app; eauto.
}
eexists (ans_ ++ ans' ++ [a] ).
exists (S n').
eexists (qs_ ++ map (pair false) tqs' ++ [(true, y)]).
cbn. repeat eapply conj.
* unfold get_qs1. rewrite !get_qs_app.
cbn. destruct decide; try congruence.
now rewrite get_qs_map_no.
* unfold get_ans1. rewrite !get_ans_app.
2:{ rewrite map_length. eapply interrogation_length; eauto. }
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
cbn. destruct decide; try congruence.
now rewrite get_ans_map_no.
* unfold get_qs2, get_ans2.
rewrite !get_qs_app.
rewrite !get_ans_app.
rewrite get_qs_map_yes, get_ans_map_yes.
eapply interrogation_app; eauto.
eapply interrogation_app; eauto.
cbn. destruct decide; try congruence. econstructor.
eapply interrogation_length; eauto.
rewrite map_length. eapply interrogation_length; eauto.
eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto.
* rewrite !map_app. eapply sinterrogation_app.
eauto.
eapply sinterrogation_app.
rewrite map_map, map_id.
eauto.
cbn.
eapply sinterrogate with (qs := []) (ans := []).
econstructor. 2: eapply H0.
cbn.
rewrite app_nil_r.
unfold get_ans1 in *. rewrite !get_ans_app.
rewrite get_ans_map_no. rewrite app_nil_r.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite Hn'.
unfold get_ans2. rewrite get_ans_app.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite get_ans_map_yes. 2: eapply interrogation_length; eauto.
rewrite E2. rewrite <- app_assoc. psimpl.
- intros Hx.
eapply H2 in Hx as Hx'. eapply HF2 in Hx' as (qs & ans & Hint & Hend).
enough (∃ (ans0 : list bool) m (qs0 : list (bool * Y)),
qs = get_qs2 qs0 /\
ans = get_ans2 qs0 ans0 /\
interrogation (tau1 x) (char_rel q) (get_qs1 qs0) (get_ans1 qs0 ans0) /\
sinterrogation (τ x) (char_rel q) (map snd qs0) ans0 (None, 0, []) (None, m, qs0)).
{ cbn in *. decompose [ex and] H. subst.
eapply count_up_2 in Hend as lem; eauto.
2:{ eapply sinterrogation_length in H6. rewrite map_length in H6. lia. }
destruct lem as (tqs' & ans' & n' & Hn' & IH1 & IH2).
eexists (_ ++ tqs').
eexists (_ ++ ans').
eexists (None, n', _ ++ map (pair true) tqs').
split.
eapply sinterrogation_app.
eauto. eassumption.
cbn.
unfold get_ans2. rewrite get_ans_app.
rewrite get_ans_map_no. rewrite app_nil_r.
unfold get_ans2 in *.
rewrite Hn'.
destruct (seval (tau1 x (get_ans1 (x2 ++ map (pair true) tqs') (x0 ++ ans'))) n') as [ [ | []] | ] eqn:EE; psimpl.
2:{ eapply sinterrogation_length in H6.
rewrite map_length in H6. lia. }
enough (p x) by tauto.
eapply H1, HF1. repeat eexists. 2: eapply seval_hasvalue'; eauto.
unfold get_ans1. rewrite get_ans_app.
2:{ eapply sinterrogation_length in H6.
rewrite map_length in H6. lia. }
eapply interrogation_app; eauto.
rewrite get_ans_map_yes.
2: eapply interrogation_length; eauto.
eauto.
}
clear Hend. induction Hint.
+ exists []. exists 0. exists []. repeat econstructor.
+ cbn in IHHint. destruct IHHint as (ans_ & m & qs_ & -> & -> & IH1 & IH2).
eapply count_up_2 in H as lem; eauto.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. lia. }
destruct lem as (tqs' & ans' & n' & Hn' & HH1 & HH2).
rename q0 into y.
destruct (seval (tau1 x (get_ans1 qs_ ans_ ++ ans')) n') as [ [ | []] | ] eqn:E2.
{
destruct (q_reflect y0) as [b Hb].
eexists (ans_ ++ ans' ++ [b;a] ).
exists (S n').
eexists (qs_ ++ map (pair true) tqs' ++ [(true, y0); (false, y)] ).
cbn. repeat eapply conj.
* unfold get_qs2. rewrite !get_qs_app.
cbn. destruct decide; try congruence.
destruct decide; try congruence.
now rewrite get_qs_map_no.
* unfold get_ans2. rewrite !get_ans_app.
2:{ rewrite map_length. eapply interrogation_length; eauto. }
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
cbn. destruct decide; try congruence.
destruct decide; try congruence.
now rewrite get_ans_map_no.
* unfold get_qs1, get_ans1.
rewrite !get_qs_app.
rewrite !get_ans_app.
rewrite get_qs_map_yes, get_ans_map_yes.
eapply interrogation_app; eauto.
eapply interrogation_app; eauto.
cbn. destruct decide; try congruence. destruct decide; try congruence. cbn.
eapply Interrogate with (qs := []) (ans := []); eauto. econstructor.
rewrite app_nil_r. eapply seval_hasvalue'; eauto.
eapply interrogation_length; eauto.
rewrite map_length. eapply interrogation_length; eauto.
eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto.
* rewrite !map_app. eapply sinterrogation_app.
eauto.
eapply sinterrogation_app.
rewrite map_map, map_id.
eauto.
cbn.
eapply sinterrogation_cons.
rewrite app_nil_r. cbn.
unfold get_ans1 in *. rewrite !get_ans_app.
rewrite get_ans_map_yes. rewrite E2.
2:{ eapply sinterrogation_length in HH1. eauto. }
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
2: eapply Hb.
unfold get_ans2. rewrite get_ans_app.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite get_ans_map_no. rewrite app_nil_r.
unfold get_ans2 in *.
rewrite Hn'. psimpl.
eapply sinterrogation_cons.
cbn. psimpl. eapply H0.
rewrite <- !app_assoc. cbn. econstructor.
}
{
enough (p x) by tauto.
eapply H1, HF1. repeat eexists.
2: eapply seval_hasvalue'; eauto.
eapply interrogation_app; eauto.
}
eexists (ans_ ++ ans' ++ [a] ).
exists (S n').
eexists (qs_ ++ map (pair true) tqs' ++ [(false, y)]).
cbn. repeat eapply conj.
* unfold get_qs2. rewrite !get_qs_app.
cbn. destruct decide; try congruence.
now rewrite get_qs_map_no.
* unfold get_ans2. rewrite !get_ans_app.
2:{ rewrite map_length. eapply interrogation_length; eauto. }
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
cbn. destruct decide; try congruence.
now rewrite get_ans_map_no.
* unfold get_qs1, get_ans1.
rewrite !get_qs_app.
rewrite !get_ans_app.
rewrite get_qs_map_yes, get_ans_map_yes.
eapply interrogation_app; eauto.
eapply interrogation_app; eauto.
cbn. destruct decide; try congruence. econstructor.
eapply interrogation_length; eauto.
rewrite map_length. eapply interrogation_length; eauto.
eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto.
* rewrite !map_app. eapply sinterrogation_app.
eauto.
eapply sinterrogation_app.
rewrite map_map, map_id.
eauto.
cbn.
eapply sinterrogate with (qs := []) (ans := []).
econstructor. 2: eapply H0.
cbn.
rewrite app_nil_r.
unfold get_ans1 in *. rewrite !get_ans_app.
rewrite get_ans_map_yes. rewrite E2.
unfold get_ans2. rewrite get_ans_app.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite get_ans_map_no.
rewrite app_nil_r. unfold get_ans2 in *. rewrite Hn'.
rewrite <- app_assoc. cbn. psimpl.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
eapply sinterrogation_length; eauto.
- intros (qs & ans & [[o n] tqs] & Hint & Hend).
assert (
qs = map snd tqs /\
interrogation (tau1 x) (λ (x0 : Y) (b : bool), if b then q x0 else ¬ q x0) (get_qs1 tqs) (get_ans1 tqs ans) /\
interrogation (tau2 x) (λ (x0 : Y) (b : bool), if b then q x0 else ¬ q x0) (get_qs2 tqs) (get_ans2 tqs ans)
) as [-> [Hi1 Hi2]].
{ eapply back in Hint; firstorder. }
cbn in Hend.
destruct o.
{ psimpl. }
destruct seval as [ [|[]] | ] eqn:E1.
* destruct (seval (tau2 x (get_ans2 tqs ans)) n) as [ [|[]] | ] eqn:E2; try psimpl.
eapply H2, HF2. eexists. eexists. split. eassumption. eapply seval_hasvalue'; eauto.
* psimpl. eapply H1, HF1. repeat eexists. eauto. eapply seval_hasvalue'; eauto.
* destruct (seval (tau2 x (get_ans2 tqs ans)) n) as [ [|[]] | ] eqn:E2; try psimpl.
eapply H2, HF2. eexists. eexists. split. eassumption. eapply seval_hasvalue'; eauto.
Qed.
End PT.
Print Assumptions main.
Lemma needed {Part : partiality} {E Q A I O} (τ0 : I -> stree E Q A O) (f : Rel Q A) e0 :
∃ τ1 : I → tree Q A O,
∀ (x : I) (b : O),
(∃ (qs : list Q) (ans : list A) (e : E), sinterrogation (τ0 x) f qs ans e0 e ∧ τ0 x e ans =! inr b)
↔ (∃ (qs : list Q) (ans : list A), interrogation (τ1 x) f qs ans ∧ τ1 x (ans) =! inr b).
Proof.
destruct (sinterrogation_equiv _ _ _ _ _ e0 τ0) as [τ1 H].
destruct (einterrogation_equiv _ _ _ _ _ e0 τ1) as [τ2 HH].
exists (λ x l, τ2 x l).
intros. rewrite H. rewrite HH. reflexivity.
Qed.
Definition OracleSemiDecidable {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :=
exists R : Functional Y bool X unit,
OracleComputable R /\
forall x, p x <-> R (char_rel q) x tt.
Lemma PT {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
(∀ y : Y, q y ∨ ¬ q y) ->
eq_dec Y ->
OracleSemiDecidable q p ->
OracleSemiDecidable q (fun x => ~ p x) ->
red_Turing p q.
Proof.
intros Hq HY [F1 [[tau1 HF1] H1]] [F2 [[tau2 HF2] H2]].
eapply Turing_reducible_without_rel.
enough
( ∃ τ : X → stree (option Y * nat * (list (bool * Y))) Y bool bool,
∀ (x : X) (b : bool), char_rel p x b ↔ (∃ (qs : list Y) (ans : list bool) e, sinterrogation (τ x) (char_rel q) qs ans (None, 0, nil) e ∧ τ x e ans =! inr b)).
{ destruct H as (τ & H). setoid_rewrite H. eapply needed.
}
eexists. eapply main.
exact HF1. exact H1. exact HF2. exact H2.
all: eauto.
Qed.
Lemma Turing_to_sdec {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
red_Turing p q ->
OracleSemiDecidable q p.
Proof.
intros [F [HF H2]].
exists (fun R x o => F R x true). split.
- eapply OracleComputable_ext.
eapply computable_bind. eapply HF.
eapply computable_if with (test := snd).
eapply computable_ret with (v := tt).
eapply computable_nothing.
cbn; split.
+ intros [[]]; firstorder.
+ destruct o. exists true; firstorder.
- firstorder.
Qed.
Lemma Turing_to_sdec_compl {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
red_Turing p q ->
OracleSemiDecidable q (compl p).
Proof.
intros [F [HF H2]].
exists (fun R x o => F R x false). split.
- eapply OracleComputable_ext.
eapply computable_bind. eapply HF.
eapply computable_if with (test := snd).
eapply computable_nothing.
eapply computable_ret with (v := tt).
cbn; split.
+ intros [[]]; firstorder.
+ destruct o. exists false; firstorder.
- firstorder.
Qed.
Lemma OracleSemiDecidable_refl {Part : partiality} X (Q : X -> Prop) :
OracleSemiDecidable Q Q.
Proof.
eapply Turing_to_sdec. eapply Turing_refl.
Qed.
Lemma semi_decidable_OracleSemiDecidable {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
semi_decidable p -> OracleSemiDecidable q p.
Proof.
intros (T & g & Hg) % SemiDecidabilityFacts.semi_decidable_part_iff.
eexists. split.
eapply (computable_partial_function (fun x => bind (g x) (fun _ => ret tt))).
intros. rewrite Hg. split.
- intros []. psimpl.
- intros. psimpl.
Qed.
Lemma OracleSemiDecidable_semi_decidable {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
decidable q -> OracleSemiDecidable q p -> semi_decidable p.
Proof.
intros [f Hf] (F & Hc & HF).
eapply SemiDecidabilityFacts.semi_decidable_part_iff.
exists unit.
setoid_rewrite HF.
clear HF p.
eapply Turing_transports_computable in Hc as [F' Hc].
specialize (Hc (fun y => ret (f y)) (char_rel q)).
unshelve epose proof (Hc _).
+ red. split; intros.
* psimpl. eapply reflects_iff, Hf.
* eapply ret_hasvalue_iff. cbn in H. eapply reflects_iff in H. specialize (Hf x).
unfold reflects in *. destruct (f x), y; firstorder congruence.
+ clear Hc. unfold pcomputes in H.
exists (fun x => F' (fun y : Y => ret (f y)) x).
intros. rewrite <- H. firstorder. destruct x0; eauto.
Qed.
Lemma red_m_transports_sdec {Part : partiality} {X Y Z} (q : Y -> Prop) (p1 : Z -> Prop) (p2 : X -> Prop) :
OracleSemiDecidable q p2 ->
red_m p1 p2 ->
OracleSemiDecidable q p1.
Proof.
intros [G [HG H1]] [f Hf].
eexists. split.
- eapply computable_bind.
eapply (computable_function f).
eapply computable_precompose with (g := snd). eapply HG.
- cbn. split.
+ intros ? % Hf % H1. eauto.
+ red in Hf. intros. rewrite Hf, H1.
destruct H as (? & ? & ?). subst. eauto.
Qed.
Lemma Turing_transports_sdec {Part : partiality} {X Y Z} (q1 : Y -> Prop) (q2 : Z -> Prop) (p : X -> Prop) :
OracleSemiDecidable q1 p ->
red_Turing q1 q2 ->
OracleSemiDecidable q2 p.
Proof.
intros [G [HG H1]] [F [HF H2]].
eexists. split.
all: cbn.
- eapply computable_comp.
eapply HF. eapply HG.
- intros. rewrite H1.
eapply OracleComputable_extensional in HG. eapply HG.
eauto.
Qed.
Lemma oracle_semi_decidable_complement_iff {Part : partiality} {X} (A : X -> Prop) {Y} (B : Y -> Prop) :
stable B -> OracleSemiDecidable B A <-> OracleSemiDecidable (fun y => ~ B y) A.
Proof.
intros DN.
split.
- intros H. apply (Turing_transports_sdec H), Turing_red_compl. exact DN.
- intros H. apply (Turing_transports_sdec H),compl_Turing_red. exact DN.
Qed.
From SyntheticComputability Require Import partial Definitions reductions Dec DecidabilityFacts.
Require Import Lia List.
From stdpp Require Import list.
Import PartialTactics.
Lemma seval_hasvalue' {partiality : partial.partiality} [A : Type] (x : part A) (a : A) n :
seval x n = Some a -> x =! a.
Proof.
intros. eapply seval_hasvalue. eauto.
Qed.
Section PT.
Context {Part : partiality} {X : Type} {Y : Type}.
Variable q : Y → Prop.
Variable p : X → Prop.
Variable F1 : Functional Y bool X ().
Variable tau1 : X → (list bool) ↛ (Y + unit).
Variable HF1 : ∀ (R : Rel Y bool) (x : X) (o : ()), F1 R x o ↔ (∃ (qs : list Y) (ans : list bool), interrogation (tau1 x) R qs ans ∧ tau1 x ans =! inr o).
Variable H1 : ∀ x : X, p x ↔ F1 (char_rel q) x ().
Variable F2 : Functional Y bool X ().
Variable tau2 : X → (list bool) ↛ (Y + unit).
Variable HF2 : ∀ (R : Rel Y bool) (x : X) (o : ()), F2 R x o ↔ (∃ (qs : list Y) (ans : list bool), interrogation (tau2 x) R qs ans ∧ tau2 x ans =! inr o).
Variable H2 : ∀ x : X, ¬ p x ↔ F2 (char_rel q) x ().
Definition get_ans B (tqs : list (bool * Y)) (ans : list bool) := (map snd (filter (fun '((b, q), a) => b = B) (zip_with pair tqs ans))).
Definition get_ans1 := get_ans true.
Definition get_ans2 := get_ans false.
Definition get_qs B (tqs : list (bool * Y)) := (map snd (filter (fun '((b, q)) => b = B) tqs)).
Definition get_qs1 := get_qs true.
Definition get_qs2 := get_qs false.
Lemma get_ans_app B t1 t2 a1 a2 :
length t1 = length a1 ->
get_ans B (t1 ++ t2) (a1 ++ a2) = get_ans B t1 a1 ++ get_ans B t2 a2.
Proof.
intros Hlen.
induction t1 in a1, Hlen |- *; destruct a1; cbn in *; try lia.
- reflexivity.
- destruct a. destruct decide.
+ cbn. f_equal. eapply IHt1. lia.
+ eapply IHt1. lia.
Qed.
Lemma get_qs_app B t1 t2 :
get_qs B (t1 ++ t2) = get_qs B t1 ++ get_qs B t2.
Proof.
induction t1.
- reflexivity.
- cbn. destruct a. destruct decide.
+ cbn. f_equal. eapply IHt1.
+ eapply IHt1.
Qed.
Definition τ := fun x '(old, n, tqs) ans =>
match old with Some q => ret (inl (None, n, tqs ++ [(false, q)], Some q))
| None =>
match seval (tau1 x (get_ans1 tqs ans)) n, seval (tau2 x (get_ans2 tqs ans)) n with
| Some (inr o), _ => ret (inr true)
| _ , Some (inr o) => ret (inr false)
| Some (inl q), Some (inl q') => ret (inl (Some q' , S n, tqs ++ [(true, q)], Some q))
| Some (inl q), _ => ret (inl (None, S n, tqs ++ [(true, q)], Some q))
| _, Some (inl q) => ret (inl (None, S n, tqs ++ [(false, q)], Some q))
| _, _ => ret (inl (None, S n, tqs, None))
end end.
Definition qs_from_tqs (tqs : list (bool * Y)) := map snd tqs.
Definition subtree (tau : list bool ↛ (Y + ())) ans l := tau (ans ++ l).
Definition subtree' {E Q A O} (tau : stree E Q A O) ans e l := tau e (ans ++ l).
Variable q_dec : forall y, q y \/ ~ q y.
Lemma q_reflect y : exists b, char_rel q y b.
Proof.
destruct (q_dec y).
exists true; eauto.
exists false; eauto.
Qed.
Variable Y_dec : eq_dec Y.
Lemma count_up_1 m tqs x ans v :
p x ->
length tqs = length ans ->
interrogation (tau2 x) (char_rel q) (get_qs2 tqs) (get_ans2 tqs ans) ->
tau1 x (get_ans1 tqs ans) =! v ->
exists tqs' ans' n',
seval (tau1 x (get_ans1 tqs ans)) n' = Some v /\
sinterrogation (subtree' (τ x) ans) (char_rel q) tqs' ans' (None,m, tqs) (None, n', tqs ++ map (pair false) tqs') /\
interrogation (subtree (tau2 x) (get_ans2 tqs ans)) (char_rel q) tqs' ans'.
Proof.
intros Hx Hlen Hi2 Hend.
eapply seval_hasvalue in Hend as [n Hend].
edestruct Wf_nat.dec_inh_nat_subset_has_unique_least_element with (P := fun n => seval (tau1 x (get_ans1 tqs ans)) n = Some v).
{ intros. clear - Y_dec. destruct seval as [ [? | []] | ]; try now clear; firstorder congruence.
all: destruct v as [ | []]; try now clear; firstorder congruence.
destruct (Y_dec y y0); try firstorder congruence.
}
{ eauto. }
clear n Hend. rename x0 into n. destruct H as [ [] ]. rename H into Hend.
clear H3.
assert (Hleast : ∀ x' : nat, x' < n -> seval (tau1 x (get_ans1 tqs ans)) x' = None).
{
intros x' Hl. destruct (seval (tau1 x (get_ans1 tqs ans)) x') as [ [ | []] | ] eqn:E.
- assert (v = inl y) as ->. { eapply hasvalue_det; eapply seval_hasvalue'; eauto. }
eapply H0 in E. lia.
- assert (v = inr ()) as ->. { eapply hasvalue_det; eapply seval_hasvalue'; eauto. }
eapply H0 in E. lia.
- reflexivity.
}
clear H0.
destruct (Nat.le_dec m n).
- revert Hi2 Hend Hlen Hleast. revert ans tqs. pattern m, n. revert m l.
eapply Nat.left_induction.
+ exact _.
+ intros. exists [], [], n. repeat eapply conj.
* eauto.
* cbn. rewrite app_nil_r. econstructor.
* econstructor.
+ intros m Hlt IH ? ? ? ? ? ?.
destruct (seval (tau2 x (get_ans2 tqs ans)) m) as [ [ | []] | ] eqn:E.
* destruct (q_reflect y) as [b Hb].
specialize (IH (ans ++ [b]) (tqs ++ [(false, y)])).
edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3).
{
unfold get_qs2. rewrite !get_qs_app.
unfold get_ans2. rewrite !get_ans_app; eauto.
cbn. destruct decide; try congruence.
cbn. econstructor. eauto. 2: eapply Hb.
eapply seval_hasvalue'; eassumption.
}
{
unfold get_ans1. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn. rewrite app_nil_r.
all: eauto.
}
{ rewrite !app_length. cbn. lia. }
{
unfold get_ans1. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn. rewrite app_nil_r.
all: eauto.
}
exists (y :: tqs'), (b :: ans'), n'. repeat eapply conj.
-- unfold get_ans1 in IH1.
rewrite get_ans_app in IH1. 2: eauto.
cbn in IH1. destruct decide; try congruence.
cbn in *. rewrite app_nil_r in IH1. eauto.
-- eapply sinterrogation_cons.
2: eauto. cbn.
rewrite app_nil_r.
assert (seval (tau1 x (get_ans1 tqs ans)) m = None) as ->.
{ eapply Hleast. lia. }
rewrite E. psimpl.
cbn. unfold subtree in *.
rewrite <- !app_assoc in IH2. cbn in *.
eapply sinterrogation_ext. 2: eassumption.
intros. unfold subtree'. cbn. now rewrite <- app_assoc.
-- eapply interrogation_cons. eapply seval_hasvalue'; eauto.
unfold subtree. rewrite app_nil_r. eassumption. eauto.
eapply interrogation_ext. 3: eauto. 2: reflexivity.
intros. unfold subtree.
unfold get_ans2. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn. now rewrite <- app_assoc.
eauto.
* edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3); eauto.
assert (~ p x). {
eapply H2.
eapply HF2. repeat eexists. 2: eapply seval_hasvalue'; eauto.
eauto.
}
tauto.
* specialize (IH ans tqs).
edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3); eauto.
exists tqs', ans', n'. repeat eapply conj.
-- eauto.
-- eapply sinterrogation_scons.
2: eauto. cbn.
rewrite app_nil_r.
assert (seval (tau1 x (get_ans1 tqs ans)) m = None) as ->.
{ eapply Hleast. lia. }
rewrite E. psimpl.
-- eauto.
- exists [], [], m. repeat eapply conj.
+ eapply seval_mono; eauto. lia.
+ cbn. rewrite app_nil_r. econstructor.
+ cbn. econstructor.
Qed.
Lemma count_up_2 m tqs x ans v :
~ p x ->
length tqs = length ans ->
interrogation (tau1 x) (char_rel q) (get_qs1 tqs) (get_ans1 tqs ans) ->
tau2 x (get_ans2 tqs ans) =! v ->
exists tqs' ans' n',
seval (tau2 x (get_ans2 tqs ans)) n' = Some v /\
sinterrogation (subtree' (τ x) ans) (char_rel q) tqs' ans' (None,m, tqs) (None, n', tqs ++ map (pair true) tqs') /\
interrogation (subtree (tau1 x) (get_ans1 tqs ans)) (char_rel q) tqs' ans'.
Proof.
intros Hx Hlen Hi2 [n Hend] % seval_hasvalue.
edestruct Wf_nat.dec_inh_nat_subset_has_unique_least_element with (P := fun n => seval (tau2 x (get_ans2 tqs ans)) n = Some v).
{ intros. clear - Y_dec. destruct seval as [ [? | []] | ]; try now clear; firstorder congruence.
all: destruct v as [ | []]; try now clear; firstorder congruence.
destruct (Y_dec y y0); try firstorder congruence.
}
{ eauto. }
clear n Hend. rename x0 into n. destruct H as [ [] ]. rename H into Hend.
clear H3.
assert (Hleast : ∀ x' : nat, x' < n -> seval (tau2 x (get_ans2 tqs ans)) x' = None).
{
intros x' Hl. destruct (seval (tau2 x (get_ans2 tqs ans)) x') as [ [ | []] | ] eqn:E.
- assert (v = inl y) as ->. { eapply hasvalue_det; eapply seval_hasvalue'; eauto. }
eapply H0 in E. lia.
- assert (v = inr ()) as ->. { eapply hasvalue_det; eapply seval_hasvalue'; eauto. }
eapply H0 in E. lia.
- reflexivity.
}
clear H0.
destruct (Nat.le_dec m n).
- revert Hi2 Hend Hlen Hleast. revert ans tqs. pattern m, n. revert m l.
eapply Nat.left_induction.
+ exact _.
+ intros. exists [], [], n. repeat eapply conj.
* eauto.
* cbn. rewrite app_nil_r. econstructor.
* econstructor.
+ intros m Hlt IH ? ? ? ? ? ?.
destruct (seval (tau1 x (get_ans1 tqs ans)) m) as [ [ | []] | ] eqn:E.
* destruct (q_reflect y) as [b Hb].
specialize (IH (ans ++ [b]) (tqs ++ [(true, y)])).
edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3).
{
unfold get_qs1. rewrite !get_qs_app.
unfold get_ans1. rewrite !get_ans_app; eauto.
cbn. destruct decide; try congruence.
cbn. econstructor. eauto.
eapply seval_hasvalue'; eauto.
eauto.
}
{
unfold get_ans2. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn.
rewrite app_nil_r; eassumption.
all: eauto.
}
{ rewrite !app_length. cbn. lia. }
{
unfold get_ans2. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn. rewrite app_nil_r.
all: eauto.
}
exists (y :: tqs'), (b :: ans'), n'. repeat eapply conj.
-- unfold get_ans2 in IH1.
rewrite get_ans_app in IH1. 2: eauto.
cbn in IH1. destruct decide; try congruence.
cbn in *. rewrite app_nil_r in IH1. eauto.
-- eapply sinterrogation_cons.
2: eauto. cbn.
rewrite app_nil_r.
rewrite E.
rewrite Hleast. 2: lia.
psimpl.
cbn. unfold subtree in *.
rewrite <- !app_assoc in IH2. cbn in *.
eapply sinterrogation_ext. 2: eassumption.
intros. unfold subtree'. cbn. now rewrite <- app_assoc.
-- eapply interrogation_cons. eapply seval_hasvalue'; eauto.
unfold subtree. rewrite app_nil_r. eassumption. eauto.
eapply interrogation_ext. 3: eauto. 2: reflexivity.
intros. unfold subtree.
unfold get_ans1. rewrite get_ans_app. cbn.
destruct decide; try congruence. cbn. now rewrite <- app_assoc.
eauto.
* edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3); eauto.
assert (p x). {
eapply H1, HF1. repeat eexists. 2: eapply seval_hasvalue'; eauto.
eauto.
}
tauto.
* specialize (IH ans tqs).
edestruct IH as (tqs' & ans' & n' & IH1 & IH2 & IH3); eauto.
exists tqs', ans', n'. repeat eapply conj.
-- eauto.
-- eapply sinterrogation_scons.
2: eauto. cbn.
rewrite app_nil_r.
rewrite E.
rewrite Hleast. 2: lia. psimpl.
-- eauto.
- exists [], [], m. repeat eapply conj.
+ eapply seval_mono; eauto. lia.
+ cbn. rewrite app_nil_r. econstructor.
+ cbn. econstructor.
Qed.
Lemma back:
∀ (x : X) (qs : list Y) (ans : list bool) (n : nat) (tqs : list (bool * Y)) o,
sinterrogation (τ x) (char_rel q) qs ans (None, 0, []) (o, n, tqs)
→ qs = map snd tqs
/\ length ans = length tqs
/\ match o with Some q => tau2 x (get_ans2 tqs ans) =! inl q | None => True end
∧ interrogation (tau1 x) (λ (x0 : Y) (b : bool), if b then q x0 else ¬ q x0) (get_qs1 tqs) (get_ans1 tqs ans)
∧ interrogation (tau2 x) (λ (x0 : Y) (b : bool), if b then q x0 else ¬ q x0) (get_qs2 tqs) (get_ans2 tqs ans).
Proof.
intros x qs ans n tqs o Hint.
remember (None, 0, []) as begin.
remember (o, n, tqs) as theend.
induction Hint in Heqbegin, Heqtheend, tqs, n, o |- *.
- subst. inversion Heqtheend; subst. cbn. repeat eapply conj; econstructor.
- subst. destruct e1' as [[o' n'] tqs'].
cbn in H. destruct o'; cbn in *; psimpl.
edestruct IHHint as (-> & Hlen & IH3 & IH1 & IH2); try reflexivity.
destruct seval as [ [? | []] | ] eqn:E1.
+ destruct (seval (tau2 x (get_ans2 tqs' ans)) n') as [ [? | []] | ] eqn:E2; psimpl.
+ psimpl.
+ destruct (seval (tau2 x (get_ans2 tqs' ans)) n') as [ [? | []] | ] eqn:E2; psimpl.
- subst. destruct e1' as [[o' n'] tqs'].
edestruct IHHint as (-> & Hlen & IH3 & IH1 & IH2); try reflexivity.
cbn in H. destruct o'; psimpl.
{
assert ((get_qs2 (tqs' ++ [(false, q0)])) = get_qs2 tqs' ++ [q0]) as Eqn1.
{ unfold get_qs2. rewrite get_qs_app. cbn. destruct decide; try congruence. reflexivity. }
assert ((get_qs1 (tqs' ++ [(false, q0)])) = get_qs1 tqs') as Eqn2.
{ unfold get_qs1. rewrite get_qs_app. cbn. destruct decide; try congruence. cbn. now rewrite app_nil_r. }
assert ((get_ans2 (tqs' ++ [(false, q0)]) (ans ++ [a])) = get_ans2 tqs' ans ++ [a]) as Eqn1'.
{ unfold get_ans2. rewrite get_ans_app. 2: lia.
cbn. now destruct decide; try congruence; cbn.
}
assert ((get_ans1 (tqs' ++ [(false, q0)]) (ans ++ [a])) = get_ans1 tqs' ans) as Eqn2'.
{ unfold get_ans1. rewrite get_ans_app. 2: lia.
cbn. destruct decide; try congruence; cbn. now rewrite app_nil_r.
}
repeat eapply conj.
+ now rewrite map_app; cbn.
+ rewrite !app_length; cbn. lia.
+ eauto.
+ rewrite Eqn2, Eqn2'. eauto.
+ rewrite Eqn1, Eqn1'. econstructor. eauto. 2: eapply H0.
eauto.
}
destruct seval as [ [? | []] | ] eqn:E1.
+ assert ((get_qs1 (tqs' ++ [(true, q0)])) = get_qs1 tqs' ++ [q0]) as Eqn1.
{ unfold get_qs1. rewrite get_qs_app. cbn. destruct decide; try congruence. reflexivity. }
assert ((get_qs2 (tqs' ++ [(true, q0)])) = get_qs2 tqs') as Eqn2.
{ unfold get_qs2. rewrite get_qs_app. cbn. destruct decide; try congruence. cbn. now rewrite app_nil_r. }
assert ((get_ans1 (tqs' ++ [(true, q0)]) (ans ++ [a])) = get_ans1 tqs' ans ++ [a]) as Eqn1'.
{ unfold get_ans1. rewrite get_ans_app. 2: lia.
cbn. now destruct decide; try congruence; cbn.
}
assert ((get_ans2 (tqs' ++ [(true, q0)]) (ans ++ [a])) = get_ans2 tqs' ans) as Eqn2'.
{ unfold get_ans2. rewrite get_ans_app. 2: lia.
cbn. destruct decide; try congruence; cbn. now rewrite app_nil_r.
}
destruct (seval (tau2 x (get_ans2 tqs' ans)) n') as [ [? | []] | ] eqn:E2; psimpl.
* repeat eapply conj.
-- now rewrite map_app.
-- rewrite !app_length; cbn. lia.
-- rewrite Eqn2'. eapply seval_hasvalue'; eauto.
-- rewrite Eqn1, Eqn1'. econstructor. eauto. 2: eapply H0.
eapply seval_hasvalue'; eauto.
-- rewrite Eqn2, Eqn2'. eauto.
* repeat eapply conj.
-- now rewrite map_app.
-- rewrite !app_length; cbn. lia.
-- eauto.
-- rewrite Eqn1, Eqn1'. econstructor. eauto. 2: eapply H0.
eapply seval_hasvalue'; eauto.
-- rewrite Eqn2, Eqn2'. eauto.
+ psimpl.
+ destruct (seval (tau2 x (get_ans2 tqs' ans)) n') as [ [? | []] | ] eqn:E2; psimpl.
assert ((get_qs2 (tqs' ++ [(false, q0)])) = get_qs2 tqs' ++ [q0]) as Eqn1.
{ unfold get_qs2. rewrite get_qs_app. cbn. destruct decide; try congruence. reflexivity. }
assert ((get_qs1 (tqs' ++ [(false, q0)])) = get_qs1 tqs') as Eqn2.
{ unfold get_qs1. rewrite get_qs_app. cbn. destruct decide; try congruence. cbn. now rewrite app_nil_r. }
assert ((get_ans2 (tqs' ++ [(false, q0)]) (ans ++ [a])) = get_ans2 tqs' ans ++ [a]) as Eqn1'.
{ unfold get_ans2. rewrite get_ans_app. 2: lia.
cbn. now destruct decide; try congruence; cbn.
}
assert ((get_ans1 (tqs' ++ [(false, q0)]) (ans ++ [a])) = get_ans1 tqs' ans) as Eqn2'.
{ unfold get_ans1. rewrite get_ans_app. 2: lia.
cbn. destruct decide; try congruence; cbn. now rewrite app_nil_r.
}
repeat eapply conj.
-- now rewrite map_app.
-- rewrite !app_length; cbn. lia.
-- eauto.
-- rewrite Eqn2, Eqn2'. eauto.
-- rewrite Eqn1, Eqn1'. econstructor. eauto. 2: eapply H0.
eapply seval_hasvalue'; eauto.
Qed.
Lemma get_ans_map_no b tqs ans :
get_ans b (map (pair (negb b)) tqs) ans = [].
Proof.
induction tqs in ans |- *; cbn. 1: reflexivity.
destruct ans; try reflexivity. cbn.
destruct decide. { destruct b; cbn in*; congruence. }
eauto.
Qed.
Lemma get_qs_map_no b tqs :
get_qs b (map (pair (negb b)) tqs) = [].
Proof.
induction tqs; cbn. 1: reflexivity.
destruct decide. { destruct b; cbn in*; congruence. }
eauto.
Qed.
Lemma get_qs_map_yes b tqs :
get_qs b (map (pair (b)) tqs) = tqs.
Proof.
induction tqs; cbn. 1: reflexivity.
destruct decide; try congruence. cbn. f_equal. eauto.
Qed.
Lemma get_ans_map_yes b tqs ans :
length tqs = length ans ->
get_ans b (map (pair b) tqs) ans = ans.
Proof.
induction tqs in ans |- *; cbn.
all: destruct ans; cbn in *; try lia.
1: reflexivity. intros.
destruct decide; try congruence.
cbn. f_equal.
eauto.
Qed.
Lemma main :
∀ (x : X) (b : bool), char_rel p x b ↔ (∃ (qs : list Y) (ans : list bool) e, sinterrogation (τ x) (char_rel q) qs ans (None, 0, nil) e ∧ τ x e ans =! inr b).
Proof.
intros. split. destruct b; cbn.
- intros Hx.
eapply H1 in Hx as Hx'. eapply HF1 in Hx' as (qs & ans & Hint & Hend).
enough (∃ (ans0 : list bool) m (qs0 : list (bool * Y)),
qs = get_qs1 qs0 /\
ans = get_ans1 qs0 ans0 /\
interrogation (tau2 x) (char_rel q) (get_qs2 qs0) (get_ans2 qs0 ans0) /\
sinterrogation (τ x) (char_rel q) (map snd qs0) ans0 (None, 0, []) (None, m, qs0)).
{ cbn in *. decompose [ex and] H. subst.
eapply count_up_1 in Hend as lem; eauto.
2:{ eapply sinterrogation_length in H6. rewrite map_length in H6. lia. }
destruct lem as (tqs' & ans' & n' & Hn' & IH1 & IH2).
eexists (_ ++ tqs').
eexists (_ ++ ans').
eexists (None, n', _ ++ map (pair false) tqs').
split.
eapply sinterrogation_app.
eauto. eassumption.
cbn.
unfold get_ans1. rewrite get_ans_app.
rewrite get_ans_map_no. rewrite app_nil_r.
unfold get_ans1 in *.
rewrite Hn'. psimpl.
eapply sinterrogation_length in H6.
rewrite map_length in H6. lia.
}
clear Hend. induction Hint.
+ exists []. exists 0. exists []. repeat econstructor.
+ cbn in IHHint. destruct IHHint as (ans_ & m & qs_ & -> & -> & IH1 & IH2).
eapply count_up_1 in H as lem; eauto.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. lia. }
destruct lem as (tqs' & ans' & n' & Hn' & HH1 & HH2).
rename q0 into y.
destruct (seval (tau2 x (get_ans false qs_ ans_ ++ ans')) n') as [ [ | []] | ] eqn:E2.
{
destruct (q_reflect y0) as [b Hb].
eexists (ans_ ++ ans' ++ [a;b] ).
exists (S n').
eexists (qs_ ++ map (pair false) tqs' ++ [(true, y); (false, y0)] ).
cbn. repeat eapply conj.
* unfold get_qs1. rewrite !get_qs_app.
cbn. destruct decide; try congruence.
now rewrite get_qs_map_no.
* unfold get_ans1. rewrite !get_ans_app.
2:{ rewrite map_length. eapply interrogation_length; eauto. }
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
cbn. destruct decide; try congruence.
now rewrite get_ans_map_no.
* unfold get_qs2, get_ans2.
rewrite !get_qs_app.
rewrite !get_ans_app.
rewrite get_qs_map_yes, get_ans_map_yes.
eapply interrogation_app; eauto.
eapply interrogation_app; eauto.
cbn. destruct decide; try congruence. destruct decide; try congruence. cbn.
eapply Interrogate with (qs := []) (ans := []); eauto. econstructor.
rewrite app_nil_r. eapply seval_hasvalue'; eauto.
eapply interrogation_length; eauto.
rewrite map_length. eapply interrogation_length; eauto.
eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto.
* rewrite !map_app. eapply sinterrogation_app.
eauto.
eapply sinterrogation_app.
rewrite map_map, map_id.
eauto.
cbn.
eapply sinterrogation_cons.
rewrite app_nil_r. cbn.
unfold get_ans1 in *. rewrite !get_ans_app.
rewrite get_ans_map_no. rewrite app_nil_r.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite Hn'.
unfold get_ans2. rewrite get_ans_app.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite get_ans_map_yes. 2: eapply interrogation_length; eauto.
rewrite E2. rewrite <- app_assoc. psimpl.
eapply H0.
eapply sinterrogation_cons.
cbn. psimpl. eapply Hb.
rewrite <- !app_assoc. cbn. econstructor.
}
{
enough (~ p x) by tauto.
eapply H2, HF2. repeat eexists.
2: eapply seval_hasvalue'; eauto.
eapply interrogation_app; eauto.
}
eexists (ans_ ++ ans' ++ [a] ).
exists (S n').
eexists (qs_ ++ map (pair false) tqs' ++ [(true, y)]).
cbn. repeat eapply conj.
* unfold get_qs1. rewrite !get_qs_app.
cbn. destruct decide; try congruence.
now rewrite get_qs_map_no.
* unfold get_ans1. rewrite !get_ans_app.
2:{ rewrite map_length. eapply interrogation_length; eauto. }
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
cbn. destruct decide; try congruence.
now rewrite get_ans_map_no.
* unfold get_qs2, get_ans2.
rewrite !get_qs_app.
rewrite !get_ans_app.
rewrite get_qs_map_yes, get_ans_map_yes.
eapply interrogation_app; eauto.
eapply interrogation_app; eauto.
cbn. destruct decide; try congruence. econstructor.
eapply interrogation_length; eauto.
rewrite map_length. eapply interrogation_length; eauto.
eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto.
* rewrite !map_app. eapply sinterrogation_app.
eauto.
eapply sinterrogation_app.
rewrite map_map, map_id.
eauto.
cbn.
eapply sinterrogate with (qs := []) (ans := []).
econstructor. 2: eapply H0.
cbn.
rewrite app_nil_r.
unfold get_ans1 in *. rewrite !get_ans_app.
rewrite get_ans_map_no. rewrite app_nil_r.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite Hn'.
unfold get_ans2. rewrite get_ans_app.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite get_ans_map_yes. 2: eapply interrogation_length; eauto.
rewrite E2. rewrite <- app_assoc. psimpl.
- intros Hx.
eapply H2 in Hx as Hx'. eapply HF2 in Hx' as (qs & ans & Hint & Hend).
enough (∃ (ans0 : list bool) m (qs0 : list (bool * Y)),
qs = get_qs2 qs0 /\
ans = get_ans2 qs0 ans0 /\
interrogation (tau1 x) (char_rel q) (get_qs1 qs0) (get_ans1 qs0 ans0) /\
sinterrogation (τ x) (char_rel q) (map snd qs0) ans0 (None, 0, []) (None, m, qs0)).
{ cbn in *. decompose [ex and] H. subst.
eapply count_up_2 in Hend as lem; eauto.
2:{ eapply sinterrogation_length in H6. rewrite map_length in H6. lia. }
destruct lem as (tqs' & ans' & n' & Hn' & IH1 & IH2).
eexists (_ ++ tqs').
eexists (_ ++ ans').
eexists (None, n', _ ++ map (pair true) tqs').
split.
eapply sinterrogation_app.
eauto. eassumption.
cbn.
unfold get_ans2. rewrite get_ans_app.
rewrite get_ans_map_no. rewrite app_nil_r.
unfold get_ans2 in *.
rewrite Hn'.
destruct (seval (tau1 x (get_ans1 (x2 ++ map (pair true) tqs') (x0 ++ ans'))) n') as [ [ | []] | ] eqn:EE; psimpl.
2:{ eapply sinterrogation_length in H6.
rewrite map_length in H6. lia. }
enough (p x) by tauto.
eapply H1, HF1. repeat eexists. 2: eapply seval_hasvalue'; eauto.
unfold get_ans1. rewrite get_ans_app.
2:{ eapply sinterrogation_length in H6.
rewrite map_length in H6. lia. }
eapply interrogation_app; eauto.
rewrite get_ans_map_yes.
2: eapply interrogation_length; eauto.
eauto.
}
clear Hend. induction Hint.
+ exists []. exists 0. exists []. repeat econstructor.
+ cbn in IHHint. destruct IHHint as (ans_ & m & qs_ & -> & -> & IH1 & IH2).
eapply count_up_2 in H as lem; eauto.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. lia. }
destruct lem as (tqs' & ans' & n' & Hn' & HH1 & HH2).
rename q0 into y.
destruct (seval (tau1 x (get_ans1 qs_ ans_ ++ ans')) n') as [ [ | []] | ] eqn:E2.
{
destruct (q_reflect y0) as [b Hb].
eexists (ans_ ++ ans' ++ [b;a] ).
exists (S n').
eexists (qs_ ++ map (pair true) tqs' ++ [(true, y0); (false, y)] ).
cbn. repeat eapply conj.
* unfold get_qs2. rewrite !get_qs_app.
cbn. destruct decide; try congruence.
destruct decide; try congruence.
now rewrite get_qs_map_no.
* unfold get_ans2. rewrite !get_ans_app.
2:{ rewrite map_length. eapply interrogation_length; eauto. }
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
cbn. destruct decide; try congruence.
destruct decide; try congruence.
now rewrite get_ans_map_no.
* unfold get_qs1, get_ans1.
rewrite !get_qs_app.
rewrite !get_ans_app.
rewrite get_qs_map_yes, get_ans_map_yes.
eapply interrogation_app; eauto.
eapply interrogation_app; eauto.
cbn. destruct decide; try congruence. destruct decide; try congruence. cbn.
eapply Interrogate with (qs := []) (ans := []); eauto. econstructor.
rewrite app_nil_r. eapply seval_hasvalue'; eauto.
eapply interrogation_length; eauto.
rewrite map_length. eapply interrogation_length; eauto.
eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto.
* rewrite !map_app. eapply sinterrogation_app.
eauto.
eapply sinterrogation_app.
rewrite map_map, map_id.
eauto.
cbn.
eapply sinterrogation_cons.
rewrite app_nil_r. cbn.
unfold get_ans1 in *. rewrite !get_ans_app.
rewrite get_ans_map_yes. rewrite E2.
2:{ eapply sinterrogation_length in HH1. eauto. }
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
2: eapply Hb.
unfold get_ans2. rewrite get_ans_app.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite get_ans_map_no. rewrite app_nil_r.
unfold get_ans2 in *.
rewrite Hn'. psimpl.
eapply sinterrogation_cons.
cbn. psimpl. eapply H0.
rewrite <- !app_assoc. cbn. econstructor.
}
{
enough (p x) by tauto.
eapply H1, HF1. repeat eexists.
2: eapply seval_hasvalue'; eauto.
eapply interrogation_app; eauto.
}
eexists (ans_ ++ ans' ++ [a] ).
exists (S n').
eexists (qs_ ++ map (pair true) tqs' ++ [(false, y)]).
cbn. repeat eapply conj.
* unfold get_qs2. rewrite !get_qs_app.
cbn. destruct decide; try congruence.
now rewrite get_qs_map_no.
* unfold get_ans2. rewrite !get_ans_app.
2:{ rewrite map_length. eapply interrogation_length; eauto. }
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
cbn. destruct decide; try congruence.
now rewrite get_ans_map_no.
* unfold get_qs1, get_ans1.
rewrite !get_qs_app.
rewrite !get_ans_app.
rewrite get_qs_map_yes, get_ans_map_yes.
eapply interrogation_app; eauto.
eapply interrogation_app; eauto.
cbn. destruct decide; try congruence. econstructor.
eapply interrogation_length; eauto.
rewrite map_length. eapply interrogation_length; eauto.
eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto.
* rewrite !map_app. eapply sinterrogation_app.
eauto.
eapply sinterrogation_app.
rewrite map_map, map_id.
eauto.
cbn.
eapply sinterrogate with (qs := []) (ans := []).
econstructor. 2: eapply H0.
cbn.
rewrite app_nil_r.
unfold get_ans1 in *. rewrite !get_ans_app.
rewrite get_ans_map_yes. rewrite E2.
unfold get_ans2. rewrite get_ans_app.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
rewrite get_ans_map_no.
rewrite app_nil_r. unfold get_ans2 in *. rewrite Hn'.
rewrite <- app_assoc. cbn. psimpl.
2:{ eapply sinterrogation_length in IH2. rewrite map_length in IH2. eauto. }
eapply sinterrogation_length; eauto.
- intros (qs & ans & [[o n] tqs] & Hint & Hend).
assert (
qs = map snd tqs /\
interrogation (tau1 x) (λ (x0 : Y) (b : bool), if b then q x0 else ¬ q x0) (get_qs1 tqs) (get_ans1 tqs ans) /\
interrogation (tau2 x) (λ (x0 : Y) (b : bool), if b then q x0 else ¬ q x0) (get_qs2 tqs) (get_ans2 tqs ans)
) as [-> [Hi1 Hi2]].
{ eapply back in Hint; firstorder. }
cbn in Hend.
destruct o.
{ psimpl. }
destruct seval as [ [|[]] | ] eqn:E1.
* destruct (seval (tau2 x (get_ans2 tqs ans)) n) as [ [|[]] | ] eqn:E2; try psimpl.
eapply H2, HF2. eexists. eexists. split. eassumption. eapply seval_hasvalue'; eauto.
* psimpl. eapply H1, HF1. repeat eexists. eauto. eapply seval_hasvalue'; eauto.
* destruct (seval (tau2 x (get_ans2 tqs ans)) n) as [ [|[]] | ] eqn:E2; try psimpl.
eapply H2, HF2. eexists. eexists. split. eassumption. eapply seval_hasvalue'; eauto.
Qed.
End PT.
Print Assumptions main.
Lemma needed {Part : partiality} {E Q A I O} (τ0 : I -> stree E Q A O) (f : Rel Q A) e0 :
∃ τ1 : I → tree Q A O,
∀ (x : I) (b : O),
(∃ (qs : list Q) (ans : list A) (e : E), sinterrogation (τ0 x) f qs ans e0 e ∧ τ0 x e ans =! inr b)
↔ (∃ (qs : list Q) (ans : list A), interrogation (τ1 x) f qs ans ∧ τ1 x (ans) =! inr b).
Proof.
destruct (sinterrogation_equiv _ _ _ _ _ e0 τ0) as [τ1 H].
destruct (einterrogation_equiv _ _ _ _ _ e0 τ1) as [τ2 HH].
exists (λ x l, τ2 x l).
intros. rewrite H. rewrite HH. reflexivity.
Qed.
Definition OracleSemiDecidable {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :=
exists R : Functional Y bool X unit,
OracleComputable R /\
forall x, p x <-> R (char_rel q) x tt.
Lemma PT {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
(∀ y : Y, q y ∨ ¬ q y) ->
eq_dec Y ->
OracleSemiDecidable q p ->
OracleSemiDecidable q (fun x => ~ p x) ->
red_Turing p q.
Proof.
intros Hq HY [F1 [[tau1 HF1] H1]] [F2 [[tau2 HF2] H2]].
eapply Turing_reducible_without_rel.
enough
( ∃ τ : X → stree (option Y * nat * (list (bool * Y))) Y bool bool,
∀ (x : X) (b : bool), char_rel p x b ↔ (∃ (qs : list Y) (ans : list bool) e, sinterrogation (τ x) (char_rel q) qs ans (None, 0, nil) e ∧ τ x e ans =! inr b)).
{ destruct H as (τ & H). setoid_rewrite H. eapply needed.
}
eexists. eapply main.
exact HF1. exact H1. exact HF2. exact H2.
all: eauto.
Qed.
Lemma Turing_to_sdec {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
red_Turing p q ->
OracleSemiDecidable q p.
Proof.
intros [F [HF H2]].
exists (fun R x o => F R x true). split.
- eapply OracleComputable_ext.
eapply computable_bind. eapply HF.
eapply computable_if with (test := snd).
eapply computable_ret with (v := tt).
eapply computable_nothing.
cbn; split.
+ intros [[]]; firstorder.
+ destruct o. exists true; firstorder.
- firstorder.
Qed.
Lemma Turing_to_sdec_compl {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
red_Turing p q ->
OracleSemiDecidable q (compl p).
Proof.
intros [F [HF H2]].
exists (fun R x o => F R x false). split.
- eapply OracleComputable_ext.
eapply computable_bind. eapply HF.
eapply computable_if with (test := snd).
eapply computable_nothing.
eapply computable_ret with (v := tt).
cbn; split.
+ intros [[]]; firstorder.
+ destruct o. exists false; firstorder.
- firstorder.
Qed.
Lemma OracleSemiDecidable_refl {Part : partiality} X (Q : X -> Prop) :
OracleSemiDecidable Q Q.
Proof.
eapply Turing_to_sdec. eapply Turing_refl.
Qed.
Lemma semi_decidable_OracleSemiDecidable {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
semi_decidable p -> OracleSemiDecidable q p.
Proof.
intros (T & g & Hg) % SemiDecidabilityFacts.semi_decidable_part_iff.
eexists. split.
eapply (computable_partial_function (fun x => bind (g x) (fun _ => ret tt))).
intros. rewrite Hg. split.
- intros []. psimpl.
- intros. psimpl.
Qed.
Lemma OracleSemiDecidable_semi_decidable {Part : partiality} {X Y} (q : Y -> Prop) (p : X -> Prop) :
decidable q -> OracleSemiDecidable q p -> semi_decidable p.
Proof.
intros [f Hf] (F & Hc & HF).
eapply SemiDecidabilityFacts.semi_decidable_part_iff.
exists unit.
setoid_rewrite HF.
clear HF p.
eapply Turing_transports_computable in Hc as [F' Hc].
specialize (Hc (fun y => ret (f y)) (char_rel q)).
unshelve epose proof (Hc _).
+ red. split; intros.
* psimpl. eapply reflects_iff, Hf.
* eapply ret_hasvalue_iff. cbn in H. eapply reflects_iff in H. specialize (Hf x).
unfold reflects in *. destruct (f x), y; firstorder congruence.
+ clear Hc. unfold pcomputes in H.
exists (fun x => F' (fun y : Y => ret (f y)) x).
intros. rewrite <- H. firstorder. destruct x0; eauto.
Qed.
Lemma red_m_transports_sdec {Part : partiality} {X Y Z} (q : Y -> Prop) (p1 : Z -> Prop) (p2 : X -> Prop) :
OracleSemiDecidable q p2 ->
red_m p1 p2 ->
OracleSemiDecidable q p1.
Proof.
intros [G [HG H1]] [f Hf].
eexists. split.
- eapply computable_bind.
eapply (computable_function f).
eapply computable_precompose with (g := snd). eapply HG.
- cbn. split.
+ intros ? % Hf % H1. eauto.
+ red in Hf. intros. rewrite Hf, H1.
destruct H as (? & ? & ?). subst. eauto.
Qed.
Lemma Turing_transports_sdec {Part : partiality} {X Y Z} (q1 : Y -> Prop) (q2 : Z -> Prop) (p : X -> Prop) :
OracleSemiDecidable q1 p ->
red_Turing q1 q2 ->
OracleSemiDecidable q2 p.
Proof.
intros [G [HG H1]] [F [HF H2]].
eexists. split.
all: cbn.
- eapply computable_comp.
eapply HF. eapply HG.
- intros. rewrite H1.
eapply OracleComputable_extensional in HG. eapply HG.
eauto.
Qed.
Lemma oracle_semi_decidable_complement_iff {Part : partiality} {X} (A : X -> Prop) {Y} (B : Y -> Prop) :
stable B -> OracleSemiDecidable B A <-> OracleSemiDecidable (fun y => ~ B y) A.
Proof.
intros DN.
split.
- intros H. apply (Turing_transports_sdec H), Turing_red_compl. exact DN.
- intros H. apply (Turing_transports_sdec H),compl_Turing_red. exact DN.
Qed.