LibLNgen.v

(* This file is distributed under the terms of the MIT License, also
   known as the X11 Licence.  A copy of this license is in the README
   file that accompanied the original distribution of this file.

   Based on code written by:
     Brian Aydemir *)

(** A library of code for supporting LNgen. *)

Require Export Metalib.LibDefaultSimp.
Require Import Metalib.Metatheory.
Require Import Lia.

(* Suppress warnings about Hint Resolve *)
Local Set Warnings "-fragile-hint-constr".


(* ********************************************************************** *)
(** * Assorted functions not in the standard library *)

(** [lt_ge_dec] is a useful comparison operation when defining the
    "close" operation on locally nameless terms. *)

Definition lt_ge_dec (n m : nat) : {n < m} + {n >= m} :=
  match Compare_dec.le_gt_dec m n with
    | left pf => right pf
    | right pf => left pf
  end.


(* *********************************************************************** *)
(** * Tactics *)

(** [generalize_wrt x] is an ad hoc tactic that generalizes the goal
    with respect to everything that [x] does not depend on.  It seems
    to work only if [x] is the most recently introduced item into the
    context. *)

Ltac generalize_wrt x :=
  repeat (progress (match goal with
    | J : _ |- _ => move J after x; generalize dependent J
    end)).

(** [apply_mutual_ind] applies to the current goal a mutual induction
    principle that is stated in the form generated by [Combined
    Scheme].  It works even in degenerate cases, i.e., when there is
    no mutual induction, only simple induction.  It is intended to be
    used only at the start of a proof, and the argument(s) to induct
    over should come first. *)

Ltac apply_mutual_ind ind :=
  match goal with
     [ |- (and _ _) ]  => apply ind
   | [ |- (prod _ _) ]  => apply ind
   | _ =>
     let H := fresh in
     first [ (* apply ind
        | *) intros H; induction H using ind
        | intros ? H; induction H using ind
        | intros ? ? H; induction H using ind
        | intros ? ? ? H; induction H using ind
        | intros ? ? ? ? H; induction H using ind
        | intros ? ? ? ? ? H; induction H using ind
        | intros ? ? ? ? ? ? H; induction H using ind
        | intros ? ? ? ? ? ? ? H; induction H using ind
        | intros ? ? ? ? ? ? ? ? H; induction H using ind
        ]
     end.

(** Renames the last hypothesis to the given identifier. *)

Ltac rename_last_into H :=
  match goal with
    | J : _ |- _ => rename J into H
  end.

(** Specializes every possible hypothesis with the given term. *)

Ltac specialize_all x :=
  repeat (match goal with
            | H : _ |- _ => specialize (H x)
          end).

(** Specialize and dispatch freshness hypothesis. *)
Ltac spec y := 
  repeat (match goal with [H0 : forall x : atom, x \notin ?L -> _ |- _ ] => 
     specialize (H0 y ltac:(auto)) end). 

(* Destruct all hypotheses with conjunctions *)
Ltac split_hyp :=
  repeat (
      match goal with
        | [ H : _ /\ _ |- _ ] => destruct H
      end).

Ltac invert_equality := 
  repeat match goal with 
    | [H : (_,_) = (_,_) |- _ ] => inversion H; subst; clear H
    | [H : (_,_,_) = (_,_,_) |- _ ] => inversion H; subst; clear H
    | [H : (_,_,_,_) = (_,_,_,_) |- _ ] => inversion H; subst; clear H
    | [H : [_] ++ _ = [_] ++ _ |- _ ] => inversion H; subst; clear H
    | [H : ( _ :: _ ) = ( _ :: _ )  |- _ ] => inversion H; subst; clear H
  end.



(* *********************************************************************** *)
(** * Facts about finite sets *)

Lemma remove_union_distrib : forall (s1 s2 : atoms) (x : atom),
  remove x (union s1 s2) [=] union (remove x s1) (remove x s2).
Proof. fsetdec. Qed.

Lemma Equal_union_compat : forall (s1 s2 s3 s4 : atoms),
  s1 [=] s3 ->
  s2 [=] s4 ->
  union s1 s2 [=] union s3 s4.
Proof. fsetdec. Qed.

Lemma Subset_refl : forall (s : atoms),
  s [<=] s.
Proof. fsetdec. Qed.

Lemma Subset_empty_any : forall (s : atoms),
  empty [<=] s.
Proof. fsetdec. Qed.

Lemma Subset_union_compat : forall (s1 s2 s3 s4 : atoms),
  s1 [<=] s3 ->
  s2 [<=] s4 ->
  union s1 s2 [<=] union s3 s4.
Proof. fsetdec. Qed.

Lemma Subset_union_left : forall (s1 s2 s3 : atoms),
  s1 [<=] s2 ->
  s1 [<=] union s2 s3.
Proof. fsetdec. Qed.

Lemma Subset_union_right : forall (s1 s2 s3 : atoms),
  s1 [<=] s3 ->
  s1 [<=] union s2 s3.
Proof. fsetdec. Qed.

Lemma Subset_union_lngen_open_upper :
  forall (s1 s2 s3 s4 s5 : atoms),
  s1 [<=] union s3 s4 ->
  s2 [<=] union s3 s5 ->
  union s1 s2 [<=] union s3 (union s4 s5).
Proof. fsetdec. Qed.


(* *********************************************************************** *)
(** * Hints *)

#[global]
Hint Resolve sym_eq : brute_force.

#[global]
Hint Extern 5 (_ = _ :> nat) => lia : brute_force.
#[global]
Hint Extern 5 (_ < _)        => lia : brute_force.
#[global]
Hint Extern 5 (_ <= _)       => lia : brute_force.

#[global]
Hint Rewrite @remove_union_distrib : lngen.
#[global]
Hint Resolve @Equal_union_compat : lngen.
#[global]
Hint Resolve @Subset_refl : lngen.
#[global]
Hint Resolve @Subset_empty_any : lngen.
#[global]
Hint Resolve @Subset_union_compat : lngen.
#[global]
Hint Resolve @Subset_union_left : lngen.
#[global]
Hint Resolve @Subset_union_right : lngen.
#[global]
Hint Resolve @Subset_union_lngen_open_upper : lngen.