Skip to content
Snippets Groups Projects
Normal view Permalink
GQMTactics.v 863 B
Newer Older
Mackie Loeffel's avatar
finished lemma A.2 and started with some tactics
Mackie Loeffel committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 
(** * Different Tactics to make working with GQM easier *)

Require Import GQM.Base.
Require Import GQM.GQM.
Require Import GQM.GQMDeduction.
Require Import GQM.GQMClassical.

(** ** hSplit
 inspired from iSplit in https://gitlab.mpi-sws.org/FP/iris-coq/blob/master/theories/proofmode/tactics.v#L739
 *)

Lemma tac_and_split : forall A B, |-- A -> |-- B -> |-- A & B.
Proof.
  move => A B HA HB.
  apply: gqm_mp.
  - by apply: gqm_mp; first by apply: gqm_andI.
  - done.
Qed.

Tactic Notation "hSplit" := move => *; apply: tac_and_split.

(** ** hAndDestruct *)

Lemma tac_and_destruct_lemma : forall A B, |-- A & B -> |-- A /\ |-- B.
Proof.
  move => A B.
  split.
  - by apply: gqm_mp; first by apply: (gqm_andE1 A B).
  - by apply: gqm_mp; first by apply: (gqm_andE2 A B).
Qed.

Tactic Notation "hAndDestruct" constr(H) := case: (tac_and_destruct_lemma _ _ H).