diff options
| author | Hannes Schulze <haschu0103@outlook.de> | 2025-10-23 09:47:09 +0200 |
|---|---|---|
| committer | Hannes Schulze <haschu0103@outlook.de> | 2025-10-23 09:47:09 +0200 |
| commit | 7a4e25ebbc9e470650851299659860b4c07bff6b (patch) | |
| tree | f5d3aaca53e0b7053e5bfefb005739d3908e1c26 /Nominal/Support.lean | |
| parent | 281326b9b7eb6561526f02ff37eab9c39aa83b58 (diff) | |
add freshness
Diffstat (limited to 'Nominal/Support.lean')
| -rw-r--r-- | Nominal/Support.lean | 49 |
1 files changed, 49 insertions, 0 deletions
diff --git a/Nominal/Support.lean b/Nominal/Support.lean index 78e8b3e..f2bf90d 100644 --- a/Nominal/Support.lean +++ b/Nominal/Support.lean @@ -245,3 +245,52 @@ lemma support_subset_supp {x : X} {S : Set ๐ธ} : PermSet.HasSupport ๐ธ x S โ end NominalSet end NominalSet + +section Freshness + +/-- A predicate quantifying a statement for "suitably fresh" atoms. + +We also write ะ a, P for for_fresh (fun a => P), using the cyrillic letter ะ. + +A proposition holds for "suitably fresh" atoms iff there are infinitely many such "suitably fresh" atoms to choose from. -/ +@[simp] def NominalSet.ForFresh {๐ธ : Type} [Infinite ๐ธ] [Countable ๐ธ] [DecidableEq ๐ธ] (P : ๐ธ โ Prop) : Prop := + {a : ๐ธ | P a}.Infinite + +macro "ะ" x:ident "," t:term : term => + `(NominalSet.ForFresh (fun $x => $t)) + +/-- We write a # x for a โ supp x. + +Note: Other conventions extend this meaning to x # y โ supp x โฉ supp y = โ
. We will restrict ourselves to x โ ๐ธ. -/ +def NominalSet.IsFresh {๐ธ : Type} [Infinite ๐ธ] [Countable ๐ธ] [DecidableEq ๐ธ] {X : Type} [NominalSet ๐ธ X] (a : ๐ธ) (x : X) : Prop := + a โ NominalSet.supp ๐ธ x + +infix:50 " # " => NominalSet.IsFresh + +namespace NominalSet + +variable {X : Type} [NominalSet ๐ธ X] + +/-- To show that an atom is fresh, it is enough to show that it doesn't occur in any finite support. -/ +lemma fresh_support {a : ๐ธ} {x : X} {S : Set ๐ธ} : PermSet.HasSupport ๐ธ x S โ S.Finite โ a โ S โ a # x := by + intro hsuppS hfinS ha + apply Set.notMem_subset + ยท exact support_subset_supp ๐ธ hsuppS hfinS + ยท exact ha + +/-- One can always pick a fresh atom. -/ +lemma fresh_exists {x : X} : โ (a : ๐ธ), a # x := by + unfold IsFresh; expose_names + have h_inf : Set.univ.Infinite := Set.infinite_univ_iff.mpr inst + have h_fin : (supp ๐ธ x).Finite := supp_finite ๐ธ + obtain โจa, โจ_, haโฉโฉ := Set.Infinite.exists_notMem_finite h_inf h_fin + use a + +/-- If a proposition holds for suitably fresh a, then one can always pick such an a. -/ +lemma for_fresh_exists {P : ๐ธ โ Prop} : (ะ a, P a) โ (โ a, P a) := by + simp; intro h + exact Set.Infinite.nonempty h + +end NominalSet + +end Freshness |