Section5WithContext.v

(** * Proofs for Section 5 starting with Definiton 5.5
everything here is based on the numbering in the extendend report
*)

Require Import GQM.Base.
Require Import GQM.GQM.
Require Import GQM.GQMDeduction.
Require Import GQM.GQMClassicalWithTactics.
Require Import GQM.Section5.

(** ** Defintion *)

Inductive GQMdedWithContext: list form -> form -> Prop :=
| gqmc_context c A: In A c -> GQMdedWithContext c A
| gqmc_gqm c A: |-- A -> GQMdedWithContext c A
| gqmc_mp c A B: GQMdedWithContext c (A ->> B) -> GQMdedWithContext c A -> GQMdedWithContext c B
| gqmc_Anec c A: GQMdedWithContext c A -> GQMdedWithContext c (|A|A).

Notation "c '|--' A"  := (GQMdedWithContext c A) (at level 80, no associativity).
Hint Constructors GQMdedWithContext : GQMDB.

Lemma gqmc_context_weakening : forall c A B, c |-- A -> B::c |-- A.
Proof.
  move => c A B.
  by elim; clear c A; eauto using in_cons with GQMDB.
Qed.

Definition context_to_and := fold_right (fun A B => A & B) Top.

Lemma lemma_5_6_1 : forall c A, c |-- A <-> |-- |A| (context_to_and c) ->> |A|A.
Proof.
  move => c A.
  split.
  - elim; clear c A => c A.
    (* the inverts and inverts ... as tactics are from lib/LibTactics.v *)
    + elim: c A; first by move => ? Hi; inverts Hi.
      move => f l IH A Hi /=.
      inverts Hi as.
      * apply: lemma_A_1.
        apply: gqm_subst_imp.
          by apply: gqm_andE1.
      * move => Hi.
        apply: gqm_mp; last by apply: (IH _ Hi).
        apply: gqm_mp; first by apply: gqm_chain2.
        apply: lemma_A_1.
        apply: gqm_subst_imp.
          by apply: gqm_andE2.
    + move => Hgqm.
      apply: gqm_mp; first by apply: gqm_I1.
      apply: gqm_Anec.
      by apply: gqm_subst.
    + move => B _ H1 _ H2.
      apply: gqm_mp; last by apply: H2.
      apply: gqm_mp; first by apply: gqm_I2.
      apply: gqm_mp; last by apply: H1.
      apply: gqm_mp; first by apply: gqm_chain.
      by apply: lemma_A_7_1.
    + move => _ IH.
        by apply: (tac_rewrite (fun X => _ ->> X) (lemma_A_7_8_1 _)).
  - move => Hgqm.
    suff H : (c |-- |A|A). {
      have He := (gqmc_gqm c _ (gqm_AE (A._[ren_ (+1)]) (Var 1))).
      asimpl in He.
      by apply: gqmc_mp; first by apply: He.
    }
    apply: gqmc_mp; first by apply: (gqmc_gqm c _ Hgqm).
    clear Hgqm A.
    apply: gqmc_Anec.
    elim: c => /=.
    + apply: gqmc_gqm.
        by apply: gqm_topI.
    + move => A l IH.
      apply: gqmc_mp; last by apply: (gqmc_context_weakening _ _ A IH).
      clear IH.
      apply: (gqmc_mp _ A); last by eauto using in_eq with GQMDB.
      apply: gqmc_gqm.
        by apply: gqm_andI.
Qed.

Lemma lemma_5_6_2_global_all : forall A, Global_Form A -> |-- A <<->> |A| A.
Proof.
  elim => // /=.
  - move => f IHf g IHg [Hf Hg].
    hSplit; last by apply: lemma_A_7_4.
    have {IHf Hf} Hf := IHf Hf.
    have {IHg Hg} Hg := IHg Hg.
    apply: (tac_rewrite (fun X => (X ->> _) ->> |A|(f ->> g)) Hf).
    apply: (tac_rewrite (fun X => (_ ->> X) ->> |A|(f ->> g)) Hg).
    apply: gqm_mp.
    + apply: gqm_mp; first by apply: gqm_negE3 (|A| f) _.
      apply: gqm_mp; first by apply: gqm_swap.
      apply: gqm_mp; first by apply: gqm_chain.
      apply: gqm_mp; first by apply: lemma_A_7_1.
      apply: gqm_Anec.
      apply: gqm_subst.
        by apply: gqm_I1.
    + apply: gqm_mp; first by apply: gqm_discardr.
      have Hneg : (|-- -! (|A| f) ->> |A| (-! f)). {
        apply: gqm_mp; first by apply: gqm_contrap2.
        apply: (tac_rewrite (fun X => ((-! (|A| -! X)) ->> |A| f)) Hf).
        by hAndDestruct (lemma_A_7_7 f).
      }
      apply: gqm_mp; last by apply: Hneg.
      apply: gqm_mp; first by apply: gqm_chain.
      apply: gqm_mp; first by apply: lemma_A_7_1.
      apply: gqm_Anec.
      apply: gqm_subst.
      apply: gqm_mp; first by apply: gqm_chain.
      by apply: gqm_negE.
  - move => f _ _.
    by apply: lemma_A_7_11_1.
Qed.


Lemma lemma_5_6_2 : forall c A,
    fold_right (fun f g => Global_Form f /\ g) True c ->
    c |-- A <-> |-- (context_to_and c) ->> A.
Proof.
  move => c A HGc.
  suff H : (|-- |A|context_to_and c ->> |A|A <-> |-- context_to_and c ->> A). {
    apply: iff_trans; last by apply: H.
    by apply: lemma_5_6_1.
  }
  apply: iff_sym.
  split => H.
  - apply: gqm_mp; first by apply: lemma_A_7_1.
    apply: gqm_Anec.
    by apply: gqm_subst.
  - apply: gqm_mp; last by apply: (lemma_A_7_4 A).
    apply: gqm_mp; first by apply: gqm_chain2.
    apply: gqm_mp; last by apply: H.
    apply: gqm_mp; first by apply: gqm_chain2.
    clear A H.
    elim: c HGc => /=.
    + move => _.
      apply: gqm_mp; first by apply: gqm_I1.
      apply: gqm_Anec.
      by apply: gqm_id.
    + move => A l IH [HG Hr].
      have {IH Hr} H := IH Hr.
      hAndDestruct (lemma_A_7_2_1 A (context_to_and l)) => _ Hand.
      apply: gqm_mp; last by apply: Hand. clear Hand.
      apply: gqm_mp; first by apply: gqm_chain2.
      apply: (tac_rewrite (fun X => X & _ ->> _) (lemma_5_6_2_global_all _ HG)).
      apply: (tac_rewrite (fun X => X) (gqm_andImpEquiv _ _ _)).
      apply: gqm_mp; first by apply: gqm_swap.
      apply: gqm_mp; last by apply: H.
      apply: gqm_mp; first by apply: gqm_chain.
      apply: gqm_mp; first by apply: gqm_swap.
      by apply: gqm_andI.
Qed.