Library reducedwordsproofs
Proof that words in free groups have unique reduced form
Developed for Coq 8.3Written by P. Christopher Staecker, updated November 2010.
We begin with a nonempty set of generators, which gives a set of Letters, each of which is either a generator or an "inverse" of a generator. A word is a list of letters, and a word is reduced when it contains no adjacent pair of a letter with its inverse. We show that every word can be related to a unique reduced word through a sequence of insertions or deletions of pairs of inverse letters.
The proof follows that found in O. Bogopolski, "Introduction to Group Theory", European Math. Soc., 2008.
We use the excluded middle three times: once explicitly, and twice via a lemma which states that every set of integers has a computable least element. Excluded middle is probably not necessary to obtain the result, but is pretty important in this proof.
See also the version without proofs.
Require Import Arith.
Require Import Omega.
Require Import List.
Set Implicit Arguments.
Unset Strict Implicit.
Load listlemmas.
Excluded middle is used
By EM, every set of integers has a computable least element
Lemma nat_well_ordered: forall (P:nat -> Prop),
(exists n:nat, P n) -> (exists m:nat, P m /\
forall k:nat, P k -> k >= m).
Proof.
intros.
assert (exists! x, P x /\ forall x', P x' -> x <= x') as G.
apply dec_inh_nat_subset_has_unique_least_element;
try intro n; try apply EM; assumption.
destruct G as [x G].
exists x; firstorder.
Qed.
(exists n:nat, P n) -> (exists m:nat, P m /\
forall k:nat, P k -> k >= m).
Proof.
intros.
assert (exists! x, P x /\ forall x', P x' -> x <= x') as G.
apply dec_inh_nat_subset_has_unique_least_element;
try intro n; try apply EM; assumption.
destruct G as [x G].
exists x; firstorder.
Qed.
V is the set of generators, assumed not empty
Words are lists of letters
Inductive Letter:Type :=
| L : V -> Letter
| Li : V -> Letter.
Definition Letter_inv (l:Letter):Letter :=
match l with
L c => Li c
| Li c => L c
end.
Lemma Letter_inv_involutive: forall l:Letter,
Letter_inv (Letter_inv l) = l.
Proof.
intros.
destruct l; simpl; auto.
Qed.
| L : V -> Letter
| Li : V -> Letter.
Definition Letter_inv (l:Letter):Letter :=
match l with
L c => Li c
| Li c => L c
end.
Lemma Letter_inv_involutive: forall l:Letter,
Letter_inv (Letter_inv l) = l.
Proof.
intros.
destruct l; simpl; auto.
Qed.
inserts l * l^-1 at the given position
Definition Word_inv_letter_insert (w:Word) (l:Letter) (pos:nat):Word :=
(sublist 0 pos w) ++ (l :: Letter_inv l :: nil) ++ (sublist pos (length w) w).
Lemma Word_ili_length: forall (u:Word) (l:Letter) (pos:nat),
length (Word_inv_letter_insert u l pos) = length u + 2.
Proof.
intros.
unfold Word_inv_letter_insert.
rewrite ? app_length.
simpl.
assert (pos >= length u \/ pos < length u) as G; try omega.
destruct G.
rewrite sublist_full; try omega.
rewrite sublist_degenerate; try omega.
simpl; omega.
rewrite ? sublist_length; omega.
Qed.
Lemma Word_ili_delete: forall (u v:Word) (l:Letter) (pos:nat),
u = sublist 0 pos v ++ sublist (pos+2) (length v) v /\
(nth pos v l = l /\ nth (pos+1) v l = Letter_inv l) /\
pos + 1 < length v
-> v = Word_inv_letter_insert u l pos.
Proof.
intros u v l pos H.
destruct H as [A H]; destruct H as [P posl]; destruct P as [P P1].
assert (length v = length u + 2) as lenv.
rewrite <- sublist_full with (l:=v) (n:=length v); try omega.
rewrite <- sublist_app with (n:=pos); try omega.
rewrite <- sublist_app with (m:=pos) (n:=pos+2); try omega.
rewrite A.
rewrite ? app_length.
rewrite ? sublist_length; try omega.
unfold Word_inv_letter_insert.
assert (sublist 0 pos v = sublist 0 pos u) as Front.
apply initial_app_eq
with (k:=sublist (pos + 2) (length v) v) (k':= sublist pos (length u) u).
rewrite ? sublist_length; try omega.
rewrite sublist_full_app; firstorder.
assert (sublist (pos + 2) (length v) v = sublist pos (length u) u) as Back.
apply terminal_app_eq
with (l:=sublist 0 pos v) (l':=sublist 0 pos u).
rewrite ? sublist_length; try omega.
rewrite sublist_full_app; firstorder.
rewrite <- Front.
rewrite <- Back.
rewrite <- sublist_full_app with (l:=v) (n:=pos) (k:=length v) at 1; try omega.
rewrite <- sublist_app with (l:=v) (m:=pos) (n:=pos + 2) (k:=length v); try omega.
f_equal; f_equal.
rewrite <- P at 1.
rewrite <- P1.
rewrite sublist_cons with (d:=l); try omega.
rewrite sublist_cons with (d:=l); try omega.
rewrite sublist_degenerate; try omega; auto.
Qed.
(sublist 0 pos w) ++ (l :: Letter_inv l :: nil) ++ (sublist pos (length w) w).
Lemma Word_ili_length: forall (u:Word) (l:Letter) (pos:nat),
length (Word_inv_letter_insert u l pos) = length u + 2.
Proof.
intros.
unfold Word_inv_letter_insert.
rewrite ? app_length.
simpl.
assert (pos >= length u \/ pos < length u) as G; try omega.
destruct G.
rewrite sublist_full; try omega.
rewrite sublist_degenerate; try omega.
simpl; omega.
rewrite ? sublist_length; omega.
Qed.
Lemma Word_ili_delete: forall (u v:Word) (l:Letter) (pos:nat),
u = sublist 0 pos v ++ sublist (pos+2) (length v) v /\
(nth pos v l = l /\ nth (pos+1) v l = Letter_inv l) /\
pos + 1 < length v
-> v = Word_inv_letter_insert u l pos.
Proof.
intros u v l pos H.
destruct H as [A H]; destruct H as [P posl]; destruct P as [P P1].
assert (length v = length u + 2) as lenv.
rewrite <- sublist_full with (l:=v) (n:=length v); try omega.
rewrite <- sublist_app with (n:=pos); try omega.
rewrite <- sublist_app with (m:=pos) (n:=pos+2); try omega.
rewrite A.
rewrite ? app_length.
rewrite ? sublist_length; try omega.
unfold Word_inv_letter_insert.
assert (sublist 0 pos v = sublist 0 pos u) as Front.
apply initial_app_eq
with (k:=sublist (pos + 2) (length v) v) (k':= sublist pos (length u) u).
rewrite ? sublist_length; try omega.
rewrite sublist_full_app; firstorder.
assert (sublist (pos + 2) (length v) v = sublist pos (length u) u) as Back.
apply terminal_app_eq
with (l:=sublist 0 pos v) (l':=sublist 0 pos u).
rewrite ? sublist_length; try omega.
rewrite sublist_full_app; firstorder.
rewrite <- Front.
rewrite <- Back.
rewrite <- sublist_full_app with (l:=v) (n:=pos) (k:=length v) at 1; try omega.
rewrite <- sublist_app with (l:=v) (m:=pos) (n:=pos + 2) (k:=length v); try omega.
f_equal; f_equal.
rewrite <- P at 1.
rewrite <- P1.
rewrite sublist_cons with (d:=l); try omega.
rewrite sublist_cons with (d:=l); try omega.
rewrite sublist_degenerate; try omega; auto.
Qed.
Direct relation.
Two words are directly related when one is a inv_letter_insert of the other. dr is irreflexive and symmetricDefinition Word_direct_rel (u v:Word):Prop :=
(exists l:Letter, exists n:nat, n <= length v /\ u = Word_inv_letter_insert v l n) \/
(exists l:Letter, exists n:nat, n <= length u /\ v = Word_inv_letter_insert u l n).
Lemma Word_dr_irrefl: forall u:Word,
~ Word_direct_rel u u.
Proof.
intros u H.
destruct H; destruct H as [l H]; destruct H as [n H];
destruct H as [H G];
assert (length u = length (Word_inv_letter_insert u l n)) as L;
try rewrite G at 1; auto;
rewrite Word_ili_length in L; omega.
Qed.
Lemma Word_dr_sym: forall u v:Word,
Word_direct_rel u v <-> Word_direct_rel v u.
Proof.
assert (forall u v, Word_direct_rel u v -> Word_direct_rel v u).
intros u v H.
destruct H; [right | left]; assumption.
split; apply H.
Qed.
Indirect relation.
Words are indirectly related if there is a chain of directly related words connecting them, chain must be more than one word long. ir is an equivalence relation
Definition Word_ir_by (u v:Word) (ws:list Word):Prop :=
(length ws > 1) /\
(hd nil ws = u /\ last ws nil = v) /\
list_prop_pairwise ws Word_direct_rel.
Definition Word_indirect_rel (u v:Word):Prop :=
exists ws:list Word, Word_ir_by u v ws.
Lemma Word_ir_by_dr: forall (u v:Word) (l:list Word) (pos:nat),
Word_ir_by u v l /\ pos < length l - 2 ->
Word_direct_rel (nth pos l nil) (nth (pos+1) l nil).
Proof.
firstorder.
Qed.
Lemma Word_dr_ir: forall u v:Word,
Word_direct_rel u v -> Word_indirect_rel u v.
Proof.
intros.
exists (u::v::nil).
split; [ simpl | split ]; auto.
intros pos G a.
simpl in G.
replace pos with 0; try omega.
simpl; exact H.
Qed.
Lemma Word_ir_refl: forall u:Word,
Word_indirect_rel u u.
Proof.
intros.
assert (c:V); try apply V_not_empty.
set (v:=(Word_inv_letter_insert u (L c) 0)).
exists (u::v::u::nil).
split; [ simpl | split ]; auto.
intros pos G a.
simpl in G.
assert (pos = 0 \/ pos = 1) as H; try omega.
destruct H;
rewrite H; simpl;
[ right | left];
exists (L c); exists 0; firstorder.
Qed.
Lemma Word_ir_sym: forall u v,
Word_indirect_rel u v <-> Word_indirect_rel v u.
Proof.
assert (forall u v, Word_indirect_rel u v -> Word_indirect_rel v u) as P.
intros u v H.
unfold Word_indirect_rel in H; destruct H as [ws H1].
exists (rev ws).
destruct H1 as [G H0]; destruct H0 as [H K].
split. rewrite rev_length; assumption.
split. split;
[ rewrite hd_rev_last | rewrite <- hd_last_rev ];
try apply H;
rewrite length_not_nil;
contradict G; rewrite G; omega.
rewrite <- list_pp_rev. assumption.
intros; rewrite Word_dr_sym; assumption.
split; apply P.
Qed.
Lemma Word_ir_trans: forall u v w,
Word_indirect_rel u v -> Word_indirect_rel v w -> Word_indirect_rel u w.
Proof.
intros u v w H1 H2.
destruct H1 as [l J];
destruct H2 as [k K].
destruct J as [lenl1 J].
destruct K as [lenk1 K].
assert (k <> nil) as knil.
contradict lenk1; rewrite lenk1; simpl; omega.
assert (tail k <> nil) as tknil.
assert (forall l, l <> (nil:list Word) -> length (tail l) = length l - 1).
intros. destruct l0. contradict H; auto. simpl. omega.
rewrite length_not_nil. rewrite H. omega. apply knil.
assert (l <> nil) as lnil.
contradict lenl1; rewrite lenl1; simpl; omega.
exists (l++ tail k).
split.
rewrite app_length; firstorder.
split.
split;
[rewrite hd_app | rewrite last_app];
try apply J; try assumption.
transitivity (last ((hd nil k::nil) ++ tail k) nil).
rewrite last_app; auto.
simpl app.
transitivity (last k nil).
destruct k; [ contradict knil | simpl ]; auto.
apply K.
intro pos.
compare pos (length l - 1);
intros H G a.
rewrite H.
rewrite app_nth1; try omega.
rewrite app_nth2; try omega.
rewrite nth_last.
replace (tail k) with (tail (skipn 0 k)); [ idtac | simpl ]; auto.
assert (tail (skipn 0 k) = skipn 1 k) as S.
destruct k; simpl; auto.
rewrite S.
replace (length l - 1 + 1 - length l) with 0; try omega.
rewrite skipn_nth; simpl.
assert (last l a = nth 0 k a) as M.
symmetry.
transitivity (hd a k). destruct k; simpl; auto.
transitivity v.
rewrite hd_indep with (b:=nil) (l:=k); auto; apply K.
transitivity (last l nil). symmetry; apply J.
apply last_indep; assumption.
rewrite M.
apply K; omega.
apply nat_total_order in H.
destruct H.
rewrite ? app_nth1; try omega.
apply J; try omega.
rewrite ? app_nth2; try omega.
replace (pos - length l) with (pos - length l + 1 - length (hd a k::nil));
[ idtac | simpl]; try omega.
replace (pos + 1 - length l) with (pos - length l + 1 + 1 - length (hd a k::nil));
[ idtac | simpl]; try omega.
rewrite <- ? app_nth2 with (l:=hd a k::nil);
[ idtac | simpl | simpl]; try omega.
replace ((hd a k :: nil) ++ tail k) with k. apply K.
replace (length k) with (length (tail k) + 1).
rewrite app_length in G.
omega.
destruct k. firstorder. simpl; omega.
destruct k; firstorder; simpl; auto.
Qed.
(length ws > 1) /\
(hd nil ws = u /\ last ws nil = v) /\
list_prop_pairwise ws Word_direct_rel.
Definition Word_indirect_rel (u v:Word):Prop :=
exists ws:list Word, Word_ir_by u v ws.
Lemma Word_ir_by_dr: forall (u v:Word) (l:list Word) (pos:nat),
Word_ir_by u v l /\ pos < length l - 2 ->
Word_direct_rel (nth pos l nil) (nth (pos+1) l nil).
Proof.
firstorder.
Qed.
Lemma Word_dr_ir: forall u v:Word,
Word_direct_rel u v -> Word_indirect_rel u v.
Proof.
intros.
exists (u::v::nil).
split; [ simpl | split ]; auto.
intros pos G a.
simpl in G.
replace pos with 0; try omega.
simpl; exact H.
Qed.
Lemma Word_ir_refl: forall u:Word,
Word_indirect_rel u u.
Proof.
intros.
assert (c:V); try apply V_not_empty.
set (v:=(Word_inv_letter_insert u (L c) 0)).
exists (u::v::u::nil).
split; [ simpl | split ]; auto.
intros pos G a.
simpl in G.
assert (pos = 0 \/ pos = 1) as H; try omega.
destruct H;
rewrite H; simpl;
[ right | left];
exists (L c); exists 0; firstorder.
Qed.
Lemma Word_ir_sym: forall u v,
Word_indirect_rel u v <-> Word_indirect_rel v u.
Proof.
assert (forall u v, Word_indirect_rel u v -> Word_indirect_rel v u) as P.
intros u v H.
unfold Word_indirect_rel in H; destruct H as [ws H1].
exists (rev ws).
destruct H1 as [G H0]; destruct H0 as [H K].
split. rewrite rev_length; assumption.
split. split;
[ rewrite hd_rev_last | rewrite <- hd_last_rev ];
try apply H;
rewrite length_not_nil;
contradict G; rewrite G; omega.
rewrite <- list_pp_rev. assumption.
intros; rewrite Word_dr_sym; assumption.
split; apply P.
Qed.
Lemma Word_ir_trans: forall u v w,
Word_indirect_rel u v -> Word_indirect_rel v w -> Word_indirect_rel u w.
Proof.
intros u v w H1 H2.
destruct H1 as [l J];
destruct H2 as [k K].
destruct J as [lenl1 J].
destruct K as [lenk1 K].
assert (k <> nil) as knil.
contradict lenk1; rewrite lenk1; simpl; omega.
assert (tail k <> nil) as tknil.
assert (forall l, l <> (nil:list Word) -> length (tail l) = length l - 1).
intros. destruct l0. contradict H; auto. simpl. omega.
rewrite length_not_nil. rewrite H. omega. apply knil.
assert (l <> nil) as lnil.
contradict lenl1; rewrite lenl1; simpl; omega.
exists (l++ tail k).
split.
rewrite app_length; firstorder.
split.
split;
[rewrite hd_app | rewrite last_app];
try apply J; try assumption.
transitivity (last ((hd nil k::nil) ++ tail k) nil).
rewrite last_app; auto.
simpl app.
transitivity (last k nil).
destruct k; [ contradict knil | simpl ]; auto.
apply K.
intro pos.
compare pos (length l - 1);
intros H G a.
rewrite H.
rewrite app_nth1; try omega.
rewrite app_nth2; try omega.
rewrite nth_last.
replace (tail k) with (tail (skipn 0 k)); [ idtac | simpl ]; auto.
assert (tail (skipn 0 k) = skipn 1 k) as S.
destruct k; simpl; auto.
rewrite S.
replace (length l - 1 + 1 - length l) with 0; try omega.
rewrite skipn_nth; simpl.
assert (last l a = nth 0 k a) as M.
symmetry.
transitivity (hd a k). destruct k; simpl; auto.
transitivity v.
rewrite hd_indep with (b:=nil) (l:=k); auto; apply K.
transitivity (last l nil). symmetry; apply J.
apply last_indep; assumption.
rewrite M.
apply K; omega.
apply nat_total_order in H.
destruct H.
rewrite ? app_nth1; try omega.
apply J; try omega.
rewrite ? app_nth2; try omega.
replace (pos - length l) with (pos - length l + 1 - length (hd a k::nil));
[ idtac | simpl]; try omega.
replace (pos + 1 - length l) with (pos - length l + 1 + 1 - length (hd a k::nil));
[ idtac | simpl]; try omega.
rewrite <- ? app_nth2 with (l:=hd a k::nil);
[ idtac | simpl | simpl]; try omega.
replace ((hd a k :: nil) ++ tail k) with k. apply K.
replace (length k) with (length (tail k) + 1).
rewrite app_length in G.
omega.
destruct k. firstorder. simpl; omega.
destruct k; firstorder; simpl; auto.
Qed.
Definition Word_reduced (u:Word):Prop :=
~ (exists v:Word, exists l:Letter, exists pos:nat,
pos <= length v /\ u = Word_inv_letter_insert v l pos).
Lemma Word_short_red: forall w:Word, length w < 2 -> Word_reduced w.
Proof.
intros.
unfold Word_reduced.
intro J.
destruct J as [v J]; destruct J as [l J]; destruct J as [pos J]; destruct J as [J1 J].
unfold Word_inv_letter_insert in J.
symmetry in J.
rewrite <- J in H.
rewrite ? app_length in H.
simpl in H.
omega.
Qed.
Lemma Word_ir_exists_reduced: forall w:Word,
exists v:Word, Word_reduced v /\ Word_indirect_rel w v.
Proof.
intros.
induction w as [| n w IH L] using length_strong_ind.
exists nil.
split.
apply Word_short_red; simpl; auto.
apply Word_ir_refl.
assert ((exists v:Word, exists l:Letter, exists pos:nat, pos <= length v /\ w = Word_inv_letter_insert v l pos) \/ Word_reduced w) as H.
apply EM.
destruct H.
destruct H as [v H]; destruct H as [l H]; destruct H as [pos H]; destruct H as [H1 H].
assert (length w = length v + 2) as uvl.
rewrite H; apply Word_ili_length.
assert (exists u:Word, Word_reduced u /\ Word_indirect_rel v u) as G.
apply IH with (l:=v); try omega.
destruct G as [u G].
exists u.
split.
apply G.
apply Word_ir_trans with (v:=v).
apply Word_dr_ir.
unfold Word_direct_rel.
left.
exists l; exists pos.
firstorder.
apply G.
exists w.
split; [ exact H | apply Word_ir_refl ].
Qed.
~ (exists v:Word, exists l:Letter, exists pos:nat,
pos <= length v /\ u = Word_inv_letter_insert v l pos).
Lemma Word_short_red: forall w:Word, length w < 2 -> Word_reduced w.
Proof.
intros.
unfold Word_reduced.
intro J.
destruct J as [v J]; destruct J as [l J]; destruct J as [pos J]; destruct J as [J1 J].
unfold Word_inv_letter_insert in J.
symmetry in J.
rewrite <- J in H.
rewrite ? app_length in H.
simpl in H.
omega.
Qed.
Lemma Word_ir_exists_reduced: forall w:Word,
exists v:Word, Word_reduced v /\ Word_indirect_rel w v.
Proof.
intros.
induction w as [| n w IH L] using length_strong_ind.
exists nil.
split.
apply Word_short_red; simpl; auto.
apply Word_ir_refl.
assert ((exists v:Word, exists l:Letter, exists pos:nat, pos <= length v /\ w = Word_inv_letter_insert v l pos) \/ Word_reduced w) as H.
apply EM.
destruct H.
destruct H as [v H]; destruct H as [l H]; destruct H as [pos H]; destruct H as [H1 H].
assert (length w = length v + 2) as uvl.
rewrite H; apply Word_ili_length.
assert (exists u:Word, Word_reduced u /\ Word_indirect_rel v u) as G.
apply IH with (l:=v); try omega.
destruct G as [u G].
exists u.
split.
apply G.
apply Word_ir_trans with (v:=v).
apply Word_dr_ir.
unfold Word_direct_rel.
left.
exists l; exists pos.
firstorder.
apply G.
exists w.
split; [ exact H | apply Word_ir_refl ].
Qed.
Idea of the proof: assume some word w has two reduced forms v and u. Then
v and u are ir by some minimal chain of intermediate words. The lengths of
these intermidiate words must increase and then decrease, since v and u are
reduced. Thus there is a particular spot on the chain when the length
increases from an insertion and then immediately decreases by a removal of
a pair of inverse letters. An argument in cases shows that such a spot in the
chain could be bypassed by doing the removal before the insertion,
contradicting the assumed minimality of the chain.
Definition length_ir_chain (ws:list Word) :=
fold_right plus 0 (map (length (A:=Letter)) ws).
Lemma length_ir_chain_app: forall l k:list Word,
length_ir_chain (l++k) = length_ir_chain l + length_ir_chain k.
Proof.
intros.
unfold length_ir_chain.
rewrite map_app.
rewrite fold_right_app.
induction l as [| b bs IH];
simpl; try rewrite IHl; auto; omega.
Qed.
Lemma Word_ir_minimal_chain_exists: forall u v:Word,
Word_indirect_rel u v ->
(exists l:list Word,
Word_ir_by u v l /\
(forall k:list Word,
Word_ir_by u v k -> length_ir_chain l <= length_ir_chain k)).
Proof.
intros.
destruct H as [ws H].
set (P := fun n:nat => exists m:list Word, Word_ir_by u v m /\ length_ir_chain m = n).
assert (P (length_ir_chain ws)).
unfold P; exists ws; split; try apply H; auto.
assert (exists m:nat, P m /\ forall k:nat, P k -> k >= m) as H1.
apply nat_well_ordered; exists (length_ir_chain ws); assumption.
destruct H1 as [x H1]. destruct H1 as [H1 H2].
unfold P in H1.
destruct H1 as [x0 H1].
exists x0.
split. apply H1.
intros.
assert (P (length_ir_chain k)) as H4.
unfold P. exists k.
split; auto.
destruct H1.
apply H2 in H4.
firstorder.
Qed.
Lemma Word_ir_unique_reduced_lemma1:
forall (a b c:Word) (abl bcl:Letter) (abpos bcpos:nat),
abpos <= length a /\ bcpos <= length c /\
b = Word_inv_letter_insert a abl abpos /\
b = Word_inv_letter_insert c bcl bcpos /\
(abpos = bcpos \/ abpos + 1 = bcpos)
-> a = c.
Proof.
intros.
destruct H as [abpl H]; destruct H as [bcpl H];
destruct H as [abrel H]; destruct H as [bcrel ps].
assert (length a = length c) as Lac.
transitivity (length b - 2);
[ rewrite abrel | rewrite bcrel ];
rewrite Word_ili_length; omega.
assert (length b = length a + 2) as Lb.
rewrite abrel.
apply Word_ili_length.
unfold Word_inv_letter_insert in *.
assert (sublist 0 abpos a = sublist 0 abpos c) as S1.
rewrite <- sublist_app with (m:=0) (n:=abpos) in bcrel; try omega.
rewrite app_ass in bcrel.
apply initial_app_eq with (k:=(abl :: Letter_inv abl :: nil) ++ sublist abpos (length a) a)
(k':= sublist abpos bcpos c ++ (bcl :: Letter_inv bcl :: nil) ++ sublist bcpos (length c) c).
rewrite ? sublist_length; omega.
transitivity b; firstorder.
destruct ps as [ps|ps].
assert (sublist bcpos (length a) a = sublist bcpos (length c) c) as S2.
apply terminal_app_eq with
(l:= sublist 0 abpos a ++ (abl :: Letter_inv abl :: nil))
(l':= sublist 0 bcpos c ++ (bcl :: Letter_inv bcl :: nil)).
rewrite ? sublist_length; omega.
transitivity b;
rewrite app_ass;
[ rewrite abrel | rewrite bcrel];
try rewrite ps; auto.
rewrite <- sublist_full_app with (n:=abpos) (k:= length c) (l:=c);
try omega.
rewrite <- S1.
rewrite ps.
rewrite <- S2.
rewrite sublist_full_app; auto.
compare abpos (length a);
intro J.
assert (bcpos > length c) as K.
rewrite <- Lac.
rewrite <- ps; omega.
contradict K; omega.
apply nat_total_order in J.
destruct J as [J|J];
[ idtac | contradict J ]; try omega.
assert (nth abpos c abl = abl) as S2.
rewrite <- sublist_full_app with (n:=bcpos) (k:=length c) (l:=c); try omega.
replace (sublist 0 bcpos c) with (sublist 0 bcpos b).
rewrite app_nth1; try rewrite sublist_length; try omega.
rewrite <- sublist_app with (n:=abpos) (k:=bcpos); try omega.
rewrite app_nth2; try rewrite sublist_length; try omega.
rewrite sublist_singleton with (d:=abl); try omega.
rewrite abrel.
rewrite app_nth2; rewrite sublist_length; try omega.
replace (abpos - (abpos - 0)) with 0; try omega.
simpl; auto.
rewrite bcrel;
rewrite sublist_sublist_front;
try rewrite sublist_length; auto; omega.
assert (nth abpos a abl = abl) as S3.
assert (bcl = Letter_inv abl) as K1.
symmetry.
transitivity (nth bcpos b abl).
rewrite abrel.
rewrite app_nth2; rewrite sublist_length; try omega.
replace (bcpos - (abpos-0)) with 1; [ simpl | omega ]; auto.
rewrite bcrel.
rewrite app_nth2; try rewrite sublist_length; try omega.
replace (bcpos - (bcpos - 0)) with 0; try omega.
simpl; auto.
assert (nth (bcpos+1) b abl = abl) as K2.
rewrite bcrel.
rewrite app_nil_head with (x:=Letter_inv bcl :: nil).
rewrite app_comm_cons.
repeat rewrite <- app_ass.
rewrite app_ass.
rewrite app_nth2;
try rewrite app_length; try rewrite sublist_length; simpl; try omega.
replace (bcpos + 1 - (bcpos - 0 + 1)) with 0; try omega.
rewrite K1.
apply Letter_inv_involutive.
rewrite <- sublist_full_app with (n:=abpos) (k:=length a) (l:=a);
try omega.
rewrite app_nth2; try rewrite sublist_length; try omega.
rewrite <- K2 at 2.
rewrite abrel.
rewrite <- app_ass.
rewrite app_nth2;
try rewrite app_length; simpl; try rewrite sublist_length; try omega.
f_equal; omega.
assert (sublist bcpos (length a) a = sublist bcpos (length c) c) as S4.
rewrite <- sublist_app with (m:=abpos) (n:=bcpos) in abrel; try omega.
apply terminal_app_eq with
(l:= sublist 0 abpos a ++ (abl :: Letter_inv abl :: nil) ++ sublist abpos bcpos a)
(l':=sublist 0 bcpos c ++ (bcl :: Letter_inv bcl :: nil)).
rewrite ? sublist_length; try omega.
transitivity b;
[ rewrite abrel | rewrite bcrel]; rewrite ? app_ass; auto.
rewrite <- sublist_full with (l:=c) (n:=length c); auto.
rewrite <- sublist_full with (l:=a) (n:=length a); auto.
rewrite <- sublist_app with (n:=abpos) (l:=c); try omega.
rewrite <- sublist_app with (l:=a) (n:=abpos); try omega.
compare (abpos) (length c);
intro K.
rewrite Lac.
rewrite <- ? K.
rewrite ? sublist_degenerate with (m:=abpos); try omega.
rewrite <- S1; auto.
apply nat_total_order in K.
destruct K as [K|K].
rewrite <- sublist_app with (m:=abpos) (n:=abpos+1) (l:=c); try omega.
rewrite <- sublist_app with (m:=abpos) (n:=abpos+1) (l:=a); try omega.
rewrite ? sublist_singleton with (d:=abl) (n:=abpos); try omega.
replace (abpos + 1) with bcpos; try assumption.
rewrite S1.
rewrite S2.
rewrite S3.
rewrite S4.
auto.
rewrite <- Lac in K.
contradict J. firstorder.
Qed.
Lemma Word_ir_unique_reduced_lemma2:
forall (a b c:Word) (abl bcl:Letter) (abpos bcpos:nat),
abpos <= length a /\ bcpos <= length c /\
b = Word_inv_letter_insert a abl abpos /\
b = Word_inv_letter_insert c bcl bcpos /\
abpos + 1 < bcpos ->
exists b':Word, (Word_direct_rel a b' /\ Word_direct_rel b' c) /\ length b' < length b.
Proof.
intros.
destruct H as [abpl H]; destruct H as [bcpl H];
destruct H as [abrel H]; destruct H as [bcrel ps].
assert (length a = length c) as Lac.
transitivity (length b - 2);
[ rewrite abrel | rewrite bcrel ];
rewrite Word_ili_length; omega.
set (b' := sublist 0 (bcpos-2) a ++ sublist bcpos (length a) a).
exists b'.
assert (length b' = length a - 2) as Lb'a.
unfold b'; rewrite app_length.
rewrite ? sublist_length; omega.
assert (length b' +4 = length b) as Lb'b.
rewrite Lb'a.
rewrite abrel.
rewrite Word_ili_length; omega.
split; try omega.
unfold Word_inv_letter_insert in *.
split; unfold Word_direct_rel;
[ left | right];
[ exists bcl | exists abl];
[ exists (bcpos - 2) | exists (abpos) ];
split; try omega;
apply Word_ili_delete.
split.
replace (bcpos - 2 + 2) with bcpos; try omega.
auto.
split; try omega.
assert (sublist (bcpos - 2) (length a) a = sublist bcpos (length b) b) as K.
rewrite <- sublist_full_app with (l:=a) (n:=abpos) (k:=length a) at 2;
try omega.
rewrite abrel at 2.
rewrite <- app_ass.
rewrite ? app_sublist2;
try rewrite app_length; try rewrite sublist_length; simpl; try omega.
f_equal; omega.
split;
[ rewrite plus_n_O with (n:= (bcpos - 2)) | idtac ];
rewrite <- sublist_nth with (l:=a) (n:=length a); try omega;
rewrite K;
rewrite bcrel at 2;
rewrite app_sublist2; try rewrite sublist_length; try omega;
replace (bcpos - 0) with (bcpos); try omega;
rewrite minus_diag;
rewrite sublist_nth; try omega;
rewrite app_nth1; simpl; try omega;
auto.
assert (sublist 0 bcpos c = sublist 0 bcpos b) as K.
rewrite bcrel.
rewrite sublist_sublist_front;
try rewrite sublist_length; auto; try omega.
split.
assert (sublist 0 abpos a = sublist 0 abpos c) as S1.
rewrite <- sublist_app with (l:=c) (n:=abpos) in bcrel; try omega.
rewrite ? app_ass in bcrel.
apply initial_app_eq with
(k:= (abl :: Letter_inv abl :: nil) ++ sublist abpos (length a) a)
(k':= sublist abpos bcpos c ++ (bcl :: Letter_inv bcl :: nil) ++ sublist bcpos (length c) c).
rewrite ? sublist_length; omega.
transitivity b;
[ rewrite abrel | rewrite bcrel ]; auto.
assert (sublist abpos (bcpos - 2) a = sublist (abpos+2) bcpos c) as S2.
transitivity (sublist (abpos + 2) bcpos b).
rewrite abrel.
rewrite <- app_ass.
rewrite app_sublist2;
try rewrite app_length;
[ idtac | try rewrite sublist_length ]; simpl; try omega.
rewrite sublist_length; try omega.
replace (abpos + 2 - (abpos - 0 + 2)) with 0; try omega.
rewrite <- sublist_app with (k:=length a) (n:=bcpos - 2); try omega.
rewrite sublist_sublist_front;
try rewrite sublist_length; try omega.
auto.
rewrite bcrel.
rewrite app_sublist1; try rewrite sublist_length; try omega.
rewrite <- sublist_app with (m:=0) (n:=abpos+2); try omega.
rewrite sublist_sublist_back; try rewrite sublist_length; try omega.
auto.
assert (sublist bcpos (length a) a = sublist bcpos (length c) c) as S3.
rewrite <- sublist_app with (m:=abpos) (n:=bcpos) in abrel; try omega.
apply terminal_app_eq with
(l:= sublist 0 abpos a ++ (abl :: Letter_inv abl :: nil) ++ sublist abpos bcpos a)
(l':= sublist 0 bcpos c ++ (bcl :: Letter_inv bcl :: nil)).
rewrite ? sublist_length; omega.
transitivity b;
[ rewrite abrel | rewrite bcrel ]; rewrite ? app_ass; auto.
unfold b' at 1.
rewrite <- sublist_app with (m:=0) (n:=abpos); try omega.
compare bcpos (length c);
intro H.
rewrite Lac.
rewrite <- ? H.
rewrite sublist_degenerate with (m:=bcpos) (n:=bcpos); try omega.
rewrite <- app_nil_end.
rewrite S1; rewrite S2; auto.
apply nat_total_order in H.
destruct H; [ idtac | contradict H]; try firstorder.
rewrite <- sublist_app with (m:=abpos + 2) (n:=bcpos) (k:=length c); try omega.
rewrite app_ass.
rewrite S1; rewrite S2; rewrite S3; auto.
split; try omega.
assert (sublist 0 (abpos+2) c = sublist 0 (abpos+2) b) as H.
rewrite <- ? sublist_app with (m:=0) (n:=abpos+2) (k:=bcpos) in K; try omega.
apply initial_app_eq with
(k':= sublist (abpos + 2) bcpos b) (k:= sublist (abpos+2) bcpos c).
rewrite ? sublist_length; omega.
exact K.
split;
replace abpos with (0 + abpos); try omega;
try rewrite <- plus_assoc;
rewrite <- sublist_nth with (n:=abpos + 2); try omega;
rewrite H;
rewrite abrel;
rewrite <- app_ass;
rewrite sublist_sublist_front;
try rewrite app_length; try rewrite sublist_length; simpl; try omega;
rewrite app_nth2; try rewrite sublist_length; try omega;
[ replace (abpos - (abpos - 0)) with 0 | replace (abpos + 1 - (abpos - 0)) with 1]; try omega;
simpl; auto.
Qed.
Theorem Word_ir_unique_reduced: forall w:Word,
exists ! v:Word, Word_reduced v /\ Word_indirect_rel w v.
Proof.
intros.
assert (exists v, Word_reduced v /\ Word_indirect_rel w v) as V.
apply Word_ir_exists_reduced.
destruct V as [v V].
exists v.
split.
exact V.
intros x H.
destruct H as [IR H].
assert (Word_indirect_rel v x) as G.
apply Word_ir_trans with (v:=w).
rewrite Word_ir_sym; apply V.
exact H.
apply Word_ir_minimal_chain_exists in G.
destruct G as [chain G]; destruct G as [G1 G2].
assert (exists pos:nat, 0 <= pos < length (chain)-2 /\
length (nth pos chain nil) < length (nth (pos + 1) chain nil) /\
length (nth (pos + 1) chain nil) > length (nth (pos + 2) chain nil)) as P.
unfold Word_ir_by in G1.
assert (length chain = 2 \/ length chain > 2) as Lc; try omega.
destruct Lc as [e | Lc].
assert (Word_direct_rel v x) as R.
replace v with (hd nil chain); try apply G1.
replace x with (last chain nil); try apply G1.
rewrite <- nth_0; rewrite <- nth_last.
rewrite e; simpl.
apply G1; omega.
destruct R as [R | R];
[ clear - V R | clear - IR R ]; firstorder.
set (P:= fun n:nat => length (nth (n+1) chain nil) > length (nth (n+2) chain nil)).
assert (P (length chain - 3)) as Pend.
unfold P.
assert (Word_direct_rel
(nth (length chain - 2) chain nil) (nth (length chain - 2+1) chain nil)) as K;
try apply G1; try omega.
replace (length chain - 2 + 1) with (length chain - 1) in *; try omega.
replace (length chain - 3 + 1) with (length chain - 2); try omega.
replace (length chain - 3 + 2) with (length chain - 1); try omega.
rewrite nth_last in *.
replace (last chain nil) with x in *; [ idtac | symmetry ]; try apply G1.
unfold Word_direct_rel in K.
destruct K as [K|K];
destruct K as [l K]; destruct K as [n K]; destruct K as [M K].
rewrite K; rewrite Word_ili_length; omega.
unfold Word_reduced in IR.
contradict IR.
exists (nth (length chain - 2) chain nil); exists l; exists n.
split; [ omega | exact K ].
assert (exists p:nat, P p /\ forall k:nat, P k -> k >= p) as K.
apply nat_well_ordered; exists (length chain - 3); auto.
destruct K as [p K]; destruct K as [K Kall].
exists p.
assert (length chain - 3 >= p) as pl.
apply Kall with (k:=length chain - 3); exact Pend.
split; try omega.
split; try apply K.
compare p 0;
intro e. rewrite e; simpl.
assert (Word_direct_rel (nth 0 chain nil) (nth 1 chain nil)) as J;
try apply G1; try omega.
rewrite nth_0 in *.
unfold Word_direct_rel in J.
destruct J as [J | J].
replace v with (hd nil chain) in V; try apply G1.
destruct V as [V W].
clear - V J; contradict V; firstorder.
destruct J as [l J]; destruct J as [n J]; destruct J as [M J].
rewrite J.
rewrite Word_ili_length.
omega.
assert (~ P (p-1)) as M.
intro J.
apply Kall in J; contradict J; omega.
unfold P in M.
apply not_gt in M.
replace (p-1+1) with p in M; try omega.
replace (p-1+2) with (p+1) in M; try omega.
assert (length (nth p chain nil) <> length (nth (p+1) chain nil)) as N.
assert (Word_direct_rel (nth p chain nil) (nth (p+1) chain nil)) as J;
try apply G1; try omega.
destruct J as [J|J]; destruct J as [l J]; destruct J as [n J]; destruct J as [N J];
rewrite J;
rewrite Word_ili_length; omega.
omega.
destruct P as [pos lens].
unfold Word_ir_by in G1.
set (a:= nth pos chain nil); set (b:=nth (pos+1) chain nil); set (c:=nth (pos+2) chain nil).
assert (Word_direct_rel a b) as abrel.
apply G1; omega.
assert (Word_direct_rel b (nth (pos+1+1) chain nil)) as bcrel.
apply G1; omega.
fold a in lens; fold b in lens; fold c in lens.
replace (pos+1+1) with (pos+2) in bcrel; try omega.
fold c in bcrel.
destruct lens as [pl ls]; destruct ls as [lab lbc].
destruct abrel as [junkab | abrel ].
destruct junkab as [l junk]; destruct junk as [n junk];
destruct junk as [nl junk].
assert (length a = length b + 2) as L.
rewrite junk; apply Word_ili_length.
contradict lab. rewrite L. omega.
destruct bcrel as [bcrel | junkbc].
Focus 2.
destruct junkbc as [l junk]; destruct junk as [n junk];
destruct junk as [nl junk].
replace (pos + 1 + 1) with (pos + 2) in junk.
assert (length c = length b + 2) as L.
rewrite junk; apply Word_ili_length.
contradict lbc; rewrite L; omega.
omega.
Unfocus.
destruct abrel as [abl abrel]; destruct abrel as [abpos abrel];
destruct abrel as [abpl abrel].
destruct bcrel as [bcl bcrel]; destruct bcrel as [bcpos bcrel];
destruct bcrel as [bcpl bcrel].
assert (length a = length c) as Lac.
transitivity (length b - 2);
[ rewrite abrel | rewrite bcrel ];
rewrite Word_ili_length; omega.
assert (forall ll:list Word, forall p:nat, forall q:nat,
let ch:=(firstn p chain ++ ll ++ skipn (p+q) chain) in
p>0 /\ p+q < length chain
-> (hd nil ch = hd nil chain /\ last ch nil = last chain nil)) as chadd.
intros ll p q K M.
unfold K.
split.
rewrite <- ? nth_0.
rewrite app_nth1; try rewrite firstn_length_nt; try omega.
rewrite firstn_nth; try omega; auto.
rewrite <- ? nth_last.
rewrite <- app_ass.
rewrite app_nth2.
rewrite skipn_nth; try omega.
rewrite ? app_length.
rewrite skipn_length; try omega.
rewrite firstn_length_nt; try omega.
f_equal.
clear - M; omega.
rewrite app_length.
rewrite skipn_length; try omega.
assert ((abpos = bcpos \/
(abpos + 1 = bcpos \/ bcpos + 1 = abpos)) \/
(abpos + 1 < bcpos \/ bcpos + 1 < abpos)) as ps; try omega.
destruct ps as [ps|ps].
assert (a = c) as aceq.
destruct ps as [ps|ps].
apply Word_ir_unique_reduced_lemma1 with
(b:=b) (abl:=abl) (bcl:=bcl) (abpos:=abpos) (bcpos:=bcpos).
firstorder.
destruct ps;
[ idtac | symmetry ];
[ apply Word_ir_unique_reduced_lemma1 with
(b:=b) (abl:=abl) (bcl:=bcl) (abpos:=abpos) (bcpos:=bcpos) |
apply Word_ir_unique_reduced_lemma1 with
(a:=c) (b:=b) (c:=a) (abl:=bcl) (bcl:=abl) (abpos:=bcpos) (bcpos:=abpos) ].
split; [ firstorder | idtac ];
split; [ firstorder | idtac ];
split; [ firstorder | idtac ];
split; [ firstorder | idtac ];
right; assumption.
split; [ firstorder | idtac ];
split; [ firstorder | idtac ];
split; [ firstorder | idtac ];
split; [ firstorder | idtac ];
right; assumption.
set (chain' := firstn (pos) chain ++ (skipn (pos+2) chain)).
assert (length chain' + 2 = length chain).
unfold chain'.
rewrite app_length.
rewrite skipn_length; try omega.
rewrite firstn_length_nt; try omega.
assert (forall p, forall d:Word, p < pos -> nth p chain' d = nth p chain d) as N1.
intros.
unfold chain'.
rewrite app_nth1; try rewrite firstn_length_nt; try omega.
rewrite firstn_nth; [ auto | omega].
assert (forall p, forall d:Word, p >= pos -> nth p chain' d = nth (p+2) chain d) as N2.
intros.
unfold chain'.
assert (length (firstn pos chain) = pos) as L; try rewrite firstn_length_nt; try omega.
rewrite app_nth2; try rewrite L; try omega.
replace (p - pos) with
(p - pos + length (firstn (pos+2) chain) - length (firstn (pos+2) chain)); try omega.
rewrite <- app_nth2 with (l:= firstn (pos+2) chain); try omega.
rewrite firstn_length_nt; try omega.
rewrite firstn_skipn.
f_equal; omega.
compare (length chain') 1.
intro K.
rewrite K in H0; simpl in H0.
rewrite <- H0 in pl; simpl in pl.
assert (pos = 0) as J by omega.
unfold a in aceq; unfold c in aceq.
rewrite J in aceq; simpl in aceq.
rewrite nth_0 in aceq.
replace 2 with (length chain - 1) in aceq; try omega.
rewrite nth_last in aceq.
transitivity (hd nil chain); [ firstorder | idtac ].
transitivity (last chain nil); try assumption.
apply G1.
intro.
assert (Word_ir_by v x chain') as Newchain.
unfold Word_ir_by.
split.
omega.
assert (hd nil chain' = hd nil chain /\ last chain' nil = last chain nil) as K.
compare pos 0; intros e;
[ idtac | try apply chadd with (ll:=nil) (p:=pos) (q:=2)]; try omega.
split;
[ rewrite <- ? nth_0 | rewrite <- ? nth_last ].
unfold chain'; rewrite e.
simpl firstn; rewrite <- app_nil_head;
rewrite skipn_nth.
replace (0+2+0) with (0+2); try omega.
rewrite <- e at 1 3.
firstorder.
unfold chain' at 2.
rewrite e; simpl firstn; rewrite <- app_nil_head.
rewrite skipn_nth.
f_equal; omega.
split.
split; destruct K as [K1 K2]; [rewrite K1 | rewrite K2]; apply G1.
unfold list_prop_pairwise.
intros p J d.
rewrite ? nth_indep with (d:= d) (d':=nil).
Focus 2.
unfold lt. replace (S(p+1)) with (p+2); try omega. exact J.
Unfocus.
Focus 2.
unfold lt. apply le_Sn_le. replace (S (S p)) with (p+2); try omega. exact J.
Unfocus.
compare pos 0; intro D.
unfold chain'.
rewrite D; simpl firstn.
rewrite <- app_nil_head.
rewrite ? skipn_nth.
rewrite plus_assoc.
apply G1; omega.
compare p (pos-1); intro C.
rewrite N1 with (p:=p); try omega.
rewrite N2; try omega.
rewrite C at 2.
replace (pos - 1 + 1 + 2) with (pos + 2); try omega.
fold c; rewrite <- aceq; unfold a.
replace pos with (p + 1); try omega.
apply G1; try omega.
apply nat_total_order in C.
destruct C as [C | C].
rewrite ? N1; try omega.
apply G1; try omega.
rewrite ? N2; try omega.
replace (p+1+2) with (p+2+1); try omega.
apply G1; try omega.
assert (length_ir_chain chain' < length_ir_chain chain) as Ncl.
rewrite <- firstn_skipn with (n:=pos) (l:=chain).
unfold chain'.
rewrite sublist_skipn with (n:=pos).
rewrite <- sublist_app with (n:=pos+2); try omega.
rewrite <- sublist_skipn.
rewrite <- sublist_app with (m:=pos) (n:=pos+1); try omega.
rewrite sublist_singleton with (n:=pos) (d:=nil) (l:=chain); try omega.
rewrite ? length_ir_chain_app.
fold a.
replace (length_ir_chain (a::nil)) with (length a);
[ idtac | unfold length_ir_chain ]; simpl; try omega.
rewrite sublist_singleton with (d:=nil) (n:=pos+1) (k:=pos+2) (l:=chain); try omega.
unfold length_ir_chain; simpl; fold b.
omega.
apply G2 in Newchain.
contradict Newchain.
firstorder.
assert (exists b':Word, (Word_direct_rel a b' /\ Word_direct_rel b' c) /\ length b' < length b) as M.
destruct ps.
apply Word_ir_unique_reduced_lemma2 with (abl:=abl) (bcl:=bcl) (abpos:=abpos) (bcpos:=bcpos).
firstorder.
assert (exists b':Word, (Word_direct_rel c b' /\ Word_direct_rel b' a) /\ length b' < length b) as M.
apply Word_ir_unique_reduced_lemma2 with
(abl:=bcl) (bcl:=abl) (abpos:=bcpos) (bcpos:=abpos) (a:=c) (c:=a).
firstorder.
destruct M as [b' M].
exists b'.
split;
try split; try rewrite Word_dr_sym; firstorder.
destruct M as [b' M].
set (chain' := (firstn (pos+1) chain) ++ (b':: nil) ++ (skipn (pos+2) chain)).
assert (length chain' = length chain) as lench.
unfold chain'.
rewrite ? app_length.
replace (length (b'::nil)) with (length (b::nil)); [ idtac | simpl ]; auto.
rewrite <- ? app_length.
unfold b.
rewrite <- sublist_singleton with (k:=pos+2); try omega.
rewrite sublist_skipn.
rewrite sublist_app; try omega.
rewrite <- sublist_skipn.
rewrite firstn_skipn; auto.
assert (Word_ir_by v x chain') as Newchain.
unfold Word_ir_by.
split. firstorder.
split.
assert (hd nil chain' = hd nil chain /\ last chain' nil = last chain nil) as K.
unfold chain'.
replace (pos+2) with (pos+1+1); try omega.
apply chadd with (ll:=b'::nil) (p:=pos+1) (q:=1); omega.
split; destruct K as [K1 K2]; [rewrite K1 | rewrite K2]; apply G1.
assert (forall p, p <> pos + 1 -> nth p chain' nil = nth p chain nil) as N.
intros p K.
apply nat_total_order in K.
destruct K as [K|K];
unfold chain'.
rewrite app_nth1; try rewrite firstn_length_nt; try omega.
rewrite firstn_nth; try omega; auto.
rewrite <- app_ass.
rewrite app_nth2;
try rewrite app_length; try rewrite firstn_length_nt; simpl; try omega.
rewrite skipn_nth.
f_equal.
omega.
assert (nth (pos+1) chain' nil = b') as N2.
unfold chain'.
rewrite app_nth2;
try rewrite firstn_length_nt; try omega.
replace (pos + 1 - (pos + 1)) with 0; try omega.
simpl; auto.
unfold list_prop_pairwise.
intros p0 G a0.
rewrite nth_indep with (n:=p0+1) (d':=nil) (l:=chain'); try omega.
rewrite nth_indep with (d':=nil) (l:=chain'); try omega.
compare p0 pos;
intro K1;
compare p0 (pos+1);
intro K2.
contradict K1; firstorder.
rewrite K1.
rewrite N2.
rewrite N; try omega.
fold a.
apply M.
rewrite K2.
rewrite N with (p:=pos + 1 + 1); try omega.
rewrite N2.
replace (pos + 1 + 1) with (pos + 2); try omega.
fold c.
apply M.
rewrite ? N; try omega.
apply G1; try omega.
assert (length_ir_chain chain' < length_ir_chain chain).
rewrite <- firstn_skipn with (n:=pos+1) (l:=chain).
unfold chain'.
rewrite ? length_ir_chain_app.
rewrite sublist_skipn with (n:=pos + 1).
rewrite sublist_cons with (m:=pos + 1) (n:= length chain) (l:=chain) (d:=nil);
try omega.
rewrite <- sublist_skipn.
rewrite app_nil_head with (x:=skipn (pos + 1 + 1) chain).
rewrite app_comm_cons.
rewrite length_ir_chain_app.
replace (pos + 1 + 1) with (pos + 2); try omega.
fold b.
unfold length_ir_chain at 2 5.
simpl; omega.
assert (length_ir_chain chain <= length_ir_chain chain') as L.
apply G2. assumption.
contradict L; omega.
Qed.
Written by P. Christopher Staecker
This page has been generated by coqdoc