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_idEquiv.
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)).
  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).
  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, 2 -> next element of global naming context after r
  psi/B: 0->(local)r, 1 -> first element of global naming context after 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).
  (* (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)).
  (* 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.

(*
  Global Naming Context antecedent: 0 -> q,...
  Global Naming Context consequent: ...
*)
Lemma lemma_A_4_2 : forall X Phi A, |-- (X.[ren (+1)] & [A](Phi.[ren (+1)])) ->> A.[ren (+1)] -> |-- (X & [E]Phi) ->> A.
Proof.
  move => X Phi A H.
  (* (1) *)
  (* (2) *)
  have H2 : (|-- (X.[ren (+1)] & -! A.[ren (+1)]) ->> -![A](Phi.[ren (+1)])) by apply: gqm_mp; first by apply: gqm_contrapAndR.
  (* (3) *)
  have H3 := (gqm_Q5 (Phi._[ren_ (+1)])).
  (* (4) *)
  have H4 : (|-- X.[ren (+1)] & -! A.[ren (+1)] ->> [A] (-! ([A] Phi.[ren (+1)])).[ren (+1)]). {
    apply: gqm_mp; last by apply: H2.
    by apply: gqm_mp; first by apply: gqm_chain.
  }
  (* (5) *)
  have Hr : ((X.[ren (+1)] & -! A.[ren (+1)]) = (X & -! A).[ren (+1)]) by asimpl.
  rewrite Hr in H4; clear Hr.
  have H5 := (gqm_univgen _ _ H4).
  (* (6) *)
  have H6 := (gqm_AE ((-! ([A] Phi._[ren_ (+1)]))._[ren_ (+1)]) (Var 0)).
  asimpl in H6.
  rewrite !ids_0_neg in H6.
  (* (7) *)
  have H7 := (lemma_A_1 _ _ H6).
  (* (8) *)
  have H8 : (|-- X & -! A ->> [A] -! ([A] Phi.[ren (+1)])). {
    apply: gqm_mp; last by apply: H5.
    apply: gqm_mp; first by apply: gqm_chain.
    by asimpl.
  }
  (* (9) noop *)
  (* (10) noop *)
  (* (11) noop *)
  (* (12) *)
  rewrite /SquareExists /All /DiamondExists.
  apply: (tac_rewrite (fun Y => _ ->> Y) (gqm_dnegEquiv _)).
  by apply: gqm_mp; first by apply: gqm_contrapAndR.
Qed.

Lemma lemma_A_4_2_simple : forall Phi A, |-- [A](Phi.[ren (+1)]) ->> A.[ren (+1)] -> |-- [E]Phi ->> A.
Proof.
  move => Phi A H.
  apply: gqm_mp; last by apply: gqm_topI.
  apply (tac_rewriteR (fun X => X) (gqm_andImpEquiv _ _ _)).
  apply: lemma_A_4_2.
  apply (tac_rewrite (fun X => X) (gqm_andImpEquiv _ _ _)).
  by apply: gqm_mp; first by apply: gqm_discard.
Qed.

(** *** Lemma A.5 *)
(* p is shifted out of the Global Naming Context *)
Lemma lemma_A_5_1_1 : forall A B, |-- A ->> B -> |-- [A]A ->> [A]B.
Proof.
    by apply: lemma_A_1.
Qed.

(* p is shifted out of the Global Naming Context *)
Lemma lemma_A_5_1_2 : forall A B, |-- A ->> B -> |-- [E]A ->> [E]B.
Proof.
  move => A B Himp.
  (* (1) *)
  (* (2) *)
  have H2 : (|-- [A](A.[ren (+1)]) ->> [A](B.[ren (+1)])). {
    apply: lemma_A_5_1_1.
    have H := (gqm_subst _ (ren_ (+1)) Himp).
    by asimpl in H.
  }
  (* (3) *)
  (* second ren (+1), because the second part does not refer to the global p*)
  have H3 : (|-- [A](B.[ren (+1)]) ->> ([E]B).[ren (+1)]). {
    (* Naming context for lemma_A_4_1:
     * r -> 0, p -> 1, (Var 1) refers to p in global context
     *)
    have H' := (lemma_A_4_1 (B._[ren_ (0 .: (+3))]) (Var 1)).
    rewrite /SquareExists /DiamondExists /All in H'.
    asimpl in H'.
    asimpl.
    rewrite !ids_0_neg.
    (* now we need to remove r->0 from the naming context *)
    have H2' := (gqm_subst _ (ren_ (0 .: id)) H').
    by asimpl in H2'.
  }
  (* (4) *)
  have H4 : (|-- [A](A.[ren (+1)]) ->> ([E]B).[ren (+1)]). {
    apply: gqm_mp; last by apply: H2.
    apply: gqm_mp; last by apply: H3.
    by apply: gqm_chain.
  }
  (* (5) *)
  by apply: lemma_A_4_2_simple.
Qed.

Lemma lemma_A_5_2_1 : forall A B, |-- A ->> B -> |-- <A>A ->> <A>B.
Proof.
  move => A B Himp.
  apply: (tac_rewrite (fun X => X ->> _) (lemma_A_2_2 _)).
  apply: (tac_rewrite (fun X => _ ->> X) (lemma_A_2_2 _)).
  apply: gqm_mp; first by apply: gqm_contrap.
  apply: lemma_A_5_1_2.
    by apply: gqm_mp; first by apply: gqm_contrap.
Qed.

Lemma lemma_A_5_2_2 : forall A B, |-- A ->> B -> |-- <E>A ->> <E>B.
Proof.
  move => A B Himp.
  apply: (tac_rewrite (fun X => X ->> _) (lemma_A_2_1 _)).
  apply: (tac_rewrite (fun X => _ ->> X) (lemma_A_2_1 _)).
  apply: gqm_mp; first by apply: gqm_contrap.
  apply: lemma_A_5_1_1.
    by apply: gqm_mp; first by apply: gqm_contrap.
Qed.

(** *** Lemma 5.3 *)

Lemma lemma_5_3 : forall Q A B, |-- A ->> B -> |-- (quant_to_form Q)A ->> (quant_to_form Q)B.
Proof.
  case => /=.
  - apply: lemma_A_5_1_1.
  - apply: lemma_A_5_2_1.
  - apply: lemma_A_5_1_2.
  - apply: lemma_A_5_2_2.
Qed.

(** ** Lemma A.6 *)

Lemma lemma_A_6_1_1 : forall A, |-- [A]A ->> [E] A.
Proof.
  move => A.
  (* A with skipped global r *)
  have H := (lemma_A_4_1 (A._[ren_ (0.: (+2)) ]) (Var 0)).
  (* remove global r*)
  have H2 := (gqm_subst _ (ren_ (0 .: id)) H).
  asimpl in H2.
  by [].
Qed.

Lemma lemma_A_6_1_2 : forall A, |-- <A>A ->> <E> A.
Proof.
  move => A.
  apply: (tac_rewrite (fun X => X ->> _) (lemma_A_2_2 _)).
  apply: (tac_rewrite (fun X => _ ->> X) (lemma_A_2_1 _)).
  apply: gqm_mp; first by apply: gqm_contrap.
  by apply: lemma_A_6_1_1.
Qed.

Lemma lemma_A_6_2_1 : forall A, |-- [E](A.[ren (+1)]) ->> [A](A.[ren (+1)]).
Proof.
  move => A.
  apply: lemma_A_4_2_simple.
  asimpl.
    by apply: gqm_id.
Qed.

Lemma lemma_A_6_2_2 : forall A, |-- <E>(A.[ren (+1)]) ->> <A>(A.[ren (+1)]).
Proof.
  move => A.
  apply: (tac_rewrite (fun X => X ->> _) (lemma_A_2_1 _)).
  apply: (tac_rewrite (fun X => _ ->> X) (lemma_A_2_2 _)).
  apply: gqm_mp; first by apply: gqm_contrap.
  have H := (lemma_A_6_2_1 (-! A)).
  by asimpl in H.
Qed.

Lemma lemma_A_6_3_1 : forall A, |-- [A]A ->> <A>A.
Proof.
  move => A.
  rewrite /DiamondAll /Exists.
  apply: lemma_A_1.
  apply: gqm_mp; first by apply: gqm_contrap3.
  have H := (gqm_AE (-! A._[ren_ (+1)]) (Var 0)).
  by asimpl in H.
Qed.

Lemma lemma_A_6_3_2 : forall A, |-- [E]A ->> <E>A.
Proof.
  move => A.
  rewrite /SquareExists /DiamondExists.
  (* other proof than in the paper *)
  apply: gqm_mp; first by apply: gqm_contrap.
  apply: (tac_rewrite (fun X => [A] -! A ->> [A] -! (|A| X)) (gqm_dnegEquiv _)).
  by apply: lemma_A_6_3_1.
Qed.

(** ** Lemma 5.4 / A.7 *)

Lemma lemma_A_7_1 : forall A B, |-- |A|(A ->> B) ->> (|A|A ->> |A|B).
Proof.
  move => A B.
    by apply: gqm_ADist.
Qed.

Lemma lemma_A_7_2_1 : forall A B, |-- |A|(A & B) <<->> (|A|A & |A| B).
Proof.
  move => A B.
  rewrite /And.
  hSplit.
  - apply: gqm_mp; last by apply: (lemma_A_7_1 (A ->> -! B) (Bot)).
    apply: gqm_mp; first by apply: gqm_chain.
    apply: (tac_rewrite (fun X => (|A| _ ->> X) ->> _) gqm_botAllEquiv).
    apply: gqm_mp; first by apply: gqm_contrap.
    (* TODO finish *)
Admitted.

Lemma lemma_A_7_2_2 : forall A B, |-- |E|(A ||| B) <<->> (|E|A ||| |E| B).
Proof.
  move => A B.
  rewrite /Exists.
  apply: (tac_rewriteR (fun X => X) (gqm_equivNegEquiv2 _ _)).
  apply: (tac_rewrite (fun X => (|A| -! X) <<->> _) (gqm_demorganOr _ _)).
  apply: (tac_rewriteR (fun X => (|A| X) <<->> _) (gqm_dnegEquiv _)).
  apply: (tac_rewriteR (fun X => _ <<->> X) (gqm_demorganAnd _ _)).
  apply: lemma_A_7_2_1.
Qed.

Lemma lemma_A_7_3_1 : forall A B, |-- A ->> B -> |-- |A|A ->> |A|B.
Proof.
  move => A B H.
  apply: lemma_A_5_1_1.
  have -> :((A.[ren (+1)] ->> B.[ren (+1)]) = ((A ->> B).[ren (+1)])) by asimpl.
    by apply: gqm_subst.
Qed.

Lemma lemma_A_7_3_2 : forall A B, |-- A ->> B -> |-- |E|A ->> |E|B.
Proof.
  move => A B H.
  rewrite /Exists.
  apply: gqm_mp; first by apply: gqm_contrap.
  apply: lemma_A_7_3_1.
  by apply: gqm_mp; first by apply: gqm_contrap.
Qed.

Lemma lemma_A_7_4 : forall A, |-- |A|A ->> A.
Proof.
  move => A.
  have H := (gqm_AE (A._[ren_ (+1)]) (Var 0)).
  by asimpl in H.
Qed.

Lemma lemma_A_7_5 : forall A, |-- A ->> |E|A.
Proof.
  move => A.
  rewrite /Exists.
  apply: gqm_mp; first by apply: gqm_contrap3.
    by apply: lemma_A_7_4.
Qed.

Lemma lemma_A_7_6 : forall A, |-- |E|A <<->> |A||E|A.
Proof.
  hSplit; by [apply: gqm_Q5 | apply: lemma_A_7_4].
Qed.

Lemma lemma_A_7_7 : forall A, |-- |E||A|A <<->> |A|A.
Proof.
  move => A.
  hSplit; last by apply: lemma_A_7_5.
  rewrite /Exists.
  apply: gqm_mp; first by apply: gqm_contrap2.
    by apply: gqm_Q5.
Qed.

Lemma lemma_A_7_8_1 : forall A, |-- |A||A|A <<->> |A|A.
Proof.
  move => A.
  hSplit; first by apply: lemma_A_7_4.
  apply: (tac_rewriteR (fun X => X ->> _) (lemma_A_7_7 _)).
  apply: (tac_rewrite (fun X => X ->> _) (lemma_A_7_6 _)).
  apply: (tac_rewrite (fun X => |A|X ->> _) (lemma_A_7_7 _)).
  apply: gqm_id.
Qed.

Lemma lemma_A_7_8_2 : forall A, |-- |E||E|A <<->> |E|A.
Proof.
  move => A.
  hSplit; last by apply: lemma_A_7_5.
  apply: (tac_rewrite (fun X => _ ->> X) (lemma_A_7_6 _)).
  apply: (tac_rewrite (fun X => |E|X ->> _) (lemma_A_7_6 _)).
  apply: (tac_rewrite (fun X => X ->> _) (lemma_A_7_7 _)).
  apply: gqm_id.
Qed.