Section5.v

(** * Proofs for Section 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.

(** ** Lemma 5.2 *)

Lemma lemma_A_1 : forall A B, |-- A ->> B -> |-- [A]A ->> [A]B.
  move => A B HA.
  have HB := (gqm_Anec _ HA).
  eauto with GQMDB.
Qed.

(** *** Lemma A.2 *)

Lemma lemma_A_2_1 : forall A, |-- <E>A <<->> -![A]-!A.
Proof.
  move => A.
  unfold DiamondExists.
  apply: gqm_equiv_id.
Qed.

Lemma lemma_A_2_2 : forall A, |-- <A>A <<->> -![E]-!A.
Proof.
  move => A.
  rewrite /DiamondAll /SquareExists /Exists /DiamondExists.
  apply: gqm_dnegEquiv.
Qed.

Lemma lemma_A_2_3 : forall A, |-- [A]A <<->> -!<E>-!A.
Proof.
  move => A.
  hRewrite (gqm_dnegEquiv A) (fun X => [A]X <<->> -!<E>-!A).
  hAndDestruct (lemma_A_2_1 (-! A)) => H1 H2.
  hSplit.
  - by apply: gqm_mp; first by apply: gqm_contrap3.
  - by apply: gqm_mp; first by apply: gqm_contrap2.
Qed.

Lemma lemma_A_2_4 : forall A, |-- [E]A <<->> -!<A>-!A.
Proof.
  move => A.
  hAndDestruct (lemma_A_2_2 (-! A)) => ? ?.
  hRewrite (gqm_dnegEquiv A) (fun X => [E]X <<->> -!(<A>-!A)).
  hSplit.
  - by apply: gqm_mp; first by apply: gqm_contrap3.
  - by apply: gqm_mp; first by apply: gqm_contrap2.
Qed.

Lemma lemma_A_2 : forall Q A, |-- (quant_to_neg_form Q)A <<->> -!((quant_to_form Q) (-! A)).
Proof.
  case => /=.
  - apply: lemma_A_2_1.
  - apply: lemma_A_2_4.
  - apply: lemma_A_2_2.
  - apply: lemma_A_2_3.
Qed.

(** *** Proof of Lemma 5.2 *)
(*
   Var 0 in A: p
   Global Naming Context: 0 -> q
 *)
Lemma lemma_A_3 : forall A, (|-- [A]A <<->> [A]A).
Proof.
  move => A.
  hSplit; first by apply: gqm_id.
  (* (1) *)
  have H1 := (gqm_Aglob (A._[ren_ (0 .: (+2))]) (Var 0)).
  rewrite /subst_ /ren_ in H1.
  asimpl in H1.
  (* (2) *)
  have Hr : (([A] A.[ren (0 .: (+2))]) = ([A]A).[ren (+1)]) by asimpl.
  rewrite Hr in H1.
  have H2 := (gqm_univgen _ _ H1).
  asimpl in H2.
  (* (3) *)
  have H3 := (gqm_AE (A._[ren_ (+1)]) Bot).
  rewrite /subst_ /ren_ in H3.
  asimpl in H3.
  (* (4) *)
  have H4 := (lemma_A_1 _ _ H3).
  (* (5) *)
  apply: gqm_mp; last by apply: H2.
  apply: gqm_mp; last by apply: H4.
  apply: gqm_chain.
Qed.

Definition lemma_5_2 := lemma_A_3.

(** ** Lemma 5.3 *)

(** *** Lemma A.4 *)
(*
  phi/A: 0->p, 1 -> r
  psi/B: 0->r
  Global Naming Context: 0 -> r
  .[ren (+1)] to express, that the global r cannot occur in the left term, because it is shadowed by the r in the binder
 *)
Lemma lemma_A_4_1 : forall A B, |-- (([A]A.[B/]).[ren (+1)])->> [E]A.
Proof.
  move => A B.
  (* have ? : (|-- (([A]((Var 3).[B/])).[ren (+1)])->> [E](Var 3)). { asimpl. } *)
  rewrite /SquareExists /DiamondExists /All.
  (* (1) is a noop here*)
  (* (2) is a noop as well*)
  (* (3) *)
  have H3 := (gqm_AE (-![A](A._[ren_ (+1)])) B).
  rewrite /subst_ /ren_ in H3.
  (* (4) *)
  asimpl in H3.
  (* (5) *)
  (* ._[ren (0 .: (+2))] to express the fact, that the global r does not occur in phi^p_psi, because it is shadowed by the r in the binder *)
  have H5 := (gqm_Aglob (A._[B/]._[ren (0 .: (+2))]) (Var 0)).
  rewrite /subst_ /ren_ /ids_ in H5.
  (* 6 *)
  apply: gqm_mp; last by apply: H5.
  asimpl.
  apply: gqm_mp; first by apply: gqm_chain.
  apply: gqm_mp; first by apply: gqm_contrap3.
  by apply: H3.
Qed.

Lemma lemma_A_4_2 : forall X Phi A, |-- (X & [A](Phi.[ren (+1)])) ->> A -> |-- (X & [E]Phi) ->> A.
Proof.
  move => X Phi A H.
  have H2 : (|-- (X & -! A) ->> -![A](Phi.[ren (+1)])) by apply: gqm_mp; first by apply: gqm_contrapAndR.
  Fail have H3 : (|-- (X & -! A) ->> [A](-![A](Phi.[ren (+1)])).[ren(+1)]) by apply: gqm_univgen.
  (* TODO: fix *)
Admitted.

(** *** Lemma A.5 *)
Lemma lemma_A_5_1_1 : forall A B, |-- A ->> B -> |-- [A]A ->> [A]B.
Proof.
    by apply: lemma_A_1.
Qed.

Lemma lemma_A_5_1_2 : forall A B, |-- A ->> B -> |-- [E]A ->> [E]B.
Proof.
  move => A B Himp.
  have H2 : (|-- [A](A.[ren (+1)]) ->> [A](B.[ren (+1)])). {
    apply: lemma_A_5_1_1.
    have H := (gqm_subst _ (@ren _ Ids_form (+1)) Himp).
    by asimpl in H.
  }
  have H3 : (|-- [A](B.[ren (+1)]) ->> [E]B). {
    suff ->:(@ren _ Ids_form (+1) = change_top (Var 0)) by apply: lemma_A_4_1.
    apply: functional_extensionality => n.
    case: n => // /=.
  }

  (* TODO*)
Abort.