(**************************************************************)
(*   Copyright Dominique Larchey-Wendling [*]                 *)
(*                                                            *)
(*                             [*] Affiliation LORIA -- CNRS  *)
(**************************************************************)
(*      This file is distributed under the terms of the       *)
(*         CeCILL v2 FREE SOFTWARE LICENSE AGREEMENT          *)
(**************************************************************)

Require Import List Arith Omega.

Require Import utils.

Set Implicit Arguments.

Section subcode.

  Variable (X : Type).
  
  Definition code := (nat * list X)%type.

  Implicit Type P : code.
  
  Definition code_start P := fst P.
  Definition code_end P := fst P + length (snd P).
  Definition code_length P := length (snd P).
 
  Definition in_code i P := code_start P <= i < code_end P.
  Definition out_code i P := i < code_start P \/ code_end P <= i.
  
  Fact in_out_code i P : in_code i P -> out_code i P -> False.
(* Goal: forall (_ : in_code i P) (_ : out_code i P), False *)
  Proof. unfold in_code, out_code; omega. Qed.

  Definition subcode P Q := 
    match P, Q with (i,li), (n,code) => exists l r, code = l ++ li ++ r /\ i = n+length l end.
    
  Arguments code_start P /.
  Arguments code_end P /.
  Arguments code_length P /.
  Arguments in_code i P /.
  Arguments out_code i P /.
  Arguments subcode P Q /.
 
  Fact in_out_code_dec i P : { in_code i P } + { out_code i P }.
  Proof. destruct P as (n,c); simpl; apply interval_dec. Qed.
  
  Infix "<sc" := subcode (at level 70, no associativity).

  Fact subcode_cons_inj i ρ δ P : (i,ρ::nil) <sc P -> (i,δ::nil) <sc P -> ρ = δ.
  Proof.
(* Goal: forall (_ : subcode (@pair nat (list X) i (@cons X ρ (@nil X))) P) (_ : subcode (@pair nat (list X) i (@cons X δ (@nil X))) P), @eq X ρ δ *)
    destruct P as (j, P).
(* Goal: forall (_ : subcode (@pair nat (list X) i (@cons X ρ (@nil X))) (@pair nat (list X) j P)) (_ : subcode (@pair nat (list X) i (@cons X δ (@nil X))) (@pair nat (list X) j P)), @eq X ρ δ *)
    intros (l1 & r1 & H1 & H2) (l2 & r2 & H3 & H4).
(* Goal: @eq X ρ δ *)
    rewrite H1 in H3.
(* Goal: @eq X ρ δ *)
    apply list_app_inj, proj2 in H3; try omega.
(* Goal: @eq X ρ δ *)
    inversion H3; trivial.
  Qed.

  Fact subcode_length P Q : P <sc Q -> code_start Q <= code_start P /\ code_end P <= code_end Q.
  Proof.
(* Goal: forall _ : subcode P Q, and (le (code_start Q) (code_start P)) (le (code_end P) (code_end Q)) *)
   destruct P as (iP,cP); destruct Q as (iQ,cQ); simpl.
(* Goal: forall _ : @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cQ (@app X l (@app X cP r))) (@eq nat iP (Init.Nat.add iQ (@length X l))))), and (le iQ iP) (le (Init.Nat.add iP (@length X cP)) (Init.Nat.add iQ (@length X cQ))) *)
   intros (l & r & H1 & H2).
(* Goal: and (le iQ iP) (le (Init.Nat.add iP (@length X cP)) (Init.Nat.add iQ (@length X cQ))) *)
   apply f_equal with (f := @length _) in H1.
(* Goal: and (le iQ iP) (le (Init.Nat.add iP (@length X cP)) (Init.Nat.add iQ (@length X cQ))) *)
   revert H1; rew length; split; omega.
  Qed.

  Fact subcode_length' P Q : P <sc Q -> length (snd P) <= length (snd Q).
  Proof.
(* Goal: forall _ : subcode P Q, le (@length X (@snd nat (list X) P)) (@length X (@snd nat (list X) Q)) *)
    revert P Q; intros [] [] (? & ? & ? & ?); simpl; subst; rew length; omega.
  Qed.

  Fact subcode_length_le : forall P Q, P <sc Q -> fst Q <= fst P 
                                               /\ fst P + length (snd P) <= fst Q + length (snd Q).
  Proof.
(* Goal: forall (P : code) (Q : prod nat (list X)) (_ : subcode P Q), and (le (@fst nat (list X) Q) (@fst nat (list X) P)) (le (Init.Nat.add (@fst nat (list X) P) (@length X (@snd nat (list X) P))) (Init.Nat.add (@fst nat (list X) Q) (@length X (@snd nat (list X) Q)))) *)
    intros (iP,cP) (iQ,cQ) (l & r & ? & ?); subst; simpl; rew length; omega.
  Qed.
  
  Fact subcode_start_in_code : forall P Q, 0 < code_length P -> P <sc Q -> in_code (code_start P) Q.
  Proof.
(* Goal: forall (P : code) (Q : prod nat (list X)) (_ : lt O (code_length P)) (_ : subcode P Q), in_code (code_start P) Q *)
    intros (iP,cP) (iQ,cQ) H (l & r & H1 & H2); simpl in *; subst; revert H; rew length; intro; omega.
  Qed.

  Fact subcode_refl P : P <sc P.
  Proof.
(* Goal: subcode P P *)
    destruct P; exists nil, nil; split; simpl.
(* Goal: @eq (list X) (@app X l r) (@app X l (@app X r (@nil X))) *)
    rewrite <- app_nil_end; auto.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    omega.
  Qed.

  Fact subcode_trans P Q R : P <sc Q -> Q <sc R -> P <sc R.
  Proof.
(* Goal: forall (_ : subcode P Q) (_ : subcode Q R), subcode P R *)
    revert P Q R; intros (iP,cP) (iQ,cQ) (iR,cR).
(* Goal: forall (_ : subcode (@pair nat (list X) iP cP) (@pair nat (list X) iQ cQ)) (_ : subcode (@pair nat (list X) iQ cQ) (@pair nat (list X) iR cR)), subcode (@pair nat (list X) iP cP) (@pair nat (list X) iR cR) *)
    intros (ll1 & rr1 & H1 & H2) (ll2 & rr2 & H3 & H4); subst.
(* Goal: subcode (@pair nat (list X) (Init.Nat.add (Init.Nat.add iR (@length X ll2)) (@length X ll1)) cP) (@pair nat (list X) iR (@app X ll2 (@app X (@app X ll1 (@app X cP rr1)) rr2))) *)
    exists (ll2++ll1), (rr1++rr2); split.
(* Goal: @eq (list X) (@app X l a) (@app X l (@app X a (@nil X))) *)
    solve list eq.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    rew length; omega.
  Qed.
  
  Fact subcode_in_code P Q i : P <sc Q -> in_code i P -> in_code i Q.
  Proof. 
(* Goal: forall (_ : subcode P Q) (_ : out_code i Q), out_code i P *)
    revert P Q; intros (iP,cP) (iQ,cQ) (l & r & H1 & H2); simpl.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    subst; rew length; omega.
  Qed.
  
  Fact subcode_out_code P Q i : P <sc Q -> out_code i Q -> out_code i P.
  Proof. 
(* Goal: forall (_ : subcode P Q) (_ : out_code i Q), out_code i P *)
    revert P Q; intros (iP,cP) (iQ,cQ) (l & r & H1 & H2); simpl.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    subst; rew length; omega.
  Qed.
  
  Fact subcode_left n m l r : n = m -> (n,l) <sc (m,l++r).
  Proof. exists nil, r; simpl; split; auto; omega. Qed.
  
  Fact subcode_right n m l r : n = m+length l -> (n,r) <sc (m,l++r).
  Proof.
(* Goal: subcode (@pair nat (list X) j a) (@pair nat (list X) i (@app X l a)) *)
    exists l, nil; split; auto.
(* Goal: @eq (list X) (@app X l r) (@app X l (@app X r (@nil X))) *)
    rewrite <- app_nil_end; auto.
  Qed.

  Fact subcode_app_end P n l r : P <sc (n,l) -> P <sc (n,l++r).
  Proof.
(* Goal: forall _ : subcode P (@pair nat (list X) (Init.Nat.add (S O) n) l), subcode P (@pair nat (list X) n (@cons X x l)) *)
    intros; apply subcode_trans with (1 := H).
(* Goal: subcode (@pair nat (list X) n l) (@pair nat (list X) n (@app X l r)) *)
    exists nil, r; auto.
  Qed.

  Fact subcode_cons P n x l : P <sc (1+n,l) -> P <sc (n,x::l).
  Proof.
(* Goal: forall _ : subcode P (@pair nat (list X) (Init.Nat.add (S O) n) l), subcode P (@pair nat (list X) n (@cons X x l)) *)
    intros; apply subcode_trans with (1 := H).
(* Goal: subcode (@pair nat (list X) (Init.Nat.add (S O) n) l) (@pair nat (list X) n (@cons X x l)) *)
    exists (x::nil), nil; split.
(* Goal: @eq (list X) (@app X l a) (@app X l (@app X a (@nil X))) *)
    solve list eq.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    rew length; omega.
  Qed.
  
  Fact in_code_subcode i P : in_code i P -> exists a, (i,a::nil) <sc P.
  Proof.
(* Goal: forall _ : in_code i P, @ex X (fun a : X => subcode (@pair nat (list X) i (@cons X a (@nil X))) P) *)
    destruct P as (iP,cP); simpl; intros H.
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    destruct (list_split_length cP) with (k := i-iP) as (l & [ | a r ] & H1 & H2).
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    omega.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    exfalso; subst; solve list eq in H; omega.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    exists a, l, r; split; auto; omega.
  Qed.

  Fact subcode_app_invert_right j Q1 Q2 i I : 
        (i,I::nil) <sc (j,Q1++Q2) -> (i,I::nil) <sc (j,Q1)
                                  \/ (i,I::nil) <sc (length Q1+j,Q2).
  Proof.
(* Goal: forall _ : subcode (@pair nat (list X) i (@cons X I (@nil X))) (@pair nat (list X) j (@app X Q1 Q2)), or (subcode (@pair nat (list X) i (@cons X I (@nil X))) (@pair nat (list X) j Q1)) (subcode (@pair nat (list X) i (@cons X I (@nil X))) (@pair nat (list X) (Init.Nat.add (@length X Q1) j) Q2)) *)
    intros (l & r & H1 & H2); simpl in *.
(* Goal: or (@ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) Q1 (@app X l (@cons X I r))) (@eq nat i (Init.Nat.add j (@length X l)))))) (@ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) Q2 (@app X l (@cons X I r))) (@eq nat i (Init.Nat.add (Init.Nat.add (@length X Q1) j) (@length X l)))))) *)
    apply list_app_cons_eq_inv in H1.
(* Goal: or (@ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) Q1 (@app X l (@cons X I r))) (@eq nat i (Init.Nat.add j (@length X l)))))) (@ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) Q2 (@app X l (@cons X I r))) (@eq nat i (Init.Nat.add (Init.Nat.add (@length X Q1) j) (@length X l)))))) *)
    destruct H1 as [ (m & G1 & G2) | (m & G1 & G2) ]; subst.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    + right; exists m, r; rew length; split; auto; omega.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    + left; exists l, m; rew length; split; auto; omega.
  Qed.

  Fact subcode_cons_invert_right j J Q i I : 
        (i,I::nil) <sc (j,J::Q) -> i = j /\ I = J
                                \/ (i,I::nil) <sc (S j,Q).
  Proof.
(* Goal: forall _ : subcode (@pair nat (list X) i (@cons X I (@nil X))) (@pair nat (list X) j (@cons X J Q)), or (and (@eq nat i j) (@eq X I J)) (subcode (@pair nat (list X) i (@cons X I (@nil X))) (@pair nat (list X) (S j) Q)) *)
    intros ([ | K l ] & r & H1 & H2); simpl in *.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    + inversion H1; left; split; auto; omega.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    + right; inversion H1; exists l, r; split; auto; omega.
  Qed.

  Variable Q : code.

  Fact subcode_app_inv i j a l r : j = i+length l -> (i,l++a++r) <sc Q -> (j,a) <sc Q.
  Proof.
(* Goal: forall (_ : @eq nat j (Init.Nat.add i (@length X l))) (_ : subcode (@pair nat (list X) i (@app X l (@app X a r))) Q), subcode (@pair nat (list X) j a) Q *)
    intro; apply subcode_trans.
(* Goal: subcode (@pair nat (list X) j a) (@pair nat (list X) i (@app X l (@app X a r))) *)
    exists l, r; auto.
  Qed.
  
  Fact subcode_cons_inv i j a r : j = i -> (i,a++r) <sc Q -> (j,a) <sc Q.
  Proof.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    intro; apply subcode_app_inv with (l := nil); simpl; omega.
  Qed.

  Fact subcode_snoc_inv i j a l : j = i+length l -> (i,l++a) <sc Q -> (j,a) <sc Q.
  Proof.
(* Goal: forall (_ : @eq nat j (Init.Nat.add i (@length X l))) (_ : subcode (@pair nat (list X) i (@app X l a)) Q), subcode (@pair nat (list X) j a) Q *)
    intros H.
(* Goal: forall _ : subcode (@pair nat (list X) i (@app X l a)) Q, subcode (@pair nat (list X) j a) Q *)
    apply subcode_trans.
(* Goal: subcode (@pair nat (list X) j a) (@pair nat (list X) i (@app X l a)) *)
    exists l, nil; split; auto.
(* Goal: @eq (list X) (@app X l a) (@app X l (@app X a (@nil X))) *)
    solve list eq.
  Qed.

  Fact subcode_cons_invert_left i I l : (i,I::l) <sc Q -> (i,I::nil) <sc Q /\ (S i,l) <sc Q.
  Proof.
(* Goal: forall _ : subcode (@pair nat (list X) i (@cons X I l)) Q, and (subcode (@pair nat (list X) i (@cons X I (@nil X))) Q) (subcode (@pair nat (list X) (S i) l) Q) *)
    intros H1; split.
    + revert H1; apply subcode_cons_inv with (a := _::nil); auto.
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
    + revert H1; apply subcode_snoc_inv with (l := _::nil); simpl; omega.
  Qed.

End subcode.

Arguments code_start {X} P /.
Arguments code_end {X} P /.
Arguments in_code {X} i P /.
Arguments out_code {X} i P /.
Arguments subcode {X} P Q /.

Infix "<sc" := subcode (at level 70, no associativity).


(* Solve many subcode goals looking for a solution into hyps *)
      
Ltac subcode_tac := 
       unfold fst, snd;
       try match goal with | H: subcode (_,?l) ?c |- subcode (_,?i) ?c 
            => (match i with ?j::nil => match type of H with context[j] => apply subcode_trans with (2 := H) end end ||
                match type of H with context[i] => apply subcode_trans with (2 := H) end)
       end;
       match goal with
         | |- subcode (_,?i) (_,?c) => focus_goal i c 
       end;
       match goal with 
         | |- subcode (_,?i::nil) (_,?l++?i::?r) => exists l, r 
         | |- subcode _ (_,?l++_++?r)            => exists l, r 
         | |- subcode (_,?i) (_,?l++?i)          => exists l, nil 
       end;
(* Goal: le (Init.Nat.sub i iP) (@length X cP) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
(* Goal: @ex X (fun a : X => @ex (list X) (fun l : list X => @ex (list X) (fun r : list X => and (@eq (list X) cP (@app X l (@cons X a r))) (@eq nat i (Init.Nat.add iP (@length X l)))))) *)
       split; auto; rew length; try omega.

(* Add it to auto so that fam sss * will try it to solve the subcode goal it generates *)

Hint Extern 4 (subcode _ _) => subcode_tac.
