Skip to content
Snippets Groups Projects
Commit cc224e94 authored by Mackie Loeffel's avatar Mackie Loeffel
Browse files

finished A.7

parent 19784f5c
No related branches found
No related tags found
No related merge requests found
Pipeline #
Hide whitespace changes
Inline Side-by-side
Showing
with 205 additions and 0 deletions
theories/Section5.v
+ 205
− 0
View file @ cc224e94
......@@ -249,6 +249,8 @@ Qed.
(** ** Lemma A.6 *)
(** *** Lemma A.6 (i) *)
Lemma lemma_A_6_1_1 : forall A, |-- [A]A ->> [E] A.
Proof.
move => A.
......@@ -269,6 +271,8 @@ Proof.
by apply: lemma_A_6_1_1.
Qed.
(** *** Lemma A.6 (ii) *)
Lemma lemma_A_6_2_1 : forall A, |-- [E](A.[ren (+1)]) ->> [A](A.[ren (+1)]).
Proof.
move => A.
......@@ -287,6 +291,8 @@ Proof.
by asimpl in H.
Qed.
(** *** Lemma A.6 (iii) *)
Lemma lemma_A_6_3_1 : forall A, |-- [A]A ->> <A>A.
Proof.
move => A.
......@@ -309,12 +315,16 @@ Qed.
(** ** Lemma 5.4 / A.7 *)
(** *** Lemma A.7 (i) *)
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 A.7 (ii) *)
Lemma lemma_A_7_2_1 : forall A B, |-- |A|(A & B) <<->> (|A|A & |A| B).
Proof.
move => A B.
......@@ -338,6 +348,8 @@ Proof.
apply: lemma_A_7_2_1.
Qed.
(** *** Lemma A.7 (iii) *)
Lemma lemma_A_7_3_1 : forall A B, |-- A ->> B -> |-- |A|A ->> |A|B.
Proof.
move => A B H.
......@@ -355,6 +367,8 @@ Proof.
by apply: gqm_mp; first by apply: gqm_contrap.
Qed.
(** *** Lemma A.7 (iv) *)
Lemma lemma_A_7_4 : forall A, |-- |A|A ->> A.
Proof.
move => A.
......@@ -362,6 +376,8 @@ Proof.
by asimpl in H.
Qed.
(** *** Lemma A.7 (v) *)
Lemma lemma_A_7_5 : forall A, |-- A ->> |E|A.
Proof.
move => A.
......@@ -370,11 +386,15 @@ Proof.
by apply: lemma_A_7_4.
Qed.
(** *** Lemma A.7 (vi) *)
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 A.7 (vii) *)
Lemma lemma_A_7_7 : forall A, |-- |E||A|A <<->> |A|A.
Proof.
move => A.
......@@ -384,6 +404,8 @@ Proof.
by apply: gqm_Q5.
Qed.
(** *** Lemma A.7 (viii) *)
Lemma lemma_A_7_8_1 : forall A, |-- |A||A|A <<->> |A|A.
Proof.
move => A.
......@@ -403,3 +425,186 @@ Proof.
apply: (tac_rewrite (fun X => X ->> _) (lemma_A_7_7 _)).
apply: gqm_id.
Qed.
(** *** Lemma A.7 (ix) *)
Lemma lemma_A_7_9_1 : forall A, |-- [A]|A|A <<->> [A]A.
Proof.
move => A.
hSplit.
- apply: lemma_A_5_1_1.
by apply: lemma_A_7_4.
- apply: gqm_univgen.
asimpl.
have H := (gqm_Aglob (A._[ren_ (0.: (+2))]) (Var 0)).
by asimpl in H.
Qed.
Lemma lemma_A_7_9_2 : forall A, |-- [E]|A|A <<->> [E]A.
Proof.
move => A.
hSplit.
- apply: lemma_A_5_1_2.
by apply: lemma_A_7_4.
- rewrite /SquareExists /DiamondExists.
apply: (tac_rewrite (fun X => _ ->> -! ([A] -! X)) (lemma_A_7_8_1 _)).
apply: gqm_id.
Qed.
Lemma lemma_A_7_9_3 : forall A, |-- <A>|A|A <<->> [A]A.
Proof.
move => A.
hSplit.
- rewrite /DiamondAll.
apply: (tac_rewrite (fun X => [A] X ->> _) (lemma_A_7_7 _)).
apply: lemma_A_5_1_1.
by apply: lemma_A_7_4.
- apply: gqm_mp; last by apply: (lemma_A_6_3_1 (|A| A)).
apply: gqm_mp; first by apply: gqm_chain2.
apply: gqm_univgen.
asimpl.
have H := (gqm_Aglob (A._[ren_ (0.: (+2))]) (Var 0)).
by asimpl in H.
Qed.
Lemma lemma_A_7_9_4 : forall A, |-- <E>|A|A <<->> [E]A.
Proof.
move => A.
rewrite /SquareExists /DiamondExists.
apply: gqm_idEquiv.
Qed.
(** *** Lemma A.7 (x) *)
Lemma lemma_A_7_10_3 : forall A, |-- <A>|E|A <<->> <A>A.
Proof.
move => A.
hSplit.
- rewrite /DiamondAll.
apply: (tac_rewrite (fun X => [A] X ->> _) (lemma_A_7_8_2 _)).
by apply: gqm_id.
- apply: lemma_A_5_2_1.
by apply: lemma_A_7_5.
Qed.
Lemma lemma_A_7_10_4 : forall A, |-- <E>|E|A <<->> <E>A.
Proof.
move => A.
hSplit.
- rewrite /DiamondExists /Exists.
apply: (tac_rewriteR (fun X => -! ([A] X) ->> _) (gqm_dnegEquiv _)).
apply: gqm_mp; first by apply: gqm_contrap.
by hAndDestruct (lemma_A_7_9_1 (-! A)).
- apply: lemma_A_5_2_2.
by apply: lemma_A_7_5.
Qed.
Lemma lemma_A_7_10_1 : forall A, |-- [A]|E|A <<->> <A>A.
Proof.
move => A.
rewrite /DiamondAll.
by apply: gqm_idEquiv.
Qed.
Lemma lemma_A_7_10_2 : forall A, |-- [E]|E|A <<->> <E>A.
Proof.
move => A.
rewrite /SquareExists.
apply: (tac_rewriteR (fun X => <E> X <<->> _) (lemma_A_7_6 _)).
by apply: lemma_A_7_10_4.
Qed.
(** *** Lemma A.7 (xi) *)
Lemma lemma_A_7_11_1 : forall A, |-- [A]A <<->> |A|[A]A.
Proof.
move => A.
hSplit; last by apply: lemma_A_7_4.
apply: gqm_univgen.
asimpl.
by apply: gqm_id.
Qed.
Lemma lemma_A_7_11_2 : forall A, |-- [E]A <<->> |A|[E]A.
Proof.
move => A.
hSplit; last by apply: lemma_A_7_4.
rewrite /SquareExists /DiamondExists.
by apply: gqm_Q5.
Qed.
Lemma lemma_A_7_11_3 : forall A, |-- <A>A <<->> |A|<A>A.
Proof.
move => A.
hSplit; last by apply: lemma_A_7_4.
(* (6) *)
rewrite /DiamondAll /Exists.
apply: gqm_mp; first by apply: gqm_I3.
apply: (tac_rewrite (fun X => -! (|A| X) ->> -! ([A] -! (|A| -! A))) (gqm_dnegEquiv _)).
fold (DiamondExists (|A| -! A)) (Exists (<E> |A| -! A)) (SquareExists (-! A)).
(* (5) *)
apply: gqm_mp; last by apply: (lemma_A_7_4 ([E] -! A)).
apply: gqm_mp; first by apply: gqm_chain2.
apply: (tac_rewriteR (fun X => _ ->> X ) (lemma_A_7_7 _)).
(* (4) *)
apply: lemma_A_7_3_2.
(* (3) *)
by hAndDestruct (lemma_A_7_11_2 (-! A)).
Qed.
Lemma lemma_A_7_11_4 : forall A, |-- <E>A <<->> |A|<E>A.
Proof.
move => A.
hSplit; last by apply: lemma_A_7_4.
(* (6) *)
rewrite /DiamondExists.
apply: gqm_mp; first by apply: gqm_I3.
fold (Exists ([A] -! A)).
apply: (tac_rewriteR (fun X => _ ->> X) (gqm_dnegEquiv _)).
(* (5) *)
apply: gqm_mp; last by apply: (lemma_A_7_4 ([A] -! A)).
apply: gqm_mp; first by apply: gqm_chain2.
apply: (tac_rewriteR (fun X => _ ->> X ) (lemma_A_7_7 _)).
(* (4) *)
apply: lemma_A_7_3_2.
(* (3) *)
by hAndDestruct (lemma_A_7_11_1 (-! A)).
Qed.
(** *** Lemma A.7 (xii) *)
Lemma lemma_A_7_12_1 : forall A, |-- [A]A <<->> |E|[A]A.
Proof.
move => A.
rewrite /Exists.
apply: (tac_rewrite (fun X => X) (gqm_equivNegEquiv2 _ _)).
apply: (tac_rewrite (fun X => -! ([A] X) <<->> |A| -! ([A] X)) (gqm_dnegEquiv _)).
by apply: lemma_A_7_11_4.
Qed.
Lemma lemma_A_7_12_2 : forall A, |-- [E]A <<->> |E|[E]A.
Proof.
move => A.
rewrite /Exists /SquareExists /DiamondExists.
apply: (tac_rewriteR (fun X => X) (gqm_equivNegEquiv _ _)).
apply: (tac_rewriteR (fun X => _ <<->> |A| X) (gqm_dnegEquiv _)).
by apply: lemma_A_7_11_1.
Qed.
Lemma lemma_A_7_12_3 : forall A, |-- <A>A <<->> |E|<A>A.
Proof.
move => A.
rewrite /Exists /DiamondAll.
apply: (tac_rewrite (fun X => X) (gqm_equivNegEquiv2 _ _)).
apply: (tac_rewrite (fun X => -! ([A] X) <<->> |A| -! ([A] X)) (gqm_dnegEquiv _)).
by apply: lemma_A_7_11_4.
Qed.
Lemma lemma_A_7_12_4 : forall A, |-- <E>A <<->> |E|<E>A.
Proof.
move => A.
rewrite /Exists /SquareExists /DiamondExists.
apply: (tac_rewriteR (fun X => X) (gqm_equivNegEquiv _ _)).
apply: (tac_rewriteR (fun X => _ <<->> |A| X) (gqm_dnegEquiv _)).
by apply: lemma_A_7_11_1.
Qed.
\ No newline at end of file
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment