Lvc.IL.InRel4

Require Import Util LengthEq AllInRel Map Env IL AutoIndTac MoreList.
Require Export DecSolve BlockType.

Set Implicit Arguments.
Inductive mutual_block {A1 A2 A3 A4} {B} `{BlockType B} {C} `{BlockType C} (R:A1A2A3A4BCProp)
: nat list A1 list A2 list A3 list A4 list B list C Prop :=
  | CS_nil n : mutual_block R n nil nil nil nil nil nil
  | CS_cons a1 a2 a3 a4 b c n AL1 AL2 AL3 AL4 L L' :
      mutual_block R (S n) AL1 AL2 AL3 AL4 L L'
       n = block_n b
       n = block_n c
       R a1 a2 a3 a4 b c
       mutual_block R n (a1::AL1) (a2::AL2) (a3::AL3) (a4::AL4) (b::L) (c::L').

Lemma mutual_block_zero {A1 A2 A3 A4} {B} `{BlockType B} {C} `{BlockType C} (R:A1A2A3A4BCProp)
      AL1 AL2 AL3 AL4 (L:list B) (L':list C) n b i
: mutual_block R i AL1 AL2 AL3 AL4 L L' get L n b block_n b = (n+i).
Proof.
  intros. general induction H2. inv H1; eauto.
  inv H1; eauto. erewrite IHget; eauto. omega.
Qed.

Lemma mutual_block_length {A1 A2 A3 A4} {B} `{BlockType B} {C} `{BlockType C} (R:A1A2A3A4BCProp)
      AL1 AL2 AL3 AL4 (L1:list B) (L2:list C) i
: mutual_block R i AL1 AL2 AL3 AL4 L1 L2 AL1 = L1 AL2 = L1 AL3 = L1 AL4 = L1 L2 = L1.
Proof.
  intros. general induction H1; dcr; simpl; eauto.
  repeat split; omega.
Qed.

Lemma mutual_block_get {A1 A2 A3 A4} {B} `{BlockType B} {C} `{BlockType C} (R:A1A2A3A4BCProp)
      AL1 AL2 AL3 AL4 (L1:list B) (L2:list C) i n b
: mutual_block R i AL1 AL2 AL3 AL4 L1 L2 get L1 n b
   a1 a2 a3 a4 c, get AL1 n a1 get AL2 n a2 get AL3 n a3 get AL4 n a4
                    get L2 n c R a1 a2 a3 a4 b c.
Proof.
  intros. general induction H2; inv H1; eauto 20 using get.
  edestruct IHget; dcr; eauto 20 using get.
Qed.

Lemma mutual_block_get_A1 {A1 A2 A3 A4} {B} `{BlockType B} {C} `{BlockType C} (R:A1A2A3A4BCProp)
      AL1 AL2 AL3 AL4 (L1:list B) (L2:list C) i n a1
: mutual_block R i AL1 AL2 AL3 AL4 L1 L2 get AL1 n a1
   a2 a3 a4 b c, get AL2 n a2 get AL3 n a3 get AL4 n a4
                   get L1 n b get L2 n c R a1 a2 a3 a4 b c.
Proof.
  intros. general induction H2; inv H1; eauto 20 using get.
  edestruct IHget; dcr; eauto 20 using get.
Qed.

Lemma mutual_approx k {A1 A2 A3 A4} {B} `{BlockType B} {C} `{BlockType C}
      (R:list A1 list A2 list A3 list A4 list B list C
         A1 A2 A3 A4 B C Prop)
      AL1 AL2 AL3 AL4 AL1' AL2' AL3' AL4' F1 F2 L1 L2
  : length AL1' = length F1
     length AL1' = length AL2'
     length AL2' = length AL3'
     length AL3' = length AL4'
     length F1 = length F2
     ( n a1 a2 a3 a4 b b', get AL1' n a1 get AL2' n a2 get AL3' n a3 get AL4' n a4
                              get F1 n b get F2 n b' R AL1 AL2 AL3 AL4 L1 L2 a1 a2 a3 a4 b b')
     ( i b, get F1 i b k + i = block_n b)
     ( i b, get F2 i b k + i = block_n b)
     mutual_block (R AL1 AL2 AL3 AL4 L1 L2) k AL1' AL2' AL3' AL4' F1 F2.
Proof.
  intros. length_equify.
  general induction H1; eauto using @mutual_block.
  econstructor; eauto using get. eapply IHlength_eq; eauto 20 using get.
  intros. exploit H7. econstructor 2. eauto. omega.
  intros. exploit H8. econstructor 2. eauto. omega.
  exploit H7; eauto using get. omega.
  exploit H8; eauto using get. omega.
Qed.

Inductive inRel {A1 A2 A3 A4} {B} `{BlockType B} {C} `{BlockType C}
          (R:list A1 list A2 list A3 list A4 list B list C
             A1 A2 A3 A4 B C Prop)
: list A1 list A2 list A3 list A4 list B list C Prop :=
  | LPM_nil : inRel R nil nil nil nil nil nil
  | LPM_app AL1 AL2 AL3 AL4 AL1' AL2' AL3' AL4' L1 L2 L1' L2' :
      inRel R AL1 AL2 AL3 AL4 L1 L2
       mutual_block (R (AL1'++AL1) (AL2'++AL2) (AL3'++AL3) (AL4'++AL4) (L1'++L1) (L2'++L2))
                     0 AL1' AL2' AL3' AL4' L1' L2'
       inRel R (AL1'++AL1) (AL2'++AL2) (AL3'++AL3) (AL4'++AL4) (L1'++L1) (L2'++L2).
Lemma inRel_less {A1 A2 A3 A4:Type} {B} `{BlockType B} {C} `{BlockType C}
      (R:list A1 list A2 list A3 list A4 list B list C
         A1 A2 A3 A4 B C Prop)
      AL1 AL2 AL3 AL4 (L:list B) (L':list C) n b
: inRel R AL1 AL2 AL3 AL4 L L' get L n b block_n b n.
Proof.
  intros. general induction H1.
  eapply get_app_cases in H3; destruct H3; dcr.
  erewrite mutual_block_zero; eauto. omega.
  rewrite IHinRel; try eapply H4. omega.
Qed.

Lemma inRel_drop {A1 A2 A3 A4:Type} {B} `{BlockType B} {C} `{BlockType C}
      (R:list A1 list A2 list A3 list A4 list B list C
         A1 A2 A3 A4 B C Prop)
      AL1 AL2 AL3 AL4 (L:list B) (L':list C) n b
: inRel R AL1 AL2 AL3 AL4 L L'
   get L n b
   inRel R
          (drop (n - block_n b) AL1)
          (drop (n - block_n b) AL2)
          (drop (n - block_n b) AL3)
          (drop (n - block_n b) AL4)
          (drop (n - block_n b) L)
          (drop (n - block_n b) L').
Proof.
  intros. general induction H1; simpl; eauto; isabsurd.
  - eapply get_app_cases in H3; destruct H3; dcr.
    + exploit (mutual_block_zero H2 H3); eauto.
      rewrite H4. orewrite (n - (n + 0)= 0). simpl; econstructor; eauto.
    + exploit (inRel_less H1 H4); eauto.
      exploit (mutual_block_length H2); dcr.
      specialize (IHinRel _ _ H4).
      repeat (rewrite drop_app_gen; [| omega]).
      assert (REO: m, block_n b n - L1' m = L1'
                        n - block_n b - m = n - L1' - block_n b). {
        intros. omega.
      }
      repeat (rewrite REO; eauto).
Qed.

Lemma inRel_nth {A1 A2 A3 A4:Type} {B} `{BlockType B} {C} `{BlockType C}
      (R:list A1 list A2 list A3 list A4 list B list C
         A1 A2 A3 A4 B C Prop)
      AL1 AL2 AL3 AL4 (L:list B) (L':list C) n b
: inRel R AL1 AL2 AL3 AL4 L L' get L n b
   a1:A1, a2:A2, a3:A3, a4:A4, c:C,
            get AL1 n a1 get AL2 n a2 get AL3 n a3 get AL4 n a4 get L' n c
             R (drop (n - block_n b) AL1) (drop (n - block_n b) AL2) (drop (n - block_n b) AL3) (drop (n - block_n b) AL4) (drop (n - block_n b) L) (drop (n - block_n b) L') a1 a2 a3 a4 b c.
Proof.
  intros. general induction H1; isabsurd.
  eapply get_app_cases in H3; destruct H3; dcr.
  - exploit (mutual_block_zero H2 H3); eauto. rewrite H4.
    orewrite (n - (n + 0) = 0). simpl.
    edestruct (mutual_block_get H2 H3); dcr.
    eauto 20 using get_app, get.
  - edestruct IHinRel; eauto; dcr.
    pose proof (mutual_block_length H2); dcr.
    do 5 eexists.
    repeat split; try (eapply get_app_right; [ | eauto ]; omega).
    exploit (inRel_less H1 H4); eauto.
    repeat (rewrite drop_app_gen; [| omega]).
    assert (REO: m, block_n b n - L1' m = L1'
                      n - block_n b - m = n - L1' - block_n b). {
      intros. omega.
    }
    repeat (rewrite REO; eauto).
Qed.

Lemma inRel_nth_A1 {A1 A2 A3 A4:Type} {B} `{BlockType B} {C} `{BlockType C}
      (R:list A1 list A2 list A3 list A4 list B list C
         A1 A2 A3 A4 B C Prop)
      AL1 AL2 AL3 AL4 (L:list B) (L':list C) n a1
: inRel R AL1 AL2 AL3 AL4 L L' get AL1 n a1
   a2:A2, a3:A3, a4:A4, b:B, c:C,
            get AL2 n a2 get AL3 n a3 get AL4 n a4 get L n b get L' n c
             R (drop (n - block_n b) AL1) (drop (n - block_n b) AL2) (drop (n - block_n b) AL3) (drop (n - block_n b) AL4) (drop (n - block_n b) L) (drop (n - block_n b) L') a1 a2 a3 a4 b c.
Proof.
  intros. general induction H1; isabsurd.
  eapply get_app_cases in H3; destruct H3; dcr.
  - edestruct (mutual_block_get_A1 H2 H3); dcr.
    exploit (mutual_block_zero H2 H8); eauto.
    eexists x, x0, x1, x2, x3.
    rewrite H4.
    orewrite (n - (n + 0) = 0). simpl.
    eauto 20 using get_app, get.
  - edestruct IHinRel; eauto; dcr.
    pose proof (mutual_block_length H2); dcr.
    do 5 eexists.
    repeat split; try (eapply get_app_right; [ | eauto ]; omega).
    exploit (inRel_less H1 H9); eauto.
    repeat (rewrite drop_app_gen; [| omega]).
    assert (REO: m, block_n x2 n - AL1' m = AL1'
                      n - block_n x2 - m = n - AL1' - block_n x2). {
      intros. omega.
    }
    repeat (rewrite REO; eauto); try congruence.
Qed.

Tactic Notation "inRel_invs" :=
  match goal with
  | [ H : inRel ?R ?A1 ?A2 ?A3 ?A4 ?B ?C, H' : get ?A1 ?n ?b |- _ ] ⇒
    let InR := fresh "InR" in
    let G := fresh "G" in
    let GetL := fresh "GetL" in
    edestruct (inRel_nth_A1 H H') as [? [? [? [? [? [? [? [? [GetL [? ]]]]] ]]]]];
    let X'' := fresh "H" in
    pose proof (inRel_drop H GetL) as X'';
    repeat get_functional
  end.

Lemma mutual_block_map_A3 {A1 A2 A3 A4} {B} `{BlockType B} {C} `{BlockType C}
      (R:list A1 list A2 list A3 list A4 list B list C
         A1 A2 A3 A4 B C Prop)
      AL1' AL1 AL2' AL2 AL3' AL3 AL4' AL4 L1' L1 L2' L2 n (f: A3 A3)
      (Rf: AL1 AL2 AL3 AL4 L1 L2 a1 a2 a3 a4 b1 b2,
          R AL1 AL2 AL3 AL4 L1 L2 a1 a2 a3 a4 b1 b2
          R AL1 AL2 (f AL3) AL4 L1 L2 a1 a2 (f a3) a4 b1 b2 )
  : mutual_block
      (R AL1 AL2 AL3 AL4 L1 L2) n AL1' AL2' AL3' AL4' L1' L2'
     mutual_block (R AL1 AL2 (f AL3) AL4 L1 L2) n AL1' AL2' (f AL3') AL4' L1' L2'.
Proof.
  intros. general induction H1; eauto using @mutual_block.
  simpl. econstructor; eauto.
Qed.

Lemma inRel_map_A3 {A1 A2 A3 A4} {B} `{BlockType B} {C} `{BlockType C}
      (R:list A1 list A2 list A3 list A4 list B list C
         A1 A2 A3 A4 B C Prop)
      AL1 AL2 AL3 AL4 L1 L2 (f: A3 A3)
      (Rf: AL1 AL2 AL3 AL4 L1 L2 a1 a2 a3 a4 b1 b2,
          R AL1 AL2 AL3 AL4 L1 L2 a1 a2 a3 a4 b1 b2
          R AL1 AL2 (f AL3) AL4 L1 L2 a1 a2 (f a3) a4 b1 b2 )
  : inRel R AL1 AL2 AL3 AL4 L1 L2
     inRel R AL1 AL2 (f AL3) AL4 L1 L2.
Proof.
  intros IR.
  general induction IR; simpl in *; eauto using @inRel.
  - rewrite List.map_app. econstructor; eauto.
    rewrite <- List.map_app.
    eapply mutual_block_map_A3; eauto.
Qed.

Lemma inRel_length {A1 A2 A3 A4} {B} `{BlockType B} {C} `{BlockType C}
      (R:list A1 list A2 list A3 list A4 list B list C
         A1 A2 A3 A4 B C Prop)
      AL1 AL2 AL3 AL4 L1 L2
  : inRel R AL1 AL2 AL3 AL4 L1 L2 length AL1 = length AL2 length AL2 = length AL3
                                    length AL3 = length AL4 length L1 = length L2.
Proof.
  intros. general induction H1; dcr; simpl; eauto.
  repeat rewrite app_length.
  exploit (mutual_block_length H2); eauto; dcr; omega.
Qed.