Library Paco.paco7

Require Export paconotation pacotacuser.
Require Import paconotation_internal pacotac pacon.
Set Implicit Arguments.

Section PACO7.

Variable T0 : Type.
Variable T1 : forall (x0: @T0), Type.
Variable T2 : forall (x0: @T0) (x1: @T1 x0), Type.
Variable T3 : forall (x0: @T0) (x1: @T1 x0) (x2: @T2 x0 x1), Type.
Variable T4 : forall (x0: @T0) (x1: @T1 x0) (x2: @T2 x0 x1) (x3: @T3 x0 x1 x2), Type.
Variable T5 : forall (x0: @T0) (x1: @T1 x0) (x2: @T2 x0 x1) (x3: @T3 x0 x1 x2) (x4: @T4 x0 x1 x2 x3), Type.
Variable T6 : forall (x0: @T0) (x1: @T1 x0) (x2: @T2 x0 x1) (x3: @T3 x0 x1 x2) (x4: @T4 x0 x1 x2 x3) (x5: @T5 x0 x1 x2 x3 x4), Type.

Record sig7T :=
  exist7T {
      proj7T0: @T0;
      proj7T1: @T1 proj7T0;
      proj7T2: @T2 proj7T0 proj7T1;
      proj7T3: @T3 proj7T0 proj7T1 proj7T2;
      proj7T4: @T4 proj7T0 proj7T1 proj7T2 proj7T3;
      proj7T5: @T5 proj7T0 proj7T1 proj7T2 proj7T3 proj7T4;
      proj7T6: @T6 proj7T0 proj7T1 proj7T2 proj7T3 proj7T4 proj7T5;
    }.

Definition uncurry7 (R: rel7 T0 T1 T2 T3 T4 T5 T6): rel1 sig7T := fun x => R (proj7T0 x) (proj7T1 x) (proj7T2 x) (proj7T3 x) (proj7T4 x) (proj7T5 x) (proj7T6 x).

Definition curry7 (R: rel1 sig7T): rel7 T0 T1 T2 T3 T4 T5 T6 :=
  fun x0 x1 x2 x3 x4 x5 x6 => R (exist7T x6).

Lemma uncurry_map7 r0 r1 (LE : r0 <7== r1) : uncurry7 r0 <1== uncurry7 r1.
Proof. intros [] H. apply LE. apply H. Qed.

Lemma uncurry_map_rev7 r0 r1 (LE: uncurry7 r0 <1== uncurry7 r1) : r0 <7== r1.
Proof.
  repeat_intros 7. intros H. apply (LE (exist7T x6) H).
Qed.

Lemma curry_map7 r0 r1 (LE: r0 <1== r1) : curry7 r0 <7== curry7 r1.
Proof.
  repeat_intros 7. intros H. apply (LE (exist7T x6) H).
Qed.

Lemma curry_map_rev7 r0 r1 (LE: curry7 r0 <7== curry7 r1) : r0 <1== r1.
Proof.
  intros [] H. apply LE. apply H.
Qed.

Lemma uncurry_bij1_7 r : curry7 (uncurry7 r) <7== r.
Proof. unfold le7. repeat_intros 7. intros H. apply H. Qed.

Lemma uncurry_bij2_7 r : r <7== curry7 (uncurry7 r).
Proof. unfold le7. repeat_intros 7. intros H. apply H. Qed.

Lemma curry_bij1_7 r : uncurry7 (curry7 r) <1== r.
Proof. intros []. intro H. apply H. Qed.

Lemma curry_bij2_7 r : r <1== uncurry7 (curry7 r).
Proof. intros []. intro H. apply H. Qed.

Lemma uncurry_adjoint1_7 r0 r1 (LE: uncurry7 r0 <1== r1) : r0 <7== curry7 r1.
Proof.
  apply uncurry_map_rev7. eapply le1_trans; [apply LE|]. apply curry_bij2_7.
Qed.

Lemma uncurry_adjoint2_7 r0 r1 (LE: r0 <7== curry7 r1) : uncurry7 r0 <1== r1.
Proof.
  apply curry_map_rev7. eapply le7_trans; [|apply LE]. apply uncurry_bij2_7.
Qed.

Lemma curry_adjoint1_7 r0 r1 (LE: curry7 r0 <7== r1) : r0 <1== uncurry7 r1.
Proof.
  apply curry_map_rev7. eapply le7_trans; [apply LE|]. apply uncurry_bij2_7.
Qed.

Lemma curry_adjoint2_7 r0 r1 (LE: r0 <1== uncurry7 r1) : curry7 r0 <7== r1.
Proof.
  apply uncurry_map_rev7. eapply le1_trans; [|apply LE]. apply curry_bij1_7.
Qed.

Definition paco7(gf : rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6)(r: rel7 T0 T1 T2 T3 T4 T5 T6) : rel7 T0 T1 T2 T3 T4 T5 T6 :=
  curry7 (paco (fun R0 => uncurry7 (gf (curry7 R0))) (uncurry7 r)).

Definition upaco7(gf : rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6)(r: rel7 T0 T1 T2 T3 T4 T5 T6) := paco7 gf r \7/ r.
Arguments paco7 : clear implicits.
Arguments upaco7 : clear implicits.
Hint Unfold upaco7.

Definition monotone7 (gf: rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6) :=
  forall x0 x1 x2 x3 x4 x5 x6 r r' (IN: gf r x0 x1 x2 x3 x4 x5 x6) (LE: r <7= r'), gf r' x0 x1 x2 x3 x4 x5 x6.

Definition _monotone7 (gf: rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6) :=
  forall r r'(LE: r <7= r'), gf r <7== gf r'.

Lemma monotone7_eq (gf: rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6) :
  monotone7 gf <-> _monotone7 gf.
Proof. unfold monotone7, _monotone7, le7. split; intros; eapply H; eassumption. Qed.

Lemma monotone7_map (gf: rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6)
      (MON: _monotone7 gf) :
  _monotone (fun R0 => uncurry7 (gf (curry7 R0))).
Proof.
  repeat_intros 3. apply uncurry_map7. apply MON; apply curry_map7; assumption.
Qed.

Lemma _paco7_mon_gen (gf gf': rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6) r r'
    (LEgf: gf <8= gf')
    (LEr: r <7= r'):
  paco7 gf r <7== paco7 gf' r'.
Proof.
  apply curry_map7. red; intros. eapply paco_mon_gen. apply PR.
  - intros. apply LEgf, PR0.
  - intros. apply LEr, PR0.
Qed.

Lemma paco7_mon_gen (gf gf': rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6) r r' x0 x1 x2 x3 x4 x5 x6
    (REL: paco7 gf r x0 x1 x2 x3 x4 x5 x6)
    (LEgf: gf <8= gf')
    (LEr: r <7= r'):
  paco7 gf' r' x0 x1 x2 x3 x4 x5 x6.
Proof.
  eapply _paco7_mon_gen; [apply LEgf | apply LEr | apply REL].
Qed.

Lemma upaco7_mon_gen (gf gf': rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6) r r' x0 x1 x2 x3 x4 x5 x6
    (REL: upaco7 gf r x0 x1 x2 x3 x4 x5 x6)
    (LEgf: gf <8= gf')
    (LEr: r <7= r'):
  upaco7 gf' r' x0 x1 x2 x3 x4 x5 x6.
Proof.
  destruct REL.
  - left. eapply paco7_mon_gen; [apply H | apply LEgf | apply LEr].
  - right. apply LEr, H.
Qed.

Section Arg7.

Variable gf : rel7 T0 T1 T2 T3 T4 T5 T6 -> rel7 T0 T1 T2 T3 T4 T5 T6.
Arguments gf : clear implicits.

Theorem _paco7_mon: _monotone7 (paco7 gf).
Proof.
  repeat_intros 3. eapply curry_map7, _paco_mon; apply uncurry_map7; assumption.
Qed.

Theorem _paco7_acc: forall
  l r (OBG: forall rr (INC: r <7== rr) (CIH: l <7== rr), l <7== paco7 gf rr),
  l <7== paco7 gf r.
Proof.
  intros. apply uncurry_adjoint1_7.
  eapply _paco_acc. intros.
  apply uncurry_adjoint1_7 in INC. apply uncurry_adjoint1_7 in CIH.
  apply uncurry_adjoint2_7.
  eapply le7_trans. eapply (OBG _ INC CIH).
  apply curry_map7.
  apply _paco_mon; try apply le1_refl; apply curry_bij1_7.
Qed.

Theorem _paco7_mult_strong: forall r,
  paco7 gf (upaco7 gf r) <7== paco7 gf r.
Proof.
  intros. apply curry_map7.
  eapply le1_trans; [| eapply _paco_mult_strong].
  apply _paco_mon; intros []; intros H; apply H.
Qed.

Theorem _paco7_fold: forall r,
  gf (upaco7 gf r) <7== paco7 gf r.
Proof.
  intros. apply uncurry_adjoint1_7.
  eapply le1_trans; [| apply _paco_fold]. apply le1_refl.
Qed.

Theorem _paco7_unfold: forall (MON: _monotone7 gf) r,
  paco7 gf r <7== gf (upaco7 gf r).
Proof.
  intros. apply curry_adjoint2_7.
  eapply _paco_unfold; apply monotone7_map; assumption.
Qed.

Theorem paco7_acc: forall
  l r (OBG: forall rr (INC: r <7= rr) (CIH: l <7= rr), l <7= paco7 gf rr),
  l <7= paco7 gf r.
Proof.
  apply _paco7_acc.
Qed.

Theorem paco7_mon: monotone7 (paco7 gf).
Proof.
  apply monotone7_eq.
  apply _paco7_mon.
Qed.

Theorem upaco7_mon: monotone7 (upaco7 gf).
Proof.
  repeat_intros 9. intros R LE0.
  destruct R.
  - left. eapply paco7_mon. apply H. apply LE0.
  - right. apply LE0, H.
Qed.

Theorem paco7_mult_strong: forall r,
  paco7 gf (upaco7 gf r) <7= paco7 gf r.
Proof.
  apply _paco7_mult_strong.
Qed.

Corollary paco7_mult: forall r,
  paco7 gf (paco7 gf r) <7= paco7 gf r.
Proof. intros; eapply paco7_mult_strong, paco7_mon; [apply PR|..]; intros; left; assumption. Qed.

Theorem paco7_fold: forall r,
  gf (upaco7 gf r) <7= paco7 gf r.
Proof.
  apply _paco7_fold.
Qed.

Theorem paco7_unfold: forall (MON: monotone7 gf) r,
  paco7 gf r <7= gf (upaco7 gf r).
Proof.
  repeat_intros 1. eapply _paco7_unfold; apply monotone7_eq; assumption.
Qed.

End Arg7.

Arguments paco7_acc : clear implicits.
Arguments paco7_mon : clear implicits.
Arguments upaco7_mon : clear implicits.
Arguments paco7_mult_strong : clear implicits.
Arguments paco7_mult : clear implicits.
Arguments paco7_fold : clear implicits.
Arguments paco7_unfold : clear implicits.

Global Instance paco7_inst (gf : rel7 T0 T1 T2 T3 T4 T5 T6->_) r x0 x1 x2 x3 x4 x5 x6 : paco_class (paco7 gf r x0 x1 x2 x3 x4 x5 x6) :=
{ pacoacc := paco7_acc gf;
  pacomult := paco7_mult gf;
  pacofold := paco7_fold gf;
  pacounfold := paco7_unfold gf }.

End PACO7.

Global Opaque paco7.

Hint Unfold upaco7.
Hint Resolve paco7_fold.
Hint Unfold monotone7.