From Tealeaves Require Export
  Classes.EqDec_eq
  Misc.NaturalNumbers.

From Tealeaves Require Import
  Theory.TraversableFunctor.

Import List.ListNotations.
Import ContainerFunctor.Notations.
Import Monoid.Notations.

(** * Transparent Atoms *)
(**********************************************************************)
Module Type AtomModule  <: UsualDecidableType.

  Parameter name: Type.

  Definition t := name.

  Parameter eq_dec: forall x y: name, {x = y} + {x <> y}.

  Parameter fresh: list name -> name.

  Parameter fresh_not_in: forall l, ~ fresh l ∈ l.

  Parameter freshen: list name -> name -> name.

  Parameter freshen_spec1: forall (l: list name) (n: name),
      ~ (n ∈ l) -> freshen l n = n.

  Parameter freshen_spec2: forall (l: list name) (n: name),
      ~ freshen l n ∈ l.

  Parameter nat_of: name -> nat.

  #[export] Hint Resolve eq_dec: core.

  Include HasUsualEq <+ UsualIsEq <+ UsualIsEqOrig.

End AtomModule.

(** * Transparent Atoms Implementation Support *)
(**********************************************************************)

(*
(* Test if x is an element of l, returning a boolean *)
Fixpoint list_in (x: nat) (l: list nat): bool :=
  match l with
  | nil => false
  | y :: rest => (x ==b y) || list_in x rest
  end.
 *)

(** ** Least Strict Upper Bound of a [list] *)
(**********************************************************************)
(** Return one greater than the greatest element in a list *)
Definition Smax (l: list nat): nat :=
  S (mapReduce (op := Monoid_op_max) (unit := Monoid_unit_max) id l).

(** <<Smax l>> is greater than every element *)
Lemma Smax_gt: forall l,
  forall (a: nat), a ∈ l -> a < Smax l.
forall (l : list nat) (a : nat), a ∈ l -> a < Smax l
Proof.
forall (l : list nat) (a : nat), a ∈ l -> a < Smax l
  intros.
l: list nat
a: nat
H: a ∈ l
a < Smax l
  induction l.
a: nat
H: a ∈ []
a < Smax []
a0: nat
l: list nat
a: nat
H: a ∈ (a0 :: l)
IHl: a ∈ l -> a < Smax l
a < Smax (a0 :: l)
  -
a: nat
H: a ∈ []
a < Smax [] inversion H.
  -
a0: nat
l: list nat
a: nat
H: a ∈ (a0 :: l)
IHl: a ∈ l -> a < Smax l
a < Smax (a0 :: l) rewrite element_of_list_cons in H.
a0: nat
l: list nat
a: nat
H: a = a0 \/ a ∈ l
IHl: a ∈ l -> a < Smax l
a < Smax (a0 :: l)
    unfold Smax.
a0: nat
l: list nat
a: nat
H: a = a0 \/ a ∈ l
IHl: a ∈ l -> a < Smax l
a < S (mapReduce id (a0 :: l))
    rewrite mapReduce_eq_mapReduce_list.
a0: nat
l: list nat
a: nat
H: a = a0 \/ a ∈ l
IHl: a ∈ l -> a < Smax l
a < S (mapReduce_list id (a0 :: l))
    rewrite mapReduce_list_cons.
a0: nat
l: list nat
a: nat
H: a = a0 \/ a ∈ l
IHl: a ∈ l -> a < Smax l
a < S (id a0 ● mapReduce_list id l)
    unfold transparent tcs.
a0: nat
l: list nat
a: nat
H: a = a0 \/ a ∈ l
IHl: a ∈ l -> a < Smax l
a < S (Nat.max (id a0) (mapReduce_list id l))
    rewrite <- mapReduce_eq_mapReduce_list.
a0: nat
l: list nat
a: nat
H: a = a0 \/ a ∈ l
IHl: a ∈ l -> a < Smax l
a < S (Nat.max (id a0) (mapReduce id l))
    unfold id.
a0: nat
l: list nat
a: nat
H: a = a0 \/ a ∈ l
IHl: a ∈ l -> a < Smax l
a < S (Nat.max a0 (mapReduce (fun x : nat => x) l))
    destruct H as [Case1 | Case2].
a0: nat
l: list nat
a: nat
Case1: a = a0
IHl: a ∈ l -> a < Smax l
a < S (Nat.max a0 (mapReduce (fun x : nat => x) l))
a0: nat
l: list nat
a: nat
Case2: a ∈ l
IHl: a ∈ l -> a < Smax l
a < S (Nat.max a0 (mapReduce (fun x : nat => x) l))
    +
a0: nat
l: list nat
a: nat
Case1: a = a0
IHl: a ∈ l -> a < Smax l
a < S (Nat.max a0 (mapReduce (fun x : nat => x) l)) subst.
a0: nat
l: list nat
IHl: a0 ∈ l -> a0 < Smax l
a0 < S (Nat.max a0 (mapReduce (fun x : nat => x) l))
      lia.
    +
a0: nat
l: list nat
a: nat
Case2: a ∈ l
IHl: a ∈ l -> a < Smax l
a < S (Nat.max a0 (mapReduce (fun x : nat => x) l)) apply IHl in Case2.
a0: nat
l: list nat
a: nat
Case2: a < Smax l
IHl: a ∈ l -> a < Smax l
a < S (Nat.max a0 (mapReduce (fun x : nat => x) l))
      rewrite PeanoNat.Nat.succ_max_distr.
a0: nat
l: list nat
a: nat
Case2: a < Smax l
IHl: a ∈ l -> a < Smax l
a <
PeanoNat.Nat.max (S a0)
  (S (mapReduce (fun x : nat => x) l))
      change ((S (mapReduce (fun x: nat => x) l))) with (Smax l).
a0: nat
l: list nat
a: nat
Case2: a < Smax l
IHl: a ∈ l -> a < Smax l
a < PeanoNat.Nat.max (S a0) (Smax l)
      lia.
Qed.

(** <<Smax l>> is not the list *)
Lemma Smax_not_in: forall l,
    ~ Smax l ∈ l.
forall l : list nat, ~ Smax l ∈ l
Proof.
forall l : list nat, ~ Smax l ∈ l
  intros.
l: list nat
~ Smax l ∈ l
  intro contra.
l: list nat
contra: Smax l ∈ l
False
  apply Smax_gt in contra.
l: list nat
contra: Smax l < Smax l
False
  lia.
Qed.

(** ** Testing Membership in a [list] *)
(**********************************************************************)
Fixpoint nat_inb (x: nat) (l: list nat): bool :=
  match l with
  | nil => false
  | y :: rest => (if x == y then true else false) || nat_inb x rest
  end.

Definition nat_freshb (x: nat) (l: list nat): bool :=
  negb (nat_inb x l).

Lemma nat_inb_iff: forall x l,
    nat_inb x l = true <-> x ∈ l.
forall (x : nat) (l : list nat),
nat_inb x l = true <-> x ∈ l
Proof.
forall (x : nat) (l : list nat),
nat_inb x l = true <-> x ∈ l
  intros.
x: nat
l: list nat
nat_inb x l = true <-> x ∈ l induction l.
x: nat
nat_inb x [] = true <-> x ∈ []
x, a: nat
l: list nat
IHl: nat_inb x l = true <-> x ∈ l
nat_inb x (a :: l) = true <-> x ∈ (a :: l)
  -
x: nat
nat_inb x [] = true <-> x ∈ [] cbn.
x: nat
false = true <-> False intuition.
  -
x, a: nat
l: list nat
IHl: nat_inb x l = true <-> x ∈ l
nat_inb x (a :: l) = true <-> x ∈ (a :: l) cbn.
x, a: nat
l: list nat
IHl: nat_inb x l = true <-> x ∈ l
((if x == a then true else false) || nat_inb x l)%bool =
true <-> a = x \/ List.In x l
    rewrite <- IHl.
x, a: nat
l: list nat
IHl: nat_inb x l = true <-> x ∈ l
((if x == a then true else false) || nat_inb x l)%bool =
true <-> a = x \/ nat_inb x l = true
    clear IHl.
x, a: nat
l: list nat
((if x == a then true else false) || nat_inb x l)%bool =
true <-> a = x \/ nat_inb x l = true
    destruct (nat_inb x l).
x, a: nat
l: list nat
((if x == a then true else false) || true)%bool = true <->
a = x \/ true = true
x, a: nat
l: list nat
((if x == a then true else false) || false)%bool =
true <-> a = x \/ false = true
    +
x, a: nat
l: list nat
((if x == a then true else false) || true)%bool = true <->
a = x \/ true = true rewrite Bool.orb_true_r.
x, a: nat
l: list nat
true = true <-> a = x \/ true = true intuition.
    +
x, a: nat
l: list nat
((if x == a then true else false) || false)%bool =
true <-> a = x \/ false = true  rewrite Bool.orb_false_r.
x, a: nat
l: list nat
(if x == a then true else false) = true <->
a = x \/ false = true
       destruct_eq_args x a; intuition.
Qed.

Corollary nat_inb_iff_false: forall x l,
    nat_inb x l = false <-> ~ (x ∈ l).
forall (x : nat) (l : list nat),
nat_inb x l = false <-> ~ x ∈ l
Proof.
forall (x : nat) (l : list nat),
nat_inb x l = false <-> ~ x ∈ l
  intros.
x: nat
l: list nat
nat_inb x l = false <-> ~ x ∈ l
  rewrite <- nat_inb_iff.
x: nat
l: list nat
nat_inb x l = false <-> nat_inb x l <> true
  destruct (nat_inb x l);
    intuition.
Qed.

Corollary nat_freshb_iff: forall x l,
    nat_freshb x l = true <-> ~ (x ∈ l).
forall (x : nat) (l : list nat),
nat_freshb x l = true <-> ~ x ∈ l
Proof.
forall (x : nat) (l : list nat),
nat_freshb x l = true <-> ~ x ∈ l
  intros.
x: nat
l: list nat
nat_freshb x l = true <-> ~ x ∈ l
  unfold nat_freshb.
x: nat
l: list nat
negb (nat_inb x l) = true <-> ~ x ∈ l
  remember (nat_inb x l).
x: nat
l: list nat
b: bool
Heqb: b = nat_inb x l
negb b = true <-> ~ x ∈ l
  symmetry in Heqb.
x: nat
l: list nat
b: bool
Heqb: nat_inb x l = b
negb b = true <-> ~ x ∈ l
  destruct b.
x: nat
l: list nat
Heqb: nat_inb x l = true
negb true = true <-> ~ x ∈ l
x: nat
l: list nat
Heqb: nat_inb x l = false
negb false = true <-> ~ x ∈ l
  -
x: nat
l: list nat
Heqb: nat_inb x l = true
negb true = true <-> ~ x ∈ l rewrite nat_inb_iff in Heqb.
x: nat
l: list nat
Heqb: x ∈ l
negb true = true <-> ~ x ∈ l
    intuition.
  -
x: nat
l: list nat
Heqb: nat_inb x l = false
negb false = true <-> ~ x ∈ l rewrite nat_inb_iff_false in Heqb.
x: nat
l: list nat
Heqb: ~ x ∈ l
negb false = true <-> ~ x ∈ l
    intuition.
Qed.

Corollary nat_freshb_false_iff: forall x l,
    nat_freshb x l = false <-> (x ∈ l).
forall (x : nat) (l : list nat),
nat_freshb x l = false <-> x ∈ l
Proof.
forall (x : nat) (l : list nat),
nat_freshb x l = false <-> x ∈ l
  intros.
x: nat
l: list nat
nat_freshb x l = false <-> x ∈ l
  unfold nat_freshb.
x: nat
l: list nat
negb (nat_inb x l) = false <-> x ∈ l
  remember (nat_inb x l).
x: nat
l: list nat
b: bool
Heqb: b = nat_inb x l
negb b = false <-> x ∈ l
  symmetry in Heqb.
x: nat
l: list nat
b: bool
Heqb: nat_inb x l = b
negb b = false <-> x ∈ l
  destruct b.
x: nat
l: list nat
Heqb: nat_inb x l = true
negb true = false <-> x ∈ l
x: nat
l: list nat
Heqb: nat_inb x l = false
negb false = false <-> x ∈ l
  -
x: nat
l: list nat
Heqb: nat_inb x l = true
negb true = false <-> x ∈ l rewrite nat_inb_iff in Heqb.
x: nat
l: list nat
Heqb: x ∈ l
negb true = false <-> x ∈ l
    intuition.
  -
x: nat
l: list nat
Heqb: nat_inb x l = false
negb false = false <-> x ∈ l rewrite nat_inb_iff_false in Heqb.
x: nat
l: list nat
Heqb: ~ x ∈ l
negb false = false <-> x ∈ l
    intuition.
Qed.

(** ** Computing Maximum Element Not in [list] *)
(**********************************************************************)

(* Compute the maximum element not in a list. Computed slightly funny to be structurally recursive.
   We start with an element known not to be in the list. Then we test all smaller numbers to see if they are elements,  and track the smallest value known not to form an element as <<candidate>>
   <<current min>> is the smallest value *)

Fixpoint min_fresh_rec
  (gas: nat) (candidate: nat)
  (l: list nat): nat :=
  match gas with
  | 0 => if nat_freshb 0 l
        then 0
        else candidate
  | S g =>
      if nat_freshb g l
      then min_fresh_rec g g l
      else min_fresh_rec g candidate l
  end.

Lemma min_fresh_rec_invariant: forall gas candidate l,
    ~ (candidate ∈ l) ->
    ~ min_fresh_rec gas candidate l ∈ l.
forall (gas candidate : nat) (l : list nat),
~ candidate ∈ l -> ~ min_fresh_rec gas candidate l ∈ l
Proof.
forall (gas candidate : nat) (l : list nat),
~ candidate ∈ l -> ~ min_fresh_rec gas candidate l ∈ l
  intros.
gas, candidate: nat
l: list nat
H: ~ candidate ∈ l
~ min_fresh_rec gas candidate l ∈ l
  generalize dependent candidate.
gas: nat
l: list nat
forall candidate : nat,
~ candidate ∈ l -> ~ min_fresh_rec gas candidate l ∈ l
  induction gas; intros.
l: list nat
candidate: nat
H: ~ candidate ∈ l
~ min_fresh_rec 0 candidate l ∈ l
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
~ min_fresh_rec (S gas) candidate l ∈ l
  -
l: list nat
candidate: nat
H: ~ candidate ∈ l
~ min_fresh_rec 0 candidate l ∈ l cbn.
l: list nat
candidate: nat
H: ~ candidate ∈ l
~ (if nat_freshb 0 l then 0 else candidate) ∈ l
    remember (nat_freshb 0 l).
l: list nat
candidate: nat
H: ~ candidate ∈ l
b: bool
Heqb: b = nat_freshb 0 l
~ (if b then 0 else candidate) ∈ l
    symmetry in Heqb.
l: list nat
candidate: nat
H: ~ candidate ∈ l
b: bool
Heqb: nat_freshb 0 l = b
~ (if b then 0 else candidate) ∈ l
    destruct b.
l: list nat
candidate: nat
H: ~ candidate ∈ l
Heqb: nat_freshb 0 l = true
~ 0 ∈ l
l: list nat
candidate: nat
H: ~ candidate ∈ l
Heqb: nat_freshb 0 l = false
~ candidate ∈ l
    +
l: list nat
candidate: nat
H: ~ candidate ∈ l
Heqb: nat_freshb 0 l = true
~ 0 ∈ l apply nat_freshb_iff in Heqb.
l: list nat
candidate: nat
H: ~ candidate ∈ l
Heqb: ~ 0 ∈ l
~ 0 ∈ l
      auto.
    +
l: list nat
candidate: nat
H: ~ candidate ∈ l
Heqb: nat_freshb 0 l = false
~ candidate ∈ l apply nat_freshb_false_iff in Heqb.
l: list nat
candidate: nat
H: ~ candidate ∈ l
Heqb: 0 ∈ l
~ candidate ∈ l
      assumption.
  -
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
~ min_fresh_rec (S gas) candidate l ∈ l cbn.
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
~
(if nat_freshb gas l
 then min_fresh_rec gas gas l
 else min_fresh_rec gas candidate l) ∈ l
    remember (nat_freshb gas l).
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
b: bool
Heqb: b = nat_freshb gas l
~
(if b
 then min_fresh_rec gas gas l
 else min_fresh_rec gas candidate l) ∈ l
    symmetry in Heqb.
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
b: bool
Heqb: nat_freshb gas l = b
~
(if b
 then min_fresh_rec gas gas l
 else min_fresh_rec gas candidate l) ∈ l
    destruct b.
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
Heqb: nat_freshb gas l = true
~ min_fresh_rec gas gas l ∈ l
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
Heqb: nat_freshb gas l = false
~ min_fresh_rec gas candidate l ∈ l
    +
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
Heqb: nat_freshb gas l = true
~ min_fresh_rec gas gas l ∈ l apply IHgas.
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
Heqb: nat_freshb gas l = true
~ gas ∈ l
      apply nat_freshb_iff in Heqb.
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
Heqb: ~ gas ∈ l
~ gas ∈ l
      assumption.
    +
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
Heqb: nat_freshb gas l = false
~ min_fresh_rec gas candidate l ∈ l apply IHgas.
gas: nat
l: list nat
IHgas: forall candidate : nat,
~ candidate ∈ l ->
~ min_fresh_rec gas candidate l ∈ l
candidate: nat
H: ~ candidate ∈ l
Heqb: nat_freshb gas l = false
~ candidate ∈ l
      assumption.
Qed.

Definition min_fresh (l: list nat): nat :=
  min_fresh_rec (Smax l) (Smax l) l.

Definition freshen (l: list nat) (n: nat): nat :=
  if nat_freshb n l then n
  else min_fresh l.

Lemma freshen_spec: forall (l: list nat) (n: nat),
    {~ n ∈ l /\ freshen l n = n} + {n ∈ l /\ freshen l n = min_fresh l}.
forall (l : list nat) (n : nat),
{~ n ∈ l /\ freshen l n = n} +
{n ∈ l /\ freshen l n = min_fresh l}
Proof.
forall (l : list nat) (n : nat),
{~ n ∈ l /\ freshen l n = n} +
{n ∈ l /\ freshen l n = min_fresh l}
  intros.
l: list nat
n: nat
{~ n ∈ l /\ freshen l n = n} +
{n ∈ l /\ freshen l n = min_fresh l}
  remember (nat_freshb n l).
l: list nat
n: nat
b: bool
Heqb: b = nat_freshb n l
{~ n ∈ l /\ freshen l n = n} +
{n ∈ l /\ freshen l n = min_fresh l}
  symmetry in Heqb.
l: list nat
n: nat
b: bool
Heqb: nat_freshb n l = b
{~ n ∈ l /\ freshen l n = n} +
{n ∈ l /\ freshen l n = min_fresh l}
  unfold freshen.
l: list nat
n: nat
b: bool
Heqb: nat_freshb n l = b
{~ n ∈ l /\
 (if nat_freshb n l then n else min_fresh l) = n} +
{n ∈ l /\
 (if nat_freshb n l then n else min_fresh l) =
 min_fresh l}
  rewrite Heqb.
l: list nat
n: nat
b: bool
Heqb: nat_freshb n l = b
{~ n ∈ l /\ (if b then n else min_fresh l) = n} +
{n ∈ l /\ (if b then n else min_fresh l) = min_fresh l}
  destruct b.
l: list nat
n: nat
Heqb: nat_freshb n l = true
{~ n ∈ l /\ n = n} + {n ∈ l /\ n = min_fresh l}
l: list nat
n: nat
Heqb: nat_freshb n l = false
{~ n ∈ l /\ min_fresh l = n} +
{n ∈ l /\ min_fresh l = min_fresh l}
  -
l: list nat
n: nat
Heqb: nat_freshb n l = true
{~ n ∈ l /\ n = n} + {n ∈ l /\ n = min_fresh l} left.
l: list nat
n: nat
Heqb: nat_freshb n l = true
~ n ∈ l /\ n = n
    apply nat_freshb_iff in Heqb; auto.
  -
l: list nat
n: nat
Heqb: nat_freshb n l = false
{~ n ∈ l /\ min_fresh l = n} +
{n ∈ l /\ min_fresh l = min_fresh l} right.
l: list nat
n: nat
Heqb: nat_freshb n l = false
n ∈ l /\ min_fresh l = min_fresh l
    apply nat_freshb_false_iff in Heqb; auto.
Qed.

Compute min_fresh_rec 100 5 [0; 1; 2].
= 3
: nat
Compute min_fresh_rec 100 5 [0; 1; 3; 4].
= 2
: nat
Compute min_fresh_rec 100 5 [1; 2; 4; 6; 8].
= 0
: nat
Compute min_fresh_rec 100 5 [0; 1; 2; 4; 6; 8].
= 3
: nat

Compute min_fresh [].
= 0
: nat
Compute min_fresh [0].
= 1
: nat
Compute min_fresh [0; 1].
= 2
: nat
Compute min_fresh [0; 2].
= 1
: nat

Compute freshen [0; 2] 2.
= 1
: nat

Compute freshen [0; 2] 4.
= 4
: nat

(** ** Transparent Atoms Implementation *)
(**********************************************************************)
Module Name <: AtomModule.

  Definition name: Type := nat.
  Definition t := name.

  Definition eq_dec := PeanoNat.Nat.eq_dec.

  Include HasUsualEq <+ UsualIsEq <+ UsualIsEqOrig.

  Definition fresh := min_fresh.

  Lemma fresh_not_in: forall l, ~ fresh l ∈ l.
forall l : list nat, ~ fresh l ∈ l
  Proof.
forall l : list nat, ~ fresh l ∈ l
    intro l.
l: list nat
~ fresh l ∈ l
    unfold fresh.
l: list nat
~ min_fresh l ∈ l
    apply min_fresh_rec_invariant.
l: list nat
~ Smax l ∈ l
    apply Smax_not_in.
  Qed.

  Definition freshen := freshen.

  Lemma freshen_spec1: forall (l: list name) (n: name),
      ~ (n ∈ l) -> freshen l n = n.
forall (l : list name) (n : name),
~ n ∈ l -> freshen l n = n
  Proof.
forall (l : list name) (n : name),
~ n ∈ l -> freshen l n = n
    intros.
l: list name
n: name
H: ~ n ∈ l
freshen l n = n
    destruct (freshen_spec l n).
l: list name
n: name
H: ~ n ∈ l
a: ~ n ∈ l /\ Names.freshen l n = n
freshen l n = n
l: list name
n: name
H: ~ n ∈ l
a: n ∈ l /\ Names.freshen l n = min_fresh l
freshen l n = n
    -
l: list name
n: name
H: ~ n ∈ l
a: ~ n ∈ l /\ Names.freshen l n = n
freshen l n = n intuition.
    -
l: list name
n: name
H: ~ n ∈ l
a: n ∈ l /\ Names.freshen l n = min_fresh l
freshen l n = n intuition.
  Qed.

  Lemma freshen_spec2: forall (l: list name) (n: name),
      ~ freshen l n ∈ l.
forall (l : list name) (n : name), ~ freshen l n ∈ l
  Proof.
forall (l : list name) (n : name), ~ freshen l n ∈ l
    intros.
l: list name
n: name
~ freshen l n ∈ l
    unfold freshen.
l: list name
n: name
~ Names.freshen l n ∈ l
    destruct (freshen_spec l n).
l: list name
n: name
a: ~ n ∈ l /\ Names.freshen l n = n
~ Names.freshen l n ∈ l
l: list name
n: name
a: n ∈ l /\ Names.freshen l n = min_fresh l
~ Names.freshen l n ∈ l
    -
l: list name
n: name
a: ~ n ∈ l /\ Names.freshen l n = n
~ Names.freshen l n ∈ l destruct a as [H1 H2].
l: list name
n: name
H1: ~ n ∈ l
H2: Names.freshen l n = n
~ Names.freshen l n ∈ l
      rewrite H2; auto.
    -
l: list name
n: name
a: n ∈ l /\ Names.freshen l n = min_fresh l
~ Names.freshen l n ∈ l destruct a as [H1 H2].
l: list name
n: name
H1: n ∈ l
H2: Names.freshen l n = min_fresh l
~ Names.freshen l n ∈ l
      rewrite H2.
l: list name
n: name
H1: n ∈ l
H2: Names.freshen l n = min_fresh l
~ min_fresh l ∈ l
      apply min_fresh_rec_invariant.
l: list name
n: name
H1: n ∈ l
H2: Names.freshen l n = min_fresh l
~ Smax l ∈ l
      apply Smax_not_in.
  Qed.

  Definition nat_of: name -> nat := fun x => x.

End Name.

(** ** Shorthands and notations *)
(**********************************************************************)
Notation name := Name.name.
Notation atom := Name.name.
Notation fresh := Name.fresh.
Notation fresh_not_in := Name.fresh_not_in.

(* Automatically unfold Name.eq *)
#[global] Arguments Name.eq /.

#[export] Instance EqDec_name: @EqDec name eq eq_equivalence := Name.eq_dec.