*Some basic things concerning lists
Lemma list_prefix_inv X (a : X) x u y v :
~ a el x -> ~ a el u -> x ++ a :: y = u ++ a :: v -> x = u /\ y = v.
Proof.
intro. revert u.
induction x; intros; destruct u; inv H1; try now firstorder.
eapply IHx in H4; try now firstorder. intuition congruence.
Qed.
Lemma split_inv X (u z x y : list X) (s : X) :
u ++ z = x ++ s :: y -> ~ s el u -> exists x' : list X, x = u ++ x'.
Proof.
revert u. induction x; cbn; intros.
- destruct u. cbn. eauto. inv H. firstorder.
- destruct u. cbn. eauto.
inv H. edestruct IHx. cbn. rewrite H3. reflexivity. firstorder. subst. cbn. eauto.
Qed.
Lemma in_split X (a : X) (x : list X) :
a el x -> exists y z, x = y ++ [a] ++ z.
Proof.
induction x; cbn; intros.
- firstorder.
- destruct H as [-> | ].
+ now exists [], x.
+ destruct (IHx H) as (y & z & ->).
now exists (a0 :: y), z.
Qed.
Definition reduces X Y (p : X -> Prop) (q : Y -> Prop) := exists f : X -> Y, forall x, p x <-> q (f x).
Notation "p ⪯ q" := (reduces p q) (at level 50).
Lemma reduces_transitive X Y Z (p : X -> Prop) (q : Y -> Prop) (r : Z -> Prop) :
p ⪯ q -> q ⪯ r -> p ⪯ r.
Proof.
intros [f ?] [g ?]. exists (fun x => g (f x)). firstorder.
Qed.
Definition symbol := nat.
Definition string := list symbol.
Definition card : Type := string * string.
Definition stack := list card.
Definition SRS := stack.
Notation "x / y" := (x,y).
Implicit Types a b : symbol.
Implicit Types x y z : string.
Implicit Types d e : card.
Implicit Types A R P : stack.
Coercion sing (n : nat) := [n].
Fixpoint tau1 (A : stack) :=
match A with
| [] => []
| (x / y) :: A => x ++ tau1 A
end.
Fixpoint tau2 (A : stack) :=
match A with
| [] => []
| (x / y) :: A => y ++ tau2 A
end.
Lemma tau1_app A B : tau1 (A ++ B) = tau1 A ++ tau1 B.
Proof.
induction A; cbn; try destruct _; simpl_list; congruence.
Qed.
Lemma tau2_app A B : tau2 (A ++ B) = tau2 A ++ tau2 B.
Proof.
induction A; cbn; try destruct _; simpl_list; congruence.
Qed.
Definition cards x := map (fun a => [a] / [a]) x.
Lemma tau1_cards x : tau1 (cards x) = x.
Proof.
induction x; cbv in *; try rewrite IHx; trivial.
Qed.
Lemma tau2_cards x : tau2 (cards x) = x.
Proof.
induction x; cbv in *; try rewrite IHx; trivial.
Qed.
Hint Rewrite tau1_app tau2_app tau1_cards tau2_cards : list.
Inductive rew (R : SRS) : string -> string -> Prop :=
rewB x y u v : u / v el R -> rew R (x ++ u ++ y) (x ++ v ++ y).
Inductive rewt (R : SRS) : string -> string -> Prop :=
rewR z : rewt R z z
| rewS x y z : rew R x y -> rewt R y z -> rewt R x z.
Lemma rewt_induct :
forall (R : SRS) z (P : string -> Prop),
(P z) ->
(forall x y : string, rew R x y -> rewt R y z -> P y -> P x) -> forall s, rewt R s z -> P s.
Proof.
intros. induction H1; firstorder.
Qed.
Scheme rewt_ind' := Induction for rewt Sort Prop.
Instance PreOrder_rewt R : PreOrder (rewt R).
Proof.
split.
- econstructor.
- hnf. intros. induction H; eauto using rewt.
Qed.
Lemma rewt_app_L R x x' y : rewt R x x' -> rewt R (y ++ x) (y ++ x').
Proof.
induction 1. reflexivity.
inv H.
replace (y ++ x0 ++ u ++ y1) with ((y ++ x0) ++ u ++ y1).
econstructor. econstructor. eassumption. simpl_list. eassumption.
now simpl_list.
Qed.
Instance Proper_rewt R : Proper (rewt R ==> rewt R ==> rewt R) (@app symbol).
Proof.
hnf. intros. hnf. intros. induction H.
- now eapply rewt_app_L.
- inv H. transitivity (x1 ++ u ++ (y1 ++ x0)). now simpl_list.
econstructor. econstructor. eassumption. rewrite <- IHrewt. now simpl_list.
Qed.
Lemma rewt_subset R P x y :
rewt R x y -> R <<= P -> rewt P x y.
Proof.
induction 1; intros.
- reflexivity.
- inv H. eauto using rewt, rew.
Qed.
Lemma rewt_left R x y z :
rewt R x y -> rew R y z -> rewt R x z.
Proof.
induction 1; eauto using rewt.
Qed.
Fixpoint sym (R : SRS) :=
match R with
[] => []
| x / y :: R => x ++ y ++ sym R
end.
Lemma sym_app P R :
sym (P ++ R) = sym P ++ sym R.
Proof.
induction P as [ | [] ]; eauto; cbn; rewrite IHP. now simpl_list.
Qed.
Lemma sym_map X (f : X -> card) l Sigma :
(forall x : X, x el l -> sym [f x] <<= Sigma) -> sym (map f l) <<= Sigma.
Proof.
intros. induction l as [ | ]; cbn in *.
- firstorder.
- pose proof (H a). destruct _. repeat eapply incl_app; eauto.
Qed.
Lemma sym_word_l R u v :
u / v el R -> u <<= sym R.
Proof.
induction R; cbn; intros.
- eauto.
- destruct a as (u', v'). destruct H; try inv H; eauto.
Qed.
Lemma sym_word_R R u v :
u / v el R -> v <<= sym R.
Proof.
induction R; cbn; intros.
- eauto.
- destruct a as (u', v'). destruct H; try inv H; eauto.
Qed.
Hint Resolve sym_word_l sym_word_R.
Lemma sym_mono A P :
A <<= P -> sym A <<= sym P.
Proof.
induction A as [ | (x,y) ]; cbn; intros.
- firstorder.
- repeat eapply incl_app.
+ eapply sym_word_l. firstorder.
+ eapply sym_word_R. firstorder.
+ firstorder.
Qed.
Lemma tau1_sym A : tau1 A <<= sym A.
Proof.
induction A as [ | (x & y) ].
- firstorder.
- cbn. eauto.
Qed.
Lemma tau2_sym A : tau2 A <<= sym A.
Proof.
induction A as [ | (x & y) ].
- firstorder.
- cbn. eauto.
Qed.
Lemma rewt_sym R x y Sigma:
sym R <<= Sigma -> x <<= Sigma -> rewt R x y -> y <<= Sigma.
Proof.
intros. induction H1.
- eauto.
- inv H1. eapply IHrewt. repeat eapply incl_app; eauto.
intros ? ?. eapply H. eapply sym_word_R; eauto.
Qed.
Fixpoint fresh (l : list nat) :=
match l with
| [] => 0
| x :: l => S x + fresh l
end.
Lemma fresh_spec' l a : a el l -> a < fresh l.
Proof.
induction l.
- firstorder.
- cbn; intros [ | ]; firstorder omega.
Qed.
Lemma fresh_spec (a : symbol) (l : string) : a el l -> fresh l <> a.
Proof.
intros H % fresh_spec'. intros <-. omega.
Qed.
Definition SRH '(R, x, a) := exists y, rewt R x y /\ a el y.
Definition SR '(R, x, y) := rewt R x y.
Definition PCP P := exists A : SRS, A <<= P /\ A <> [] /\ tau1 A = tau2 A.
Definition MPCP '((x,y), P) := exists A : SRS, A <<= x/y :: P /\ x ++ tau1 A = y ++ tau2 A.
Definition CFP '(R, a) := exists A : SRS, A <<= R /\ A <> [] /\ sigma a A = rev (sigma a A).
Definition CFI '(R1, R2, a) := exists A1 A2, A1 <<= R1 /\ A2 <<= R2 /\ A1 <> [] /\ A2 <> [] /\ sigma a A1 = sigma a A2.