diff options
| -rw-r--r-- | Nominal/Instances.lean | 19 | ||||
| -rw-r--r-- | Nominal/Support.lean | 49 |
2 files changed, 66 insertions, 2 deletions
diff --git a/Nominal/Instances.lean b/Nominal/Instances.lean index dcf079f..215f3f9 100644 --- a/Nominal/Instances.lean +++ b/Nominal/Instances.lean @@ -25,7 +25,7 @@ instance : NominalSet ๐ธ ๐ธ where intro a; use {a} exact โจNominalSet.supp_atom' ๐ธ, Set.finite_singleton aโฉ -lemma NominalSet.supp_atom {a : ๐ธ} : supp ๐ธ a = {a} := by +@[simp] lemma NominalSet.supp_atom {a : ๐ธ} : supp ๐ธ a = {a} := by ext b; constructor ยท apply support_subset_supp ๐ธ ยท exact NominalSet.supp_atom' ๐ธ @@ -46,6 +46,9 @@ lemma NominalSet.supp_atom {a : ๐ธ} : supp ๐ธ a = {a} := by rw [hโ] at hโ exact hc.left hโ +@[simp] lemma NominalSet.fresh_atom {a b : ๐ธ} : a # b โ a โ b := by + simp [IsFresh] + end Atoms /-! @@ -66,13 +69,16 @@ def NominalSet.discrete (X : Type) : DiscreteNominalSet ๐ธ X where ยท intro ฯ hฯ; simp [PermSet.fix']; rfl ยท exact Set.finite_empty -lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet ๐ธ X] {x : X} : supp ๐ธ x = โ
:= by +@[simp] lemma NominalSet.supp_discrete {X : Type} [DiscreteNominalSet ๐ธ X] {x : X} : supp ๐ธ x = โ
:= by rw [โ Set.subset_empty_iff] apply Set.sInter_subset_of_mem constructor ยท intro ฯ hฯ; simp [PermSet.fix', DiscreteNominalSet.is_discrete] ยท exact Set.finite_empty +@[simp] lemma NominalSet.fresh_discrete {X : Type} [DiscreteNominalSet ๐ธ X] {a : ๐ธ} {x : X} : a # x := by + simp [IsFresh] + /-- We consider Unit a discrete nominal set. -/ instance : DiscreteNominalSet ๐ธ Unit := NominalSet.discrete ๐ธ Unit @@ -121,6 +127,9 @@ instance : NominalSet ๐ธ (X ร Y) where suffices ฯ โ PermSet.fix' ๐ธ (x, y) by simp [PermSet.fix'] at this; exact this.right exact (hS.out.left hฯ).out +@[simp] lemma NominalSet.fresh_product {a : ๐ธ} {x : X} {y : Y} : a # (x, y) โ a # x โง a # y := by + simp [IsFresh] + lemma NominalSet.supp_product_comm {x : X} {y : Y} : supp ๐ธ (x, y) = supp ๐ธ (y, x) := by simp; apply Set.union_comm @@ -176,4 +185,10 @@ instance : NominalSet ๐ธ (X โ Y) where suffices ฯ โ PermSet.fix' ๐ธ (.inr y : X โ Y) by simp [PermSet.fix'] at this; exact this exact (hS.out.left hฯ).out +@[simp] lemma NominalSet.fresh_coproductโ {a : ๐ธ} {x : X} : a # (.inl x : X โ Y) โ a # x := by + simp [IsFresh] + +@[simp] lemma NominalSet.fresh_coproductโ {a : ๐ธ} {y : Y} : a # (.inr y : X โ Y) โ a # y := by + simp [IsFresh] + end Coproducts 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 |