(***************************************************************************
* Tactics to Automate Reasoning about Freshness                            *
* Brian Aydemir & Arthur Charguéraud, July 2007, Coq v8.1                  *
***************************************************************************)

Set Implicit Arguments.
Require Import LibTactics List Metatheory_Var.

(* todo: add comments *)
(* todo: nettoyer les preuves de fresh en utilisant calc_fset *)
(* todo: simplifier notin_union_r1 et notin_union_r2 *)

(* ********************************************************************** *)
(** ** Tactics for fresh and notin *)

Ltac notin_from_fresh_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.
Proof. intros. rewrite~ <- notin_singleton. Qed.

Lemma notin_singleton_l : forall x y,
  x <> y -> x \notin {{y}}.
Proof. intros. rewrite~ notin_singleton. Qed.

Lemma notin_singleton_swap : forall x y,
  x \notin {{y}} -> y \notin {{x}}.
Proof.
  intros. apply notin_singleton_l.
  apply sym_not_eq. apply~ notin_singleton_r.
Qed.

Lemma notin_union_r : forall x E F,
  x \notin (E \u F) -> (x \notin E) /\ (x \notin F).
Proof. intros. rewrite~ <- notin_union. Qed.

Lemma notin_union_r1 : forall x E F,
  x \notin (E \u F) -> (x \notin E).
Proof. introv. rewrite* notin_union. Qed.

Lemma notin_union_r2 : forall x E F,
  x \notin (E \u F) -> (x \notin F).
Proof. introv. rewrite* notin_union. Qed.

Lemma notin_union_l : forall x E F,
  x \notin E -> x \notin F -> x \notin (E \u F).
Proof. intros. rewrite~ notin_union. Qed.

Lemma notin_var_gen : forall E F,
  (forall x, x \notin E -> x \notin F) ->
  (var_gen E) \notin F.
Proof. intros. auto~ var_gen_spec. Qed.

Implicit Arguments notin_singleton_r    [x y].
Implicit Arguments notin_singleton_l    [x y].
Implicit Arguments notin_singleton_swap [x y].
Implicit Arguments notin_union_r  [x E F].
Implicit Arguments notin_union_r1 [x E F].
Implicit Arguments notin_union_r2 [x E F].
Implicit Arguments notin_union_l  [x E F].

(** Tactics to deal with notin.  *)

Ltac notin_solve_target_from x E H :=
  match type of H with 
  | x \notin E => constr:(H)
  | x \notin (?F \u ?G) =>  
     let H' :=
        match F with 
        | context [E] => constr:(notin_union_r1 H)
        | _ => match G with 
          | context [E] => constr:(notin_union_r2 H)
          | _ => fail 20
          end
        end in
     notin_solve_target_from x E H' 
  end.

Ltac notin_solve_target x E :=
  match goal with 
  | H: x \notin ?L |- _ =>
    match L with context[E] =>
      let F := notin_solve_target_from x E H in
      apply F 
    end
  | H: x <> ?y |- _ => 
     match E with {{y}} => 
       apply (notin_singleton_l H)
     end
  end.

Ltac notin_solve_one :=
  match goal with
  | |- ?x \notin {{?y}} => 
     apply notin_singleton_swap; 
     notin_solve_target y ({{x}}) 
  | |- ?x \notin ?E => 
    notin_solve_target x E
  (* If x is an evar, tries to instantiate it.
     Problem: it might loop ! 
  | |- ?x \notin ?E => 
     match goal with y:var |- _ =>
       match y with 
       | x => fail 1
       | _ =>
         let H := fresh in cuts H: (y \notin E); 
         [ apply H | notin_solve_target y E ]
        end
     end
  *)
  end.

Ltac notin_simpl :=
  match goal with 
  | |- _ \notin (_ \u _) => apply notin_union_l; notin_simpl 
  | |- _ \notin ({}) => apply notin_empty; notin_simpl
  | |- ?x <> ?y => apply notin_singleton_r; notin_simpl
  | |- _ => idtac
  end.

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

Ltac notin_simpl_hyps := (* forward-chaining *)
  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_simpl2.

Ltac notin_solve_false :=
  match goal with 
  | H: ?x \notin ?E |- _ =>
    match E with context[x] =>
      apply (@notin_same x); 
      let F := notin_solve_target_from x ({{x}}) H in
      apply F
    end 
  | H: ?x <> ?x |- _ => apply H; reflexivity
  end.

Ltac notin_false :=
  match goal with
  | |- False => notin_solve_false
  | _ => false; notin_solve_false
  end.

Ltac notin_solve :=
  notin_from_fresh_in_context;
  first [ notin_simpl; try notin_solve_one
        | notin_false ].

(* 
TODO:
  | |- ?x \notin ?E => 
	progress (unfold x); notin_simpl
  | |- (var_gen ?x) \notin _ =>
        apply notin_var_gen; intros; notin_simpl
*)

(***************************************************************************)
(** Automation: hints to solve "notin" subgoals automatically. *)

Hint Extern 1 (_ \notin _) => notin_solve.
Hint Extern 1 (_ <> _ :> var) => notin_solve.
Hint Extern 1 (_ <> _ :> Var_as_OT.t) => notin_solve.
Hint Extern 1 ((_ \notin _) /\ _) => splits.


(* ********************************************************************** *)
(** ** Tactics for fresh *)

Lemma fresh_union_r : forall xs L1 L2 n,
  fresh (L1 \u L2) n xs -> fresh L1 n xs /\ fresh L2 n xs.
Proof.
  induction xs; simpl; intros; destruct n;
  tryfalse*. auto.
  destruct H. split; split; auto.
  forwards*: (@IHxs (L1 \u {{a}}) L2 n).
   rewrite union_comm.
   rewrite union_comm_assoc.
   rewrite* union_assoc.
  forwards*: (@IHxs L1 (L2 \u {{a}}) n).
   rewrite* union_assoc.
Qed.

Lemma fresh_union_r1 : forall xs L1 L2 n,
  fresh (L1 \u L2) n xs -> fresh L1 n xs.
Proof. intros. forwards*: fresh_union_r. Qed.

Lemma fresh_union_r2 : forall xs L1 L2 n,
  fresh (L1 \u L2) n xs -> fresh L2 n xs.
Proof. intros. forwards*: fresh_union_r. Qed.

Lemma fresh_union_l : forall xs L1 L2 n,
  fresh L1 n xs -> fresh L2 n xs -> fresh (L1 \u L2) n xs.
Proof.
  induction xs; simpl; intros; destruct n; tryfalse*. auto.
  destruct H. destruct H0. split~.
  forwards~ K: (@IHxs (L1 \u {{a}}) (L2 \u {{a}}) n). 
  rewrite <- (union_same {{a}}).
  rewrite union_assoc.
  rewrite <- (@union_assoc L1).
  rewrite (@union_comm L2).
  rewrite (@union_assoc L1).
  rewrite* <- union_assoc.
Qed.

Lemma fresh_empty : forall L n xs,
  fresh L n xs -> fresh {} n xs.
Proof.
  intros. rewrite <- (@union_empty_r L) in H.
  destruct* (fresh_union_r _ _ _ _ H).
Qed.

Lemma fresh_length : forall L n xs,
  fresh L n xs -> n = length xs.
Proof.
  intros. gen n L. induction xs; simpl; intros n L Fr;
    destruct n; tryfalse*. 
  auto.
  rewrite* <- (@IHxs n (L \u {{a}})).
Qed.

Lemma fresh_resize : forall L n xs,
  fresh L n xs -> forall m, m = n -> fresh L m xs.
Proof.
  introv Fr Eq. subst~.
Qed.

Lemma fresh_resize_length : forall L n xs,
  fresh L n xs -> fresh L (length xs) xs.
Proof.
  introv Fr. rewrite* <- (fresh_length _ _ _ Fr).
Qed.

Implicit Arguments fresh_union_r [xs L1 L2 n].
Implicit Arguments fresh_union_r1 [xs L1 L2 n].
Implicit Arguments fresh_union_r2 [xs L1 L2 n].
Implicit Arguments fresh_union_l [xs L1 L2 n].
Implicit Arguments fresh_empty  [L n xs].
Implicit Arguments fresh_length [L n xs].
Implicit Arguments fresh_resize [L n xs].
Implicit Arguments fresh_resize_length [L n xs].

Ltac fresh_solve_target_from E n xs H :=
  match type of H with 
  | fresh E n xs => constr:(H)
  | fresh E ?m xs => 
      match n with 
      | length xs => constr:(fresh_resize_length H) 
      | _ => 
         match goal with 
         | Eq: m = n |- _ => constr:(fresh_resize H _ (sym_eq Eq)) 
         | Eq: n = m |- _ => constr:(fresh_resize H _ Eq) 
         end
      end
  | fresh (?F \u ?G) ?m xs => 
     let H' :=
        match F with 
        | context [E] => constr:(fresh_union_r1 H)
        | _ => match G with 
          | context [E] => constr:(fresh_union_r2 H)
          | _ => fail 20
          end
        end in
     fresh_solve_target_from E n xs H' 
  end.

Ltac fresh_solve_target E n xs :=
  match goal with H: fresh ?L _ xs |- _ =>
    match L with context[E] =>
      let F := fresh_solve_target_from E n xs H in
      apply F 
    end
  end.

Ltac fresh_solve_one :=
  match goal with 
  | |- fresh ?E ?n ?xs =>   
    fresh_solve_target E n xs 
  | |- fresh {} ?n ?xs =>
    match goal with H: fresh ?F ?m xs |- _ =>
      apply (fresh_empty H);
      fresh_solve_target F n xs 
    end
  end.

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

Ltac fresh_solve_by_notins :=
  simpl; splits; try notin_solve.

Ltac fresh_solve :=
  fresh_simpl; 
  first [ fresh_solve_one 
        | fresh_solve_by_notins 
        | idtac ].


(***************************************************************************)
(** Automation: hints to solve "fresh" subgoals automatically. *)

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

(* TODO: automation of fresh_length properties *)