Lvc.IL.InRel

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

Set Implicit Arguments.

Inductive mutual_block {A} {B} `{BlockType B} {C} `{BlockType C} (R:ABCProp)
: nat list A list B list C Prop :=
| CS_nil n : mutual_block R n nil nil nil
| CS_cons a b c n AL L L' :
mutual_block R (S n) AL L L'
n = block_n b
n = block_n c
R a b c
mutual_block R n (a::AL) (b::L) (c::L').

Lemma mutual_block_zero {A} {B} `{BlockType B} {C} `{BlockType C} R
(AL:list A) (L:list B) (L':list C) n b i
: mutual_block R i AL 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_zero' {A} {B} `{BlockType B} {C} `{BlockType C} R
(AL:list A) (L:list B) (L':list C) n b i
: mutual_block R i AL L L' get L' n b block_n b = (n+i).
Proof.
intros. general induction H2. inv H1; eauto.
inv H1; eauto. erewrite (IHget _ _ _ _ _ _ _ _ H5); eauto. omega.
Qed.

Lemma mutual_block_length {A} {B} `{BlockType B} {C} `{BlockType C} R
(AL:list A) (L:list B) (L':list C) i
: mutual_block R i AL L L' length AL = length L length L = length L'.
Proof.
intros. general induction H1; dcr; simpl; eauto.
Qed.

Lemma mutual_block_get {A} {B} `{BlockType B} {C} `{BlockType C} R
(AL:list A) (L:list B) (L':list C) i n b
: mutual_block R i AL L L' get L n b
a c, get AL n a get L' n c R a b c.
Proof.
intros. general induction H2; inv H1; eauto using get.
edestruct IHget as [? [? [? []]]]; try do 2 eexists; eauto using get.
Qed.

Lemma mutual_approx_impl {A} {B} `{BlockType B} {C} `{BlockType C}
(R: list A list B list C A B C Prop)
(AL:list A) DL F1 F2 AL' F1' F2' i L1 L2
: length AL = length F1
length F1 = length F2
F1' = drop i F1
F2' = drop i F2
AL' = drop i AL
( n a b b', get AL n a get F1 n b get F2 n b' R DL L1 L2 a b b')
( i b, get F1 i b i = block_n b)
( i b, get F2 i b i = block_n b)
mutual_block (R DL L1 L2) i AL' F1' F2'.
Proof.
intros LenEq1 LenEq2 LenF1' LenF2' LenAL' GET I1 I2.
assert (LenAL1:length_eq AL' F1'). subst; eauto using drop_length_stable with len.
assert (LenAL2:length_eq AL' F2'). subst; eauto using drop_length_stable with len.
general induction LenAL1; inv LenAL2; eauto using @mutual_block.
- econstructor; eauto using drop_eq.
eapply IHLenAL1; eauto using drop_shift_1.
Qed.

Lemma mutual_approx {A} {B} `{BlockType B} {C} `{BlockType C}
(R: list A list B list C A B C Prop)
(AL:list A) DL F1 F2 L1 L2
: length AL = length F1
length F1 = length F2
( n a b b', get AL n a get F1 n b get F2 n b' R DL L1 L2 a b b')
( i b, get F1 i b i = block_n b)
( i b, get F2 i b i = block_n b)
mutual_block (R DL L1 L2) 0 AL F1 F2.
Proof.
intros. eapply mutual_approx_impl; eauto.
Qed.

Lemma mutual_block_mon A B (H : BlockType B) (C : Type)
(H0 : BlockType C)
(R R': A B C Prop) AL L1 L2 n
: mutual_block R n AL L1 L2
( a b c, R a b c R' a b c)
mutual_block R' n AL L1 L2.
Proof.
intros. general induction H1.
- econstructor.
- econstructor; eauto.
Qed.

Inductive inRel {A} {B} `{BlockType B} {C} `{BlockType C}
(R:list A list B list C A B C Prop)
: list A list B list C Prop :=
| LPM_nil : inRel R nil nil nil
| LPM_app AL AL' L1 L2 L1' L2' :
inRel R AL L1 L2
mutual_block (R (AL'++AL) (L1'++L1) (L2'++L2)) 0 AL' L1' L2'
inRel R (AL'++AL) (L1'++L1) (L2'++L2).

Lemma inRel_length {A} {B} `{BlockType B} {C} `{BlockType C} R
(AL:list A) (L:list B) (L':list C)
: inRel R AL L L' length AL = length L length L = length L'.
Proof.
intros. general induction H1; dcr; simpl; eauto.
repeat rewrite app_length.
exploit (mutual_block_length H2); eauto; dcr; omega.
Qed.

Lemma inRel_less {A} {B} `{BlockType B} {C} `{BlockType C} R
(AL:list A) (L:list B) (L':list C) n b
: inRel R AL L L' get L n b block_n b n.
Proof.
intros. general induction H1. inv H2; eauto.
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 {A} {B} `{BlockType B} {C} `{BlockType C} R
(LT:list A) (L:list B) (L':list C) n b
: inRel R LT L L'
get L n b
inRel R
(drop (n - block_n b) LT)
(drop (n - block_n b) L)
(drop (n - block_n b) L').
Proof.
intros. general induction H1; simpl; eauto.
- inv H2.
- 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.
specialize (IHinRel _ _ H4).
assert (length L1' + (n - length L1') = n) by omega.
rewrite <- H6.
orewrite (length L1' + (n - length L1') - block_n b
= length L1' + (n - length L1' - block_n b)).
exploit (mutual_block_length H2). dcr.
Typeclasses eauto := 5.
rewrite <- H8 at 1.
rewrite H9 at 4.
repeat rewrite drop_app. eauto.
Qed.

Lemma inRel_nth {A} {B} `{BlockType B} {C} `{BlockType C} R
(AL:list A) (L:list B) (L':list C) n b
: inRel R AL L L' get L n b
a:A, c:C,
get AL n a get L' n c R (drop (n - block_n b) AL) (drop (n - block_n b) L) (drop (n - block_n b) L') a 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) as [? [? [? []]]].
do 2 eexists. repeat split; eauto using get_app.
- edestruct IHinRel; eauto; dcr. do 2 eexists.
pose proof (mutual_block_length H2); dcr.
repeat split; try (eapply get_app_right; eauto; omega).
orewrite (n = length L1' + (n - length L1')).
exploit (inRel_less H1 H4).
orewrite (length L1' + (n - length L1') - block_n b
= length L1' + (n - length L1' - block_n b)).
Typeclasses eauto :=10.
rewrite <- H8 at 1. repeat rewrite drop_app. rewrite H10. rewrite drop_app.
rewrite <- H10. eauto.
Qed.

Lemma inRel_nthA {A} {B} `{BlockType B} {C} `{BlockType C} R
(AL:list A) (L:list B) (L':list C) n a
: inRel R AL L L' get AL n a
b:B, c:C,
get L n b get L' n c R (drop (n - block_n b) AL) (drop (n - block_n b) L) (drop (n - block_n b) L') a b c.
Proof.
intros.
exploit (inRel_length H1); eauto; dcr.
edestruct (get_length_eq _ H2 H4); eauto.
edestruct (inRel_nth H1 H3); eauto; dcr.
get_functional; subst.
do 2 eexists; split; eauto.
Qed.

Lemma inRel_nthC {A} {B} `{BlockType B} {C} `{BlockType C} R
(AL:list A) (L:list B) (L':list C) n c
: inRel R AL L L' get L' n c
a:A, b:B,
get AL n a get L n b R (drop (n - block_n b) AL) (drop (n - block_n b) L) (drop (n - block_n b) L') a b c.
Proof.
intros.
exploit (inRel_length H1); eauto; dcr.
edestruct (get_length_eq _ H2 (eq_sym H5)); eauto.
edestruct (inRel_nth H1 H3); eauto; dcr.
get_functional; subst.
do 2 eexists; split; eauto.
Qed.

Lemma inRel_mon A B (H : BlockType B) (C : Type)
(H0 : BlockType C)
(R R': list A list B list C A B C Prop) AL L1 L2
: inRel R AL L1 L2
( AL L1 L2 a b c, R AL L1 L2 a b c R' AL L1 L2 a b c)
inRel R' AL L1 L2.
Proof.
intros. general induction H1.
- econstructor.
- econstructor; eauto using mutual_block_mon.
Qed.

Tactic Notation "inRel_invs" :=
match goal with
| [ H : inRel ?R ?A ?B ?C, H' : get ?B ?n ?b |- _ ] ⇒
let InR := fresh "InR" in let G := fresh "G" in
edestruct (inRel_nth H H') as [? [? [? [G InR]]]]; (try eassumption); dcr; inversion InR; try subst;
let X'' := fresh "H" in pose proof (inRel_drop H H') as X'';
repeat get_functional; (try subst)

| [ H : inRel ?R ?A ?B ?C, H' : get ?A ?n ?a |- _ ] ⇒
let InR := fresh "InR" in let G := fresh "G" in
edestruct (inRel_nthA H H') as [? [? [? [G InR]]]]; (try eassumption); dcr; inversion InR; try subst;
repeat get_functional; (try subst)

| [ H : inRel ?R ?A ?B ?C, H' : get ?C ?n ?c |- _ ] ⇒
let InR := fresh "InR" in let G := fresh "G" in
edestruct (inRel_nthC H H') as [? [? [? [G InR]]]]; (try eassumption); dcr; inversion InR; try subst;
repeat get_functional; (try subst)
end.