Require Import Coq.Classes.RelationClasses.
Require Import Coq.Setoids.Setoid.
Require Import Coq.Classes.Morphisms.
From ChargeCore.Logics Require Import ILogic ILEmbed.

Set Implicit Arguments.
Unset Strict Implicit.
Set Maximal Implicit Insertion.

Definition Fun (A B : Type) := A -> B.

Section ILogic_Pre.
  Context T (ord: relation T) {HPre : PreOrder ord}.
  Context {A : Type} `{IL: ILogic A}.

  Record ILPreFrm := mkILPreFrm {
    ILPreFrm_pred :> T -> A;
    ILPreFrm_closed: forall t t': T, ord t t' ->
      ILPreFrm_pred t |-- ILPreFrm_pred t'
  }.

  Notation "'mk'" := @mkILPreFrm.

  Global Instance ILPreFrm_m (P: ILPreFrm): Proper (ord ++> lentails) (ILPreFrm_pred P).
  Proof.
(* Goal: @Proper (forall _ : T, A) (@respectful T A ord (@lentails A ILOps)) (ILPreFrm_pred P) *)
    intros t t' Ht. apply ILPreFrm_closed; assumption.
  Qed.

  Program Definition ILPreFrm_atom (a : A) := mk (fun t => a) _.

  Local Obligation Tactic :=
    repeat match goal with
    | |- ord _ _ -> _ => intros Hord; try setoid_rewrite Hord; reflexivity
    | |- _ => intro
    end.

  Global Program Instance ILPre_Ops : ILogicOps ILPreFrm := {|
    lentails P Q := forall t:T, (ILPreFrm_pred P) t |-- (ILPreFrm_pred Q) t;
    ltrue        := mk (fun t => ltrue) _;
    lfalse       := mk (fun t => lfalse) _;
    limpl    P Q := mk (fun t => Forall t', Forall Ht' : ord t t', (ILPreFrm_pred P) t' -->> (ILPreFrm_pred Q) t') _;
    land     P Q := mk (fun t => (ILPreFrm_pred P) t //\\ (ILPreFrm_pred Q) t) _;
    lor      P Q := mk (fun t => (ILPreFrm_pred P) t \\// (ILPreFrm_pred Q) t) _;
    lforall  A P := mk (fun t => Forall a, (ILPreFrm_pred (P a)) t) _;
    lexists  A P := mk (fun t => Exists a, (ILPreFrm_pred (P a)) t) _
  |}.
  Next Obligation.
(* Goal: @lentails A ILOps ((fun t : T => @lforall A ILOps T (fun t' : T => @lforall A ILOps (ord t t') (fun _ : ord t t' => @limpl A ILOps (ILPreFrm_pred P t') (ILPreFrm_pred Q t')))) t) ((fun t : T => @lforall A ILOps T (fun t' : T => @lforall A ILOps (ord t t') (fun _ : ord t t' => @limpl A ILOps (ILPreFrm_pred P t') (ILPreFrm_pred Q t')))) t') *)
    apply lforallR; intro t''.
(* Goal: @lentails A ILOps (@lforall A ILOps T (fun t' : T => @lforall A ILOps (ord t t') (fun _ : ord t t' => @limpl A ILOps (ILPreFrm_pred P t') (ILPreFrm_pred Q t')))) (@lforall A ILOps (ord t' t'') (fun _ : ord t' t'' => @limpl A ILOps (ILPreFrm_pred P t'') (ILPreFrm_pred Q t''))) *)
    apply lforallR; intro Ht'.
(* Goal: @lentails A ILOps (@lforall A ILOps T (fun t' : T => @lforall A ILOps (ord t t') (fun _ : ord t t' => @limpl A ILOps (ILPreFrm_pred P t') (ILPreFrm_pred Q t')))) (@limpl A ILOps (ILPreFrm_pred P t'') (ILPreFrm_pred Q t'')) *)
    apply lforallL with t''.
(* Goal: @lentails A ILOps (@lforall A ILOps (ord t t'') (fun _ : ord t t'' => @limpl A ILOps (ILPreFrm_pred P t'') (ILPreFrm_pred Q t''))) (@limpl A ILOps (ILPreFrm_pred P t'') (ILPreFrm_pred Q t'')) *)
    assert (ord t t'') as Ht'' by (transitivity t'; assumption).
(* Goal: @lentails A ILOps (@lforall A ILOps (ord t t'') (fun _ : ord t t'' => @limpl A ILOps (ILPreFrm_pred P t'') (ILPreFrm_pred Q t''))) (@limpl A ILOps (ILPreFrm_pred P t'') (ILPreFrm_pred Q t'')) *)
    apply lforallL with Ht''; reflexivity.
  Defined.
  Next Obligation.
(* Goal: @lentails A ILOps ((fun t : T => @lor A ILOps (ILPreFrm_pred P t) (ILPreFrm_pred Q t)) t) ((fun t : T => @lor A ILOps (ILPreFrm_pred P t) (ILPreFrm_pred Q t)) t') *)
    simpl; rewrite H; reflexivity.
  Defined.
  Next Obligation.
(* Goal: @lentails A ILOps ((fun t : T => @lor A ILOps (ILPreFrm_pred P t) (ILPreFrm_pred Q t)) t) ((fun t : T => @lor A ILOps (ILPreFrm_pred P t) (ILPreFrm_pred Q t)) t') *)
    simpl; rewrite H; reflexivity.
  Defined.
  Next Obligation.
(* Goal: @lentails A ILOps ((fun t : T => @lexists A ILOps A0 (fun a : A0 => ILPreFrm_pred (P a) t)) t) ((fun t : T => @lexists A ILOps A0 (fun a : A0 => ILPreFrm_pred (P a) t)) t') *)
    simpl; setoid_rewrite H; reflexivity.
  Defined.
  Next Obligation.
(* Goal: @lentails A ILOps ((fun t : T => @lexists A ILOps A0 (fun a : A0 => ILPreFrm_pred (P a) t)) t) ((fun t : T => @lexists A ILOps A0 (fun a : A0 => ILPreFrm_pred (P a) t)) t') *)
    simpl; setoid_rewrite H; reflexivity.
  Defined.

  Program Definition ILPre_ILogic : ILogic ILPreFrm.
  Proof.
(* Goal: @ILogic (option A) ILOption_Ops *)
   split; unfold lentails; simpl; intros.
    - split; red; [reflexivity|].
(* Goal: forall (x y z : forall _ : T, A) (_ : forall t : T, @lentails A ILOps (x t) (y t)) (_ : forall t : T, @lentails A ILOps (y t) (z t)) (t : T), @lentails A ILOps (x t) (z t) *)
      intros P Q R HPQ HQR t.
(* Goal: @lentails A ILOps (ILPreFrm_pred P t) (ILPreFrm_pred R t) *)
      transitivity ((ILPreFrm_pred Q) t); [apply HPQ | apply HQR].
    - apply ltrueR.
    - apply lfalseL.
    - apply lforallL with x; apply H.
    - apply lforallR; intro x; apply H.
    - apply lexistsL; intro x; apply H.
    - apply lexistsR with x; apply H.
    - apply landL1; eapply H; assumption.
    - apply landL2; eapply H; assumption.
    - apply lorR1; eapply H; assumption.
    - apply lorR2; eapply H; assumption.
    - apply landR; [eapply H | eapply H0]; assumption.
    - apply lorL; [eapply H | eapply H0]; assumption.
    - apply landAdj.
(* Goal: @lentails A ILOps (ILPreFrm_pred C t) (@limpl A ILOps (ILPreFrm_pred P t) (ILPreFrm_pred Q t)) *)
      etransitivity; [apply H|]. apply lforallL with t.
(* Goal: @lentails A ILOps (@lforall A ILOps (ord t t) (fun _ : ord t t => @limpl A ILOps (ILPreFrm_pred P t) (ILPreFrm_pred Q t))) (@limpl A ILOps (ILPreFrm_pred P t) (ILPreFrm_pred Q t)) *)
      apply lforallL; reflexivity.
    - apply lforallR; intro t'; apply lforallR; intro Hord. apply limplAdj.
      rewrite ->Hord; eapply H; assumption.
  Qed.

  Global Existing Instance ILPre_ILogic.

  Global Instance ILPreFrm_pred_m {H : PreOrder ord}:
    Proper (lentails ++> ord ++> lentails) ILPreFrm_pred.
  Proof.
    intros P P' HPt t t' Ht. rewrite ->Ht. apply HPt.
  Qed.

  Global Instance ILPreFrm_pred_equiv_m:
    Equivalence ord ->
    Proper (lequiv ==> ord ==> lequiv) ILPreFrm_pred.
  Proof.
(* Goal: forall _ : @Equivalence T ord, @Proper (forall (_ : ILPreFrm) (_ : T), A) (@respectful ILPreFrm (forall _ : T, A) (@lequiv ILPreFrm ILPre_Ops) (@respectful T A ord (@lequiv A ILOps))) ILPreFrm_pred *)
    intros Hord P P' HPt t t' Ht. split.
    - rewrite ->Ht. apply HPt.
    - symmetry in Ht. rewrite <-Ht. apply HPt.
  Qed.

  Global Instance ILPreFrm_pred_entails_eq_m:
    Proper (lentails ++> eq ++> lentails) ILPreFrm_pred.
  Proof.
(* Goal: @Proper (forall (_ : ILPreFrm) (_ : T), A) (@respectful ILPreFrm (forall _ : T, A) (@lequiv ILPreFrm ILPre_Ops) (@respectful T A (@eq T) (@lequiv A ILOps))) ILPreFrm_pred *)
    intros P P' HPt t t' Ht. subst; apply HPt.
  Qed.

  Global Instance ILPreFrm_pred_equiv_eq_m:
    Proper (lequiv ==> eq ==> lequiv) ILPreFrm_pred.
  Proof.
(* Goal: @Proper (forall (_ : ILPreFrm) (_ : T), A) (@respectful ILPreFrm (forall _ : T, A) (@lequiv ILPreFrm ILPre_Ops) (@respectful T A (@eq T) (@lequiv A ILOps))) ILPreFrm_pred *)
    intros P P' HPt t t' Ht. split; subst; apply HPt.
  Qed.

  Program Definition ILPreAtom {HPre : PreOrder ord} (t: T) :=
    mk (fun t' => Exists x : ord t t', ltrue) _.
  Next Obligation.
(* Goal: @lentails A ILOps ((fun t' : T => @lexists A ILOps (ord t t') (fun _ : ord t t' => @ltrue A ILOps)) t0) ((fun t' : T => @lexists A ILOps (ord t t') (fun _ : ord t t' => @ltrue A ILOps)) t') *)
    apply lexistsL; intro H1.
(* Goal: @lentails A ILOps (@ltrue A ILOps) (@lexists A ILOps (ord t t') (fun _ : ord t t' => @ltrue A ILOps)) *)
    apply lexistsR; [transitivity t0; assumption | apply ltrueR].
  Qed.

End ILogic_Pre.

Arguments ILPreFrm [T] _ _ {ILOps} : rename.
Arguments mkILPreFrm {T} [ord] [A] {ILOps} _ _ : rename.

Section Embed_ILogic_Pre.
  Context T (ord: relation T) {HPre : PreOrder ord}.
  Context {A : Type} `{ILA: ILogic A}.
  Context {B : Type} `{ILB: ILogic B}.
  Context {HEmbOp : EmbedOp A B} {HEmb : Embed A B}.

(*
  Program Instance EmbedILPreDropOpEq : EmbedOp A (ILPreFrm ord A) := {
     embed := fun a => mkILPreFrm (fun x => a) _
  }.

  Instance EmbedILPreDropEq : Embed A (ILPreFrm ord A).
  Proof.
(* Goal: @Embed (forall _ : T, A) (@ILFun_Ops T A ILOps) (forall _ : T, B) (@ILFun_Ops T B ILOps0) (@EmbedILFunOp T) *)
    split; intros.
    + simpl; intros. assumption.
    + split; intros t; simpl; reflexivity.
    + split; intros t; simpl; reflexivity.
    + split; intros t; simpl.
(* Goal: @lentails A ILOps (@lforall A ILOps (ord t t) (fun _ : ord t t => @limpl A ILOps (ILPreFrm_pred P t) (ILPreFrm_pred Q t))) (@limpl A ILOps (ILPreFrm_pred P t) (ILPreFrm_pred Q t)) *)
      * lforallL t. apply lforallL; reflexivity.
      * lforallR x H; reflexivity.
  Qed.
 *)
   Global Program Instance EmbedILPreDropOp : EmbedOp A (ILPreFrm ord B) := {
     embed := fun a => mkILPreFrm (fun x => embed a) _
  }.

  Global Instance EmbedILPreDrop : Embed A (ILPreFrm ord B).
  Proof.
(* Goal: @Embed (forall _ : T, A) (@ILFun_Ops T A ILOps) (forall _ : T, B) (@ILFun_Ops T B ILOps0) (@EmbedILFunOp T) *)
    split; intros.
    + simpl; intros. apply embed_sound; assumption.
    + split; intros t; simpl; apply embedlforall.
    + split; intros t; simpl; apply embedlexists.
    + split; intros t; simpl.
(* Goal: @lentails B ILOps0 (@lforall B ILOps0 T (fun t' : T => @lforall B ILOps0 (ord t t') (fun _ : ord t t' => @limpl B ILOps0 (@embed A B HEmbOp a) (@embed A B HEmbOp b)))) (@embed A B HEmbOp (@limpl A ILOps a b)) *)
      * apply lforallL with t. apply lforallL; [reflexivity | apply embedImpl].
      * apply lforallR; intro x; apply lforallR; intro H. apply embedImpl.
  Qed.

  Global Program Instance EmbedILPreOp : EmbedOp (ILPreFrm ord A) (ILPreFrm ord B) := {
     embed := fun a => mkILPreFrm (fun x => embed ((ILPreFrm_pred a) x)) _
  }.
  Next Obligation.
(* Goal: @lentails B ILOps0 (@embed A B HEmbOp (@ILPreFrm_pred T ord A ILOps a t)) (@embed A B HEmbOp (@ILPreFrm_pred T ord A ILOps a t')) *)
  	rewrite H. reflexivity.
  Defined.

  Global Instance EmbedILPre : Embed (ILPreFrm ord A) (ILPreFrm ord B).
  Proof.
(* Goal: @Embed (forall _ : T, A) (@ILFun_Ops T A ILOps) (forall _ : T, B) (@ILFun_Ops T B ILOps0) (@EmbedILFunOp T) *)
    split; intros.
    + simpl; intros. apply embed_sound; apply H.
    + split; intros t; simpl; apply embedlforall.
    + split; intros t; simpl; apply embedlexists.
    + split; intros t; simpl;
      do 2 setoid_rewrite <- embedlforall;
      apply lforallR; intro t'; apply lforallR; intro H;
(* Goal: @lentails B ILOps0 (@embed A B HEmbOp (@limpl A ILOps a b)) (@limpl B ILOps0 (@embed A B HEmbOp a) (@embed A B HEmbOp b)) *)
      apply lforallL with t'; apply lforallL with H; apply embedImpl.
  Qed.

End Embed_ILogic_Pre.

(** If [Frm] is a ILogic, then the function space [T -> Frm] is also an ilogic,
    for any type [T]. All connectives are just pointwise liftings. *)

Section ILogic_Fun.
  Context (T: Type).
  Context {A : Type} `{IL: ILogic A}.

  Global Program Instance ILFun_Ops : ILogicOps ((fun x y => x -> y) T A) := {|
    lentails P Q := forall t:T, P t |-- Q t;
    ltrue        := fun t => ltrue;
    lfalse       := fun t => lfalse;
    limpl    P Q := fun t => P t -->> Q t;
    land     P Q := fun t => P t //\\ Q t;
    lor      P Q := fun t => P t \\// Q t;
    lforall  A P := fun t => Forall a, P a t;
    lexists  A P := fun t => Exists a, P a t
  |}.

  Program Definition ILFun_ILogic : @ILogic _ ILFun_Ops.
  Proof.
(* Goal: @ILogic (option A) ILOption_Ops *)
    split; unfold lentails; simpl; intros.
    - split; red; [reflexivity|].
(* Goal: forall (x y z : forall _ : T, A) (_ : forall t : T, @lentails A ILOps (x t) (y t)) (_ : forall t : T, @lentails A ILOps (y t) (z t)) (t : T), @lentails A ILOps (x t) (z t) *)
      intros P Q R HPQ HQR t. transitivity (Q t); [apply HPQ | apply HQR].
    - apply ltrueR.
    - apply lfalseL.
    - apply lforallL with x; apply H.
    - apply lforallR; intros; apply H.
    - apply lexistsL; intros; apply H.
    - apply lexistsR with x; apply H.
    - apply landL1; intuition.
    - apply landL2; intuition.
    - apply lorR1; intuition.
    - apply lorR2; intuition.
    - apply landR; intuition.
    - apply lorL; intuition.
    - apply landAdj; intuition.
    - apply limplAdj; intuition.
  Qed.

  Global Existing Instance ILFun_ILogic.

End ILogic_Fun.

Section ILogic_Option.
  Context {A : Type} `{IL: ILogic A}.

  Definition toProp (P : option A) :=
    match P with
    | Some P => P
    | None => lfalse
    end.

  Global Program Instance ILOption_Ops : ILogicOps (option A) :=
  {| lentails P Q := toProp P |-- toProp Q
   ; ltrue        := Some ltrue
   ; lfalse       := Some lfalse
   ; limpl    P Q := Some (toProp P -->> toProp Q)
   ; land     P Q := Some (toProp P //\\ toProp Q)
   ; lor      P Q := Some (toProp P \\// toProp Q)
   ; lforall  A P := Some (Forall a, toProp (P a))
   ; lexists  A P := Some (Exists a, toProp (P a))
   |}.

  Program Definition ILOption_ILogic : ILogic (option A).
  Proof.
(* Goal: @ILogic (option A) ILOption_Ops *)
    split; unfold lentails; simpl; intros.
    - split; red; [reflexivity|].
(* Goal: forall (x y z : option A) (_ : @lentails A ILOps (toProp x) (toProp y)) (_ : @lentails A ILOps (toProp y) (toProp z)), @lentails A ILOps (toProp x) (toProp z) *)
      intros P Q R HPQ HQR. transitivity (toProp Q); [apply HPQ | apply HQR].
    - apply ltrueR.
    - apply lfalseL.
    - apply lforallL with x; apply H.
    - apply lforallR; intros; apply H.
    - apply lexistsL; intros; apply H.
    - apply lexistsR with x; apply H.
    - apply landL1; intuition.
    - apply landL2; intuition.
    - apply lorR1; intuition.
    - apply lorR2; intuition.
    - apply landR; intuition.
    - apply lorL; intuition.
    - apply landAdj; intuition.
    - apply limplAdj; intuition.
  Qed.

End ILogic_Option.

Section Embed_ILogic_Fun.
  Context {A : Type} `{ILA: ILogic A}.
  Context {B : Type} `{ILB: ILogic B}.
  Context {HEmbOp : EmbedOp A B} {HEmb : Embed A B}.

  Program Instance EmbedILFunDropOp {T} : EmbedOp A (T -> B) :=
  { embed := fun a t => embed a }.

  Local Existing Instance ILFun_Ops.

  Instance EmbedILFunDrop {T} : Embed A (T -> B).
  Proof.
(* Goal: @Embed (forall _ : T, A) (@ILFun_Ops T A ILOps) (forall _ : T, B) (@ILFun_Ops T B ILOps0) (@EmbedILFunOp T) *)
    split; intros.
    + simpl; intros. apply embed_sound; assumption.
    + split; intros t; simpl; apply embedlforall.
    + split; intros t; simpl; apply embedlexists.
    + split; intros t; simpl; apply embedImpl.
  Qed.

  Program Instance EmbedILFunOp {T} : EmbedOp (T -> A) (T -> B) :=
  { embed := fun a x => embed (a x) }.

  Instance EmbedILFun {T} : Embed (T -> A) (T -> B).
  Proof.
(* Goal: @Embed (forall _ : T, A) (@ILFun_Ops T A ILOps) (forall _ : T, B) (@ILFun_Ops T B ILOps0) (@EmbedILFunOp T) *)
    split; intros.
    + simpl; intros. apply embed_sound; apply H.
    + split; intros t; simpl; apply embedlforall.
    + split; intros t; simpl; apply embedlexists.
    + split; intros t; simpl; apply embedImpl.
  Qed.

End Embed_ILogic_Fun.
(*
Section ILogicFunInv.

	Context {A B} `{IL : ILogic (A -> B)}.

  Program Definition ILFun_Ops : ILogicOps (T -> A) := {|
    lentails P Q := forall t:T, P t |-- Q t;
    ltrue        := fun t => ltrue;
    lfalse       := fun t => lfalse;
    limpl    P Q := fun t => P t -->> Q t;
    land     P Q := fun t => P t //\\ Q t;
    lor      P Q := fun t => P t \\// Q t;
    lforall  A P := fun t => Forall a, P a t;
    lexists  A P := fun t => Exists a, P a t
  |}.


End ILogicFunInv.
*)
Global Opaque ILOption_Ops.
Global Opaque ILFun_Ops.
Global Opaque ILPre_Ops.
