From 038397ba1e336c3c36516d291cb6563711ef79ea Mon Sep 17 00:00:00 2001
From: Mackie Loeffel <mackie.loeffel@web.de>
Date: Mon, 30 Apr 2018 13:09:41 +0200
Subject: [PATCH] started with hRewrite

---
 theories/GQM.v                     |   4 +-
 theories/GQMClassical.v            |   7 ++
 theories/GQMClassicalWithTactics.v |  14 +++
 theories/GQMTactics.v              | 193 ++++++++++++++++++++++++++++-
 theories/Section5.v                |  23 ++--
 5 files changed, 224 insertions(+), 17 deletions(-)

diff --git a/theories/GQM.v b/theories/GQM.v
index caee351..e25f8a1 100644
--- a/theories/GQM.v
+++ b/theories/GQM.v
@@ -63,7 +63,7 @@ Definition quant_to_neg_form(q : Quantifier) : form -> form :=
 
 (** ** Decidable Equality *)
 
-Lemma dceq_v : forall n n0,  {Var n = Var n0} + {Var n <> Var n0}.
+Lemma dceq_v : forall n n0, decidable (Var n = Var n0).
 Proof.
   elim.
   - case; by [ left | right].
@@ -80,7 +80,7 @@ Proof.
       by rewrite Heq.
 Qed.
 
-Lemma dceq_f: forall (A B: form), {A = B} + {A <> B}.
+Lemma dceq_f: forall (A B: form), decidable (A = B).
 Proof.
   elim; intros; case: B; try by [right];
     try by [ move => f2; case: (X f2); try by [move => ->; left];
diff --git a/theories/GQMClassical.v b/theories/GQMClassical.v
index c8c30e2..a64475f 100644
--- a/theories/GQMClassical.v
+++ b/theories/GQMClassical.v
@@ -59,6 +59,13 @@ Proof.
   - apply: (gqm_I1 (B ->> C) A).
 Qed.
 
+Lemma gqm_chain2 : forall A B C, |-- (A ->> B) ->> (B ->> C) ->> (A ->> C).
+Proof.
+  move => A B C.
+  apply: gqm_mp; first by apply: gqm_swap.
+  by apply: gqm_chain.
+Qed.
+
 Lemma gqm_discard : forall A B C, |-- (A ->> C) ->> (B ->> A ->> C).
 Proof.
   eauto with GQMDB.
diff --git a/theories/GQMClassicalWithTactics.v b/theories/GQMClassicalWithTactics.v
index 727dea9..996f034 100644
--- a/theories/GQMClassicalWithTactics.v
+++ b/theories/GQMClassicalWithTactics.v
@@ -9,4 +9,18 @@ Require Export GQM.GQMTactics.
 Lemma gqm_equiv_id : forall A, |-- A <<->> A.
 Proof.
   hSplit; apply: gqm_id.
+Qed.
+
+Lemma gqm_equiv_comm : forall {A} {B}, |-- A <<->> B -> |-- B <<->> A.
+Proof.
+  move => A B Heq.
+  hAndDestruct Heq.
+  by hSplit.
+Qed.
+
+Lemma gqm_dnegEquivR : forall A, |-- -! -! A <<->> A.
+Proof.
+  move => A.
+  apply: gqm_equiv_comm.
+  by apply: gqm_dnegEquiv.
 Qed.
\ No newline at end of file
diff --git a/theories/GQMTactics.v b/theories/GQMTactics.v
index 3c370d0..3e0c778 100644
--- a/theories/GQMTactics.v
+++ b/theories/GQMTactics.v
@@ -29,4 +29,195 @@ Proof.
   - by apply: gqm_mp; first by apply: (gqm_andE2 A B).
 Qed.
 
-Tactic Notation "hAndDestruct" constr(H) := case: (tac_and_destruct_lemma _ _ H).
\ No newline at end of file
+Tactic Notation "hAndDestruct" constr(H) := case: (tac_and_destruct_lemma _ _ H); try clear H.
+
+(** ** hRewrite *)
+
+(* Set Typeclasses Debug. *)
+
+Class Rewriteable (X : form -> form) := { form_rewrite : forall A B, |-- A <<->> B -> |-- X A <<->> X B }.
+
+Instance id_rewriteable : Rewriteable (fun X => X) := {}. done. Qed.
+
+Instance square_all_rewriteable(r : form -> form) `{Rewriteable r} : Rewriteable (fun X => [A] (r X)) := {}.
+Proof.
+  case: H => Hr.
+  move => A B Heq.
+  hAndDestruct (Hr _ _ Heq) => HAB HBA.
+  hSplit.
+  - apply: gqm_mp; first by apply: gqm_ADist.
+    by apply: gqm_Anec.
+  - apply: gqm_mp; first by apply: gqm_ADist.
+    by apply: gqm_Anec.
+Qed.
+
+Instance square_all_id_rewriteable: Rewriteable SquareAll | 100 := {}.
+Proof.
+  by case: (square_all_rewriteable ssrfun.id).
+Qed.
+
+Instance imp_l_rewriteable(r : form -> form) `{Rewriteable r} (X :form) : Rewriteable (fun B => r B ->> X) := {}.
+Proof.
+  case: H => Hr.
+  move => A B Heq.
+  hAndDestruct (Hr _ _ Heq) => HAB HBA.
+  by hSplit; apply: gqm_mp; try by apply: gqm_chain2.
+Qed.
+
+Instance imp_r_rewriteable(r : form -> form) `{Rewriteable r} (X :form) : Rewriteable (fun B => X ->> r B) := {}.
+Proof.
+  case: H => Hr.
+  move => A B Heq.
+  hAndDestruct (Hr _ _ Heq) => HAB HBA.
+  by hSplit; apply: gqm_mp; try by apply: gqm_chain.
+Qed.
+
+Instance imp_rewriteable_id(X :form) : Rewriteable (Imp X) | 100 := {}.
+Proof.
+    by have [] := (@imp_r_rewriteable ssrfun.id id_rewriteable X).
+Qed.
+
+(* Instance imp_both_rewriteable(r1 : form -> form)(r2 : form -> form) `{Rewriteable r1} `{Rewriteable r2} (X :form) : Rewriteable (fun B => r1 B ->> r2 B) := {}. *)
+(* Proof. *)
+  (* case: H => Hr1. *)
+  (* case: H0 => Hr2. *)
+  (* move => A B Heq. *)
+  (* hAndDestruct (Hr1 _ _ Heq) => HAB1 HBA1. *)
+  (* hAndDestruct (Hr2 _ _ Heq) => HAB2 HBA2. *)
+  (* hSplit. *)
+  (* - apply:  *)
+(* Qed. *)
+
+
+Instance box_rewriteable(r : form -> form) `{Rewriteable r} : Rewriteable (fun X => |[]| (r X)) := {}.
+Proof.
+  case: H => Hr.
+  move => A B Heq.
+  have ? := (Hr _ _ Heq).
+  apply: gqm_mp; first by apply: gqm_BoxCon.
+  by apply: gqm_Anec.
+Qed.
+
+Instance box_id_rewriteable: Rewriteable Box | 100 := {}.
+Proof.
+  by case: (box_rewriteable ssrfun.id).
+Qed.
+
+(* Instance subst_rewriteable(r : form -> form) `{Rewriteable r} (f: var -> form) : Rewriteable (fun X => subst f (r X)) := {}. *)
+(* Proof. *)
+  (* case: H => Hr. *)
+  (* move => A B Heq. *)
+  (* have H := (Hr _ _ Heq). *)
+  (* have -> : (((r A).[f] <<->> (r B).[f]) = subst f (r A <<->> r B)) by asimpl. *)
+
+(* Qed. *)
+
+
+(* this is here for testing purposes *)
+Lemma gqm_dnegEquiv : forall A, |-- (A <<->> -! -! A).
+Proof.
+  move => A.
+  hSplit.
+  - apply: gqm_dnegI.
+  - apply: gqm_dnegE.
+Qed.
+
+Example rewrite_test_1 : forall A B, |-- A ->> B -> |-- A ->> -!-!B.
+Proof.
+  move => A B Himp.
+  hAndDestruct (@form_rewrite (fun X => A ->> X) _ _ _ (gqm_dnegEquiv B)) => Ha _.
+  apply: gqm_mp; first by apply: Ha.
+  done.
+Qed.
+
+Example rewrite_test_2 : forall A B, |-- [A](A ->> B) -> |-- [A](A ->> -!-!B).
+Proof.
+  move => A B Himp.
+  have H : (|-- [A](A ->> B) <<->> [A](A ->> -!-!B)). {
+    apply: (form_rewrite _ _ (gqm_dnegEquiv B)).
+  }
+  hAndDestruct H => H _.
+  apply: gqm_mp; first by apply H.
+  done.
+Qed.
+
+Example rewrite_test_3 : forall A B, |-- [A](A ->> [A] B) -> |-- [A](A ->> [A]-!-!B).
+Proof.
+  move => A B Himp.
+  have H : (|-- [A](A ->> [A]B) <<->> [A](A ->> [A]-!-!B)). {
+    apply: (form_rewrite _ _ (gqm_dnegEquiv B)).
+  }
+  hAndDestruct H => H _.
+  apply: gqm_mp; first by apply H.
+  done.
+Qed.
+
+Example rewrite_test_4 : forall A B, |-- [A](A ->> [A]|[]| B) -> |-- [A](A ->> [A]|[]|-!-!B).
+Proof.
+  move => A B Himp.
+  have H : (|-- [A](A ->> [A]|[]|B) <<->> [A](A ->> [A]|[]|-!-!B)). {
+    apply: (form_rewrite _ _ (gqm_dnegEquiv B)).
+  }
+  hAndDestruct H => H _.
+  apply: gqm_mp; first by apply H.
+  done.
+Qed.
+
+(* Example rewrite_test_5 : forall A, |-- |A|A -> |-- |A|-!-!A. *)
+(* Proof. *)
+  (* move => A Himp. *)
+  (* have H : (|-- |A|A <<->> |A|-!-!A). { *)
+    (* Set Typeclasses Debug. *)
+    (* apply (@form_rewrite All _ _ _ (gqm_dnegEquiv A)). *)
+  (* } *)
+  (* hAndDestruct H => H _. *)
+  (* apply: gqm_mp; first by apply H. *)
+  (* done. *)
+(* Qed. *)
+
+(* Example rewrite_test_5 : forall A B, |-- (A <<->> B) -> |-- (A <<->> -!-!B). *)
+(* Proof. *)
+  (* move => A B Himp. *)
+  (* have H : (|-- (A <<->> B) <<->> (A <<->> -!-!B)). { *)
+    (* apply (@form_rewrite (fun X => A <<->> X) _ _ _ (gqm_dnegEquiv B)). *)
+  (* } *)
+  (* hAndDestruct H => H _. *)
+  (* apply: gqm_mp; first by apply H. *)
+  (* done. *)
+(* Qed. *)
+
+Lemma tac_rewrite(r: form -> form) `{Rewriteable r} :
+  forall A B, |-- A <<->> B -> |-- r A -> |-- r B.
+Proof.
+  case: H => Hr.
+  move => A B Heq HA.
+  hAndDestruct (Hr _ _ Heq) => HAB _.
+  by apply: gqm_mp; first by apply HAB.
+Qed.
+
+Example rewrite_test_1' : forall A B, |-- A ->> B -> |-- A ->> -!-!B.
+Proof.
+  move => A B Himp.
+  by apply: (tac_rewrite (fun X => A ->> X) _ _ (gqm_dnegEquiv B)).
+Qed.
+
+Tactic Notation "hRewrite" constr(Heq) constr(fShape) :=
+  apply: (tac_rewrite fShape _ _ Heq).
+
+Example rewrite_test_2' : forall A B, |-- [A](A ->> B) -> |-- [A](A ->> -!-!B).
+Proof.
+  move => A B Himp.
+  by hRewrite (gqm_dnegEquiv B) (fun X => [A](A ->> X)).
+Qed.
+
+Example rewrite_test_3' : forall A B, |-- [A](A ->> [A] B) -> |-- [A](A ->> [A]-!-!B).
+Proof.
+  move => A B Himp.
+  by hRewrite (gqm_dnegEquiv B) (fun X => [A](A ->> [A] X)).
+Qed.
+
+Example rewrite_test_4' : forall A B, |-- [A](A ->> [A]|[]| B) -> |-- [A](A ->> [A]|[]|-!-!B).
+Proof.
+  move => A B Himp.
+  by hRewrite (gqm_dnegEquiv B) (fun X => [A](A ->> [A]|[]| X)).
+Qed.
diff --git a/theories/Section5.v b/theories/Section5.v
index 87c3e3a..352dec3 100644
--- a/theories/Section5.v
+++ b/theories/Section5.v
@@ -35,32 +35,27 @@ Proof.
     by hAndDestruct (lemma_A_2_1 (|A| -! A)).
 Qed.
 
-(* TODO: this proof is quite long, whereas it is not very difficult. find a way to shorten it *)
 Lemma lemma_A_2_3 : forall A, |-- [A]A <<->> -!<E>-!A.
 Proof.
   move => A.
   hSplit.
   - apply: gqm_mp; first by apply: gqm_contrap3.
-    apply: gqm_mp.
-    + apply: gqm_mp; first by apply: (gqm_chain _ (-! ([A] -! -! A))).
-      apply: gqm_mp; first by apply: gqm_contrap.
-      apply: lemma_A_1.
-      apply: gqm_dnegI.
-    + by hAndDestruct (lemma_A_2_1 (-! A)).
+    hRewrite (gqm_dnegEquivR A) (fun X => <E> -! A ->> -! ([A] X)).
+    by hAndDestruct (lemma_A_2_1 (-! A)).
   - apply: gqm_mp; first by apply: gqm_contrap2.
-    apply: gqm_mp.
-    + apply: gqm_mp; first by apply: (gqm_chain _ (-! ([A] -! -! A))).
-      apply: gqm_mp; first by apply: gqm_contrap.
-        by apply: gqm_id.
-    + apply: gqm_mp; first by apply: gqm_contrap.
-      apply: lemma_A_1.
-      by apply: gqm_dnegE.
+    hRewrite (gqm_dnegEquivR A) (fun X => -! ([A] X) ->> <E> -! A).
+    by hAndDestruct (lemma_A_2_1 (-! A)).
 Qed.
 
 Lemma lemma_A_2_4 : forall A, |-- [E]A <<->> -!<A>-!A.
 Proof.
   move => A.
   hSplit.
+  (* - apply: gqm_mp; first by apply: gqm_contrap3. *)
+    (* Set Typeclasses Debug. *)
+    (* apply (tac_rewrite (fun X => <A> -! A ->> -! ([E] X)) _ _ (gqm_dnegEquivR A)). *)
+    (* hRewrite (gqm_dnegEquivR A) (fun X => <A> -! A ->> -! ([E] X)). *)
+
   - apply: gqm_mp.
     + apply: gqm_mp; first by apply: (gqm_chain _ (([E] -! -! A))).
       apply: gqm_mp; first by apply: gqm_contrap3.
-- 
GitLab