diff options
Diffstat (limited to 'Nominal/Instances')
| -rw-r--r-- | Nominal/Instances/Abstraction.lean | 39 |
1 files changed, 22 insertions, 17 deletions
diff --git a/Nominal/Instances/Abstraction.lean b/Nominal/Instances/Abstraction.lean index 85ce3ad..891f00f 100644 --- a/Nominal/Instances/Abstraction.lean +++ b/Nominal/Instances/Abstraction.lean @@ -36,14 +36,13 @@ attribute [ext] NameAbstraction' namespace NameAbstraction' instance : SMul (FPerm 𝔸) (NameAbstraction' 𝔸 X) where - smul π x := .mk (π x.atom) (π • x.body) + smul π x := .mk (π • x.atom) (π • x.body) @[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 instance : PermSet 𝔸 (NameAbstraction' 𝔸 X) where - smul π x := .mk (π x.atom) (π • x.body) one_smul := by intro _; ext <;> simp [one_smul] mul_smul := by intro _ _ _; ext <;> simp [mul_smul] @@ -74,31 +73,37 @@ variable {𝔸 : Type} [Infinite 𝔸] [Countable 𝔸] [DecidableEq 𝔸] {X : def AlphaEq (x y : NameAbstraction' 𝔸 X) : Prop := И c, ⸨c, x.atom⸩ • x.body = ⸨c, y.atom⸩ • y.body -/-- Alternatively define alpha equivalence as an equivariant relation. -/ -private def AlphaEq' (c : 𝔸) (xy : NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X) : Prop := +/-- Alternatively define alpha equivalence as an equivariant relation. + +This is used to show some properties using the Equivariance.for_fresh_* lemmas about the freshness quantifier. -/ +private def AlphaEqPred (c : 𝔸) (xy : NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X) : Prop := ⸨c, xy.fst.atom⸩ • xy.fst.body = ⸨c, xy.snd.atom⸩ • xy.snd.body -private lemma alpha_eq_iff {x y : NameAbstraction' 𝔸 X} : AlphaEq x y = (И c, AlphaEq' c (x, y)) := by +private lemma alpha_eq_iff_pred {x y : NameAbstraction' 𝔸 X} : AlphaEq x y = (И c, AlphaEqPred c (x, y)) := by apply NominalSet.for_fresh_ext - simp [AlphaEq'] + simp [AlphaEqPred] -private lemma alpha_eq_equivariant' : EquivariantRelation 𝔸 (AlphaEq' : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by - intro a x π h - sorry +private lemma alpha_eq_pred_equivariant : EquivariantRelation 𝔸 (AlphaEqPred : 𝔸 → NameAbstraction' 𝔸 X × NameAbstraction' 𝔸 X → Prop) := by + intro a x π + rw [AlphaEqPred, AlphaEqPred] + intro h + have h' : π • ⸨a, x.fst.atom⸩ • x.fst.body = π • ⸨a, x.snd.atom⸩ • x.snd.body := by congr + simp [smul_smul, FPerm.mul_swap_eq_swap_mul] at h' + simpa [smul_smul] 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) ∧ AlphaEq' c (x, y)) by - rw [alpha_eq_iff, this] + 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_equivariant' - aesop + exact alpha_eq_pred_equivariant + simp only [Prod.fresh, AlphaEqPred, @and_assoc] 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) → AlphaEq' c (x, y)) by - rw [alpha_eq_iff, this] + 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_equivariant' - aesop + exact alpha_eq_pred_equivariant + simp only [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 |