Library TLC.LibVar

Set Implicit Arguments.
From TLC Require Import LibTactics LibList LibLogic LibNat LibEpsilon LibReflect.
From TLC 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 Inhab_var : Inhab var.

This type is comparable.

Parameter var_compare : var -> var -> bool.

Parameter var_compare_eq : forall (x y:var),
var_compare x y = isTrue (x = y).

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 Inhab_var : Inhab var.
Proof using. apply (Inhab_of_val 0). Qed.

Fixpoint var_compare (x y : nat) :=
  match x, y with
  | O, O => true
  | S x', S y' => var_compare x' y'
  | _, _ => false
  end.

Lemma var_compare_eq : forall (x y:var),
  var_compare x y = isTrue (x = y).
Proof using.
  unfold var. intros x; induction x; intros y; destruct y;
   simpl; rew_bool_eq; try nat_math.
  rewrite IHx. rew_bool_eq. nat_math.
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 using.
  unfold var_gen_list. induction l; introv I.
  rewrite from_list_nil in I. false (in_empty_inv I).
  rewrite from_list_cons in I. rew_listx.
   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 using.
  intros. unfold var_gen. epsilon l. applys fset_finite.
  intros Hl. 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 using. 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.

Lemma var_freshes : forall L n,
  { xs : list var | fresh L n xs }.
Proof using.
  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 using. intros. rewrite~ <- notin_singleton. Qed.

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

Lemma notin_singleton_swap : forall x y,
  x \notin \{y } -> y \notin \{x }.
Proof using.
  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 using. intros. rewrite~ <- notin_union. Qed.

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

Lemma notin_union_r2 : forall x E F,
  x \notin (E \u F ) -> (x \notin F ).
Proof using. 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 using. 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 using. intros. autos~ var_gen_spec. Qed.

Arguments notin_singleton_r [x] [y].
Arguments notin_singleton_l [x] [y].
Arguments notin_singleton_swap [x] [y].
Arguments notin_union_r [x] [E] [F].
Arguments notin_union_r1 [x] [E] [F].
Arguments notin_union_r2 [x] [E] [F].
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
  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
  | _ => intros_all; false; notin_solve_false
  end.

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

Ltac notin_solve :=
  notin_of_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.

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 using.
  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 using. 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 using. 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 using.
  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 using.
  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 using.
  intros. gen n L. induction xs; simpl; intros n L Fr;
    destruct n; tryfalse*.
  auto.
  rew_list. 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 using.
  introv Fr Eq. subst~.
Qed.

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

Arguments fresh_union_r [xs] [L1] [L2] [n].
Arguments fresh_union_r1 [xs] [L1] [L2] [n].
Arguments fresh_union_r2 [xs] [L1] [L2] [n].
Arguments fresh_union_l [xs] [L1] [L2] [n].
Arguments fresh_empty [L] [n] [xs].
Arguments fresh_length [L] [n] [xs].
Arguments fresh_resize [L] [n] [xs].
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 using.
  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.