(**************************************************************************
* TLC: A library for Coq                                                  *
* Variable names                                                          *
**************************************************************************)

Set Implicit Arguments.
Require Import LibTactics LibList LibLogic LibNat LibEpsilon.
Require Export LibFset.


(* ********************************************************************** *)
(** * Abstract Definition of Variables *)

Module Type VariablesType.

(** We leave the type of variables abstract. *)

Parameter var : Set.

(** This type is inhabited. *)

Parameter var_inhab : Inhab var.

(** We can build sets of variables. *)

Definition vars := fset var.

(** Finally, we have a means of generating fresh variables. *)

Parameter var_gen : vars -> var.
Parameter var_gen_spec : forall E, (var_gen E) \notin E.
Parameter var_fresh : forall (L : vars), { x : var | x \notin L }.

End VariablesType.


(* ********************************************************************** *)
(** * Concrete Implementation of Variables *)

Module Export Variables : VariablesType.

Definition var := nat.

Lemma var_inhab : Inhab var.
Proof. apply (prove_Inhab 0). Qed.

Definition vars := fset var.

Definition var_gen_list (l : list nat) :=
  1 + fold_right plus O l.

Lemma var_gen_list_spec : forall n l,
  n \in from_list l -> n < var_gen_list l.
Proof.
  unfold var_gen_list. induction l; introv I.
  rewrite from_list_nil in I. false (in_empty_elim I).
  rewrite from_list_cons in I. rew_list.
   rewrite in_union in I. destruct I as [H|H].
     rewrite in_singleton in H. subst. nat_math.
     specializes IHl H. nat_math.
Qed.

Definition var_gen (E : vars) : var :=
  var_gen_list (epsilon (fun l => E = from_list l)).

Lemma var_gen_spec : forall E, (var_gen E) \notin E.
Proof.
  intros. unfold var_gen. spec_epsilon as l.
  applys fset_finite. rewrite Hl. introv H.
  forwards M: var_gen_list_spec H. nat_math.
Qed.

Lemma var_fresh : forall (L : vars), { x : var | x \notin L }.
Proof. intros L. exists (var_gen L). apply var_gen_spec. Qed.

End Variables.


(* ********************************************************************** *)
(** ** Lists of variables of given length and given freshness *)

(** Freshness of n variables from a set L and from one another. *)

Fixpoint fresh (L : vars) (n : nat) (xs : list var) {struct xs} : Prop :=
  match xs, n with
  | nil, O => True
  | x::xs', S n' => x \notin L /\ fresh (L \u \{x}) n' xs'
  | _,_ => False
  end.

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

(* It is possible to build a list of n fresh variables. *)

Lemma var_freshes : forall L n, 
  { xs : list var | fresh L n xs }.
Proof.
  intros. gen L. induction n; intros L.
  exists* (nil : list var).
  destruct (var_fresh L) as [x Fr].
   destruct (IHn (L \u \{x})) as [xs Frs].
   exists* (x::xs).
Qed.


(* ********************************************************************** *)
(** ** Picking fresh names *)

(** [gather_vars_for_type T F] return the union of all the finite sets
  of variables [F x] where [x] is a variable from the context such that
  [F x] type checks. In other words [x] has to be of the type of the
  argument of [F]. The resulting union of sets does not contain any
  duplicated item. This tactic is an extreme piece of hacking necessary
  because the tactic language does not support a "fold" operation on
  the context. *)

Ltac gather_vars_with F :=
  let rec gather V :=
    match goal with
    | H: ?S |- _ =>
      let FH := constr:(F H) in
      match V with
      | \{} => gather FH
      | context [FH] => fail 1
      | _ => gather (FH \u V)
      end
    | _ => V
    end in
  let L := gather (\{}:vars) in eval simpl in L.

(** [beautify_fset V] assumes that [V] is built as a union of finite
  sets and return the same set cleaned up: empty sets are removed and
  items are laid out in a nicely parenthesized way *)

Ltac beautify_fset V :=
  let rec go Acc E :=
     match E with
     | ?E1 \u ?E2 => let Acc1 := go Acc E1 in
                     go Acc1 E2
     | \{}  => Acc
     | ?E1 => match Acc with
              | \{} => E1
              | _ => constr:(Acc \u E1)
              end
     end
  in go (\{}:vars) V.

(** [pick_fresh_gen L Y] expects [L] to be a finite set of variables
  and adds to the context a variable with name [Y] and a proof that
  [Y] is fresh for [L]. *)

Ltac pick_fresh_gen L Y :=
  let Fr := fresh "Fr" in
  let L := beautify_fset L in
  (destruct (var_fresh L) as [Y Fr]).

(** [pick_fresh_gens L n Y] expects [L] to be a finite set of variables
  and adds to the context a list of variables with name [Y] and a proof 
  that [Y] is of length [n] and contains variable fresh for [L] and
  distinct from one another. *)

Ltac pick_freshes_gen L n Y :=
  let Fr := fresh "Fr" in
  let L := beautify_fset L in
  (destruct (var_freshes L n) as [Y Fr]).




(* ********************************************************************** *)
(** ** Tactics for notin *)

Implicit Types x : var.

(** 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_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_from_fresh_in_context :=
  repeat (match goal with H: fresh _ _ _ |- _ =>
    progress (simpl in H; destructs H) end).

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

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

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

(* ********************************************************************** *)
(** ** 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.
  rew_length. 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].

Lemma fresh_single_notin : forall x xs n,
  fresh \{x} n xs ->
  x \notin from_list xs.
Proof.
  induction xs; destruct n; introv F; simpl in F; tryfalse.
  rewrite~ from_list_nil.
  destruct F as [Fr F']. lets [? ?]: (fresh_union_r F').
   specializes IHxs n. rewrite~ from_list_cons.
Qed.

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 ].

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

(* LATER: more automation of fresh_length properties *)