diff options
Diffstat (limited to 'Nominal/Instances/Abstraction.lean')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 98 |
1 files changed, 48 insertions, 50 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 269e80f..1fab31a 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -113,26 +113,21 @@ 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 +private 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] apply Equivariance.for_fresh_iff_exists 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 +private 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] apply Equivariance.for_fresh_iff_all exact alpha_eq_pred_equivariant simp [Prod.fresh, AlphaEqPred] -/-- 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 +private 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 constructor · rw [alpha_eq_iff_exists] intro h @@ -250,89 +245,90 @@ def mk {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : Ty Quotient.mk (setoid 𝔸 X).toSetoid (.mk a x) /-- We write `⟪a⟫ x` instead of the usual `⟨a⟩ x` because `⟨⟩` is already heavily used in Lean for constructors. -/ -notation "⟪" a "⟫ " t => mk a t +notation "⟪" a "⟫ " x:60 => mk a x instance : NominalSet 𝔸 (NameAbstraction 𝔸 X) := Quotient.instNominalSet 𝔸 @[simp] -lemma smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • (⟪a⟫ x) = ⟪π • a⟫ π • x := by congr +lemma smul {π : FPerm 𝔸} {a : 𝔸} {x : X } : π • ⟪a⟫ x = ⟪π • a⟫ π • x := by congr /-- Two name abstractions are equal iff they are alpha-equivalent. -/ -lemma eq_iff_alpha_eq {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ AlphaEq ⟨a, x⟩ ⟨b, y⟩ := by +lemma eq_iff_alpha_eq {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y ↔ AlphaEq ⟨a, x⟩ ⟨b, y⟩ := by rw [mk, mk, Quotient.eq_iff_equiv] rfl -/-- Lifting of alpha_eq_iff_exists to name abstractions. -/ -lemma eq_iff_exists {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ ∃ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y ∧ ⸨c, a⸩ • x = ⸨c, b⸩ • y := by +/-- The freshness quantifier in the AlphaEq definition is equivalent to "there exists some c # (x, y)". -/ +lemma eq_iff_exists {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y ↔ ∃ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y ∧ ⸨c, a⸩ • x = ⸨c, b⸩ • y := by simp only [eq_iff_alpha_eq, alpha_eq_iff_exists, NameAbstraction'.fresh, ne_eq] ac_nf -/-- Lifting of alpha_eq_iff_exists to name abstractions. -/ -lemma eq_iff_all {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ ∀ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y → ⸨c, a⸩ • x = ⸨c, b⸩ • y := by +/-- The freshness quantifier in the AlphaEq definition is equivalent to "for all c # (x, y)". -/ +lemma eq_iff_all {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y ↔ ∀ c, c ≠ a ∧ c ≠ b ∧ c # x ∧ c # y → ⸨c, a⸩ • x = ⸨c, b⸩ • y := by simp only [eq_iff_alpha_eq, alpha_eq_iff_all, NameAbstraction'.fresh, ne_eq] ac_nf -/-- Lifting of alpha_eq_iff_cases to name abstractions. -/ -lemma eq_iff_cases {a b : 𝔸} {x y : X} : (⟪a⟫ x) = (⟪b⟫ y) ↔ (a = b ∧ x = y) ∨ (a ≠ b ∧ a # y ∧ x = ⸨a, b⸩ • y) := by +/-- 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 eq_iff_cases {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y ↔ (a = b ∧ x = y) ∨ (a ≠ b ∧ a # y ∧ x = ⸨a, b⸩ • y) := by simp [eq_iff_alpha_eq, alpha_eq_iff_cases] +private lemma raw_supp_swap {a b : 𝔸} {x y : X} : ⟪a⟫ x = ⟪b⟫ y → NominalSet.supp 𝔸 (⟨b, y⟩ : NameAbstraction' 𝔸 X) = {b} ∪ (NominalSet.supp 𝔸 x \ {a}) := by + intro haeq + rw [eq_iff_cases] at haeq + cases haeq with + | inl h => + rw [h.left, h.right] + simp only [NameAbstraction'.supp, Set.union_singleton, Set.union_diff_self, Set.singleton_union] + | inr h => + simp only [NameAbstraction'.supp, Set.union_comm] + rw [h.right.right, NominalSet.supp_equivariant 𝔸 y ⸨a, b⸩] + ext c + by_cases h₁ : c = b + · simp [h₁] + · by_cases h₂ : c = a + · simp [h₂, show a ∉ NominalSet.supp 𝔸 y by exact h.right.left] + · simp [h₁, h₂, ← PermSet.atom_set_swap_ne_ne] + @[simp] lemma supp {a : 𝔸} {x : X} : NominalSet.supp 𝔸 (⟪a⟫ x) = NominalSet.supp 𝔸 x \ {a} := by - -- XXX: This is rather ugly... - have hswap : ∀ (b : 𝔸) (y : X), (⟪a⟫ x) = (⟪b⟫ y) → NominalSet.supp 𝔸 (⟨b, y⟩ : NameAbstraction' 𝔸 X) = {b} ∪ (NominalSet.supp 𝔸 x \ {a}) := by - intro b y heq - rw [eq_iff_cases] at heq - cases heq with - | inl h => - rw [h.left, h.right] - simp only [NameAbstraction'.supp, Set.union_singleton, Set.union_diff_self, Set.singleton_union] - | inr h => - simp only [NameAbstraction'.supp, Set.union_comm] - rw [h.right.right, NominalSet.supp_equivariant 𝔸 y ⸨a, b⸩] - ext c - by_cases h₁ : c = b - · simp [h₁] - · by_cases h₂ : c = a - · simp [h₂, show a ∉ NominalSet.supp 𝔸 y by exact h.right.left] - · simp [h₁, h₂, ← PermSet.atom_set_swap_ne_ne] rw [mk, Quotient.supp] ext b constructor · by_cases h_eq : a = b - · contrapose; intro h - subst h_eq + · -- The interesting case: Show that we don't need a in the support. + subst h_eq; contrapose; intro _ simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, Set.mem_setOf_eq, Classical.not_imp, not_forall, not_or] have hfin : (NominalSet.supp 𝔸 x).Finite := NominalSet.supp_finite 𝔸 obtain ⟨c, hc⟩ := Infinite.exists_notMem_finset (hfin.toFinset ∪ {a}) simp only [Finset.union_singleton, Finset.mem_insert, Set.Finite.mem_toFinset, not_or] at hc use ⟨c, ⸨a, c⸩ • x⟩ - have haeq : (⟪c⟫ ⸨a, c⸩ • x) = (⟪a⟫ x) := by + have haeq : ⟪c⟫ ⸨a, c⸩ • x = ⟪a⟫ x := by rw [eq_iff_cases] right exact ⟨hc.left, hc.right, by rw [FPerm.swap_comm]⟩ - constructor - · exact Quotient.exact haeq - · constructor - · exact Ne.symm hc.left - · suffices a ∉ NominalSet.supp 𝔸 (⟨c, ⸨a, c⸩ • x⟩ : NameAbstraction' 𝔸 X) by - simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, not_or] at this - exact this.right - rw [hswap c (⸨a, c⸩ • x) haeq.symm] - simp [Ne.symm hc.left] - · intro h + have hraw : a ∉ NominalSet.supp 𝔸 (⟨c, ⸨a, c⸩ • x⟩ : NameAbstraction' 𝔸 X) := by + rw [raw_supp_swap 𝔸 X haeq.symm] + simp [Ne.symm hc.left] + simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, not_or] at hraw + exact ⟨Quotient.exact haeq, Ne.symm hc.left, hraw.right⟩ + · -- For all other cases, it suffices that supp (⟪a⟫ x) ⊆ supp (a, x) ∪ {a}. + intro h specialize h ⟨a, x⟩ (by rfl) simp only [NameAbstraction'.supp, Set.union_singleton, Set.mem_insert_iff, Ne.symm h_eq, false_or] at h rw [Set.mem_diff_singleton] exact ⟨h, Ne.symm h_eq⟩ - · intro h x' hx' + · -- Show that this is actually the least support. + intro h x' hx' suffices NominalSet.supp 𝔸 x' = {x'.atom} ∪ NominalSet.supp 𝔸 x \ {a} by rw [this] exact Set.mem_union_right {x'.atom} h - apply hswap + apply raw_supp_swap apply Quotient.sound exact (Setoid.symm hx') -@[simp] lemma fresh {a b : 𝔸} {x : X} : b # (⟪a⟫ x) ↔ b # x ∨ b = a := by +@[simp] +lemma fresh {a b : 𝔸} {x : X} : b # ⟪a⟫ x ↔ b # x ∨ b = a := by simp only [NominalSet.IsFresh, supp, Set.mem_diff, Set.mem_singleton_iff, not_and_or, Decidable.not_not] end NameAbstraction @@ -346,4 +342,6 @@ Name abstraction can also be considered as a functor `Nom → Nom`. -/ section Functor + + end Functor |