Lvc.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:A->B->C->Prop)
: 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 ->
exists 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
-> (forall n a b b', get AL n a -> get F1 n b -> get F2 n b' -> R DL L1 L2 a b b')
-> (forall i b, get F1 i b -> i = block_n b)
-> (forall 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
-> (forall n a b b', get AL n a -> get F1 n b -> get F2 n b' -> R DL L1 L2 a b b')
-> (forall i b, get F1 i b -> i = block_n b)
-> (forall 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
-> (forall 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 ->
exists a:A, exists 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 ->
exists b:B, exists 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 ->
exists a:A, exists 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
-> (forall 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)
(*match goal with
| H' : get ?A ?n ?b, H'' : ?x :: ?DL = drop ?n ?Lv |- _ =>
(try rewrite <- H'' in X'');
let X' := fresh H in
pose proof (get_drop_eq H' H'') as X'; inversion X'; try subst; try clear X'
end *)
| [ 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)
(*match goal with
| H' : get ?A ?n ?b, H'' : ?x :: ?DL = drop ?n ?Lv |- _ =>
(try rewrite <- H'' in X'');
let X' := fresh H in
pose proof (get_drop_eq H' H'') as X'; inversion X'; try subst; try clear X'
end *)
| [ 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.
Require Export DecSolve BlockType.
Set Implicit Arguments.
Inductive mutual_block {A} {B} `{BlockType B} {C} `{BlockType C} (R:A->B->C->Prop)
: 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 ->
exists 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
-> (forall n a b b', get AL n a -> get F1 n b -> get F2 n b' -> R DL L1 L2 a b b')
-> (forall i b, get F1 i b -> i = block_n b)
-> (forall 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
-> (forall n a b b', get AL n a -> get F1 n b -> get F2 n b' -> R DL L1 L2 a b b')
-> (forall i b, get F1 i b -> i = block_n b)
-> (forall 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
-> (forall 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 ->
exists a:A, exists 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 ->
exists b:B, exists 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 ->
exists a:A, exists 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
-> (forall 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)
(*match goal with
| H' : get ?A ?n ?b, H'' : ?x :: ?DL = drop ?n ?Lv |- _ =>
(try rewrite <- H'' in X'');
let X' := fresh H in
pose proof (get_drop_eq H' H'') as X'; inversion X'; try subst; try clear X'
end *)
| [ 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)
(*match goal with
| H' : get ?A ?n ?b, H'' : ?x :: ?DL = drop ?n ?Lv |- _ =>
(try rewrite <- H'' in X'');
let X' := fresh H in
pose proof (get_drop_eq H' H'') as X'; inversion X'; try subst; try clear X'
end *)
| [ 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.