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.
    + 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.