Library Combi.Combi.skewpart: Skew Partitions
Skew partitions:
- hb_strip inn out == out/inn is an horizontal border strip. That is inn is included in out and each column contain at most one box
- vb_strip inn out == out/inn is a vertical border strip. That is inn is included in out and each row contain at most one box
- mindropeq s1 s2 == the minimal d such that drop d s1 == drop d s2
- ribbon_from inn out == out/inn is a ribbon shape starting at row 0
- ribbon inn out == out/inn is a ribbon shape
- ribbon_on start stop inn out <-> out/inn is a ribbon shape starting and ending at rows start and stop.
- ribbon_height inn out == the height of the shape out/inn
- add_ribbon_on sh start stop rem == adds a ribbon to sh from start to stop with rem boxes at row start. The result may not be a partition if there is an extra box.
- add_ribbon sh nbox pos == tries to add a ribbon of size nbox.+1 ending at row pos to the shape sh. Returns Some (res, h) where res is the outer shape partition and h its height on success, or None if not. Compared to add_ribbon_on, the result is always a partition on success.
- add_ribbon_intpartn sh nbox pos == sigma type version of add_ribbon. Takes sh : 'P_d for some d and returns None or Some (res, hgt) where res is of type 'P_(nbox.+1 + m).
- neig4 (r, c) == the 4 neighbors of r, c.
- neig4box b == idem as a box_in_skew inner outer where b is itself a box in out/inn
- conn4_skew inner outer == the skew shape out/inn is 4-connected
- has_no_square inner outer == the shape out/inn has no 2x2 square
- ribbon_textbook inner outer == the textbook definition.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect.
Require Import tools sorted partition.
Set Implicit Arguments.
From mathcomp Require Import all_ssreflect.
Require Import tools sorted partition.
Set Implicit Arguments.
Fixpoint hb_strip inner outer :=
if inner is inn0 :: inn then
if outer is out0 :: out then
(head 0 out <= inn0 <= out0) && (hb_strip inn out)
else false
else if outer is out0 :: out then out == [::]
else true.
Fixpoint vb_strip inner outer :=
if outer is out0 :: out then
if inner is inn0 :: inn then
(inn0 <= out0 <= inn0.+1) && (vb_strip inn out)
else (out0 == 1) && (vb_strip [::] out)
else inner == [::].
Lemma hb_strip_included inner outer :
hb_strip inner outer -> included inner outer.
Lemma hb_strip_size inner outer :
hb_strip inner outer -> size inner <= size outer <= (size inner).+1.
Lemma vb_strip_included inner outer :
vb_strip inner outer -> included inner outer.
Lemma hb_stripP inner outer :
is_part inner -> is_part outer ->
reflect
(forall i, nth 0 outer i.+1 <= nth 0 inner i <= nth 0 outer i)
(hb_strip inner outer).
Lemma vb_stripP inner outer :
is_part inner -> is_part outer ->
reflect
(forall i, nth 0 inner i <= nth 0 outer i <= (nth 0 inner i).+1)
(vb_strip inner outer).
if inner is inn0 :: inn then
if outer is out0 :: out then
(head 0 out <= inn0 <= out0) && (hb_strip inn out)
else false
else if outer is out0 :: out then out == [::]
else true.
Fixpoint vb_strip inner outer :=
if outer is out0 :: out then
if inner is inn0 :: inn then
(inn0 <= out0 <= inn0.+1) && (vb_strip inn out)
else (out0 == 1) && (vb_strip [::] out)
else inner == [::].
Lemma hb_strip_included inner outer :
hb_strip inner outer -> included inner outer.
Lemma hb_strip_size inner outer :
hb_strip inner outer -> size inner <= size outer <= (size inner).+1.
Lemma vb_strip_included inner outer :
vb_strip inner outer -> included inner outer.
Lemma hb_stripP inner outer :
is_part inner -> is_part outer ->
reflect
(forall i, nth 0 outer i.+1 <= nth 0 inner i <= nth 0 outer i)
(hb_strip inner outer).
Lemma vb_stripP inner outer :
is_part inner -> is_part outer ->
reflect
(forall i, nth 0 inner i <= nth 0 outer i <= (nth 0 inner i).+1)
(vb_strip inner outer).
Usual definition : at most one box on each row
Lemma vb_strip_diffP inner outer :
is_part inner -> is_part outer ->
reflect
(included inner outer /\ all (geq 1) (outer / inner))
(vb_strip inner outer).
Lemma vb_strip_conj inner outer :
is_part inner -> is_part outer ->
vb_strip inner outer -> hb_strip (conj_part inner) (conj_part outer).
Lemma hb_strip_conj inner outer :
is_part inner -> is_part outer ->
hb_strip inner outer -> vb_strip (conj_part inner) (conj_part outer).
Lemma hb_strip_conjE inner outer :
is_part inner -> is_part outer ->
hb_strip (conj_part inner) (conj_part outer) = vb_strip inner outer.
Lemma vb_strip_conjE inner outer :
is_part inner -> is_part outer ->
vb_strip (conj_part inner) (conj_part outer) = hb_strip inner outer.
is_part inner -> is_part outer ->
reflect
(included inner outer /\ all (geq 1) (outer / inner))
(vb_strip inner outer).
Lemma vb_strip_conj inner outer :
is_part inner -> is_part outer ->
vb_strip inner outer -> hb_strip (conj_part inner) (conj_part outer).
Lemma hb_strip_conj inner outer :
is_part inner -> is_part outer ->
hb_strip inner outer -> vb_strip (conj_part inner) (conj_part outer).
Lemma hb_strip_conjE inner outer :
is_part inner -> is_part outer ->
hb_strip (conj_part inner) (conj_part outer) = vb_strip inner outer.
Lemma vb_strip_conjE inner outer :
is_part inner -> is_part outer ->
vb_strip (conj_part inner) (conj_part outer) = hb_strip inner outer.
Section MinDropEq.
Variable (T : eqType).
Implicit Types (s : seq T).
Fact ex_dropeq s1 s2 : exists n, drop n s1 == drop n s2.
Definition mindropeq s1 s2 := ex_minn (ex_dropeq s1 s2).
Lemma mindropeqC s1 s2 : mindropeq s1 s2 = mindropeq s2 s1.
Lemma mindropeq0 s1 s2 : mindropeq s1 s2 = 0 -> s1 = s2.
Lemma mindropeq_eq s : mindropeq s s = 0.
Lemma mindropeq_leq s1 s2 : mindropeq s1 s2 <= maxn (size s1) (size s2).
Lemma mindropeq_nil s : mindropeq [::] s = size s.
Lemma mindropeq_cons_eq a b s : a != b -> mindropeq (a :: s) (b :: s) = 1.
Lemma mindropeq_cons_neq a b s1 s2 :
s1 != s2 -> mindropeq (a :: s1) (b :: s2) = (mindropeq s1 s2).+1.
Lemma mindropeq_nthP x0 s t p :
x0 \notin s -> x0 \notin t ->
reflect
(nth x0 s p != nth x0 t p /\ (forall i, i > p -> nth x0 s i = nth x0 t i))
(mindropeq s t == p.+1).
End MinDropEq.
Variable (T : eqType).
Implicit Types (s : seq T).
Fact ex_dropeq s1 s2 : exists n, drop n s1 == drop n s2.
Definition mindropeq s1 s2 := ex_minn (ex_dropeq s1 s2).
Lemma mindropeqC s1 s2 : mindropeq s1 s2 = mindropeq s2 s1.
Lemma mindropeq0 s1 s2 : mindropeq s1 s2 = 0 -> s1 = s2.
Lemma mindropeq_eq s : mindropeq s s = 0.
Lemma mindropeq_leq s1 s2 : mindropeq s1 s2 <= maxn (size s1) (size s2).
Lemma mindropeq_nil s : mindropeq [::] s = size s.
Lemma mindropeq_cons_eq a b s : a != b -> mindropeq (a :: s) (b :: s) = 1.
Lemma mindropeq_cons_neq a b s1 s2 :
s1 != s2 -> mindropeq (a :: s1) (b :: s2) = (mindropeq s1 s2).+1.
Lemma mindropeq_nthP x0 s t p :
x0 \notin s -> x0 \notin t ->
reflect
(nth x0 s p != nth x0 t p /\ (forall i, i > p -> nth x0 s i = nth x0 t i))
(mindropeq s t == p.+1).
End MinDropEq.
Fixpoint ribbon_from inner outer :=
if inner is inn0 :: inn then
if outer is out0 :: out then
(inn0 < out0) &&
((out == inn) || ((head 0 out == inn0.+1) && (ribbon_from inn out)))
else false
else if outer is out0 :: out then head 0 out <= 1
else false.
Fixpoint ribbon inner outer :=
ribbon_from inner outer ||
if (inner, outer) is (inn0 :: inn, out0 :: out) then
(out0 == inn0) && (ribbon inn out)
else false.
Definition ribbon_on start stop inner outer :=
[/\ forall i, i > stop -> nth 0 outer i = nth 0 inner i,
forall i, start <= i < stop -> nth 0 outer i.+1 = (nth 0 inner i).+1,
nth 0 inner start < nth 0 outer start &
forall i, i < start -> nth 0 outer i = nth 0 inner i].
Definition ribbon_height inner outer := count (ltn 0) (outer / inner).
Section Test.
Goal ~~ ribbon_from [::] [::].
Goal ~~ ribbon_from [:: 2] [:: 2].
Goal ribbon_from [::] [:: 4].
Goal ribbon_from [:: 2] [:: 4].
Goal ~~ ribbon_from [:: 2] [:: 4; 2].
Goal ribbon_from [:: 2] [:: 3].
Goal ribbon_from [:: 2] [:: 4; 3].
Goal ribbon_from [:: 3; 2] [:: 4; 4].
Goal ~~ ribbon_from [:: 3; 2] [:: 4; 4; 1].
Goal ~~ ribbon_from [:: 3; 2] [:: 4; 4; 2].
Goal ribbon_from [:: 3; 2; 2] [:: 4; 4; 2].
Goal ~~ ribbon_from [:: 2; 2] [:: 4; 4].
Goal ribbon [:: 2] [:: 3].
Goal ribbon [:: 2; 2] [:: 3; 2].
Goal ribbon [:: 2; 2] [:: 3; 3].
Goal ribbon [:: 5; 3; 2; 2] [:: 5; 4; 4; 2].
Goal ~~ ribbon [:: 5; 3; 2; 2] [:: 5; 4; 4; 2; 1].
Goal ~~ ribbon [::] [::].
Goal ~~ ribbon [:: 2; 1] [:: 2; 1].
End Test.
Lemma ribbon_from_impl inn out : ribbon_from inn out -> ribbon inn out.
Lemma ribbon_consK inn0 inn out0 out :
ribbon (inn0 :: inn) (out0 :: out) -> (out == inn) || ribbon inn out.
Lemma ribbonE inn0 inn out0 out :
inn0 < out0 ->
ribbon (inn0 :: inn) (out0 :: out) = ribbon_from (inn0 :: inn) (out0 :: out).
Lemma ribbon_from_noneq inner outer : ribbon_from inner outer -> inner != outer.
Lemma ribbon_noneq inner outer : ribbon inner outer -> outer != inner.
Lemma ribbon_onSS start stop inn0 inn out0 out :
ribbon_on start.+1 stop.+1 (inn0 :: inn) (out0 :: out)
<-> inn0 == out0 /\ ribbon_on start stop inn out.
Section RibbonOn.
Variables (start stop : nat) (inner outer : seq nat).
Hypotheses (partinn : is_part inner)
(partout : is_part outer)
(Hrib : ribbon_on start stop inner outer).
Lemma ribbon_on_start_stop : start <= stop.
Lemma ribbon_on_nth_leq i :
(start <= i <= stop) = (nth 0 inner i < nth 0 outer i).
Lemma ribbon_on_is_skew r c :
in_skew inner outer (r, c) -> start <= r <= stop.
Lemma ribbon_on_included : included inner outer.
Lemma ribbon_on_start_le : start <= size inner.
Lemma ribbon_on_stop_lt : stop < size outer.
Lemma ribbon_on_height : (stop - start).+1 = ribbon_height inner outer.
Lemma ribbon_on_mindropeq : mindropeq inner outer = stop.+1.
Lemma ribbon_on_stopE : stop = (mindropeq inner outer).-1.
Lemma ribbon_on_startE :
start = mindropeq inner outer - ribbon_height inner outer.
Lemma ribbon_on_sumn :
sumn (outer / inner) = (stop - start) + (nth 0 outer start - nth 0 inner stop).
End RibbonOn.
Lemma ribbon_on_inj inner outer start1 stop1 start2 stop2 :
is_part inner ->
ribbon_on start1 stop1 inner outer ->
ribbon_on start2 stop2 inner outer ->
(start1, stop1) = (start2, stop2).
Lemma ribbon_fromP inner outer :
is_part inner -> is_part outer ->
reflect (exists stop, ribbon_on 0 stop inner outer)
(ribbon_from inner outer).
Lemma ribbon_from_mindropeq inner outer :
is_part inner -> is_part outer -> ribbon_from inner outer ->
ribbon_on 0 (mindropeq inner outer).-1 inner outer.
Lemma ribbonP inner outer :
is_part inner -> is_part outer ->
reflect (exists start stop, ribbon_on start stop inner outer)
(ribbon inner outer).
Lemma ribbon_mindropeq inner outer :
is_part inner -> is_part outer -> ribbon inner outer ->
let min := mindropeq inner outer in
let height := ribbon_height inner outer in
ribbon_on (min - height) min.-1 inner outer.
Lemma ribbon_from_included inner outer :
ribbon_from inner outer -> included inner outer.
Lemma ribbon_included inner outer :
ribbon inner outer -> included inner outer.
Lemma ribbon_sumn_lt inner outer :
is_part outer -> ribbon inner outer -> sumn inner < sumn outer.
Lemma ribbon_sumn_diffE inner outer :
is_part outer -> ribbon inner outer ->
(sumn (outer / inner)).-1.+1 = (sumn (outer / inner)).
Fixpoint startrem acc sh nbox pos :=
if (pos, sh) is (p.+1, s0 :: s) then
let c := nth 0 s p + nbox in
let cpos := s0 + pos in
if c >= cpos then (acc, c - cpos)
else startrem acc.+1 s nbox p
else (acc + (pos - nbox), nbox - pos).
Lemma startrem_acc_geq acc sh nbox pos : acc <= (startrem acc sh nbox pos).1.
Lemma startrem_leq_pos sh nbox pos : (startrem 0 sh nbox pos).1 <= pos.
Lemma startrem_leq_size sh nbox pos :
let (start, rem) := startrem 0 sh nbox pos in
0 < rem -> start <= size sh.
Lemma startrem_leq sh nbox pos :
let (start, rem) := startrem 0 sh nbox pos in
0 < rem -> start <= minn pos (size sh).
Lemma startrem_accE acc sh nbox pos :
let (start, rem) := startrem acc sh nbox pos in
nth 0 sh (start - acc) + pos + rem = nth 0 sh pos + (start - acc) + nbox.
Lemma startremE sh nbox pos :
let (start, rem) := startrem 0 sh nbox pos in
nth 0 sh start + pos + rem = nth 0 sh pos + start + nbox.
Lemma eq_interv_part sh st1 st2 v :
is_part sh ->
nth 0 sh st1.+1 <= st1 + v <= nth 0 sh st1 ->
nth 0 sh st2.+1 <= st2 + v <= nth 0 sh st2 ->
st1 = st2.
Lemma startrem_accP acc sh nbox pos :
is_part sh ->
let (start, rem) := startrem acc sh nbox pos in
0 < rem ->
(start == acc) || (nth 0 sh (start - acc) + rem <= nth 0 sh (start - acc).-1).
Lemma startrem0P acc sh nbox pos :
nth 0 sh 0 + pos <= nth 0 sh pos + nbox ->
startrem acc sh nbox pos = (acc, nth 0 sh pos + nbox - (nth 0 sh 0 + pos)).
Lemma ribbon_on0_startrem stop inner outer acc :
is_part inner ->
is_part outer ->
ribbon_on 0 stop inner outer ->
startrem acc inner (sumn (outer / inner)) stop =
(acc, nth 0 outer 0 - nth 0 inner 0).
Lemma ribbon_on_startrem_acc start stop inner outer acc :
is_part inner ->
is_part outer ->
ribbon_on start stop inner outer ->
startrem acc inner (sumn (outer / inner)) stop =
(acc + start, nth 0 outer start - nth 0 inner start).
Lemma ribbon_on_startrem start stop inner outer :
is_part inner ->
is_part outer ->
ribbon_on start stop inner outer ->
startrem 0 inner (sumn (outer / inner)) stop =
(start, nth 0 outer start - nth 0 inner start).
Lemma ribbon_startrem inner outer :
is_part inner -> is_part outer -> ribbon inner outer ->
let min := mindropeq inner outer in
let height := ribbon_height inner outer in
startrem 0 inner (sumn (outer / inner)) (mindropeq inner outer).-1 =
(min - height, nth 0 outer (min - height) - nth 0 inner (min - height)).
Definition add_ribbon_on sh start stop rem :=
(take start sh)
++ (nth 0 sh start + rem :: map S (drop start (take stop sh)))
++ drop stop.+1 sh ++ nseq (stop - size sh) 1.
Definition add_ribbon sh nbox pos :=
let: (start, rem) := startrem 0 sh nbox.+1 pos in
if rem > 0 then
Some (add_ribbon_on sh start pos rem, (pos - start).+1)
else None.
Section NThAddRibbon.
Variable (sh : seq nat) (start stop rem : nat).
Hypothesis (lesmin : start <= minn stop (size sh)).
#[local] Notation res := (add_ribbon_on sh start stop rem).
if inner is inn0 :: inn then
if outer is out0 :: out then
(inn0 < out0) &&
((out == inn) || ((head 0 out == inn0.+1) && (ribbon_from inn out)))
else false
else if outer is out0 :: out then head 0 out <= 1
else false.
Fixpoint ribbon inner outer :=
ribbon_from inner outer ||
if (inner, outer) is (inn0 :: inn, out0 :: out) then
(out0 == inn0) && (ribbon inn out)
else false.
Definition ribbon_on start stop inner outer :=
[/\ forall i, i > stop -> nth 0 outer i = nth 0 inner i,
forall i, start <= i < stop -> nth 0 outer i.+1 = (nth 0 inner i).+1,
nth 0 inner start < nth 0 outer start &
forall i, i < start -> nth 0 outer i = nth 0 inner i].
Definition ribbon_height inner outer := count (ltn 0) (outer / inner).
Section Test.
Goal ~~ ribbon_from [::] [::].
Goal ~~ ribbon_from [:: 2] [:: 2].
Goal ribbon_from [::] [:: 4].
Goal ribbon_from [:: 2] [:: 4].
Goal ~~ ribbon_from [:: 2] [:: 4; 2].
Goal ribbon_from [:: 2] [:: 3].
Goal ribbon_from [:: 2] [:: 4; 3].
Goal ribbon_from [:: 3; 2] [:: 4; 4].
Goal ~~ ribbon_from [:: 3; 2] [:: 4; 4; 1].
Goal ~~ ribbon_from [:: 3; 2] [:: 4; 4; 2].
Goal ribbon_from [:: 3; 2; 2] [:: 4; 4; 2].
Goal ~~ ribbon_from [:: 2; 2] [:: 4; 4].
Goal ribbon [:: 2] [:: 3].
Goal ribbon [:: 2; 2] [:: 3; 2].
Goal ribbon [:: 2; 2] [:: 3; 3].
Goal ribbon [:: 5; 3; 2; 2] [:: 5; 4; 4; 2].
Goal ~~ ribbon [:: 5; 3; 2; 2] [:: 5; 4; 4; 2; 1].
Goal ~~ ribbon [::] [::].
Goal ~~ ribbon [:: 2; 1] [:: 2; 1].
End Test.
Lemma ribbon_from_impl inn out : ribbon_from inn out -> ribbon inn out.
Lemma ribbon_consK inn0 inn out0 out :
ribbon (inn0 :: inn) (out0 :: out) -> (out == inn) || ribbon inn out.
Lemma ribbonE inn0 inn out0 out :
inn0 < out0 ->
ribbon (inn0 :: inn) (out0 :: out) = ribbon_from (inn0 :: inn) (out0 :: out).
Lemma ribbon_from_noneq inner outer : ribbon_from inner outer -> inner != outer.
Lemma ribbon_noneq inner outer : ribbon inner outer -> outer != inner.
Lemma ribbon_onSS start stop inn0 inn out0 out :
ribbon_on start.+1 stop.+1 (inn0 :: inn) (out0 :: out)
<-> inn0 == out0 /\ ribbon_on start stop inn out.
Section RibbonOn.
Variables (start stop : nat) (inner outer : seq nat).
Hypotheses (partinn : is_part inner)
(partout : is_part outer)
(Hrib : ribbon_on start stop inner outer).
Lemma ribbon_on_start_stop : start <= stop.
Lemma ribbon_on_nth_leq i :
(start <= i <= stop) = (nth 0 inner i < nth 0 outer i).
Lemma ribbon_on_is_skew r c :
in_skew inner outer (r, c) -> start <= r <= stop.
Lemma ribbon_on_included : included inner outer.
Lemma ribbon_on_start_le : start <= size inner.
Lemma ribbon_on_stop_lt : stop < size outer.
Lemma ribbon_on_height : (stop - start).+1 = ribbon_height inner outer.
Lemma ribbon_on_mindropeq : mindropeq inner outer = stop.+1.
Lemma ribbon_on_stopE : stop = (mindropeq inner outer).-1.
Lemma ribbon_on_startE :
start = mindropeq inner outer - ribbon_height inner outer.
Lemma ribbon_on_sumn :
sumn (outer / inner) = (stop - start) + (nth 0 outer start - nth 0 inner stop).
End RibbonOn.
Lemma ribbon_on_inj inner outer start1 stop1 start2 stop2 :
is_part inner ->
ribbon_on start1 stop1 inner outer ->
ribbon_on start2 stop2 inner outer ->
(start1, stop1) = (start2, stop2).
Lemma ribbon_fromP inner outer :
is_part inner -> is_part outer ->
reflect (exists stop, ribbon_on 0 stop inner outer)
(ribbon_from inner outer).
Lemma ribbon_from_mindropeq inner outer :
is_part inner -> is_part outer -> ribbon_from inner outer ->
ribbon_on 0 (mindropeq inner outer).-1 inner outer.
Lemma ribbonP inner outer :
is_part inner -> is_part outer ->
reflect (exists start stop, ribbon_on start stop inner outer)
(ribbon inner outer).
Lemma ribbon_mindropeq inner outer :
is_part inner -> is_part outer -> ribbon inner outer ->
let min := mindropeq inner outer in
let height := ribbon_height inner outer in
ribbon_on (min - height) min.-1 inner outer.
Lemma ribbon_from_included inner outer :
ribbon_from inner outer -> included inner outer.
Lemma ribbon_included inner outer :
ribbon inner outer -> included inner outer.
Lemma ribbon_sumn_lt inner outer :
is_part outer -> ribbon inner outer -> sumn inner < sumn outer.
Lemma ribbon_sumn_diffE inner outer :
is_part outer -> ribbon inner outer ->
(sumn (outer / inner)).-1.+1 = (sumn (outer / inner)).
Fixpoint startrem acc sh nbox pos :=
if (pos, sh) is (p.+1, s0 :: s) then
let c := nth 0 s p + nbox in
let cpos := s0 + pos in
if c >= cpos then (acc, c - cpos)
else startrem acc.+1 s nbox p
else (acc + (pos - nbox), nbox - pos).
Lemma startrem_acc_geq acc sh nbox pos : acc <= (startrem acc sh nbox pos).1.
Lemma startrem_leq_pos sh nbox pos : (startrem 0 sh nbox pos).1 <= pos.
Lemma startrem_leq_size sh nbox pos :
let (start, rem) := startrem 0 sh nbox pos in
0 < rem -> start <= size sh.
Lemma startrem_leq sh nbox pos :
let (start, rem) := startrem 0 sh nbox pos in
0 < rem -> start <= minn pos (size sh).
Lemma startrem_accE acc sh nbox pos :
let (start, rem) := startrem acc sh nbox pos in
nth 0 sh (start - acc) + pos + rem = nth 0 sh pos + (start - acc) + nbox.
Lemma startremE sh nbox pos :
let (start, rem) := startrem 0 sh nbox pos in
nth 0 sh start + pos + rem = nth 0 sh pos + start + nbox.
Lemma eq_interv_part sh st1 st2 v :
is_part sh ->
nth 0 sh st1.+1 <= st1 + v <= nth 0 sh st1 ->
nth 0 sh st2.+1 <= st2 + v <= nth 0 sh st2 ->
st1 = st2.
Lemma startrem_accP acc sh nbox pos :
is_part sh ->
let (start, rem) := startrem acc sh nbox pos in
0 < rem ->
(start == acc) || (nth 0 sh (start - acc) + rem <= nth 0 sh (start - acc).-1).
Lemma startrem0P acc sh nbox pos :
nth 0 sh 0 + pos <= nth 0 sh pos + nbox ->
startrem acc sh nbox pos = (acc, nth 0 sh pos + nbox - (nth 0 sh 0 + pos)).
Lemma ribbon_on0_startrem stop inner outer acc :
is_part inner ->
is_part outer ->
ribbon_on 0 stop inner outer ->
startrem acc inner (sumn (outer / inner)) stop =
(acc, nth 0 outer 0 - nth 0 inner 0).
Lemma ribbon_on_startrem_acc start stop inner outer acc :
is_part inner ->
is_part outer ->
ribbon_on start stop inner outer ->
startrem acc inner (sumn (outer / inner)) stop =
(acc + start, nth 0 outer start - nth 0 inner start).
Lemma ribbon_on_startrem start stop inner outer :
is_part inner ->
is_part outer ->
ribbon_on start stop inner outer ->
startrem 0 inner (sumn (outer / inner)) stop =
(start, nth 0 outer start - nth 0 inner start).
Lemma ribbon_startrem inner outer :
is_part inner -> is_part outer -> ribbon inner outer ->
let min := mindropeq inner outer in
let height := ribbon_height inner outer in
startrem 0 inner (sumn (outer / inner)) (mindropeq inner outer).-1 =
(min - height, nth 0 outer (min - height) - nth 0 inner (min - height)).
Definition add_ribbon_on sh start stop rem :=
(take start sh)
++ (nth 0 sh start + rem :: map S (drop start (take stop sh)))
++ drop stop.+1 sh ++ nseq (stop - size sh) 1.
Definition add_ribbon sh nbox pos :=
let: (start, rem) := startrem 0 sh nbox.+1 pos in
if rem > 0 then
Some (add_ribbon_on sh start pos rem, (pos - start).+1)
else None.
Section NThAddRibbon.
Variable (sh : seq nat) (start stop rem : nat).
Hypothesis (lesmin : start <= minn stop (size sh)).
#[local] Notation res := (add_ribbon_on sh start stop rem).
Put some local result in the environment
#[local] Lemma less : start <= stop.
Let less := less.
#[local] Lemma lessz : start <= size sh.
Let lessz := lessz.
#[local] Lemma sztd :
size (drop start (take stop sh)) = minn stop (size sh) - start.
Let sztd := sztd.
Lemma nth_add_ribbon_lt_start i : i < start -> nth 0 res i = nth 0 sh i.
Lemma nth_add_ribbon_start : nth 0 res start = nth 0 sh start + rem.
Lemma nth_add_ribbon_in i :
start < i.+1 <= stop -> nth 0 res i.+1 = (nth 0 sh i).+1.
Lemma nth_add_ribbon_stop_lt i : stop < i -> nth 0 res i = nth 0 sh i.
Lemma add_ribbon_on_remP : rem > 0 -> ribbon_on start stop sh res.
Lemma is_part_add_ribbon_on nbox :
is_part sh -> rem > 0 ->
startrem 0 sh nbox stop = (start, rem) -> is_part res.
End NThAddRibbon.
Section Tests.
Goal add_ribbon_on [:: 2; 2; 1; 1] 0 0 2 = [:: 4; 2; 1; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 1 1 2 = [:: 2; 4; 1; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 0 1 2 = [:: 4; 3; 1; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 0 2 2 = [:: 4; 3; 3; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 2 2 1 = [:: 2; 2; 2; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 2 3 1 = [:: 2; 2; 2; 2].
Goal add_ribbon_on [:: 2; 2; 1; 1] 2 4 1 = [:: 2; 2; 2; 2; 2].
Goal add_ribbon_on [:: 2; 2; 1; 1] 2 5 1 = [:: 2; 2; 2; 2; 2; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 2 6 1 = [:: 2; 2; 2; 2; 2; 1; 1].
Goal startrem 0 [:: 2; 2; 1; 1] 2 0 = (0, 2).
Goal add_ribbon [:: 2; 2; 1; 1] 1 0 = Some ([:: 4; 2; 1; 1], 1).
Goal startrem 0 [:: 2; 2; 1; 1] 2 1 = (0, 1).
Goal add_ribbon [:: 2; 2; 1; 1] 1 1 = Some ([:: 3; 3; 1; 1], 2).
Let less := less.
#[local] Lemma lessz : start <= size sh.
Let lessz := lessz.
#[local] Lemma sztd :
size (drop start (take stop sh)) = minn stop (size sh) - start.
Let sztd := sztd.
Lemma nth_add_ribbon_lt_start i : i < start -> nth 0 res i = nth 0 sh i.
Lemma nth_add_ribbon_start : nth 0 res start = nth 0 sh start + rem.
Lemma nth_add_ribbon_in i :
start < i.+1 <= stop -> nth 0 res i.+1 = (nth 0 sh i).+1.
Lemma nth_add_ribbon_stop_lt i : stop < i -> nth 0 res i = nth 0 sh i.
Lemma add_ribbon_on_remP : rem > 0 -> ribbon_on start stop sh res.
Lemma is_part_add_ribbon_on nbox :
is_part sh -> rem > 0 ->
startrem 0 sh nbox stop = (start, rem) -> is_part res.
End NThAddRibbon.
Section Tests.
Goal add_ribbon_on [:: 2; 2; 1; 1] 0 0 2 = [:: 4; 2; 1; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 1 1 2 = [:: 2; 4; 1; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 0 1 2 = [:: 4; 3; 1; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 0 2 2 = [:: 4; 3; 3; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 2 2 1 = [:: 2; 2; 2; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 2 3 1 = [:: 2; 2; 2; 2].
Goal add_ribbon_on [:: 2; 2; 1; 1] 2 4 1 = [:: 2; 2; 2; 2; 2].
Goal add_ribbon_on [:: 2; 2; 1; 1] 2 5 1 = [:: 2; 2; 2; 2; 2; 1].
Goal add_ribbon_on [:: 2; 2; 1; 1] 2 6 1 = [:: 2; 2; 2; 2; 2; 1; 1].
Goal startrem 0 [:: 2; 2; 1; 1] 2 0 = (0, 2).
Goal add_ribbon [:: 2; 2; 1; 1] 1 0 = Some ([:: 4; 2; 1; 1], 1).
Goal startrem 0 [:: 2; 2; 1; 1] 2 1 = (0, 1).
Goal add_ribbon [:: 2; 2; 1; 1] 1 1 = Some ([:: 3; 3; 1; 1], 2).
Tests :
sage: s[2, 2] * p[1] s[2, 2, 1] + s[3, 2]
Tests :
sage: s[2, 2] * p[2] -s[2, 2, 1, 1] + s[2, 2, 2] - s[3, 3] + s[4, 2]
Goal pmap (add_ribbon [:: 2; 2] 1) (iota 0 10) =
[:: ([:: 4; 2], 1); ([:: 3; 3], 2); ([:: 2; 2; 2], 1); ([:: 2; 2; 1; 1], 2)].
[:: ([:: 4; 2], 1); ([:: 3; 3], 2); ([:: 2; 2; 2], 1); ([:: 2; 2; 1; 1], 2)].
Tests :
sage: s[3, 2, 1, 1] * p[4] -s[3, 2, 1, 1, 1, 1, 1, 1] + s[3, 2, 2, 2, 2] + s[3, 3, 3, 2] - s[5, 4, 1, 1] + s[7, 2, 1, 1]
Goal pmap (add_ribbon [:: 3; 2; 1; 1] 3) (iota 0 10) =
[:: ([:: 7; 2; 1; 1], 1);
([:: 5; 4; 1; 1], 2);
([:: 3; 3; 3; 2], 3);
([:: 3; 2; 2; 2; 2], 3);
([:: 3; 2; 1; 1; 1; 1; 1; 1], 4)].
[:: ([:: 7; 2; 1; 1], 1);
([:: 5; 4; 1; 1], 2);
([:: 3; 3; 3; 2], 3);
([:: 3; 2; 2; 2; 2], 3);
([:: 3; 2; 1; 1; 1; 1; 1; 1], 4)].
Tests :
sage: s[2, 2] * p[5] s[2, 2, 1, 1, 1, 1, 1] - s[2, 2, 2, 1, 1, 1] + s[3, 3, 3] - s[6, 3] + s[7, 2]
Goal pmap (add_ribbon [:: 2; 2] 4) (iota 0 8) =
[:: ([:: 7; 2], 1); ([:: 6; 3], 2); ([:: 3; 3; 3], 3);
([:: 2; 2; 2; 1; 1; 1], 4); ([:: 2; 2; 1; 1; 1; 1; 1], 5)].
[:: ([:: 7; 2], 1); ([:: 6; 3], 2); ([:: 3; 3; 3], 3);
([:: 2; 2; 2; 1; 1; 1], 4); ([:: 2; 2; 1; 1; 1; 1; 1], 5)].
Tests :
sage: s[2, 2, 1] * p[5] s[2, 2, 1, 1, 1, 1, 1, 1] - s[2, 2, 2, 2, 1, 1] + s[4, 3, 3] - s[6, 3, 1] + s[7, 2, 1]
Goal pmap (add_ribbon [:: 2; 2; 1] 4) (iota 0 8) =
[:: ([:: 7; 2; 1], 1); ([:: 6; 3; 1], 2); ([:: 4; 3; 3], 3);
([:: 2; 2; 2; 2; 1; 1], 4); ([:: 2; 2; 1; 1; 1; 1; 1; 1], 5)].
[:: ([:: 7; 2; 1], 1); ([:: 6; 3; 1], 2); ([:: 4; 3; 3], 3);
([:: 2; 2; 2; 2; 1; 1], 4); ([:: 2; 2; 1; 1; 1; 1; 1; 1], 5)].
Tests :
s[5, 5, 2, 1, 1, 1, 1, 1, 1, 1, 1, 1] - s[5, 5, 2, 2, 2, 2, 1, 1, 1] + s[5, 5, 3, 3, 2, 2, 1] - s[5, 5, 4, 3, 2, 2] + s[7, 6, 6, 1, 1] - s[11, 6, 2, 1, 1] + s[12, 5, 2, 1, 1]
Goal pmap (add_ribbon [:: 5; 5; 2; 1; 1] 6) (iota 0 15) =
[:: ([:: 12; 5; 2; 1; 1], 1); ([:: 11; 6; 2; 1; 1], 2);
([:: 7; 6; 6; 1; 1], 3); ([:: 5; 5; 4; 3; 2; 2], 4);
([:: 5; 5; 3; 3; 2; 2; 1], 5); ([:: 5; 5; 2; 2; 2; 2; 1; 1; 1], 6);
([:: 5; 5; 2; 1; 1; 1; 1; 1; 1; 1; 1; 1], 7)].
Goal let sh := [:: 2; 2] in
all (fun p => ribbon sh p.1) (pmap (add_ribbon sh 0) (iota 0 8)).
Goal let sh := [:: 2; 2] in
all (fun p => ribbon sh p.1) (pmap (add_ribbon sh 4) (iota 0 8)).
Goal let sh := [:: 2; 2; 1] in
all (fun p => ribbon sh p.1) (pmap (add_ribbon sh 4) (iota 0 8)).
Goal let sh := [:: 5; 5; 2; 1; 1] in
all (fun p => ribbon sh p.1) (pmap (add_ribbon sh 6) (iota 0 15)).
End Tests.
Section Spec.
Variables (sh : seq nat).
Hypothesis (partsh : is_part sh).
Variable (nbox pos : nat).
Variables (res : seq nat) (hgt : nat).
Hypothesis (Hret : add_ribbon sh nbox pos = Some (res, hgt)).
Lemma sumn_mapS s : sumn [seq i.+1 | i <- s] = sumn s + size s.
Lemma sumn_add_ribbon : sumn res = nbox.+1 + sumn sh.
Lemma is_part_add_ribbon : is_part res.
Lemma is_part_of_add_ribbon : is_part_of_n (nbox.+1 + sumn sh) res.
Lemma size_add_ribbon : size res = maxn (size sh) pos.+1.
Lemma add_ribbon_height : hgt = ribbon_height sh res.
Lemma add_ribbon_onP : ribbon_on (pos.+1 - hgt) pos sh res.
Lemma add_ribbonP : ribbon sh res.
Lemma included_add_ribbon : included sh res.
End Spec.
Lemma ribbon_on_addE start stop inner outer :
is_part inner -> is_part outer -> ribbon_on start stop inner outer ->
add_ribbon_on inner start stop (nth 0 outer start - nth 0 inner start) =
outer.
Lemma ribbon_addE inner outer :
is_part inner -> is_part outer -> ribbon inner outer ->
add_ribbon inner (sumn (outer / inner)).-1 (mindropeq inner outer).-1 =
Some (outer, ribbon_height inner outer).
Section IntPartN.
Variable (m : nat) (la : 'P_m).
Variable nbox : nat.
#[local] Notation "'Pr" := 'P_(nbox.+1 + m).
Let val_id := fun p : ('Pr * nat) => let: (sh, h) := p in (val sh, h).
Fact add_ribbon_intpartn_spec pos :
{ res : option ('Pr * nat) | omap val_id res = add_ribbon la nbox pos }.
Definition add_ribbon_intpartn (pos : nat) : option ('Pr * nat) :=
let: exist res _ := add_ribbon_intpartn_spec pos in res.
Lemma add_ribbon_intpartnE pos :
add_ribbon la nbox pos =omap val_id (add_ribbon_intpartn pos).
Lemma add_ribbon_intpartnP pos res h :
add_ribbon_intpartn pos = Some (res, h) ->
add_ribbon la nbox pos = Some (val res, h).
End IntPartN.
[:: ([:: 12; 5; 2; 1; 1], 1); ([:: 11; 6; 2; 1; 1], 2);
([:: 7; 6; 6; 1; 1], 3); ([:: 5; 5; 4; 3; 2; 2], 4);
([:: 5; 5; 3; 3; 2; 2; 1], 5); ([:: 5; 5; 2; 2; 2; 2; 1; 1; 1], 6);
([:: 5; 5; 2; 1; 1; 1; 1; 1; 1; 1; 1; 1], 7)].
Goal let sh := [:: 2; 2] in
all (fun p => ribbon sh p.1) (pmap (add_ribbon sh 0) (iota 0 8)).
Goal let sh := [:: 2; 2] in
all (fun p => ribbon sh p.1) (pmap (add_ribbon sh 4) (iota 0 8)).
Goal let sh := [:: 2; 2; 1] in
all (fun p => ribbon sh p.1) (pmap (add_ribbon sh 4) (iota 0 8)).
Goal let sh := [:: 5; 5; 2; 1; 1] in
all (fun p => ribbon sh p.1) (pmap (add_ribbon sh 6) (iota 0 15)).
End Tests.
Section Spec.
Variables (sh : seq nat).
Hypothesis (partsh : is_part sh).
Variable (nbox pos : nat).
Variables (res : seq nat) (hgt : nat).
Hypothesis (Hret : add_ribbon sh nbox pos = Some (res, hgt)).
Lemma sumn_mapS s : sumn [seq i.+1 | i <- s] = sumn s + size s.
Lemma sumn_add_ribbon : sumn res = nbox.+1 + sumn sh.
Lemma is_part_add_ribbon : is_part res.
Lemma is_part_of_add_ribbon : is_part_of_n (nbox.+1 + sumn sh) res.
Lemma size_add_ribbon : size res = maxn (size sh) pos.+1.
Lemma add_ribbon_height : hgt = ribbon_height sh res.
Lemma add_ribbon_onP : ribbon_on (pos.+1 - hgt) pos sh res.
Lemma add_ribbonP : ribbon sh res.
Lemma included_add_ribbon : included sh res.
End Spec.
Lemma ribbon_on_addE start stop inner outer :
is_part inner -> is_part outer -> ribbon_on start stop inner outer ->
add_ribbon_on inner start stop (nth 0 outer start - nth 0 inner start) =
outer.
Lemma ribbon_addE inner outer :
is_part inner -> is_part outer -> ribbon inner outer ->
add_ribbon inner (sumn (outer / inner)).-1 (mindropeq inner outer).-1 =
Some (outer, ribbon_height inner outer).
Section IntPartN.
Variable (m : nat) (la : 'P_m).
Variable nbox : nat.
#[local] Notation "'Pr" := 'P_(nbox.+1 + m).
Let val_id := fun p : ('Pr * nat) => let: (sh, h) := p in (val sh, h).
Fact add_ribbon_intpartn_spec pos :
{ res : option ('Pr * nat) | omap val_id res = add_ribbon la nbox pos }.
Definition add_ribbon_intpartn (pos : nat) : option ('Pr * nat) :=
let: exist res _ := add_ribbon_intpartn_spec pos in res.
Lemma add_ribbon_intpartnE pos :
add_ribbon la nbox pos =omap val_id (add_ribbon_intpartn pos).
Lemma add_ribbon_intpartnP pos res h :
add_ribbon_intpartn pos = Some (res, h) ->
add_ribbon la nbox pos = Some (val res, h).
End IntPartN.
Section ConnectCompl.
Variables (T : finType) (e : rel T).
Lemma connect_rev : (connect (fun x : T => e^~ x)) =2 (fun x => (connect e)^~x).
Lemma connect_from_sym : symmetric e -> connect_sym e.
Lemma same_connect_rev : connect_sym e -> connect e =2 connect (fun x y => e y x).
End ConnectCompl.
Variables (T : finType) (e : rel T).
Lemma connect_rev : (connect (fun x : T => e^~ x)) =2 (fun x => (connect e)^~x).
Lemma connect_from_sym : symmetric e -> connect_sym e.
Lemma same_connect_rev : connect_sym e -> connect e =2 connect (fun x y => e y x).
End ConnectCompl.
Definition neig4 rc :=
let: (r, c) := rc in [:: (r, c.-1); (r, c.+1); (r.-1, c); (r.+1, c)].
Lemma neig4_sym rc1 rc2 : rc1 \in neig4 rc2 -> rc2 \in neig4 rc1.
Lemma grel_neig4_sym : symmetric (grel neig4).
Section Connected4.
Variable (inner outer : seq nat).
#[local] Notation box := (box_skew inner outer).
Definition neig4box (b : box) : seq box := pmap insub (neig4 b).
Lemma neig4boxE :
relpre val (grel neig4) =2 grel (fun b : box => pmap insub (neig4 b)).
Lemma neig4box_sym : symmetric (grel neig4box).
End Connected4.
let: (r, c) := rc in [:: (r, c.-1); (r, c.+1); (r.-1, c); (r.+1, c)].
Lemma neig4_sym rc1 rc2 : rc1 \in neig4 rc2 -> rc2 \in neig4 rc1.
Lemma grel_neig4_sym : symmetric (grel neig4).
Section Connected4.
Variable (inner outer : seq nat).
#[local] Notation box := (box_skew inner outer).
Definition neig4box (b : box) : seq box := pmap insub (neig4 b).
Lemma neig4boxE :
relpre val (grel neig4) =2 grel (fun b : box => pmap insub (neig4 b)).
Lemma neig4box_sym : symmetric (grel neig4box).
End Connected4.
Definition conn4_skew inner outer :=
n_comp (grel (@neig4box inner outer)) predT == 1.
Definition has_no_square inner outer :=
[forall b : box_skew inner outer, ~~ in_skew inner outer (b.1.+1, b.2.+1)].
Definition ribbon_textbook inner outer :=
[&& inner != outer,
included inner outer,
conn4_skew inner outer &
has_no_square inner outer].
Section TextBookDefStartStop.
Variable (start stop : nat) (inner outer : seq nat).
Hypotheses (partinn : is_part inner) (partout : is_part outer).
Hypothesis (Hrib : ribbon_on start stop inner outer).
#[local] Notation box := (box_skew inner outer).
Implicit Type (b : box).
#[local] Notation neig4 := (grel (@neig4box inner outer)).
Lemma conn4_sym : symmetric (connect neig4).
#[local] Definition ribbon_box_ex inner outer :=
let start := (mindropeq inner outer) - ribbon_height inner outer in
(start, nth 0 inner start).
Lemma ribbon_on_box_exE :
ribbon_box_ex inner outer = (start, nth 0 inner start).
Lemma ribbon_on_box_exP : in_skew inner outer (ribbon_box_ex inner outer).
Definition ribbon_on_box_ex : box := BoxSkew ribbon_on_box_exP.
#[local] Notation boxex := ribbon_on_box_ex.
Lemma ribbon_on_conn4_box_ex b : connect neig4 boxex b.
Lemma ribbon_on_conn4 b1 b2 : connect neig4 b1 b2.
Lemma ribbon_on_conn4_skew : conn4_skew inner outer.
Lemma ribbon_on_no_square r c :
in_skew inner outer (r, c) -> ~~ in_skew inner outer (r.+1, c.+1).
End TextBookDefStartStop.
Section TextBookImplDef.
Variable (inner outer : seq nat).
Hypotheses (partinn : is_part inner) (partout : is_part outer).
Hypothesis (Htb : ribbon_textbook inner outer).
#[local] Notation box := (box_skew inner outer).
#[local] Notation stop := (mindropeq inner outer).-1.
#[local] Notation neig4 := (grel (@neig4box inner outer)).
Implicit Type (b : box).
#[local] Lemma incl : included inner outer.
Lemma mindropeq_non0 : mindropeq inner outer != 0.
Lemma ribbontb_stop_ltn : nth 0 inner stop < nth 0 outer stop.
Lemma ribbontb_start_subproof : exists i, nth 0 inner i < nth 0 outer i.
Definition ribbontb_start := ex_minn ribbontb_start_subproof.
#[local] Notation start := ribbontb_start.
Lemma ribbon_textbook_on : ribbon_on start stop inner outer.
End TextBookImplDef.
Theorem ribbon_textbookE inner outer :
is_part inner -> is_part outer ->
ribbon inner outer = ribbon_textbook inner outer.
n_comp (grel (@neig4box inner outer)) predT == 1.
Definition has_no_square inner outer :=
[forall b : box_skew inner outer, ~~ in_skew inner outer (b.1.+1, b.2.+1)].
Definition ribbon_textbook inner outer :=
[&& inner != outer,
included inner outer,
conn4_skew inner outer &
has_no_square inner outer].
Section TextBookDefStartStop.
Variable (start stop : nat) (inner outer : seq nat).
Hypotheses (partinn : is_part inner) (partout : is_part outer).
Hypothesis (Hrib : ribbon_on start stop inner outer).
#[local] Notation box := (box_skew inner outer).
Implicit Type (b : box).
#[local] Notation neig4 := (grel (@neig4box inner outer)).
Lemma conn4_sym : symmetric (connect neig4).
#[local] Definition ribbon_box_ex inner outer :=
let start := (mindropeq inner outer) - ribbon_height inner outer in
(start, nth 0 inner start).
Lemma ribbon_on_box_exE :
ribbon_box_ex inner outer = (start, nth 0 inner start).
Lemma ribbon_on_box_exP : in_skew inner outer (ribbon_box_ex inner outer).
Definition ribbon_on_box_ex : box := BoxSkew ribbon_on_box_exP.
#[local] Notation boxex := ribbon_on_box_ex.
Lemma ribbon_on_conn4_box_ex b : connect neig4 boxex b.
Lemma ribbon_on_conn4 b1 b2 : connect neig4 b1 b2.
Lemma ribbon_on_conn4_skew : conn4_skew inner outer.
Lemma ribbon_on_no_square r c :
in_skew inner outer (r, c) -> ~~ in_skew inner outer (r.+1, c.+1).
End TextBookDefStartStop.
Section TextBookImplDef.
Variable (inner outer : seq nat).
Hypotheses (partinn : is_part inner) (partout : is_part outer).
Hypothesis (Htb : ribbon_textbook inner outer).
#[local] Notation box := (box_skew inner outer).
#[local] Notation stop := (mindropeq inner outer).-1.
#[local] Notation neig4 := (grel (@neig4box inner outer)).
Implicit Type (b : box).
#[local] Lemma incl : included inner outer.
Lemma mindropeq_non0 : mindropeq inner outer != 0.
Lemma ribbontb_stop_ltn : nth 0 inner stop < nth 0 outer stop.
Lemma ribbontb_start_subproof : exists i, nth 0 inner i < nth 0 outer i.
Definition ribbontb_start := ex_minn ribbontb_start_subproof.
#[local] Notation start := ribbontb_start.
Lemma ribbon_textbook_on : ribbon_on start stop inner outer.
End TextBookImplDef.
Theorem ribbon_textbookE inner outer :
is_part inner -> is_part outer ->
ribbon inner outer = ribbon_textbook inner outer.