# Library ExampleABA

We construct the TRS with one rule

ABA : A -> B(A)

and a convergent reduction of length omega

A ->> B(B(B(..)))

Require Import Rewriting.

Set Implicit Arguments.

# Signature

Inductive symbol : Set := A | B.

Definition beq_symb (f g : symbol) : bool :=
match f, g with
| A, A => true
| B, B => true
| _, _ => false
end.

Lemma beq_symb_ok : forall f g, beq_symb f g = true <-> f = g.
Proof.
intros f g.
split; intro H.
destruct f; destruct g; simpl; (reflexivity || discriminate).
subst g; destruct f; simpl; reflexivity.
Qed.

Definition arity (f : symbol) : nat :=
match f with
| A => 0
| B => 1
end.

# Variables

Definition variable : Set := nat.

Fixpoint beq_var (x y : variable) : bool :=
match x, y with
| 0, 0 => true
| S x', S y' => beq_var x' y'
| _, _ => false
end.

Lemma beq_var_ok : forall x y, beq_var x y = true <-> x = y.
Proof.
induction x as [|x IH]; destruct y;
simpl; split; intro H; try (reflexivity || discriminate).
f_equal. exact (proj1 (IH _) H).
apply (proj2 (IH _)). inversion H. reflexivity.
Qed.

# Terms

Definition F : signature := Signature arity beq_symb_ok.
Definition X : variables := Variables beq_var_ok.

Notation term := (term F X).
Notation fterm := (finite_term F X).

Function application with no arguments.
Notation "f !" := (@Fun F X f (vnil fterm)) (at level 70).
Notation "f !!" := (@FFun F X f (vnil fterm)) (at level 70).

Function application with one argument.
Notation "f @ a" := (@Fun F X f (vcons a (vnil term))) (right associativity, at level 75).
Notation "f @@ a" := (@FFun F X f (vcons a (vnil fterm))) (right associativity, at level 75).

Some terms.
Definition test_A : term := A!.
Definition test_BA : term := B @ A!.
Definition test_BBA : term := B @ B @ A!.

Finite versions.
Definition ftest_A : fterm := A!!.
Definition ftest_BA : fterm := B @@ A!!.
Definition ftest_BBA : fterm := B @@ B @@ A!!.

B(B(B(...))).
CoFixpoint repeat_B : term :=
B @ repeat_B.

# Contexts

Notation context := (context F X).

Function application with one argument.
Notation "f @@@ a" := (@CFun F X f 0 0 (@refl_equal nat (arity B)) (vnil term) a (vnil term)) (right associativity, at level 75).

Notation id_sub := (empty_substitution F X).

# Rewriting

Notation trs := (trs F X).

Rewrite rule A -> B(A).

Definition ABA_l : fterm := A!!.
Definition ABA_r : fterm := B @@ A!!.

Lemma ABA_wf :
is_var ABA_l = false /\
incl (vars ABA_r) (vars ABA_l).
Proof.
split; simpl.
reflexivity.
intros a H.
assumption.
Qed.

Definition ABA : rule := Rule ABA_l ABA_r ABA_wf.
Definition ABA_trs : trs := ABA :: nil.

Lemma ABA_left_linear :
trs_left_linear ABA_trs.
Proof.
constructor; constructor.
Qed.

# Rewrite sequences

Notation Step := (Step ABA_trs).
Notation Nil := (Nil ABA_trs).

Notation "s [>] t" := (step ABA_trs s t) (at level 40).
Notation "s ->> t" := (sequence ABA_trs s t) (at level 40).

Lemma ABA_in :
In ABA ABA_trs.
Proof.
left. reflexivity.
Qed.

Zero-step rewrite sequence A ->> A.
Definition s_A : (A!) ->> (A!) := Nil (A!).

Lemma fact_term_bis_A :
@Fun F X A (vmap (substitute id_sub) (vnil fterm)) [~] (A !).
Proof.
constructor.
intro.
contradiction (vnil False).
Qed.

Require Import Equality.

Lemma fact_term_bis_BA :
@Fun F X B (vmap (substitute id_sub) (vcons (A !!) (vnil fterm))) [~] (B @ A !).
Proof.
constructor.
intro i.
dependent destruction i.
apply fact_term_bis_A.
contradiction (vnil False).
Qed.

Step A -> B(A).
Single-step rewrite sequence A ->> B(A).
Definition s_A_BA : (A!) ->> (B @ A!) := Cons s_A p_A_BA.

Lemma fact_term_bis_BA' :
(B @ @Fun F X A (vmap (substitute id_sub) (vnil fterm))) [~]
(B @ @Fun F X A (fun x : Fin 0 => vnil fterm x)).
Proof.
constructor.
intro i.
dependent destruction i.
apply fact_term_bis_A.
contradiction (vnil False).
Qed.

Lemma fact_term_bis_BBA :
(B @ @Fun F X B (vmap (substitute id_sub) (vcons (A !!) (vnil fterm)))) [~]
(B @ B @ @Fun F X A (fun x : Fin 0 => vnil fterm x)).
Proof.
constructor.
intro i.
dependent destruction i.
apply fact_term_bis_BA.
contradiction (vnil False).
Qed.

Step B(A) -> B(B(A)).
Two-step reduction A ->> B(B(A)).
Definition s_A_BBA : (A!) ->> (B @ B @ A!) := Cons s_A_BA p_BA_BBA.

B(B(...(A)...)) with n applications of B.
Fixpoint nB_A (n : nat) : term :=
match n with
| 0 => A!
| S n => B @ (nB_A n)
end.

B(B(...(Hole)...)) with n applications of B.
Fixpoint nB_Hole (n : nat) : context :=
match n with
| 0 => Hole
| S n => B @@@ (nB_Hole n)
end.

Lemma fact_term_bis_nBA :
forall n,
fill (nB_Hole n) (@Fun F X A (vmap (substitute id_sub) (vnil fterm))) [~]
nB_A n.
Proof.
induction n as [| n IH]; simpl; constructor; intro i.
contradiction (vnil False).
dependent destruction i.
apply IH.
contradiction (vnil False).
Qed.

Lemma fact_term_bis_BnBA :
forall n,
fill (nB_Hole n) (@Fun F X B (vmap (substitute id_sub) (vcons (A !!) (vnil fterm)))) [~]
(B @ nB_A n).
Proof.
induction n as [| n IH]; simpl.
apply fact_term_bis_BA.
constructor.
intro i.
dependent destruction i.
apply IH.
contradiction (vnil False).
Qed.

Step B(B(...(A)...)) -> B(B(B(...(A)...))) with n applications of B at left side.
n-step rewrite sequence A -1-> B(A) -2-> B(B(A)) -3-> ... -n-> B(B(B(...(A)...))) with n applications of B at right side.
Fixpoint s_A_nBA (n : nat) : (A!) ->> (nB_A n) :=
match n as m in nat return (A!) ->> (nB_A m) with
| 0 => Nil (A!)
| S n => Cons (s_A_nBA n) (p_nBA_nBBA n)
end.

Lemma term_eq_up_to_n_nB_A_repeat_B :
forall n,
term_eq_up_to n (nB_A n) repeat_B.
Proof.
induction n as [| n IH]; simpl.
constructor.
rewrite (peek_eq repeat_B); simpl.
constructor.
intro i.
dependent destruction i.
apply IH.
dependent destruction i.
Qed.

Lemma converges_nB_A : converges nB_A repeat_B.
Proof.
intro d.
exists d.
intros m H.
simpl.
apply term_eq_up_to_weaken_generalized with m.
assumption.
apply term_eq_up_to_n_nB_A_repeat_B.
Qed.

Omega-step reduction A -1-> B(A) -2-> B(B(A)) -3-> ... B(B(B(...))).
This rewrite sequence is well-formed
Lemma wf_s_A_repeat_B :
wf s_A_repeat_B.
Proof.
split.
induction n; simpl; trivial.
intros n m H.
induction H; simpl.
exists (inl _ tt).
apply embed_refl.
destruct IHle as [i IH].
exists (inr _ i).
assumption.
Qed.

Open Scope ord_scope.

Compression lemma is meaningless for this reduction, but maybe we should show just that.
Lemma length_s_A_repeat_B_le_omega :
length s_A_repeat_B <= omega.
Proof.
simpl.
constructor.
intro n.
apply ord_le_pd_right with (existT (fun (n : nat) => pd_type n) (S n) (inl _ tt)).
simpl.
induction n as [| n IH]; simpl.
constructor.
apply Ord_le_Succ with (inl (pd_type n) tt).
assumption.
Qed.

Let's also show the other direction.
Lemma omega_le_length_s_A_repeat_B :
omega <= length s_A_repeat_B.
Proof.
simpl.
constructor.
intro n.
apply ord_le_pd_right with (existT (fun (n : nat) => pd_type (length (s_A_nBA n))) (S n) (inl _ tt)).
simpl.
induction n as [| n IH]; simpl.
constructor.
apply Ord_le_Succ with (inl (pd_type (length (s_A_nBA n))) tt).
assumption.
Qed.

Just because both directions are so similar.
Lemma length_s_A_repeat_B_eq_omega :
length s_A_repeat_B == omega.
Proof.
split; simpl;
constructor;
intro n;
[ apply ord_le_pd_right with (existT (fun (n : nat) => pd_type n) (S n) (inl _ tt))
| apply ord_le_pd_right with (existT (fun (n : nat) => pd_type (length (s_A_nBA n))) (S n) (inl _ tt)) ];
induction n as [| n IH]; simpl;
[ constructor
| apply Ord_le_Succ with (inl (pd_type n) tt); assumption
| constructor
| apply Ord_le_Succ with (inl (pd_type (length (s_A_nBA n))) tt); assumption ].
Qed.

Close Scope ord_scope.