Require Import Coq.Sorting.Permutation.
Require Import Logic.lib.List_Func_ext.
Require Import Logic.GeneralLogic.Base.
Require Import Logic.GeneralLogic.ProofTheory.BasicSequentCalculus.
Require Import Logic.MinimunLogic.Syntax.
Require Import Logic.MinimunLogic.ProofTheory.Minimun.
Require Import Logic.MinimunLogic.ProofTheory.RewriteClass.
Require Import Logic.MinimunLogic.ProofTheory.ProofTheoryPatterns.
Require Import Logic.PropositionalLogic.Syntax.
Require Import Logic.PropositionalLogic.ProofTheory.Intuitionistic.
Require Import Logic.PropositionalLogic.ProofTheory.RewriteClass.

Local Open Scope logic_base.
Local Open Scope syntax.
Import PropositionalLanguageNotation.

Section DerivableRulesFromPatterns.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Context {L: Language}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {minL: MinimunLanguage L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {pL: PropositionalLanguage L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {Gamma: ProofTheory L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {minAX: MinimunAxiomatization L Gamma}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}
        {prodp: expr -> expr -> expr}.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Lemma prodp_comm {Comm: Commutativity L Gamma prodp}: forall x y,
  |-- prodp x y <--> prodp y x.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (prodp x y) (prodp y x)) *)
  apply solve_andp_intros; apply prodp_comm_impp.
Qed.

Section AdjointTheorems.

Context {funcp: expr -> expr -> expr}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {Adj: Adjointness L Gamma prodp funcp}.

Lemma prodp_orp_distr_l: forall x y z: expr,
  |-- prodp (x || y) z <--> (prodp x z || prodp y z).
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  apply solve_andp_intros.
  + apply adjoint.
(* Goal: @provable L Gamma (@impp L minL (prodp (@falsep L pL) x) (@falsep L pL)) *)
    apply solve_orp_impp; apply adjoint.
    - apply orp_intros1.
    - apply orp_intros2.
  + apply solve_orp_impp.
    - apply prodp_mono1.
(* Goal: @provable L Gamma (@impp L minL x (@orp L pL x y)) *)
      apply orp_intros1.
    - apply prodp_mono1.
(* Goal: @provable L Gamma (@impp L minL y (@orp L pL x y)) *)
      apply orp_intros2.
Qed.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Lemma prodp_orp_distr_r {Comm: Commutativity L Gamma prodp}: forall x y z: expr,
  |-- prodp x (y || z) <--> (prodp x y || prodp x z).
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (prodp x (@falsep L pL)) (@falsep L pL)) *)
  rewrite prodp_comm.
(* Goal: @provable L Gamma (@iffp L minL pL (prodp (@orp L pL y z) x) (@orp L pL (prodp x y) (prodp x z))) *)
  rewrite prodp_orp_distr_l.
(* Goal: @provable L Gamma (@iffp L minL pL (@orp L pL (prodp y x) (prodp z x)) (@orp L pL (prodp x y) (prodp x z))) *)
  rewrite !(prodp_comm _ x).
(* Goal: @provable L Gamma (@iffp L minL pL x x) *)
  apply provable_iffp_refl.
Qed.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Lemma orp_funcp {Comm: Commutativity L Gamma prodp}: forall x y z: expr,
  |-- funcp (x || y) z <--> (funcp x z && funcp y z).
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  apply solve_andp_intros.
  + apply solve_impp_andp.
    - apply funcp_mono.
(* Goal: @provable L Gamma (@impp L minL x (@orp L pL x y)) *)
      * apply orp_intros1.
      * apply provable_impp_refl.
    - apply funcp_mono.
(* Goal: @provable L Gamma (@impp L minL y (@orp L pL x y)) *)
      * apply orp_intros2.
      * apply provable_impp_refl.
  + apply adjoint.
(* Goal: @provable L Gamma (@impp L minL (prodp (@andp L pL (funcp x z) (funcp y z)) (@orp L pL x y)) z) *)
    rewrite prodp_orp_distr_r.
(* Goal: @provable L Gamma (@impp L minL (prodp (@falsep L pL) x) (@falsep L pL)) *)
    apply solve_orp_impp; apply adjoint.
    - apply andp_elim1.
    - apply andp_elim2.
Qed.

Lemma funcp_andp_distr_r: forall x y z: expr,
  |-- funcp x (y && z)  <--> (funcp x y && funcp x z).
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  apply solve_andp_intros.
  + apply solve_impp_andp.
    - apply funcp_mono2.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (funcp x y) (funcp x z)) (funcp x y)) *)
      apply andp_elim1.
    - apply funcp_mono2.
(* Goal: @provable L Gamma (@impp L minL (@andp L pL (funcp x y) (funcp x z)) (funcp x z)) *)
      apply andp_elim2.
  + apply adjoint.
(* Goal: @provable L Gamma (@impp L minL (prodp (@falsep L pL) x) (@falsep L pL)) *)
    apply solve_impp_andp; apply adjoint.
    - apply andp_elim1.
    - apply andp_elim2.
Qed.

Lemma falsep_prodp: forall x: expr,
  |-- prodp falsep x <--> falsep.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  apply solve_andp_intros.
  + apply adjoint.
(* Goal: @provable L Gamma (@impp L minL (@falsep L pL) (prodp (@falsep L pL) x)) *)
    apply falsep_elim.
  + apply falsep_elim.
Qed.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Lemma prodp_falsep {Comm: Commutativity L Gamma prodp}: forall x: expr,
  |-- prodp x falsep <--> falsep.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (prodp x (@falsep L pL)) (@falsep L pL)) *)
  rewrite prodp_comm.
(* Goal: @provable L Gamma (@iffp L minL pL (prodp (@falsep L pL) x) (@falsep L pL)) *)
  rewrite falsep_prodp.
(* Goal: @provable L Gamma (@iffp L minL pL x x) *)
  apply provable_iffp_refl.
Qed.

End AdjointTheorems.

Section MonoTheorems.

Context {Mono: Monotonicity L Gamma prodp}.

Lemma prodp_iffp: forall x1 x2 y1 y2,
  |-- x1 <--> x2 ->
  |-- y1 <--> y2 ->
  |-- prodp x1 y1 <--> prodp x2 y2.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  apply solve_andp_intros.
  + apply prodp_mono.
    - eapply solve_andp_elim1; exact H.
    - eapply solve_andp_elim1; exact H0.
  + apply prodp_mono.
    - eapply solve_andp_elim2; exact H.
    - eapply solve_andp_elim2; exact H0.
Qed.

Lemma fold_left_iffp: forall x1 x2 xs1 xs2,
  (Forall2 (fun x1 x2 => |-- x1 <--> x2) xs1 xs2) ->
  |-- x1 <--> x2 ->
  |-- fold_left prodp xs1 x1 <--> fold_left prodp xs2 x2.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  apply solve_andp_intros.
  + apply fold_left_mono.
    - revert H; apply Forall2_impl.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
      intros.
(* Goal: @provable L Gamma (@impp L minL a b) *)
      eapply solve_andp_elim1; exact H.
    - eapply solve_andp_elim1; exact H0.
  + apply fold_left_mono.
    - apply Forall2_rev.
(* Goal: @Forall2 (@expr L) (@expr L) (fun b a : @expr L => @provable L Gamma (@impp L minL a b)) xs1 xs2 *)
      revert H; apply Forall2_impl.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
      intros.
(* Goal: @provable L Gamma (@impp L minL b a) *)
      eapply solve_andp_elim2; exact H.
    - eapply solve_andp_elim2; exact H0.
Qed.

End MonoTheorems.

Section AssocTheorems.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Context {e: expr}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {Mono: Monotonicity L Gamma prodp}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {Assoc: Associativity L Gamma prodp}.

Lemma prodp_assoc: forall x y z, |-- prodp x (prodp y z) <--> prodp (prodp x y) z.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  apply solve_andp_intros.
  + apply prodp_assoc1.
  + apply prodp_assoc2.
Qed.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Context {LU: LeftUnit L Gamma e prodp}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {RU: RightUnit L Gamma e prodp}.

Lemma assoc_fold_left_fold_right_equiv: forall xs,
  |-- fold_left prodp xs e <--> fold_right prodp e xs.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  apply solve_andp_intros.
  + apply assoc_fold_left_fold_right.
  + apply assoc_fold_right_fold_left.
Qed.

Lemma assoc_prodp_fold_left_equiv: forall xs1 xs2,
  |-- prodp (fold_left prodp xs1 e) (fold_left prodp xs2 e) <--> fold_left prodp (xs1 ++ xs2) e.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  apply solve_andp_intros.
  + apply assoc_prodp_fold_left.
  + apply assoc_fold_left_app.
Qed.

End AssocTheorems.

Section CommAssocTheorems.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Context {e: expr}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {Mono: Monotonicity L Gamma prodp}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {Comm: Commutativity L Gamma prodp}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {Assoc: Associativity L Gamma prodp}.

Lemma assoc_fold_left_Permutation: forall x ys1 ys2,
  Permutation ys1 ys2 ->
  |-- fold_left prodp ys1 x <--> fold_left prodp ys2 x.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
  pose proof @proper_permutation_fold_left _ _ _ _ prodp.
  assert (forall x y, |-- x <--> y -> forall z1 z2, z1 = z2 -> |-- prodp x z1 <--> prodp y z2)
    by (intros; subst; apply prodp_iffp; [auto | apply provable_iffp_refl]).
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
  specialize (H0 H1); clear H1.
  assert (forall x1 x2 y z, |-- x1 <--> x2 -> |-- prodp (prodp x1 y) z <--> prodp (prodp x2 z) y).
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
  {
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
    intros.
    rewrite <- !prodp_assoc.
(* Goal: @provable L Gamma (@iffp L minL pL (prodp x1 (prodp y z)) (prodp x2 (prodp z y))) *)
    apply prodp_iffp; [auto | apply prodp_comm].
  }
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
  specialize (H0 H1); clear H1.
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
  apply H0; auto.
(* Goal: @provable L Gamma (@iffp L minL pL x x) *)
  apply provable_iffp_refl.
Qed.

End CommAssocTheorems.

End DerivableRulesFromPatterns.

Section ProofTheoryPatterns.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Context {L: Language}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {minL: MinimunLanguage L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {pL: PropositionalLanguage L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {Gamma: ProofTheory L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {minAX: MinimunAxiomatization L Gamma}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}.

Lemma Build_LeftUnit': forall {e: expr} {prodp: expr -> expr -> expr},
  (forall x: expr, |-- prodp e x <--> x) ->
  LeftUnit L Gamma e prodp.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @RightUnit L minL Gamma e prodp *)
  constructor; intros; specialize (H x); revert H; AddSequentCalculus Gamma.
  + rewrite !provable_derivable.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
    intros.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (prodp (prodp x y) z) (prodp x (prodp y z))) *)
    eapply deduction_andp_elim1; eauto.
  + rewrite !provable_derivable.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
    intros.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (prodp x (prodp y z)) (prodp (prodp x y) z)) *)
    eapply deduction_andp_elim2; eauto.
Qed.

Lemma Build_RightUnit': forall {e: expr} {prodp: expr -> expr -> expr},
  (forall x: expr, |-- prodp x e <--> x) ->
  RightUnit L Gamma e prodp.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @RightUnit L minL Gamma e prodp *)
  constructor; intros; specialize (H x); revert H; AddSequentCalculus Gamma.
  + rewrite !provable_derivable.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
    intros.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (prodp (prodp x y) z) (prodp x (prodp y z))) *)
    eapply deduction_andp_elim1; eauto.
  + rewrite !provable_derivable.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
    intros.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (prodp x (prodp y z)) (prodp (prodp x y) z)) *)
    eapply deduction_andp_elim2; eauto.
Qed.

Lemma Build_Associativity': forall {prodp: expr -> expr -> expr},
  (forall x y z: expr, |-- prodp (prodp x y) z <--> prodp x (prodp y z)) ->
  Associativity L Gamma prodp.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @Associativity L minL Gamma prodp *)
  constructor; intros; specialize (H x y z); revert H; AddSequentCalculus Gamma.
  + rewrite !provable_derivable.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
    intros.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (prodp x (prodp y z)) (prodp (prodp x y) z)) *)
    eapply deduction_andp_elim2; eauto.
  + rewrite !provable_derivable.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
    intros.
(* Goal: @derivable L Gamma (@empty_context L) (@impp L minL (prodp (prodp x y) z) (prodp x (prodp y z))) *)
    eapply deduction_andp_elim1; eauto.
Qed.

End ProofTheoryPatterns.

Section PatternInstances.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Context {L: Language}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {minL: MinimunLanguage L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {pL: PropositionalLanguage L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {Gamma: ProofTheory L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {minAX: MinimunAxiomatization L Gamma}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}.

Lemma impp_andp_Adjoint: Adjointness L Gamma andp impp.
Proof.
(* Goal: @Adjointness L minL Gamma (@andp L pL) (@impp L minL) *)
  constructor; AddSequentCalculus Gamma.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros; split; intros.
  + eapply modus_ponens; [| exact H].
(* Goal: @provable L Gamma (@impp L minL (@impp L minL (@andp L pL x y) z) (@impp L minL x (@impp L minL y z))) *)
    apply impp_uncurry.
  + eapply modus_ponens; [| exact H].
(* Goal: @provable L Gamma (@impp L minL (@impp L minL x (@impp L minL y z)) (@impp L minL (@andp L pL x y) z)) *)
    apply impp_curry.
Qed.

Lemma andp_Comm: Commutativity L Gamma andp.
Proof.
  constructor.
  AddSequentCalculus Gamma.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
  rewrite provable_derivable.
  eapply deduction_andp_elim1.
  rewrite <- provable_derivable.
  apply andp_comm.
Qed.

Lemma andp_Mono: Monotonicity L Gamma andp.
Proof.
  eapply @Adjoint2Mono.
  + auto.
  + apply impp_andp_Adjoint.
  + apply andp_Comm.
Qed.

Lemma andp_LU: LeftUnit L Gamma TT andp.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @LeftUnit L minL Gamma (@truep L minL pL) (@andp L pL) *)
  apply Build_LeftUnit'.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL (@truep L minL pL) x) x) *)
  apply truep_andp.
Qed.

Lemma andp_RU: RightUnit L Gamma TT andp.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @RightUnit L minL Gamma (@truep L minL pL) (@andp L pL) *)
  apply Build_RightUnit'.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL x (@truep L minL pL)) x) *)
  apply andp_truep.
Qed.

Lemma andp_Assoc: Associativity L Gamma andp.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @Associativity L minL Gamma (@andp L pL) *)
  apply Build_Associativity'.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL (@andp L pL x y) z) (@andp L pL x (@andp L pL y z))) *)
  apply andp_assoc.
Qed.

End PatternInstances.

Section DerivableRules.

(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
Context {L: Language}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {minL: MinimunLanguage L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {pL: PropositionalLanguage L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {Gamma: ProofTheory L}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {minAX: MinimunAxiomatization L Gamma}
(* Goal: forall (x1 x2 y z : @expr L) (_ : @provable L Gamma (@iffp L minL pL x1 x2)), @provable L Gamma (@iffp L minL pL (prodp (prodp x1 y) z) (prodp (prodp x2 z) y)) *)
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) prodp ys1 x) (@fold_left (@expr L) (@expr L) prodp ys2 x)) *)
        {ipGamma: IntuitionisticPropositionalLogic L Gamma}.

Lemma falsep_andp: forall x: expr,
  |-- FF && x <--> FF.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL (@falsep L pL) x) (@falsep L pL)) *)
  apply (@falsep_prodp _ _ _ _ _ _ _ _ impp_andp_Adjoint).
Qed.

Lemma andp_falsep: forall x: expr,
  |-- x && FF <--> FF.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL x (@falsep L pL)) (@falsep L pL)) *)
  apply (@prodp_falsep _ _ _ _ _ _ _ _ impp_andp_Adjoint andp_Comm).
Qed.

Lemma andp_orp_distr_l: forall x y z: expr,
  |-- (x || y) && z <--> (x && z) || (y && z).
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL (@orp L pL x y) z) (@orp L pL (@andp L pL x z) (@andp L pL y z))) *)
  apply (@prodp_orp_distr_l _ _ _ _ _ _ _ _ impp_andp_Adjoint).
Qed.

Lemma andp_orp_distr_r: forall x y z: expr,
  |-- x && (y || z) <--> (x && y) || (x && z).
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@andp L pL x (@orp L pL y z)) (@orp L pL (@andp L pL x y) (@andp L pL x z))) *)
  apply (@prodp_orp_distr_r _ _ _ _ _ _ _ _ impp_andp_Adjoint andp_Comm).
Qed.

Definition multi_and (xs: list expr): expr := fold_left andp xs truep.

Lemma multi_and_spec: forall (xs: list expr),
  |-- multi_and xs <--> fold_right andp TT xs.
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (multi_and xs) (@fold_right (@expr L) (@expr L) (@andp L pL) (@truep L minL pL) xs)) *)
  unfold multi_and.
(* Goal: @provable L Gamma (@iffp L minL pL (@fold_left (@expr L) (@expr L) (@andp L pL) xs (@truep L minL pL)) (@fold_right (@expr L) (@expr L) (@andp L pL) (@truep L minL pL) xs)) *)
  pose proof @assoc_fold_left_fold_right_equiv _ _ _ _ _ _ andp TT andp_Mono andp_Assoc andp_LU andp_RU.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL (@fold_right (@expr L) (@expr L) (@andp L pL) (@truep L minL pL) xs) y) (@fold_right (@expr L) (@expr L) (@impp L minL) y xs)) *)
  auto.
Qed.

Lemma multi_and_multi_imp: forall (xs: list expr) (y: expr),
  |-- (multi_and xs --> y) <--> (multi_imp xs y).
Proof.
(* Goal: forall (xs : list (@expr L)) (y : @expr L), @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  intros.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@multi_imp L minL xs y)) *)
  unfold multi_imp.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL (multi_and xs) y) (@fold_right (@expr L) (@expr L) (@impp L minL) y xs)) *)
  rewrite multi_and_spec.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL (@fold_right (@expr L) (@expr L) (@andp L pL) (@truep L minL pL) xs) y) (@fold_right (@expr L) (@expr L) (@impp L minL) y xs)) *)
  induction xs as [| x xs].
  + simpl.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL (@truep L minL pL) y) y) *)
    apply truep_impp.
  + simpl.
    rewrite <- impp_curry_uncurry.
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL x (@impp L minL (@fold_right (@expr L) (@expr L) (@andp L pL) (@truep L minL pL) xs) y)) (@impp L minL x (@fold_right (@expr L) (@expr L) (@impp L minL) y xs))) *)
    apply impp_proper_iffp; [apply provable_iffp_refl |].
(* Goal: @provable L Gamma (@iffp L minL pL (@impp L minL (@fold_right (@expr L) (@expr L) (@andp L pL) (@truep L minL pL) xs) y) (@fold_right (@expr L) (@expr L) (@impp L minL) y xs)) *)
    auto.
Qed.

End DerivableRules.
