Library Metatheory_Fresh

Require Import Lib_Tactic List Metatheory_Var.

Ltac fresh_simpl_to_notin_in_context :=
  repeat (match goal with H: fresh _ _ _ |- _ =>
    progress (simpl in H; destructs H) end).

Tactics for notin


For efficiency, we avoid rewrites by splitting equivalence.

Lemma notin_singleton_r : forall x y,
  x \notin {{y}} -> x <> y.

Lemma notin_singleton_l : forall x y,
  x <> y -> x \notin {{y}}.

Lemma notin_singleton_swap : forall x y,
  x \notin {{y}} -> y \notin {{x}}.

Lemma notin_union_r : forall x E F,
  x \notin (E \u F) -> (x \notin E) /\ (x \notin F).

Lemma notin_union_l : forall x E F,
  x \notin E -> x \notin F -> x \notin (E \u F).

Tactics to deal with notin. It interacts with union singleton and empty, but not inclusion.

Ltac notin_solve_from x E H :=
  match type of H with x \notin ?L =>
    match L with context[E] =>
      match L with
      | E => exact H
      | ?F \u ?G =>
        let P := constr:(@notin_union_r x F G H) in
        let PF := eval simpl in (proj1 P) in
        let PG := eval simpl in (proj2 P) in
        solve [ notin_solve_from x E PF | notin_solve_from x E PG ]
      end
    end
  end.

Ltac notin_solve_from_context x E :=
  match goal with H: x \notin _ |- _ =>
    notin_solve_from x E H end.

Ltac notin_solve_one :=
  match goal with
  | |- _ \notin {} =>
    apply notin_empty
  | |- ?x \notin {{?y}} =>     apply notin_singleton_l; solve
    [ assumption | apply sym_not_eq; assumption ]
  | |- ?x \notin {{?y}} =>     apply notin_singleton_swap; notin_solve_from_context y ({{x}})
  | |- ?x \notin ?E =>     notin_solve_from_context x E
  end.

Ltac notin_simpl :=
  try match goal with |- _ \notin (_ \u _) =>
    apply notin_union_l; notin_simpl end.

Ltac notin_simpl_hyps :=   try match goal with
  | H: _ \notin {} |- _ =>
     clear H; notin_simpl_hyps
  | H: ?x \notin {{?y}} |- _ =>
     puts (@notin_singleton_r x y H);
     clear H; notin_simpl_hyps
   | H: ?x \notin (?E \u ?F) |- _ =>
     let H1 := fresh "Fr" in let H2 := fresh "Fr" in
     destruct (@notin_union_r x E F H) as [H1 H2];
     clear H; notin_simpl_hyps
  end.

Ltac notin_simpls :=
  notin_simpl_hyps; notin_simpl.

Ltac notin_solve :=
  fresh_simpl_to_notin_in_context;
  notin_simpl; notin_solve_one.

Ltac notin_contradiction :=
  match goal with H: ?x \notin ?E |- _ =>
    match E with context[x] =>
      let K := fresh in assert (K : x \notin {{x}});
        [ notin_solve_one | contradictions; apply (notin_same K) ]
    end
  end.

Ltac notin_neq_solve :=
  apply notin_singleton_r; notin_solve.

Demo for notin

Lemma test_notin_solve_1 : forall x E F G,
  x \notin E \u F -> x \notin G -> x \notin (E \u G).

Lemma test_notin_solve_2 : forall x y E F G,
  x \notin E \u {{y}} \u F -> x \notin G ->
  x \notin {{y}} /\ y \notin {{x}}.

Lemma test_notin_solve_3 : forall x y,
  x <> y -> x \notin {{y}} /\ y \notin {{x}}.

Lemma test_notin_contradiction : forall x y E F G,
  x \notin (E \u {{x}} \u F) -> y \notin G.

Lemma test_neq_solve : forall x y E F,
  x \notin (E \u {{y}} \u F) -> y \notin E ->
  y <> x /\ x <> y.

Automation: hints to solve "notin" subgoals automatically.

Hint Extern 1 (_ \notin _) => notin_solve.

Hint Extern 1 (_ \in _ -> False) =>
  repeat match goal with
  | H: context [?x \in ?E -> False] |- _ =>
    fold (not (x \in E)) in H
  | |- context [?x \in ?E -> False] =>
    fold (not (x \in E)) end.

Hint Extern 1 (_ <> _ :> var) => notin_neq_solve.
Hint Extern 1 (_ <> _ :> S.elt) => notin_neq_solve.

Tactics for fresh


Hint Extern 1 (fresh _ _ _) => simpl.

Lemma fresh_union_r : forall xs L1 L2 n,
  fresh (L1 \u L2) n xs -> fresh L1 n xs /\ fresh L2 n xs.

Lemma fresh_union_l : forall xs L1 L2 n,
  fresh L1 n xs -> fresh L2 n xs -> fresh (L1 \u L2) n xs.

Lemma fresh_empty : forall L n xs,
  fresh L n xs -> fresh {} n xs.

Lemma fresh_length : forall xs L n,
  fresh L n xs -> n = length xs.

Lemma fresh_resize : forall n xs L,
  fresh L n xs -> fresh L (length xs) xs.

Ltac fresh_solve_from xs n E H :=
  match type of H with fresh ?L _ _ =>
    match L with context[E] =>
      match L with
      | E => exact H
      | ?F \u ?G =>
        let P := constr:(@fresh_union_r xs F G n H) in
        let PF := eval simpl in (proj1 P) in
        let PG := eval simpl in (proj2 P) in
        solve [ fresh_solve_from xs n E PF | fresh_solve_from xs n E PG ]
      end
    end
  end.

Ltac fresh_solve_from_context xs n E :=
  match goal with H: fresh _ n xs |- _ =>
    fresh_solve_from xs n E H end.

Ltac fresh_solve_one :=
  match goal with
  | |- fresh {} ?n ?xs =>
    match goal with H: fresh ?L n xs |- _ =>
      apply (@fresh_empty L n xs H) end
  | |- fresh ?E ?n ?xs =>
    fresh_solve_from_context xs n E
  | |- fresh _ (length ?xs) ?xs =>
    match goal with H: fresh _ ?n xs |- _ =>
      progress (apply (@fresh_resize n)); fresh_solve_one end
  end.

Ltac fresh_simpl :=
  try match goal with |- fresh (_ \u _) _ _ =>
    apply fresh_union_l; fresh_simpl end.

Ltac fresh_simpl_to_notin_in_goal :=
  simpl; splits.

Ltac fresh_simpl_to_notin_solve :=
  fresh_simpl_to_notin_in_context;
  fresh_simpl_to_notin_in_goal;
  notin_solve.

Ltac fresh_solve :=
  try fresh_simpl;
  (fresh_solve_one || fresh_simpl_to_notin_solve).

Demo for notin

Lemma test_fresh_solve_1 : forall xs L1 L2 n,
  fresh (L1 \u L2) n xs -> fresh L1 n xs.

Lemma test_fresh_solve_2 : forall xs L1 L2 n,
 fresh (L1 \u L2) n xs -> fresh L2 n xs.

Lemma test_fresh_solve_3 : forall xs L1 L2 n,
 fresh (L1 \u L2) n xs -> fresh {} n xs.

Lemma test_fresh_solve_4 : forall xs L1 L2 n,
 fresh (L1 \u L2) n xs -> fresh L1 (length xs) xs.

Automation: hints to solve "fresh" subgoals automatically.

Hint Extern 1 (fresh _ _ _) => fresh_solve.