From Coq Require Import Lia List Init.Nat.
From PCF2.Autosubst Require Import pcf_2 unscoped.
From PCF2 Require Import preliminaries pcf_2_system pcf_2_utils CE CE_facts SATIS SATIS_facts PS PS_facts.
From PCF2.external Require Import SR.
From PCF2.external.Synthetic Require Import Definitions DecidabilityFacts ReducibilityFacts.
Set Default Goal Selector "!".
Lemma satisfies_rule_enc_ind (t: tm) (v: bool) (enc: str -> tm) (R: list (str * str)) (f g: str * str -> tm) (W0: str) (W: str) :
word_encoding enc v -> ((base_context (2*(length W) + 2)) ++ ((make_rule_types R)) ++ (cons (T W0) nil)) ⊢ t: Base -> fun_rule_encoding enc R f -> fun_rule_encoding enc R g -> satisfies t v enc R f W0 W -> satisfies t v enc R g W0 W.
Proof.
intros word_enc typed_t enc_f enc_g satis_s.
unfold satisfies.
enough (base_context (2 * length W + 2) ⊢ Subst_tm (t_subst enc R f W0 W) t ≡ Subst_tm (t_subst enc R g W0 W) t: Base).
- eapply obs_equiv_rewrite_right with (t := Subst_tm (t_subst enc R f W0 W) t).
4, 5: easy.
{apply basefun_var_applied_typed. fold (T W). eapply enc_typed; eauto. }
all: eapply subst_preserves; eauto; eapply t_subst_well_typed; eauto.
- eapply subst_equiv; eauto.
1, 2: eapply t_subst_well_typed; eauto.
intros n A H. unfold t_subst. destruct (leb n (2 * (length W) + 1)) eqn: e1.
+ rewrite leb_le_true in e1. rewrite nth_error_app1 in H.
* rewrite (base_context_some_base _ _ _ H). apply obs_equiv_refl.
constructor. now rewrite (base_context_some_base _ _ _ H) in H.
* rewrite length_base_context. lia.
+ rewrite leb_le_false in e1. destruct (leb n (2 * (length W) + 1 + length R)) eqn: e2.
* rewrite leb_le_true in e2. destruct (nth_error R (n - (2 * length W + 2))) eqn: e3.
{ rewrite nth_error_app2 in H.
2: rewrite length_base_context; lia.
rewrite nth_error_app1 in H.
- destruct (arith_technical _ _ _ e1 e2) as [n' [eq1 eq2]].
destruct (rule_some n' R eq1) as [r [Hr1 Hr2]]. rewrite length_base_context in H. rewrite eq2 in H.
assert (eq3: 2 * length W + 1 + 1 + n' - (2 * length W + 2) = n') by lia. rewrite eq3 in H. rewrite eq2, eq3 in e3.
rewrite Hr2 in H. injection H. rewrite Hr1 in e3. injection e3. intros ? ?; subst.
assert (H1: In p R). {eapply nth_error_In; eauto. }
unfold fun_rule_encoding in enc_f. rewrite Forall_forall in enc_f. specialize (enc_f p H1).
unfold fun_rule_encoding in enc_g. rewrite Forall_forall in enc_g. specialize (enc_g p H1).
eapply equiv_empty_imp_equiv_nonempty.
1, 2: destruct p; firstorder.
eapply rule_enc_equiv; eauto.
- rewrite length_base_context, make_rule_types_length. lia.
}
rewrite nth_error_None in e3. lia.
* rewrite leb_le_false in e2. destruct (leb n (2 * length W + 2 + length R)) eqn: e3.
-- rewrite leb_le_true in e3.
rewrite nth_error_app2 in H. 2: rewrite length_base_context; lia.
rewrite nth_error_app2 in H. 2: rewrite length_base_context, make_rule_types_length; lia.
assert (eq1: n = 2 * length W + 2 + length R) by lia. rewrite eq1 in H. rewrite length_base_context, make_rule_types_length in H.
assert (eq2: 2 * length W + 2 + length R - (2 * length W + 2) - length R = 0) by lia.
rewrite eq2 in H. cbn in H. assert (A = T W0).
{ cbn in *. now injection H. }
subst. apply equiv_empty_imp_equiv_nonempty.
1, 2: eapply enc_typed; eauto.
eapply obs_equiv_refl. eapply enc_typed; eauto.
-- rewrite leb_le_false in e3.
assert (n < length (base_context (2 * length W + 2) ++ make_rule_types R ++ T W0 :: nil)).
{ rewrite <- nth_error_Some. intros H1. now rewrite H1 in H. }
rewrite app_length, app_length, length_base_context, make_rule_types_length in H0. cbn in H0.
lia.
Qed.
Definition fun_rule_encoding_many (E: list (val_word_enc)) (R: list (str * str)) (g: nat -> str * str -> tm) :=
forall n p, nth_error E n = Some p -> fun_rule_encoding (fst (proj1_sig p)) R (g n).
Lemma fun_rule_enc_exist (enc: str -> tm) (v: bool) (enc_val: word_encoding enc v) (R: list (str * str)):
exists f, fun_rule_encoding enc R f.
Proof.
specialize rules_eq_decidable. intros H. unfold eq_dec in H.
rewrite decidable_iff in H. destruct H as [H].
induction R.
- exists (fun _ => bot). apply Forall_nil.
- destruct IHR as [f Hf].
destruct (rule_enc_exist enc v enc_val a) as [F HF].
exists (fun r => if H (r, a) then F else f r).
apply Forall_cons.
+ destruct (H (a, a)); eauto.
easy.
+ apply Forall_forall. unfold fun_rule_encoding in Hf. rewrite Forall_forall in Hf.
intros r Hr. destruct (H (r, a)).
* cbn in e. now subst.
* now apply Hf.
Qed.
Lemma fun_rule_encoding_many_exist (E: list (val_word_enc)) (R: list (str * str)):
exists g, fun_rule_encoding_many E R g.
Proof.
specialize bool_eq_dec. intros H. unfold eq_dec in H.
rewrite decidable_iff in H. destruct H as [H].
induction E.
- exists (fun _ _ => bot). intros n p Hp. now destruct n.
- destruct IHE as [g Hg]. destruct a as [[enc v] enc_val]. destruct (fun_rule_enc_exist enc v enc_val R) as [f Hf].
exists (fun n => match n with | 0 => f | S n => g n end).
intros n p H'.
destruct n; cbn in *.
+ destruct p as [[a w] a_val]. cbn in *. injection H'. intros eq eq'. subst. easy.
+ unfold fun_rule_encoding_many in Hg. now apply Hg.
Qed.
Definition ps_system_char_bool (n: nat) (s t: tm) (T: ty) (sys: ps_system):=
forall p, In p sys <-> exists l, length l = n /\ (Forall (fun t => is_bval t = true) l) /\ fst p = apply_args s (rev l) /\ snd p = apply_args t l.
Lemma list_val_exist (n: nat):
sig (fun l: list (list tm * list tm) => forall p, In p l <-> exists l', length l' = n /\ (Forall (fun t => is_bval t = true) l') /\ fst p = rev l' /\ snd p = l').
Proof.
induction n.
- exists ((nil, nil) :: nil). intros [p1 p2]. split.
{ intros H. exists nil. firstorder; now injection H. }
intros [l' [H1 [H2 [H4 H5]]]]. rewrite length_zero_iff_nil in H1. subst.
cbn in H4, H5. rewrite H4, H5. cbn. now left.
- destruct IHn as [l H]. exists (map (fun p => (fst p ++ tt :: nil, tt :: snd p)) l ++ map (fun p => (fst p ++ ff :: nil, ff :: snd p)) l ++ map (fun p => (fst p ++ bot :: nil, bot :: snd p)) l).
intros [p1 p2]. split.
+ intros H1. rewrite in_app_iff, in_app_iff in H1.
destruct H1 as [H1 | [H1 | H1]].
* rewrite in_map_iff in H1. destruct H1 as [p [H1 H2]].
rewrite H in H2. destruct H2 as [l' [H3 [H4 [H5 H6]]]].
exists (tt :: l'). firstorder. 1: cbn; congruence.
all: rewrite <- H1; cbn.
1: now rewrite H5. now rewrite H6.
* rewrite in_map_iff in H1. destruct H1 as [p [H1 H2]].
rewrite H in H2. destruct H2 as [l' [H3 [H4 [H5 H6]]]].
exists (ff :: l'). firstorder. 1: cbn; congruence.
all: rewrite <- H1; cbn.
1: now rewrite H5. now rewrite H6.
* rewrite in_map_iff in H1. destruct H1 as [p [H1 H2]].
rewrite H in H2. destruct H2 as [l' [H3 [H4 [H5 H6]]]].
exists (bot :: l'). firstorder. 1: cbn; congruence.
all: rewrite <- H1; cbn.
1: now rewrite H5. now rewrite H6.
+ intros [l' [H1 [H2 [H3 H4]]]]. rewrite in_app_iff, in_app_iff. rewrite in_map_iff, in_map_iff, in_map_iff.
destruct l'. 1: easy. rewrite Forall_cons_iff in H2. destruct t; try easy.
* left. exists (rev l', l'). cbn in *. split. 1: now rewrite H3, H4.
rewrite H. exists l'. now firstorder.
* right. left. exists (rev l', l'). cbn in *. split. 1: now rewrite H3, H4.
rewrite H. exists l'. now firstorder.
* right. right. exists (rev l', l'). cbn in *. split. 1: now rewrite H3, H4.
rewrite H. exists l'. now firstorder.
Qed.
Lemma ps_system_char_bool_exist (n: nat) (s t: tm) (T: ty):
(cons T nil) ⊢ s: (base_fun n Base) -> nil ⊢ t: (base_fun n Base)
-> sig (fun sys => ps_system_well_formed sys T /\ ps_system_char_bool n s t T sys).
Proof.
intros typed_s typed_t.
destruct (list_val_exist n) as [l Hl].
exists (map (fun p => (apply_args s (fst p), apply_args t (snd p))) l).
split.
- unfold ps_system_well_formed. rewrite Forall_forall.
intros [p1 p2] H. cbn. rewrite in_map_iff in H. destruct H as [[l1 l2] [H1 H2]].
rewrite Hl in H2. destruct H2 as [l' [len_l' [H2 [H3 H4]]]]. cbn in H4, H3, H1. subst.
assert (e1: p1 = apply_args s (rev l')) by now injection H1.
assert (e2: p2 = apply_args t l') by now injection H1. subst.
split.
+ eapply base_fun_applied_typed. 1: now simpl_list.
apply Forall_impl with (P := fun t => is_bval t = true). 2: now apply Forall_rev.
intros a Ha. destruct a; easy.
+ eapply base_fun_applied_typed; eauto.
apply Forall_impl with (P := fun t => is_bval t = true). 2: easy.
intros a Ha. destruct a; easy.
- unfold ps_system_char_bool. intros [p1 p2].
split.
+ intros Hp. rewrite in_map_iff in Hp. destruct Hp as [l' [H1 H2]].
rewrite Hl in H2. destruct H2 as [l'' [H3 [H4 [H5 H6]]]]. exists l''. firstorder.
1: rewrite <- H1, H5; now cbn.
rewrite <- H1, H6; now cbn.
+ intros [l' [H1 [H2 [H3 H4]]]]. rewrite in_map_iff.
exists (rev l', l'). firstorder. cbn in *. now rewrite H3, H4.
Qed.
Definition subst_list (l: list tm) :=
fun n =>
if ltb n (length l) then
match nth_error l n with
| None => bot
| Some t => t
end
else var_tm (n - length l).
Lemma subst_list_last (l l': list tm) (t: tm):
(subst_list (l ++ t:: l')) (length l) = t.
Proof.
unfold subst_list. destruct (ltb (length l) (length (l ++ t :: l'))) eqn: e.
- rewrite ltb_lt_true in e. assert (nth_error (l ++ t :: l') (length l) = Some t).
+ clear e. induction l.
* easy.
* cbn. eapply IHl.
+ now rewrite H.
- rewrite ltb_lt_false in e. rewrite app_length in e. cbn in e. lia.
Qed.
Lemma subst_list_subst' (t: tm) (l m: list tm):
closed t -> (Forall closed l) -> Subst_tm (subst_list (l ++ m)) (apply_args t (var_seq 0 (length l))) = apply_args t l.
Proof.
intros closed_t closed_l. induction (length l) eqn: e in t, l, m, closed_t, closed_l |-*.
- cbn. rewrite length_zero_iff_nil in e. subst. now rewrite closed_subst.
- assert (H: l <> nil). 1: intros H; rewrite <- length_zero_iff_nil in H; lia.
specialize (exists_last H). intros [l' [a Hl']]. rewrite <- e.
rewrite Hl'. rewrite apply_args_app.
simpl_list. rewrite var_seq_split. rewrite apply_args_app. cbn.
assert (H1: (l' ++ a :: nil) ++ m = l' ++ a :: m).
+ rewrite <- app_assoc. now cbn.
+ rewrite H1. rewrite subst_list_last.
enough (H2: Subst_tm (subst_list (l' ++ a :: m)) (apply_args t (var_seq 0 (length l'))) = apply_args t l') by now rewrite H2.
assert (H2: length l' = n).
{ rewrite Hl', app_length in e. cbn in e. lia. }
rewrite H2. apply IHn; eauto.
rewrite Forall_forall in closed_l.
rewrite Forall_forall. intros x H3. apply closed_l.
rewrite Hl'. apply in_or_app. now left.
Qed.
Lemma subst_list_subst (t: tm) (l: list tm):
closed t -> (Forall closed l) -> Subst_tm (subst_list l) (apply_args t (var_seq 0 (length l))) = apply_args t l.
Proof.
intros H1 H2. assert (H: l = l ++ nil) by now simpl_list.
rewrite H at 1. now rewrite subst_list_subst'.
Qed.
Lemma subst_list_shift (l: list tm) (a: tm) (t: tm):
Subst_tm (scons a ids) (Subst_tm (up_tm_tm (subst_list l)) t) = Subst_tm (subst_list (a :: l)) t.
Proof.
asimpl. apply subst_charact. intros n. destruct n.
- unfold subst_list. asimpl. destruct (ltb 0 (length (a :: l))) eqn: e1.
1: easy. rewrite ltb_lt_false in e1. cbn in e1. lia.
- unfold subst_list. asimpl. destruct (ltb n (length l)) eqn: e1.
+ rewrite ltb_lt_true in e1.
destruct (ltb (S n) (length (a :: l))) eqn: e2.
* rewrite ltb_lt_true in e2. cbn. destruct (nth_error l n) eqn: e3.
all: easy.
* rewrite ltb_lt_false in e2. cbn in e2. lia.
+ rewrite ltb_lt_false in e1. destruct (ltb (S n) (length (a :: l))) eqn: e2.
* rewrite ltb_lt_true in e2. cbn in e2. lia.
* easy.
Qed.
Lemma subst_nil_ids t:
Subst_tm (subst_list nil) t = t.
Proof.
assert (H: Subst_tm ids t = t) by now asimpl.
rewrite <- H at 2. apply subst_charact. intro n. unfold subst_list.
cbn. assert (H1: n - 0 = n) by lia. rewrite H1. easy.
Qed.
Lemma lam_args_subst (t: tm) (l: list tm):
apply_args (lam_T (length l) t) (rev l) ≻* Subst_tm (subst_list l) t.
Proof.
induction l in t |-*.
1: now rewrite subst_nil_ids.
assert (eq1: rev (a :: l) = rev l ++ a :: nil) by now simpl_list.
rewrite eq1, apply_args_app. assert (eq2: length (a :: l) = length l + 1). 1: cbn; lia.
rewrite eq2, lam_T_split. eapply steps_PreOrder.
- apply apply_args_steps_body. rewrite IHl. constructor 2.
- cbn. rewrite Beta. now rewrite subst_list_shift.
Qed.
Lemma t_subst_char (enc: str -> tm) (R: list (str * str)) (f: str * str -> tm) (W0 W: str) v:
word_encoding enc v -> fun_rule_encoding enc R f ->
forall n A, nth_error (base_context (2 * length W + 2) ++ make_rule_types R ++ T W0 :: nil) n = Some A -> (iter (2 * length W + 2) Up_tm_tm (subst_list (map f R ++ (enc W0 :: nil)))) n = (t_subst enc R f W0 W) n.
Proof.
intros enc_val H n A H'.
unfold t_subst. destruct (leb n (2 * length W + 1)) eqn: e1.
- rewrite leb_le_true in e1. rewrite up_tm_tm_iter1. 2: lia. easy.
- rewrite leb_le_false in e1. destruct (leb n (2 * length W + 1 + length R)) eqn: e2.
+ rewrite leb_le_true in e2. destruct (nth_error R (n - (2 * length W + 2))) eqn: e.
* rewrite up_tm_tm_iter2. 2: lia. destruct (arith_technical _ _ _ e1 e2) as [n' [H1 H2]].
rewrite H2. rewrite H2 in e. assert (eq: (2 * length W + 1 + 1 + n' - (2 * length W + 2)) = n') by lia.
rewrite eq in *. unfold subst_list. destruct (ltb n' (length (map f R ++ enc W0 :: nil))) eqn: e3.
{ rewrite ltb_lt_true in e3. destruct (nth_error (map f R ++ enc W0 :: nil) n') eqn: e'.
- rewrite nth_error_app1 in e'.
+ destruct (rule_some _ _ H1) as [r [Hr1 Hr2]].
rewrite nth_error_nth' with (d := f (nil, nil)) in e' .
2: rewrite map_length; lia. erewrite map_nth in e'. rewrite Hr1 in e. injection e. intros H3.
rewrite (@nth_error_nth' (str * str)) with (d := (nil, nil)) in Hr1. 2: lia.
injection Hr1. intro H4. rewrite H4 in e'. injection e'. intros eq'.
rewrite <- eq'. rewrite <- H3. unfold fun_rule_encoding in H.
rewrite iter_ren_closed. 1: easy. eapply typed_empty_closed.
assert (H5: rule_encoding enc r (f r)).
* rewrite Forall_forall in H. apply H. eapply nth_error_In. rewrite <- nth_error_nth' in Hr1. 2: lia. eauto.
* destruct H5. eauto.
+ simpl_list. lia.
- rewrite nth_error_None in e'. lia. }
rewrite ltb_lt_false in e3. rewrite app_length, map_length in e3. lia.
* rewrite nth_error_None in e. lia.
+ rewrite leb_le_false in e2. destruct (leb n (2 * length W + 2 + length R)) eqn: e3.
* rewrite up_tm_tm_iter2. 2: lia. assert (n = 2 * length W + 2 + length R).
{ assert (n < length (base_context (2 * length W + 2) ++ make_rule_types R ++ T W0 :: nil)).
1: apply nth_error_Some; intros H1; now rewrite H1 in H'.
rewrite app_length, app_length, length_base_context, make_rule_types_length in H0. cbn in H0. lia. }
assert (H1: n - (2 * length W + 2) = length R). 1: lia.
rewrite H1. unfold subst_list. destruct (ltb (length R) (length (map f R ++ enc W0 :: nil))) eqn: e4.
-- destruct (nth_error (map f R ++ enc W0 :: nil) (length R)) eqn: e.
++ rewrite nth_error_app2 in e. 2: rewrite map_length; lia.
rewrite map_length in e. assert (H2: length R - length R = 0) by lia.
rewrite H2 in e. cbn in e. injection e. intros ?; subst.
rewrite iter_ren_closed. 1: easy. eapply typed_empty_closed. eapply enc_typed; eauto.
++ rewrite nth_error_None in e. rewrite ltb_lt_true in e4. lia.
-- rewrite ltb_lt_false, app_length, map_length in e4. cbn in e4. lia.
* rewrite leb_le_false in e3. assert (eq: n < length (base_context (2 * length W + 2) ++ make_rule_types R ++ T W0 :: nil)).
-- apply nth_error_Some. intros H1. now rewrite H1 in H'.
-- rewrite app_length, app_length, make_rule_types_length, length_base_context in eq. cbn in eq. lia.
Qed.
Lemma subst_bool_var (σ: nat -> tm) (n: nat):
nil ⊢ σ [base_context n] -> exists l, length l = n /\ (Forall (fun t => is_bval t = true) l) /\ (forall n' v, nth_error l n' = Some v -> σ n' ≻* v).
Proof.
intros subst_wt. induction n in σ, subst_wt |-*.
- exists nil. firstorder. now destruct n'.
- assert (nil ⊢ σ [base_context n]).
+ intros n' T HT. apply subst_wt. assert (n' < length (base_context (S n))).
* rewrite <- nth_error_Some. intros H'. rewrite nth_error_None in H'.
assert (nth_error (base_context n) n' <> None) by now destruct (nth_error (base_context n) n').
rewrite nth_error_Some in H. rewrite length_base_context in H, H'. lia.
* rewrite <- nth_error_Some in H. destruct (nth_error (base_context (S n)) n') eqn: e.
2: easy. rewrite (base_context_some_base n n' T). 2: easy. rewrite (base_context_some_base (S n) n' t); easy.
+ specialize (IHn σ H). destruct IHn as [l [l_len [Hl1 Hl2]]].
assert (H1: nil ⊢ σ n: Base).
{apply subst_wt. assert (H1: n < length (base_context (S n))).
- rewrite length_base_context; lia.
- rewrite <- nth_error_Some in H1. destruct (nth_error (base_context (S n)) n) eqn: e. 2: try easy.
rewrite (base_context_some_base (S n) n t); easy.
}
destruct (weak_normalisation_comp (σ n) H1) as [v [eval_v v_val]]. destruct v; try easy.
* exists (l ++ tt :: nil). split. 1: simpl_list; cbn; rewrite l_len; lia.
split.
-- rewrite Forall_app. firstorder.
-- intros n' v' H3. destruct (ltb n' (length l)) eqn: e.
++ rewrite ltb_lt_true in e. rewrite nth_error_app1 in H3.
2: easy. now apply Hl2.
++ rewrite ltb_lt_false in e. rewrite nth_error_app2 in H3.
2: easy. assert (n' = n).
{ assert (H4: nth_error (tt :: nil) (n' - length l) <> None) by now destruct (nth_error (tt :: nil) (n' - length l)).
rewrite nth_error_Some in H4. cbn in H4. lia. }
subst. assert (H4: length l - length l = 0) by lia.
rewrite H4 in H3. cbn in H3. injection H3; intros eq; subst.
firstorder.
* exists (l ++ ff :: nil). split. 1: simpl_list; cbn; rewrite l_len; lia.
split.
-- rewrite Forall_app. firstorder.
-- intros n' v' H3. destruct (ltb n' (length l)) eqn: e.
++ rewrite ltb_lt_true in e. rewrite nth_error_app1 in H3.
2: easy. now apply Hl2.
++ rewrite ltb_lt_false in e. rewrite nth_error_app2 in H3.
2: easy. assert (n' = n).
{ assert (H4: nth_error (ff :: nil) (n' - length l) <> None) by now destruct (nth_error (ff :: nil) (n' - length l)).
rewrite nth_error_Some in H4. cbn in H4. lia. }
subst. assert (H4: length l - length l = 0) by lia.
rewrite H4 in H3. cbn in H3. injection H3; intros eq; subst.
firstorder.
* exists (l ++ bot :: nil). split. 1: simpl_list; cbn; rewrite l_len; lia.
split.
-- rewrite Forall_app. firstorder.
-- intros n' v' H3. destruct (ltb n' (length l)) eqn: e.
++ rewrite ltb_lt_true in e. rewrite nth_error_app1 in H3.
2: easy. now apply Hl2.
++ rewrite ltb_lt_false in e. rewrite nth_error_app2 in H3.
2: easy. assert (n' = n).
{ assert (H4: nth_error (bot :: nil) (n' - length l) <> None) by now destruct (nth_error (bot :: nil) (n' - length l)).
rewrite nth_error_Some in H4. cbn in H4. lia. }
subst. assert (H4: length l - length l = 0) by lia.
rewrite H4 in H3. cbn in H3. injection H3; intros eq; subst.
firstorder.
Qed.
Lemma fun_rule_enc_rev enc R f:
fun_rule_encoding enc R f -> fun_rule_encoding enc (rev R) f.
Proof.
intros H. now apply Forall_rev.
Qed.
Definition ps_system_type (W0: str) (W: str) (R: list(str * str)) :=
T W0 ⟶ rule_fun (rev R) (T W).
Definition ps_system_char_enc (enc: str -> tm) (v: bool) (enc_val: word_encoding enc v) (R: list (str * str)) (f: str * str -> tm) (W0: str) (W: str) (sys: ps_system) :=
(forall t, ((base_context (2*(length W) + 2)) ++ ((make_rule_types R)) ++ (cons (T W0) nil)) ⊢ t: Base -> satisfies t v enc R f W0 W -> solves_ps_system sys (lam_T (2 * length W + length R + 3) t))
/\ (forall sol, nil ⊢ sol : ps_system_type W0 W R -> solves_ps_system sys sol -> satisfies (apply_args sol (rev (var_seq 0 (2 * length W + length R + 3)))) v enc R f W0 W).
Lemma ps_system_char_enc_exist (enc: str -> tm) (v: bool) (enc_val: word_encoding enc v) (R: list (str * str)) (f: str * str -> tm) (W0: str) (W: str):
fun_rule_encoding enc R f ->
sig (fun sys: ps_system => ps_system_well_formed sys (ps_system_type W0 W R) /\ ps_system_char_enc enc v enc_val R f W0 W sys).
Proof.
intros f_enc.
assert (H: sig (fun sys => ps_system_well_formed sys (ps_system_type W0 W R) /\ ps_system_char_bool (2*(length W) + 2) (apply_args (var_tm 0) ((enc W0) :: (map f (rev R)))) (enc W) (ps_system_type W0 W R) sys)).
- apply ps_system_char_bool_exist.
+ rewrite apply_args_cons.
assert ((ps_system_type W0 W R :: nil) ⊢ app (var_tm 0) (enc W0): (rule_fun (rev R) (T W))).
* eapply app_typed with (typ1 := T W0). 1: now constructor.
assert (H1: ps_system_type W0 W R :: nil = nil ++ ps_system_type W0 W R :: nil) by easy.
rewrite H1. apply type_weakening. eapply enc_typed; eauto.
* eapply apply_args_typed with (l1 := (make_rule_types (rev R))).
1: unfold rule_fun in H; easy.
1: unfold make_rule_types; now rewrite map_length, map_length.
intros n A' t' H1 H2. assert (H3: n < length (rev R)).
{ assert (H3: nth_error (map f (rev R)) n <> None) by now destruct (nth_error (map f (rev R)) n). rewrite nth_error_Some in H3. now rewrite map_length in H3. }
destruct (rule_some _ _ H3) as [r [Hr1 Hr2]]. erewrite nth_error_map, Hr1 in H2.
cbn in H2. injection H2. intros ?; subst. rewrite Hr2 in H1; injection H1; intros ?; subst.
assert (H4: ps_system_type W0 W R :: nil = nil ++ ps_system_type W0 W R :: nil) by easy.
rewrite H4. apply type_weakening. enough (H5: rule_encoding enc r (f r)) by now destruct H5.
unfold fun_rule_encoding in f_enc.
rewrite Forall_forall in f_enc. apply f_enc. apply In_rev. eapply nth_error_In; eauto.
+ now eapply enc_typed.
- destruct H as [sys [sys_wf Hsys]].
exists sys. split. 1: easy. split.
+ intros t typed_t H_t. eapply Forall_forall. intros [p1 p2] H1.
specialize (Hsys (p1, p2)). rewrite Hsys in H1.
destruct H1 as [l [l_len [con_val [eq_1 eq_2]]]].
specialize (Forall_rev con_val). intros con_val_rev.
rewrite eq_1, eq_2.
assert (subst_wt: nil ⊢ subst_list l [base_context (2 *length W + 2)]).
{rewrite <- l_len. intros n p Hp. unfold subst_list. destruct (ltb n (length l)) eqn: e.
- destruct (nth_error l n) eqn: e'.
+ rewrite Forall_forall in con_val. specialize (con_val t0 (nth_error_In _ _ e')).
enough (p = Base). {subst. now destruct t0. }
eapply base_context_some_base; eauto.
+ rewrite nth_error_None in e'.
rewrite ltb_lt_true in e. lia.
- rewrite ltb_lt_false in e.
assert (n < length (base_context (length l))).
+ apply nth_error_Some. intros e'. now rewrite e' in Hp.
+ rewrite length_base_context in H. lia. }
specialize (H_t (subst_list l) subst_wt). rewrite <- l_len in H_t. cbn in H_t. rewrite <- (rev_length l) in H_t.
rewrite rev_length, (subst_list_subst (enc W) l) in H_t.
2: eapply typed_empty_closed; eapply enc_typed; eauto.
2: now eapply val_list_closed.
rewrite subst_apply_args. rewrite subst_map_closed_list.
2: now eapply val_list_closed.
rewrite subst_apply_args. rewrite subst_map_closed_list.
2: now eapply rule_enc_word_enc_closed'.
asimpl. enough (H: apply_args (apply_args (lam_T (2 * length W + length R + 3) t) ((enc W0) :: (map f (rev R)))) (rev l) ≻* Subst_tm (subst_list l) (Subst_tm (t_subst enc R f W0 W) t)) by now rewrite H.
assert (eq1: 2 * length W + length R + 3 = (length R + 1) + (2 * length W + 2)) by lia.
rewrite eq1, lam_T_split. assert (eq2: length (map f R ++ (enc W0 :: nil)) = length R + 1).
{ simpl_list. cbn. lia. }
rewrite <- eq2. eapply steps_PreOrder.
* eapply apply_args_steps_body. assert (H1: (enc W0) :: (map f (rev R)) = rev((map f R) ++ (enc W0 :: nil))).
{ simpl_list. now rewrite <- map_rev. }
rewrite H1.
apply lam_args_subst.
* rewrite lam_T_shift_subst. rewrite <- l_len. assert (H1: l = rev (rev l)) by now simpl_list.
rewrite lam_args_subst.
enough (H2: Subst_tm (iter (length l) Up_tm_tm (subst_list (map f R ++ (enc W0 :: nil)))) t = Subst_tm (t_subst enc R f W0 W) t).
{ rewrite H2; constructor 2. }
eapply subst_charact_typed. 1: exact typed_t. rewrite l_len. eapply t_subst_char; eauto.
+ intros sol typed_sol Hsol σ subst_wt. rewrite subst_apply_args.
rewrite closed_subst. 2: eapply typed_empty_closed; now apply (enc_typed _ v).
assert (H1: rev (var_seq 0 (2 * length W + length R + 3)) = rev (var_seq (2 * length W + 2) (length R + 1)) ++ rev (var_seq 0 (2 * length W + 2))).
{ assert (eq: 2 * length W + length R + 3 = 2 * length W + 2 + (length R + 1)) by lia.
now rewrite eq, var_seq_split, rev_app_distr. }
rewrite H1, apply_args_app.
rewrite subst_apply_args. rewrite t_subst_map_var_id'. rewrite subst_apply_args, subst_apply_args.
rewrite t_subst_map_var_rules'. rewrite (closed_subst sol). 2: eapply typed_empty_closed; eauto.
rewrite subst_apply_args. rewrite (closed_subst sol). 2: eapply typed_empty_closed; eauto.
rewrite (subst_map_closed_list _ ((enc W0) :: (map f (rev R)))).
2: now eapply rule_enc_word_enc_closed'.
destruct (subst_bool_var σ (2 * length W + 2) subst_wt) as [l [l_len [l_val Hl]]].
assert (H2: length (map (Subst_tm σ) (var_seq 0 (2 * length W + 2))) = length l).
{simpl_list. now rewrite length_var_seq. }
assert (H3: forall (n : nat) (t t' : tm), nth_error (map (Subst_tm σ) (var_seq 0 (2 * length W + 2))) n = Some t -> nth_error l n = Some t' -> t ≻* t').
{intros n t t' Ht Ht'.
enough (t = σ n).
{ subst. now eapply Hl. }
assert (nth_error l n <> None).
{ intro H; now rewrite H in Ht'. }
rewrite nth_error_Some in H. specialize (var_seq_map_nth _ 0 _ σ H).
intros H'. rewrite l_len in H'. rewrite H' in Ht. now injection Ht. }
erewrite (apply_args_steps_list _ _ l); eauto.
erewrite (apply_args_steps_list _ (map (Subst_tm σ) (rev (var_seq 0 (2 * length W + 2)))) (rev l)); eauto.
{enough (In (apply_args (apply_args (var_tm 0) (enc W0 :: map f (rev R))) (rev l), apply_args (enc W) l) sys).
- unfold solves_ps_system in Hsol. rewrite Forall_forall in Hsol. specialize (Hsol (apply_args (apply_args (var_tm 0) (enc W0 :: map f (rev R))) (rev l), apply_args (enc W) l) H).
cbn in Hsol. assert (H4: fold_right (fun arg t : tm => app t arg) (var_tm 0) (rev (map f (rev R)) ++ enc W0 :: nil) = apply_args (var_tm 0) (enc W0 :: map f (rev R))).
1: now cbn.
rewrite H4 in Hsol.
rewrite subst_apply_args in Hsol. rewrite subst_map_closed_list in Hsol.
2: apply Forall_rev; now eapply val_list_closed.
rewrite subst_apply_args in Hsol. rewrite subst_map_closed_list in Hsol.
2: now eapply rule_enc_word_enc_closed'.
now asimpl in Hsol.
- destruct (Hsys (apply_args (apply_args (var_tm 0) (enc W0 :: map f (rev R))) (rev l), apply_args (enc W) l)). cbn in *.
apply H0. exists l. split. 1: easy.
split; easy. }
1: simpl_list; now rewrite l_len, length_var_seq.
intros n t t' Ht Ht'.
assert (map (Subst_tm σ) (var_seq 0 (2 * length W + 2)) = rev (rev (map (Subst_tm σ) (var_seq 0 (2 * length W + 2))))) by now simpl_list.
eapply H3 with (n := 2 * length W + 2 - S n).
* assert ((var_seq 0 (2 * length W + 2)) = rev (rev (var_seq 0 (2 * length W + 2)))) by now simpl_list.
rewrite H. rewrite <- (length_var_seq (2 * length W + 2) 0) at 2. rewrite <- (map_length (Subst_tm σ)), <- (rev_length (map (Subst_tm σ) (var_seq 0 (2 * length W + 2)))).
rewrite <- rev_nth_error1. 1: now rewrite <- map_rev. 1: exact bot.
rewrite <- map_rev. rewrite <- nth_error_Some. intros ?. now destruct (nth_error (map (Subst_tm σ) (rev (var_seq 0 (2 * length W + 2))))).
* rewrite <- Ht'. rewrite <- rev_nth_error2. 1: now rewrite l_len. 1: exact bot.
rewrite <- rev_length. apply nth_error_Some. intros ?. now destruct (nth_error (rev l) n).
Qed.
Lemma ps_system_char_SATIS (E: list (val_word_enc)) (R: list (str * str)) (g: nat -> str * str -> tm) (W0: str) (W: str):
fun_rule_encoding_many E R g ->
sig (fun sys: ps_system => ps_system_well_formed sys (ps_system_type W0 W R) /\
(forall t, (base_context (2 * length W + 2) ++ make_rule_types R ++ T W0 :: nil) ⊢ t : Base -> (forall n p, nth_error E n = Some p -> satisfies t (snd (proj1_sig p)) (fst (proj1_sig p)) R (g n) W0 W) -> solves_ps_system sys (lam_T (2 * length W + length R + 3) t))
/\ (forall sol, nil ⊢ sol : ps_system_type W0 W R -> solves_ps_system sys sol -> forall n p, nth_error E n = Some p -> satisfies (apply_args sol (rev (var_seq 0 (2 * length W + length R + 3)))) (snd (proj1_sig p)) (fst (proj1_sig p)) R (g n) W0 W)).
Proof.
intro H. induction E in g, H |-*.
- exists nil. split.
1: apply Forall_nil.
split.
+ intros. apply Forall_nil.
+ intros. now destruct n.
- assert (fun_rule_encoding_many E R (fun n => g (S n))).
+ intros n p Hp. apply H. firstorder.
+ specialize (IHE _ H0). assert (fun_rule_encoding (fst (proj1_sig a)) R (g 0)) by now eapply H.
specialize (ps_system_char_enc_exist (fst (proj1_sig a)) (snd (proj1_sig a)) (proj2_sig a) R (g 0) W0 W H1).
intros [sys' [Hsys'1 Hsys'2]]. destruct IHE as [sys [Hsys1 Hsys2]].
exists (sys ++ sys').
split.
* unfold ps_system_well_formed. now rewrite Forall_app.
* destruct Hsys2 as [Hsys2 Hsys3]. destruct Hsys'2 as [Hsys'2 Hsys'3]. split.
-- intros t typed_t H2. unfold solves_ps_system. rewrite Forall_app.
split.
** apply Hsys2. 1: easy. intros n p Hp. now apply H2.
** apply Hsys'2. 1: easy. now eapply H2.
-- intros sol typed_sol Hsol n p Hp. unfold solves_ps_system in Hsol. rewrite Forall_app in Hsol. destruct n.
** cbn in Hp. inv Hp. apply Hsys'3; easy.
** now apply Hsys3.
Qed.
Lemma ps_system_type_list_to_fun_rev W0 W R:
ps_system_type W0 W R = list_to_fun (rev ((base_context (2*(length W) + 2)) ++ ((make_rule_types R)) ++ (cons (T W0) nil))) Base.
Proof.
unfold ps_system_type. rewrite rev_app_distr, rev_app_distr. rewrite <- app_assoc. rewrite list_to_fun_app'.
unfold rule_fun. rewrite list_to_fun_app'.
enough (H: T W = list_to_fun (rev (base_context (2 * length W + 2))) Base).
- rewrite H. unfold make_rule_types. rewrite <- map_rev. easy.
- now rewrite base_context_rev, T_list_to_fun.
Qed.
Lemma reduces_SATIS_PS:
forall E R, reduces (SATIS E R) PS.
Proof.
intros E R. destruct (fun_rule_encoding_many_exist E R) as [g Hg].
exists (fun '(W0, W) => let sys: ps_system := proj1_sig (ps_system_char_SATIS E R g W0 W Hg) in
let sys_wf := match proj2_sig (ps_system_char_SATIS E R g W0 W Hg) with conj H' _ => H' end
in exist _ (sys, (ps_system_type W0 W R)) sys_wf); cbn.
intros [W0 W]. assert (len: length ((base_context (2*(length W) + 2)) ++ ((make_rule_types R)) ++ (cons (T W0) nil)) = 2 * length W + length R + 3).
{simpl_list. unfold make_rule_types. rewrite length_base_context, map_length. cbn. lia. }
destruct (ps_system_char_SATIS E R g W0 W Hg) as [sys [sys_wf [Hsys Hsys']]]; cbn. split.
- intros H1. unfold ps_system_solvable. destruct H1 as [t [Ht Ht']]. exists (lam_T (2* length W + length R + 3) t). split.
+ cbn. fold (iter (length W + (length W + 0) + length R + 3) (fun t => lam t) t). assert (H1: iter (length W + (length W + 0) + length R + 3) (fun t => lam t) t = lam_T (2 * length W + length R + 3) t) by easy.
rewrite H1. rewrite ps_system_type_list_to_fun_rev.
rewrite <- len. now apply lam_list_to_type.
+ apply Hsys. 1: easy. intros n p Hp. rewrite Forall_forall in Ht'. eapply Ht'.
1: eapply nth_error_In. all: eauto.
- intros [sol [typed_sol Hsol]]. exists (apply_args sol (rev (var_seq 0 (2 * length W + length R + 3)))).
split.
+ rewrite <- len. apply fun_rev_to_context. now rewrite <- ps_system_type_list_to_fun_rev.
+ rewrite Forall_forall. intros p Hp f f_enc. destruct (In_nth_error _ _ Hp) as [n Hn]. specialize (Hsys' sol typed_sol Hsol n p Hn). eapply satisfies_rule_enc_ind with (f := g n); eauto.
* destruct p. now cbn.
* rewrite <- len. apply fun_rev_to_context. now rewrite <- ps_system_type_list_to_fun_rev.
Qed.
Lemma reduces_co_SATIS_co_PS:
forall E R, reduces (complement (SATIS E R)) (complement PS).
Proof.
intros E R. apply reduces_complement. apply reduces_SATIS_PS.
Qed.