diff options
Diffstat (limited to 'Nominal')
| -rw-r--r-- | Nominal/Equivariance.lean | 16 | ||||
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 86 | ||||
| -rw-r--r-- | Nominal/Permutations.lean | 5 |
3 files changed, 99 insertions, 8 deletions
diff --git a/Nominal/Equivariance.lean b/Nominal/Equivariance.lean index 50cf7c2..57c6d11 100644 --- a/Nominal/Equivariance.lean +++ b/Nominal/Equivariance.lean @@ -161,6 +161,17 @@ lemma supp_eq_if_inj {x : X} {f : X → Y} : Equivariant 𝔸 f → Function.Inj end Equivariant +/-- If there is an equivariant surjection from a nominal set into an (FPerm 𝔸)-Set, then that set is nominal. -/ +def NominalSet.fromEquivariantSurjective {X Y : Type} [NominalSet 𝔸 X] [PermSet 𝔸 Y] (f : X → Y) (hequi : Equivariant 𝔸 f) (hsurj : Function.Surjective f) : NominalSet 𝔸 Y where + fin_supp := by + intro y + obtain ⟨x, hx⟩ := hsurj y + use (NominalSet.supp 𝔸 x) + constructor + · rw [← hx] + exact Equivariant.preserve_support 𝔸 hequi (supp_is_support 𝔸) + · exact supp_finite 𝔸 + /-- supp is an equivariant function. -/ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸) := by intro x π; ext a; constructor @@ -182,6 +193,11 @@ lemma NominalSet.supp_equivariant : Equivariant 𝔸 (supp 𝔸 : X → Set 𝔸 · apply Set.Finite.smul_set exact hS.out.right +/-- Freshness is an equivariant relation. -/ +lemma NominalSet.fresh_equivariant : EquivariantRelation 𝔸 (NominalSet.IsFresh : 𝔸 → X → Prop) := by + intro x y π h + rwa [IsFresh, supp_equivariant, Set.smul_mem_smul_set_iff] + end Nominal /-! diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index d7fade9..508167e 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -22,15 +22,15 @@ This structure, along with the obvious permutation action, forms a nominal set w -/ section RawStructure -variable (X : Type) [NominalSet 𝔸 X] - /-- The structure forming a name abstraction. -/ -structure NameAbstraction' where +structure NameAbstraction' (𝔸 : Type) [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] (X : Type) [NominalSet 𝔸 X] where /-- The atom that is abstracted away. -/ atom : 𝔸 /-- The body from which the atom is abstracted. -/ body : X +variable (X : Type) [NominalSet 𝔸 X] + attribute [ext] NameAbstraction' namespace NameAbstraction' @@ -38,7 +38,7 @@ namespace NameAbstraction' instance : SMul (FPerm 𝔸) (NameAbstraction' 𝔸 X) where smul π x := .mk (π • x.atom) (π • x.body) -@[simp] lemma smul_atom (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).atom = π x.atom := rfl +@[simp] lemma smul_atom (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).atom = π • x.atom := rfl @[simp] lemma smul_body (π : FPerm 𝔸) (x : NameAbstraction' 𝔸 X) : (π • x).body = π • x.body := rfl @@ -46,10 +46,32 @@ instance : PermSet 𝔸 (NameAbstraction' 𝔸 X) where one_smul := by intro _; ext <;> simp [one_smul] mul_smul := by intro _ _ _; ext <;> simp [mul_smul] -instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) where - fin_supp := sorry +private def ofPair (x : (𝔸 × X)) : NameAbstraction' 𝔸 X := ⟨x.fst, x.snd⟩ + +private lemma ofPair_injective : Function.Injective (ofPair 𝔸 X) := by + intro x y hxy + simp only [ofPair, mk.injEq] at hxy + ext + · exact hxy.left + · exact hxy.right -@[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by sorry +private lemma ofPair_surjective : Function.Surjective (ofPair 𝔸 X) := by + intro x + use ⟨x.atom, x.body⟩ + simp [ofPair] + +private lemma ofPair_equivariant : Equivariant 𝔸 (ofPair 𝔸 X) := by + intro x π + ext <;> simp [ofPair] + +instance : NominalSet 𝔸 (NameAbstraction' 𝔸 X) := + NominalSet.fromEquivariantSurjective 𝔸 (ofPair 𝔸 X) (ofPair_equivariant 𝔸 X) (ofPair_surjective 𝔸 X) + +@[simp] lemma supp {x : NameAbstraction' 𝔸 X} : NominalSet.supp 𝔸 x = NominalSet.supp 𝔸 x.body ∪ {x.atom} := by + have h : NominalSet.supp 𝔸 (ofPair 𝔸 X (x.atom, x.body)) = NominalSet.supp 𝔸 (x.atom, x.body) := + Equivariant.supp_eq_if_inj 𝔸 (ofPair_equivariant 𝔸 X) (ofPair_injective 𝔸 X) + simp only [Prod.supp, NominalSet.supp_atom, ofPair] at h + rwa [Set.union_comm] at h @[simp] lemma fresh {a : 𝔸} {x : NameAbstraction' 𝔸 X} : a # x ↔ a ≠ x.atom ∧ a # x.body := by simp [NominalSet.IsFresh] @@ -91,6 +113,7 @@ private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred simp only [smul_smul, FPerm.mul_swap_eq_swap_mul] at h' simpa [smul_smul] +/-- The freshness quantifier in the definition is equivalent to "there exists some c # (x, y)". -/ lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by suffices (∃ c, c # x ∧ c # y ∧ ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∃ c, c # (x, y) ∧ AlphaEqPred c (x, y)) by rw [alpha_eq_iff_pred, this] @@ -98,6 +121,7 @@ lemma alpha_eq_iff_exists {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∃ exact alpha_eq_pred_equivariant simp [Prod.fresh, AlphaEqPred, @and_assoc] +/-- The freshness quantifier in the definition is equivalent to "for all c # (x, y)". -/ lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body := by suffices (∀ c, c # x ∧ c # y → ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body) = (∀ c, c # (x, y) → AlphaEqPred c (x, y)) by rw [alpha_eq_iff_pred, this] @@ -105,7 +129,53 @@ lemma alpha_eq_iff_all {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ ∀ c, exact alpha_eq_pred_equivariant simp [Prod.fresh, AlphaEqPred] -lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.atom = y.atom ∧ x.body = y.body) ∨ (x.atom ≠ y.atom ∧ x.atom # y ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by sorry +/-- An alternative definition of α-equivalence: + +For ⟪a⟫ x = ⟪b⟫ y, we either have (a, x) = (b, y) or x is just (a b) y, requiring that a is not in the support of y. -/ +lemma alpha_eq_iff_cases {x y : NameAbstraction' 𝔸 X} : AlphaEq x y ↔ (x.atom = y.atom ∧ x.body = y.body) ∨ (x.atom ≠ y.atom ∧ x.atom # y.body ∧ x.body = ⸨x.atom, y.atom⸩ • y.body) := by + by_cases h_eq : x.atom = y.atom + · constructor + · sorry + · sorry + · constructor + · rw [alpha_eq_iff_exists] + intro h; right + obtain ⟨c, ⟨hcx, ⟨hcy, hc⟩⟩⟩ := h + constructor + · exact h_eq + · simp at hcx + simp at hcy + have h_atom : (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • c # (⸨c, y.atom⸩ * ⸨c, x.atom⸩) • x.body := + NominalSet.fresh_equivariant 𝔸 _ _ _ hcx.right + -- TODO: Refactor into lemma + have h_swap : ⸨c, x.atom⸩ * ⸨c, y.atom⸩ = ⸨x.atom, y.atom⸩ * ⸨c, x.atom⸩ := by + ext a + simp [FPerm.swap] + by_cases h₁ : (a = c) <;> by_cases h₂ : (a = x.atom) <;> by_cases h₃ : (a = y.atom) + · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)] + · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)] + · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)] + · simp [h₁, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)] + · simp [h₂, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq, Equiv.swap_apply_of_ne_of_ne hcx.left hcy.left] + · simp [h₂, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq, Equiv.swap_apply_of_ne_of_ne hcx.left hcy.left] + · simp [h₃, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcy.left) (Ne.symm h_eq)] + · simp [Equiv.swap_apply_of_ne_of_ne h₁ h₃, Equiv.swap_apply_of_ne_of_ne h₁ h₂, Equiv.swap_apply_of_ne_of_ne h₂ h₃] + rw [mul_smul, PermSet.atom_swap, PermSet.atom_swap, Equiv.swap_apply_left, Equiv.swap_apply_of_ne_of_ne (Ne.symm hcx.left) h_eq] at h_atom + rw [mul_smul, hc, ← mul_smul, FPerm.swap_mul_self, one_smul] at h_atom + constructor + · exact h_atom + · calc + x.body = ⸨c, x.atom⸩ • ⸨c, x.atom⸩ • x.body := by rw [← mul_smul, FPerm.swap_mul_self, one_smul] + _ = (⸨c, x.atom⸩ * ⸨c, y.atom⸩) • y.body := by rw [mul_smul, hc] + _ = ⸨x.atom, y.atom⸩ • ⸨c, x.atom⸩ • y.body := by rw [← mul_smul, h_swap] + _ = ⸨x.atom, y.atom⸩ • y.body := by rw [NominalSet.fresh_swap_fix 𝔸 hcy.right h_atom] + · rw [alpha_eq_iff_all] + intro h c ⟨hcx, hcy⟩ + simp at hcy + simp only [h_eq, false_and, ne_eq, not_false_eq_true, true_and, false_or] at h + -- TODO: Use new lemma from before + have h_swap : ⸨c, x.atom⸩ * ⸨x.atom, y.atom⸩ = ⸨c, y.atom⸩ * ⸨c, x.atom⸩ := sorry + rw [h.right, ← mul_smul, h_swap, mul_smul, NominalSet.fresh_swap_fix 𝔸 hcy.right h.left] private lemma alpha_eq_refl (x : NameAbstraction' 𝔸 X) : AlphaEq x x := by sorry diff --git a/Nominal/Permutations.lean b/Nominal/Permutations.lean index b8d510e..62d7470 100644 --- a/Nominal/Permutations.lean +++ b/Nominal/Permutations.lean @@ -133,6 +133,11 @@ lemma mul_swap_eq_swap_mul {π : FPerm X} {a b : X} : π * ⸨a, b⸩ = ⸨π a, apply ext apply Equiv.mul_swap_eq_swap_mul +/-- Lifting of Equiv.swap_mul_self to finite permutations. -/ +lemma swap_mul_self {a b : X} : ⸨a, b⸩ * ⸨a, b⸩ = 1 := by + apply ext + simp [swap] + /-- If c is not equal to a or b, then (a b) leaves c unchanged. -/ lemma swap_neq {a b c : X} : c ≠ a → c ≠ b → ⸨a, b⸩ c = c := by intro ha hb |