Library baseTac

Require Import include.
Require Import memory.
Require Import memdata.
Require Import Lists.ListSet.
Require Import language.
Require Import opsem.
Require Import assertion.

Ltac mytac_1 :=
  match goal with
    | H : exists _, _ |- _ => destruct H; mytac_1
    | H : (_ /\ _) |- _ => destruct H; mytac_1
    | |- _ /\ _ => split; mytac_1
    
    | H : emposabst _ |- _ =>
      unfold emposabst in H; subst; mytac_1
    
    | H : MemMod.join empmem _ _ |- _ =>
      apply MemMod.join_emp_eq in H; subst; mytac_1
    | H : MemMod.join _ empmem _ |- _ =>
      apply MemMod.join_comm in H; apply MemMod.join_emp_eq in H; subst; mytac_1
    | |- MemMod.join empmem _ _ =>
      apply MemMod.join_emp; mytac_1
    | |- MemMod.join _ empmem _ =>
      apply MemMod.join_comm; apply MemMod.join_emp; mytac_1

    | H : EnvMod.join empenv _ _ |- _ =>
      apply EnvMod.join_emp_eq in H; subst; mytac_1
    | H : EnvMod.join _ empenv _ |- _ =>
      apply EnvMod.join_comm in H; apply EnvMod.join_emp_eq in H; subst; mytac_1
    | |- EnvMod.join empenv _ _ =>
      apply EnvMod.join_emp; mytac_1
    | |- EnvMod.join _ empenv _ =>
      apply EnvMod.join_comm; apply EnvMod.join_emp; mytac_1
    
    | H : OSAbstMod.join empabst _ _ |- _ =>
      apply OSAbstMod.join_emp_eq in H; subst; mytac_1
    | H : OSAbstMod.join _ empabst _ |- _ =>
      apply OSAbstMod.join_comm in H; apply OSAbstMod.join_emp_eq in H; subst; mytac_1
    | |- OSAbstMod.join empabst _ _ =>
       apply OSAbstMod.join_emp; mytac_1
    | |- OSAbstMod.join _ empabst _ =>
      apply OSAbstMod.join_comm; apply OSAbstMod.join_emp; mytac_1

    | H : MemMod.join ?a ?b ?ab |- MemMod.join ?b ?a ?ab =>
      apply MemMod.join_comm; auto
    | H : EnvMod.join ?a ?b ?ab |- EnvMod.join ?b ?a ?ab =>
      apply EnvMod.join_comm; auto
    | H : OSAbstMod.join ?a ?b ?ab |- OSAbstMod.join ?b ?a ?ab =>
      apply OSAbstMod.join_comm; auto

    | H : MemMod.join ?a ?b ?ab |- MemMod.disj ?a ?b =>
      apply MemMod.join_disj_meq in H; destruct H; auto
    | H : EnvMod.join ?a ?b ?ab |- EnvMod.disj ?a ?b =>
      apply EnvMod.join_disj_meq in H; destruct H; auto
    | H : OSAbstMod.join ?a ?b ?ab |- OSAbstMod.disj ?a ?b =>
      apply OSAbstMod.join_disj_meq in H; destruct H; auto
    | H : MemMod.join ?a ?b ?ab |- MemMod.disj ?b ?a =>
      apply MemMod.join_comm; mytac_1
    | H : EnvMod.join ?a ?b ?ab |- EnvMod.disj ?b ?a =>
      apply EnvMod.join_comm; mytac_1
    | H : OSAbstMod.join ?a ?b ?ab |- OSAbstMod.disj ?b ?a =>
      apply OSAbstMod.join_comm; mytac_1

    | H : MemMod.meq _ _ |- _ => apply MemMod.meq_eq in H; mytac_1
    | H : EnvMod.meq _ _ |- _ => apply EnvMod.meq_eq in H; mytac_1
    | H : OSAbstMod.meq _ _ |- _ => apply OSAbstMod.meq_eq in H; mytac_1
    | H : (_, _) = (_, _) |- _ => inversion H; clear H; mytac_1
    | H : ?x = ?x |- _ => clear H; mytac_1
    | |- ?x = ?x => reflexivity
    
    | |- MemMod.join _ ?a ?a => apply MemMod.join_emp; mytac_1
    | |- MemMod.join ?a _ ?a => apply MemMod.join_comm; mytac_1
    | |- EnvMod.join _ ?a ?a => apply EnvMod.join_emp; mytac_1
    | |- EnvMod.join ?a _ ?a => apply EnvMod.join_comm; mytac_1
    | |- OSAbstMod.join _ ?a ?a => apply OSAbstMod.join_emp; mytac_1
    | |- OSAbstMod.join ?a _ ?a => apply OSAbstMod.join_comm; mytac_1
    
    | |- empmem = _ => reflexivity; mytac_1
    | |- _ = empmem => reflexivity; mytac_1
    
    | |- empenv = _ => reflexivity; mytac_1
    | |- _ = empenv => reflexivity; mytac_1

    | |- emposabst _ => unfold emposabst; reflexivity; mytac_1
    | |- empabst = _ => reflexivity; mytac_1
    | |- _ = empabst => reflexivity; mytac_1
    
    | |- empisr = _ => reflexivity; mytac_1
    | |- _ = empisr => reflexivity; mytac_1
    
    | H : True |- _ => clear H; mytac_1
    | |- True => auto
    | _ => try (progress subst; mytac_1)
  end.

Ltac mytac := repeat progress mytac_1.

Ltac trysimplall := repeat progress (simpl substmo in *;
simpl substaskst in *;
simpl getmem in *;
simpl getabst in *;
simpl substmo in *;
simpl getisr in *;
simpl getis in *;
simpl getie in *;
simpl gettopis in *;
simpl getcs in *;
simpl get_smem in *;
simpl get_mem in *;
simpl gettopis in *;
simpl starinv_isr in *;
simpl empst in *).