(***************************************************************************
* Generic Variables for Programming Language Metatheory                    *
* Brian Aydemir & Arthur Charguéraud, July 2007, Coq v8.1                  *
***************************************************************************)

Set Implicit Arguments.
Require Import List Max Omega OrderedType OrderedTypeEx.
Require Import LibTactics Metatheory_Set.


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

Module Type VariablesType.

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

Parameter var : Set.

(** This type is inhabited. *)

Parameter var_default : var.

(** Variables are ordered. *)

Declare Module Var_as_OT : UsualOrderedType with Definition t := var.

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

Module Import VarSet := FinSet Var_as_OT.

Open Local Scope fset_scope.

Definition vars := VarSet.fset.

(** 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 *)

(* todo: clean up the implementation of this module, and move elsewhere *)

Module Variables : VariablesType.

Definition var := nat.

Definition var_default : var := O.

Module Var_as_OT := Nat_as_OT.

Module Import VarSet := FinSet Var_as_OT.

Open Local Scope fset_scope.

Definition vars := VarSet.fset.

Open Scope nat_scope.

Lemma max_lt_l :
  forall (x y z : nat), x <= y -> x <= max y z.
Proof.
  induction x; auto with arith.
  induction y; induction z; simpl; auto with arith.
Qed.

Lemma finite_nat_list_max : forall (l : list nat),
  { n : nat | forall x, In x l -> x <= n }.
Proof.
  induction l as [ | l ls IHl ].
  exists 0; intros x H; inversion H.
  inversion IHl as [x H].
  exists (max x l); intros y J; simpl in J; inversion J.
    subst; auto with arith.
    assert (y <= x); auto using max_lt_l.
Qed.

Lemma finite_nat_list_max' : forall (l : list nat),
  { n : nat | ~ In n l }.
Proof.
  intros l. case (finite_nat_list_max l); intros x H.
  exists (S x). intros J. assert (K := H _ J); omega.
Qed.

Definition var_gen (L : vars) : var :=
  proj1_sig (finite_nat_list_max' (of_list L)).

Lemma var_gen_spec : forall E, (var_gen E) \notin E.
Proof.
  unfold var_gen. intros E.
  destruct (finite_nat_list_max' (of_list E)) as [n pf].
  simpl. intros a.
  assert (In n (of_list E)). 
  skip. skip. (* todo: complete properties in fset *)
  (* todo
  rewrite <- InA_iff_In.
  auto using elements_1.
  intuition.
  *)
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.


(* ********************************************************************** *)
(** * Properties of variables *)

Export Variables.
Export Variables.VarSet.
Open Scope fset_scope.

(** Equality on variables is decidable. *)

Module Var_as_OT_Facts := OrderedTypeFacts Variables.Var_as_OT.

Lemma eq_var_dec : forall x y : var, {x = y} + {x <> y}.
Proof.
  exact Var_as_OT_Facts.eq_dec.
Qed.


(* ********************************************************************** *)
(** ** Dealing with list of variables *)

(** 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.

(** Triviality : If a list xs contains n fresh variables, then
    the length of xs is n. *)

Lemma fresh_length : forall xs L n,
  fresh L n xs -> n = length xs.
Proof.
  induction xs; simpl; intros; destruct n; 
  try solve [ false~ | fequals* ].
Qed.

(* 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.