Module Sigma

Set Implicit Arguments.
Require Import MyTactics.
Require Import Types.
Require Import TypeEquality.
Require Import Environments.
Require Import Typing.


Ltac sigma :=
  repeat match goal with
  | h1: tyeq (TyRegion ?r) ?sigma, h2: jv ?R nil nil ?v (TyAt ?sigma) |- _ =>
      assert (jv R nil nil v (TyAt (TyRegion r)));
      [ eauto using tyeq_symmetric, tyeq_at | clear h2 ]
  | h1: tyeq (TyRegion ?r) ?sigma, h2: jv ?R nil nil ?v (TyRegionCap ?rk ?sigma ?T) |- _ =>
      assert (jv R nil nil v (TyRegionCap rk (TyRegion r) T));
      [ eauto 8 using tyeq_symmetric, tyeq_regioncap | clear h2 ]
  | h: tyeq (TyRegion ?r) ?sigma |- jv _ _ _ _ (TyAt ?sigma) =>
      eapply JVEq with (T1 := TyAt (TyRegion r));
      [ idtac | eauto using tyeq_at | eauto ]
  | h: tyeq (TyRegion ?r) ?sigma |- jv _ _ _ _ (TyRegionCap ?rk ?sigma ?T) =>
      eapply JVEq with (T1 := TyRegionCap rk (TyRegion r) T);
      [ idtac | eauto using tyeq_regioncap | eauto ]
  | h: tyeq (TyRegion ?r) ?rho |- jv _ _ _ _ (TyRegionCapPunched ?rho ?T ?sigma) =>
      eapply JVEq with (T1 := TyRegionCapPunched (TyRegion r) T sigma);
      [ idtac | eauto 6 using tyeq_regioncappunched | eauto ]
  | h: tyeq (TyRegion ?s) ?sigma |- jv _ _ _ _ (TyRegionCapPunched ?rho ?T ?sigma) =>
      eapply JVEq with (T1 := TyRegionCapPunched rho T (TyRegion s));
      [ idtac | eauto 6 using tyeq_regioncappunched | eauto ]
  end.