From 236d6d9c0982505808d06d6beb637746af9bab02 Mon Sep 17 00:00:00 2001
From: Michael Sippel <micha@fragmental.art>
Date: Sun, 22 Sep 2024 15:52:06 +0200
Subject: [PATCH] add env_wf

---
 coq/typing/env.v | 32 ++++++++++++++++++++++++++++++++
 1 file changed, 32 insertions(+)

diff --git a/coq/typing/env.v b/coq/typing/env.v
index d4c0719..251fb16 100644
--- a/coq/typing/env.v
+++ b/coq/typing/env.v
@@ -1,5 +1,37 @@
+Require Import Metatheory.
 Require Import Atom.
 Require Import Environment.
 Require Import debruijn.
 
 Notation env := (list (atom * type_DeBruijn)).
+
+(* env is well-formed if each atom is bound at most once
+ * and every binding is to a locally closed type
+ *)
+Inductive env_wf : env -> Prop :=
+  | env_wf_empty :
+    env_wf []
+
+  | env_wf_type : forall Γ x τ,
+    env_wf Γ ->
+    type_lc τ ->
+    x `notin` (dom Γ) ->
+    env_wf ((x,τ)::Γ)
+.
+
+Ltac gather_atoms :=
+  let A := gather_atoms_with (fun x : atoms => x) in
+  let B := gather_atoms_with (fun x : atom => singleton x) in
+  let C := gather_atoms_with (fun x : list (atom * type_DeBruijn) => dom x) in
+  let D := gather_atoms_with (fun x : expr_DeBruijn => expr_fv x) in
+  constr:(A `union` B `union` C `union` D).
+
+
+Tactic Notation "pick" "fresh" ident(x) :=
+  let L := gather_atoms in
+  (pick fresh x for L).
+
+Tactic Notation
+      "pick" "fresh" ident(atom_name) "and" "apply" constr(lemma) :=
+  let L := gather_atoms in
+  pick fresh atom_name excluding L and apply lemma.