(***************************************************************************
* Bundles of Modules for Developments in Programming Language Metatheory   *
* Arthur Charguéraud, July 2007, Coq v8.1pl4                               *
***************************************************************************)

Set Implicit Arguments.
Require Import LibTactics List Metatheory_Var Metatheory_Fresh.


(* ********************************************************************** *)
(** ** Tactics: Case Analysis on Variables *)

(** We define notations for the equality of variables (our free variables)
  and for the equality of naturals (our bound variables represented using
  de Bruijn indices). *)

Notation "x == y" := (eq_var_dec x y) (at level 67).
Notation "i === j" := (Peano_dec.eq_nat_dec i j) (at level 67).

(** Tactic for comparing two bound or free variables. *)

Ltac case_nat_base :=
  let destr x y := destruct (x === y); [try subst x | idtac] in
  match goal with
  | H: context [?x === ?y] |- _ => destr x y
  | |- context [?x === ?y]      => destr x y
  end.

Tactic Notation "case_nat" := 
  case_nat_base;
  try solve [ match goal with H: ?x <> ?x |- _ => 
               false_goal; apply H; reflexivity end ].
Tactic Notation "case_nat" "~" := case_nat; auto_tilde.
Tactic Notation "case_nat" "*" := case_nat; auto_star.

Ltac case_var_base :=
  let destr x y := destruct (x == y); [try subst x | idtac] in
  match goal with
  | H: context [?x == ?y] |- _ => destr x y
  | |- context [?x == ?y]      => destr x y
  end.

Tactic Notation "case_var" := 
  case_var_base; try solve [ notin_false ].
Tactic Notation "case_var" "~" := case_var; auto_tilde.
Tactic Notation "case_var" "*" := case_var; auto_star.




(* ********************************************************************** *)
(** ** Tactics: Picking Names Fresh from the Context *)

(** [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 {} 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 {} 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: Applying Lemmas With Quantification Over Cofinite Sets *)

(** [apply_fresh_base] tactic is a helper to build tactics that apply an
  inductive constructor whose first argument should be instanciated
  by the set of names already used in the context. Those names should
  be returned by the [gather] tactic given in argument. For each premise
  of the inductive rule starting with an universal quantification of names
  outside the set of names instanciated, a subgoal with be generated by
  the application of the rule, and in those subgoal we introduce the name
  quantified as well as its proof of freshness. *)

Ltac apply_fresh_base_simple lemma gather :=
  let L0 := gather in let L := beautify_fset L0 in
  first [apply (@lemma L) | eapply (@lemma L)].

Ltac intros_fresh x :=
   first [
     let Fr := fresh "Fr" x in 
     intros x Fr
  |  let x2 := 
       match goal with |- forall _:?T, _ =>
       match T with 
       | var => fresh "y"
       | vars => fresh "ys" 
       | list var => fresh "ys" 
       | _ => fresh "y"
       end end in
     let Fr := fresh "Fr" x2 in 
     intros x2 Fr ].

Ltac apply_fresh_base lemma gather var_name :=
  apply_fresh_base_simple lemma gather; 
  try (match goal with
    | |- forall _:_, _ \notin _ -> _ => intros_fresh var_name
    | |- forall _:_, fresh _ _ _ -> _ => intros_fresh var_name
    end).

(** [exists_fresh_gen G y Fry] picks a variable [y] fresh from
    the current context. [Fry] is the name of the freshness
    hypothesis, and [G] is the local tactic [gather_vars]. *)

Ltac exists_fresh_gen G y Fry :=
  let L := G in exists L; intros y Fry.


(* ********************************************************************** *)
(** * Applying lemma modulo a simple rewriting *)

(** [do_rew] is used to perform the sequence: 
  rewrite the goal, execute a tactic, rewrite the goal back *)

Tactic Notation "do_rew" constr(E) tactic(T) :=
  rewrite <- E; T; try rewrite E.

Tactic Notation "do_rew" "<-" constr(E) tactic(T) :=
  rewrite E; T; try rewrite <-  E.

Tactic Notation "do_rew" "*" constr(E) tactic(T) :=
  rewrite <- E; T; auto*; try rewrite* E.
Tactic Notation "do_rew" "*" "<-" constr(E) tactic(T) :=
 rewrite E; T; auto*; try rewrite* <- E.

(** [do_rew_2] is the same as [do_rew] but it does rewrite twice *)

Tactic Notation "do_rew_2" constr(E) tactic(T) :=
  do 2 rewrite <- E; T; try do 2 rewrite E.

Tactic Notation "do_rew_2" "<-" constr(E) tactic(T) :=
  do 2 rewrite E; T; try do 2 rewrite <- E.

(** [do_rew_all] is the same as [do_rew] but it does rewrite twice *)

Tactic Notation "do_rew_all" constr(E) tactic(T) :=
  rewrite_all <- E; T; try rewrite_all E.

Tactic Notation "do_rew_all" "<-" constr(E) tactic(T) :=
  rewrite_all E; T; try rewrite_all <- E.


(*--todo: rest deprecated ?*)

(* ********************************************************************** *)
(** * Some results on lists *)

Lemma list_map_id : forall (A : Set) l,
  List.map (fun t : A => t) l = l.
Proof.
  induction l; simpl; f_equal*.
Qed.

Lemma list_concat_right : forall (A : Set) (x : A) l1 l2,
  l1 ++ (x :: l2) = (l1 ++ (x :: nil)) ++ l2.
Proof.
  intros. induction l1; simpl; f_equal*.
Qed.

Lemma list_map_nth : forall (A : Set) (f : A -> A) d l n,
  f d = d -> 
  f (List.nth n l d) = List.nth n (List.map f l) d.
Proof.
  induction l; simpl; introv Fix; destruct* n.
Qed.


(* ********************************************************************** *)
(** * Property over lists *)

Inductive list_forall (A : Set) (P : A -> Prop) : list A -> Prop :=
  | list_forall_nil : list_forall P nil
  | list_forall_cons : forall L x,
       list_forall P L -> P x -> list_forall P (x::L).

Hint Constructors list_forall.

Lemma list_forall_concat : forall (A : Set) (P : A -> Prop) L1 L2,
  list_forall P L1 -> 
  list_forall P L2 ->
  list_forall P (L1 ++ L2).
Proof.
  induction L1; simpl; intros. auto. inversions* H.
Qed.


(* ********************************************************************** *)
(** * Property over lists of given length *)

Definition list_for_n (A : Set) (P : A -> Prop) (n : nat) (L : list A) :=
  n = length L /\ list_forall P L.

Lemma list_for_n_concat : forall (A : Set) (P : A -> Prop) n1 n2 L1 L2,
  list_for_n P n1 L1 -> 
  list_for_n P n2 L2 ->
  list_for_n P (n1+n2) (L1 ++ L2).
Proof.
  unfold list_for_n. intros. split. 
  rewrite* app_length. apply* list_forall_concat.
Qed.

Hint Extern 1 (?n = length ?xs) => 
 match goal with H: list_for_n _ ?n ?xs |- _ => 
  apply (proj1 H) end.

Hint Extern 1 (length ?xs = ?n) => 
 match goal with H: list_for_n _ ?n ?xs |- _ => 
  apply (sym_eq (proj1 H)) end.


(* ********************************************************************** *)
(** * Tactic for instantiating cofinitely quantified hypotheses *)

(** [inst_notin H y as H'] expects [H] to be of the form
  [forall x, x \notin L, P x] and creates an hypothesis [H']
  of type [P y]. It tries to prove the subgoal [y \notin L]
  by [auto]. This tactic is very useful to apply induction
  hypotheses given in the cases with binders. *)

Tactic Notation "inst_notin" constr(lemma) constr(var)
                "as" ident(hyp_name) :=
  let go L := let Fr := fresh in assert (Fr : var \notin L);
     [ notin_solve | lets hyp_name: (@lemma var Fr); clear Fr ] in
  match type of lemma with
    forall _, _ \notin ?L -> _ => go L end.

Tactic Notation "inst_notin" "~" constr(lemma) constr(var)
                "as" ident(hyp_name) :=
  inst_notin lemma var as hyp_name; auto_tilde.

Tactic Notation "inst_notin" "*" constr(lemma) constr(var)
                "as" ident(hyp_name) :=
  inst_notin lemma var as hyp_name; auto_star.

(* --todo: deviendra inutile avec le apply_in généralisé *)