Module rs_admissible

Require Import ssreflect ssrbool ssrfun eqtype ssrnat seq div choice fintype.
Require Import finset zmodp ssralg rs_definitions aux_lemmas rs_dvf advf_type.

Set Implicit Arguments.
Unset Strict Implicit.
Import Prenex Implicits.






Section admissible.


Section rs_adm_prop5.

Section sequences_norep.

Fixpoint subseq (T:eqType) (s1 s2 : seq T) :=
if s2 is y :: s2' then if s1 is x :: s1' then if (x \in s2) then subseq s1' s2 else false else true
else s1 == [::].


Lemma subseqtail (s2 r2:seq (seq nat)) :
   r2!= [::] -> subseq s2 (behead r2) -> subseq s2 r2.


Lemma last_last (k a1:nat)(a2:seq nat): a2!=[::] -> last k a2 = last k (a1::a2).


Lemma last_in (k i:nat)(a:seq nat): (a!=[::]) -> ((last k a)= i) -> (i \in a).

Lemma in_concat (s1 k:nat)(s2:seq nat): (s1 \in s2 ++ [:: k]) = ((s1 \in s2) || (s1 == k)).


Lemma uniq_last (n i:nat)(s:seq nat): (s!=[::]) -> (n= last i s) -> uniq (n::s)=false.



Lemma subseq_norep_seq (s:seq nat)(rest: seq (seq nat)):
  subseq [::s] rest -> norep rest -> uniq s.


Lemma norepik (i k:nat):
  i != k -> norep [:: [:: i, k & [::]]].


Lemma noreprev (k:nat)(s:seq nat): norep [::s] -> (k\in s)=false ->
   norep ([::s ++ [::k]]) = norep ((k::s)::[::]).


Lemma norep_cat (r1 r2:seq (seq nat)): norep (r1 ++ r2) = norep r1 && norep r2.


Lemma norephead (s1:seq nat)(s2:seq (seq nat)): norep(s1::s2) -> norep [::s1].


Lemma getfirstE_in (k:nat)(s2:seq nat)(rest:seq(seq nat)):
  s2 \in rest -> head 0 s2 = k -> s2 \in getfirstE k rest.


End sequences_norep.



Section getfirst_last.

Lemma getfirstE_headtail (k:nat)(t:seq nat)(s:seq (seq nat)):
  getfirstE k (t::s) = ((getfirstE k (t::nil))++ (getfirstE k s)).



Lemma getlastE_headtail (k:nat)(t:seq nat)(s:seq (seq nat)):
  getlastE k (t::s) = ((getlastE k (t::nil))++ (getlastE k s)).


Lemma getfirstEnil (k:nat)(t:seq nat)(s:seq (seq nat)):
  getfirstE k (t::s) = [::] -> ((getfirstE k s)=[::]).


Lemma getlastEnil (k:nat)(t:seq nat)(s:seq (seq nat)):
  getlastE k (t::s) = [::] -> ((getlastE k s)=[::]) .


Lemma in_getfirstE (k:nat)(s1:seq nat)(s:seq (seq nat)):
  s1 \in s -> head 0 s1 = k -> getfirstE k s!= [::].

Lemma in_getlastE (k:nat)(s1:seq nat)(s:seq (seq nat)):
  s1 \in s -> last 0 s1 = k -> getlastE k s!= [::].


Lemma ingetlastE_last (i:nat)(x:seq nat)(rest:seq (seq nat)):
    x \in getlastE i rest -> last 0 x = i.


Lemma ingetfirst (i:nat)(x:seq nat)(rest:seq (seq nat)):
    x \in getfirstE i rest -> head 0 x = i.


Lemma subseq_subseqgetfirstE (k:nat)(s2 rest : seq (seq nat)):
  (subseq s2 rest) -> subseq (getfirstE k s2) (getfirstE k rest).


Lemma ingetlastE (k:nat)(s2:seq nat)(rest:seq(seq nat)):
  s2 \in rest -> last 0 s2 = k -> s2 \in getlastE k rest.



Lemma subseq_subseqgetlastE (k:nat)(s2 rest : seq (seq nat)):
  (subseq s2 rest) -> subseq (getlastE k s2) (getlastE k rest).


Lemma subseq_concat (a b rest:seq (seq nat)):
  subseq (a++b) rest = subseq a rest && subseq b rest.


Lemma inseq (i a1: seq nat)(a2:seq (seq nat)): i \in a2 -> i \in (a1::a2).


Lemma insubseq (s:seq nat)(r:seq (seq nat)):
  s \in r -> subseq [::s] r.


Lemma subseq_behead (r:seq (seq nat)):
  subseq (behead r) r.


Lemma subseq_getfirstE (k:nat)(rest:seq (seq nat)):
 (subseq (getfirstE k rest)rest).


Lemma subseq_getlastE (i:nat)(rest:seq (seq nat)): (subseq (getlastE i rest)rest).

End getfirst_last.





Section canAddOrder.


Lemma norepAddOrders (i k:nat)(s:seqZ2): i!=k -> s!= [::]
 ->((head false s) != false) -> canAddOrders i k s [::] ->
 norep (addOrders i k s [::]) = norep (addOrders i (k+1) (behead s) ((i::k::nil)::nil)).



Lemma canAddOrder_tail (i k:nat)(a:seq nat)(rest: seq (seq nat)):
 (i!=k) -> uniq a ->
     (canAddOrder i k (a ::rest)) -> (canAddOrder i k rest).



Lemma last_possize (s:seq nat):
uniq s -> s!=[::] -> ((index (last 0 s) s) = (size s) - 1).



Lemma norepAddOrder_order_head (i k:nat)(d1:seq nat)(d2:seq (seq nat)):
i != k -> norep (d1::d2) ->
canAddOrder i k (d1::d2) -> norep (addOrder_order i k d1) = true.



Lemma canAddOrder_norep (i k:nat)(d:seq (seq nat)):
 i != k -> norep d->
 canAddOrder i k d -> norep (addOrder_orders i k d).


Lemma canAddOrder_nocycles (i k:nat)(s1:seq nat)(rest: seq (seq nat)):
  i!=k -> rest !=[::] -> s1 \in rest -> canAddOrder i k rest -> nocycles_order i k s1.


Lemma subseq_canAddOrder (i k:nat)(s2 rest:seq (seq nat)):
  i!=k -> norep rest -> subseq s2 rest -> canAddOrder i k rest -> canAddOrder i k s2.


End canAddOrder.


Section canAOrder.


Lemma in_nocycles_concat (s:seq nat) (rest lasts:seq (seq nat)):
  s \in rest -> nocycles_concat_orders rest lasts -> nocycles_concat_order s lasts.


Lemma subseq_nocycles (s rest lasts:seq (seq nat)):
  subseq s rest -> nocycles_concat_orders rest lasts -> nocycles_concat_orders s lasts.


Lemma nocycles_headtail (s1:seq nat)(firsts s2:seq (seq nat)):
   nocycles_concat_orders firsts (s1::s2) = nocycles_concat_orders firsts [::s1] && nocycles_concat_orders firsts s2.


Lemma in_nocycles (s1:seq nat)(firsts rest : seq (seq nat)):
  s1 \in rest -> nocycles_concat_orders firsts rest -> nocycles_concat_orders firsts [::s1].




Lemma subseq_nocycles2 (s rest firsts:seq (seq nat)):
  subseq s rest -> nocycles_concat_orders firsts rest -> nocycles_concat_orders firsts s.


Lemma nocycles_subseq (i k: nat)(s2 rest:seq (seq nat)):
  (i!=k) -> subseq s2 rest ->(nocycles_concat_orders (getfirstE k rest) (getlastE i rest)) ->
(nocycles_concat_orders (getfirstE k s2) (getlastE i s2)).


Lemma norep_seq_canAOrder (i k:nat)(a:seq nat)(rest: seq (seq nat)):
 (i!=k) -> uniq a ->
     (canAOrder i k (rest)) -> (canAOrder i k (behead rest)).


Lemma canAcanAdd_norep (i k:nat)(a c:seq nat)(r:seq (seq nat)):
 i!=k -> norep r -> head 0 a = k -> last 0 c = i -> subseq [::a] r -> subseq [::c] r ->
 canAOrder i k r -> canAddOrder i k r -> norep [::c ++ a].



Lemma norep_addOrder_concat (i k: nat)(r:orders)(rest: orders * orders):
 (i != k) -> norep r ->
 (forall x:seq nat, x \in (fst rest) -> head 0 x = k) ->
 (forall x:seq nat, x \in (snd rest) -> last 0 x = i) ->
  subseq (fst rest) r -> subseq (snd rest) r ->
  canAddOrder i k r -> canAOrder i k r ->
  norep (addOrder_concat rest).
move=> H3.
functional induction addOrder_concat rest.
 by done.
 by done.
 rewrite /fst /snd in IHo.
  rewrite e e0 => H5 H6 H7 H11.
  have H10: (forall x : seq nat, x \in d -> last 0 x = i).
    by move=> x H; move: (H7 x); rewrite inE H Bool.orb_true_r => ->.
  rewrite /subseq -/subseq.
  case H12: r=> [|r1 r2]; first by done.
  rewrite H12 in IHo H5 H11.
  case H13:(c \in (r1::r2)); last by done.
  rewrite norep_cat => H14 H15 H16.
  move: (IHo H5 H6 H10 H11 H14 H15 H16) => ->.
  have HH2: (a \in [::a]); first by rewrite inE.
  have HH3: (c \in c::d); first by rewrite inE; apply/orP; left.
  move: (H7 c HH3) => H17.
  move: (H6 a HH2)=>H18.
  have H19: (subseq [::c] (r1::r2)); first by rewrite /subseq H13.
  by rewrite (canAcanAdd_norep H3 H5 H18 H17 H11 H19 H16 H15).
 rewrite /fst /snd in IHo.
  rewrite e e0 {1}/subseq -/subseq norep_cat => H5 H6 H7.
  case H12: r=> [|r1 r2]; first by done.
  case H13: (a \in r1 :: r2); last by done.
  rewrite H12 in IHo H5 => H11 H14 H15 H16.
  have H10:(forall x : seq nat, x \in b -> head 0 x = k).
    by move=> x H; move: (H6 x); rewrite inE H Bool.orb_true_r => ->.
  move: (IHo H5 H10 H7 H11 H14 H15 H16) => ->.
  have HH3: (c \in [::c]); first by rewrite inE.
  have HH2: (a \in a::b); first by rewrite inE; apply/orP; left.
  move: (H7 c HH3) => H17.
  move: (H6 a HH2)=>H18.
  have H19: (subseq [::a] (r1::r2)); first by rewrite /subseq H13.
  by rewrite (canAcanAdd_norep H3 H5 H18 H17 H19 H14 H16 H15).
 rewrite /fst /snd in IHo IHo0.
  rewrite e e0 {1}/subseq -/subseq !norep_cat => H5 H6 H7.
  case H12: r=> [|r1 r2]; first by done.
  case H13: (a \in r1 :: r2); last by done.
  rewrite H12 in IHo H5 IHo0 => H15 H16 H17 H18.
  have H10:(forall x : seq nat, x \in b -> head 0 x = k).
    by move=> x H; move: (H6 x); rewrite inE H Bool.orb_true_r => ->.
  move: (IHo0 H5 H10 H7 H15 H16 H17 H18) => ->.
  have H19:(forall x : seq nat, x \in [:: a] -> head 0 x = k).
    by move=> x; rewrite inE => H; move: (H6 x); rewrite inE H Bool.orb_true_l => ->.
  have H20:(forall x : seq nat, x \in d -> last 0 x = i).
    by move=> x H; move: (H7 x); rewrite inE H Bool.orb_true_r => ->.
  have H21: (subseq [::a] (r1::r2)); first by rewrite /subseq H13.
  move: H16; rewrite /subseq -/subseq.
  case H22:(c \in r1 :: r2); last by done.
  move=> H23.
  move: (IHo H5 H19 H20 H21 H23 H17 H18) => ->.
  have HH2: (a \in a::b); first by rewrite inE; apply/orP; left.
  have HH3: (c \in c::d); first by rewrite inE; apply/orP; left.
  move: (H7 c HH3) => H24.
  move: (H6 a HH2)=> H25.
  have H26: (subseq [::c] (r1::r2)); first by rewrite /subseq H22.
  by rewrite (canAcanAdd_norep H3 H5 H25 H24 H21 H26 H18 H17).
Qed.