Section PCP_CFP.
Variable P : SRS.
Definition Sigma := sym P.
Notation "#" := (fresh Sigma).
Definition gamma (A : SRS) := map (fun '(x,y) => (x, rev y)) A.
Lemma sigma_gamma a A :
sigma a (gamma A) = tau1 A ++ a ++ rev (tau2 A).
Proof.
induction A as [ | (x & y) ]; unfold gamma in *; cbn.
- reflexivity.
- rewrite IHA. now simpl_list.
Qed.
Definition palin X (A : list X) := A = rev A.
Lemma tau_eq_iff A a :
~ a el sym A ->
tau1 A = tau2 A <-> palin (sigma a (gamma A)).
Proof.
rewrite sigma_gamma. unfold palin.
simpl_list. intuition.
- now rewrite H0.
- eapply list_prefix_inv in H0; firstorder using tau1_sym, tau2_sym.
Qed.
Lemma gamma_invol A :
gamma (gamma A) = A.
Proof.
induction A as [ | (x,y) ]; cbn.
- reflexivity.
- simpl_list. now rewrite <- IHA at 2.
Qed.
Lemma gamma_mono A B :
A <<= gamma B -> gamma A <<= B.
Proof.
induction A as [ | (x,y) ]; cbn; intros.
- firstorder.
- intros ? [ <- | ].
+ assert ( x/y el gamma B) by firstorder.
unfold gamma in H0. eapply in_map_iff in H0 as ((x',y') & ? & ?).
inv H0. now simpl_list.
+ firstorder.
Qed.
End PCP_CFP.
Theorem PCP_CFP :
PCP ⪯ CFP.
Proof.
exists (fun P => (gamma P, fresh (sym P))).
intros P. split; intros.
- destruct H as (A & Hi & He & H).
exists (gamma A). repeat split.
+ eapply gamma_mono. now rewrite gamma_invol.
+ destruct A; cbn in *; congruence.
+ eapply tau_eq_iff. intros F % (sym_mono (P := P)) % fresh_spec; now try eapply F. eauto.
- destruct H as (B & Hi & He & H).
exists (gamma B). repeat split.
+ now eapply gamma_mono.
+ destruct B; cbn in *; congruence.
+ eapply tau_eq_iff with (a := fresh (sym P)).
* intros F % (sym_mono (P := P)) % fresh_spec. now eapply F. now eapply gamma_mono.
* rewrite gamma_invol. eassumption.
Qed.