Lvc.Infra.Indexwise

Require Import Util Coq.Lists.List Setoid Coq.Lists.SetoidList Omega Containers.OrderedTypeEx.
Require Export Infra.Option EqDec AutoIndTac Get.

Set Implicit Arguments.

Definition indexwise_P {A} (P:A Prop) LA :=
   n a, get LA n a P a.

Definition indexwise_P_dec {A} {P:AProp} LA
           (Rdec:( n a, get LA n a Computable (P a)))
      : Computable (indexwise_P P LA).
unfold Computable. revert LA Rdec. fix 1. intros LA Rdec.
destruct LA; try now left; isabsurd.
intros. destruct (Rdec 0 a).
- eauto using get.
- destruct (indexwise_P_dec LA).
  + intros. eauto using get.
  + clear indexwise_P_dec. left; hnf; intros; inv H; eauto.
  + right; intro HH. eapply n; hnf; intros; eapply HH; eauto using get.
- right; intro. eapply n; hnf; intros. eapply H; eauto using get.
Defined.

Definition indexwise_R {A} {B} (R:ABProp) LA LB :=
n a b, get LA n a get LB n b R a b.

Definition indexwise_R_dec {A} {B} {R:ABProp} LA LB (Rdec:( n a b, get LA n a get LB n b Computable (R a b)))
      : Computable (indexwise_R R LA LB).
unfold Computable. revert LA LB Rdec. fix 2. intros LA LB Rdec.
destruct LA, LB; try now left; isabsurd.
intros. destruct (Rdec 0 a b).
- eauto using get.
- eauto using get.
- destruct (indexwise_R_dec LA LB).
  + intros. eauto using get.
  + left. hnf; intros. destruct n; inv H; inv H0; eauto.
  + right; intro HH. eapply n; hnf; intros; eapply HH; eauto using get.
- right; intro. eapply n; hnf; intros. eapply H; eauto using get.
Defined.

Definition indexwise_R3 {A} {B} {C} (R:A B C Prop) LA LB LC :=
n a b c, get LA n a get LB n b get LC n c R a b c.

Definition indexwise_R3_dec {A} {B} {C} {R:A B C Prop} LA LB LC
           (Rdec:( n a b c, get LA n a get LB n b get LC n c Computable (R a b c)))
      : Computable (indexwise_R3 R LA LB LC).
unfold Computable. revert LA LB LC Rdec. fix 2. intros LA LB LC Rdec.
destruct LA, LB, LC; try now left; isabsurd.
intros. destruct (Rdec 0 a b c).
- eauto using get.
- eauto using get.
- eauto using get.
- destruct (indexwise_R3_dec LA LB LC).
  + intros. eauto using get.
  + left. hnf; intros. destruct n; inv H; inv H0; inv H1; eauto.
  + right; intro HH. eapply n; hnf; intros; eapply HH; eauto using get.
- right; intro. eapply n; hnf; intros. eapply H; eauto using get.
Defined.

Definition indexwise_R4 {A} {B} {C} {D} (R:A B C D Prop) LA LB LC LD :=
n a b c d, get LA n a get LB n b get LC n c get LD n d R a b c d.

Definition indexwise_R4_dec {A} {B} {C} {D} {R:A B C D Prop} LA LB LC LD
           (Rdec:( n a b c d, get LA n a get LB n b get LC n c get LD n d
                              Computable (R a b c d)))
      : Computable (indexwise_R4 R LA LB LC LD).
unfold Computable. revert LA LB LC LD Rdec. fix 2. intros LA LB LC LD Rdec.
destruct LA, LB, LC, LD; try now left; isabsurd.
intros. destruct (Rdec 0 a b c d); try now eapply getLB.
- destruct (indexwise_R4_dec LA LB LC LD).
  + intros. eapply Rdec; eauto using get.
  + left. hnf; intros n ? ? ? ? GET1 GET2 GET3 GET4.
    destruct n; inv GET1; inv GET2; inv GET3; inv GET4; eauto.
  + right; intro HH. eapply n; hnf; intros; eapply HH; eauto using get.
- right; intro. eapply n; hnf; intros. eapply H; eauto using get.
Defined.