diff options
Diffstat (limited to 'Nominal/LambdaCalculus')
| -rw-r--r-- | Nominal/LambdaCalculus/Terms.lean | 69 |
1 files changed, 43 insertions, 26 deletions
diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean index c698b65..0ca0418 100644 --- a/Nominal/LambdaCalculus/Terms.lean +++ b/Nominal/LambdaCalculus/Terms.lean @@ -118,26 +118,47 @@ lemma trans {t u s : Preterm} : AlphaEq' t u → AlphaEq' u s → AlphaEq' t s : end AlphaEq' private lemma pick_fresh {t : Preterm} : ∀ x ∉ t.fv, ∃ u, t ≈ u ∧ x ∉ u.vars := by + suffices ∀ (π : FPerm Var), ∀ x ∉ (π • t).fv, ∃ u, (π • t) ≈ u ∧ x ∉ u.vars by + specialize this 1 + simp only [one_smul] at this + exact this induction' t <;> all_goals expose_names - · intro x h - use .var a + · intro π x h + use .var (π a) exact ⟨by rfl, h⟩ - · rw [Preterm.fv] - intro x h - have hinf : ({x} ∪ a_1.vars)ᶜ.Infinite := by + · intro π x h + have hinf : ({x} ∪ (π • a_1).vars)ᶜ.Infinite := by apply Set.Finite.infinite_compl - exact Set.Finite.union (Set.finite_singleton x) (Preterm.vars_finite a_1) + exact Set.Finite.union (Set.finite_singleton x) (Preterm.vars_finite (π • a_1)) obtain ⟨c, hc⟩ := hinf.nonempty - simp only [Set.singleton_union, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at hc - obtain ⟨u, hu⟩ := a_ih c (fun h => hc.right (Preterm.fv_subset_vars a_1 h)) - use Preterm.abs c (⸨a, c⸩ • u) - simp [Preterm.vars] + rw [Preterm.smul_abs, Preterm.fv, Set.mem_diff, Set.mem_singleton_iff, not_and, not_not] at h + rw [Set.singleton_union, Set.mem_compl_iff, Set.mem_insert_iff, not_or] at hc + have hc' : c ∉ (π • a_1).fv := fun h => hc.right (Preterm.fv_subset_vars _ h) + obtain ⟨u, hu⟩ := a_ih (⸨π • a, c⸩ * π) x (by + rw [mul_smul, Preterm.fv_equivariant] + intro hcontra + by_cases hxa : x = π • a + · rw [hxa, ← PermSet.atom_set_swap_right] at hcontra + exact hc' hcontra + · rw [← PermSet.atom_set_swap_ne_ne _ hxa (Ne.symm hc.left)] at hcontra + exact hxa (h hcontra)) + use .abs c u constructor - · trans - · exact AlphaEq.cong_abs hu.left - · exact AlphaEq.rename (fun h => hu.right (Preterm.fv_subset_vars u h)) - · sorry - · sorry + · symm; trans + · exact AlphaEq.cong_abs hu.left.symm + · rw [Preterm.smul_abs, mul_smul]; symm + apply AlphaEq.rename hc' + · rw [Preterm.vars, Set.singleton_union, Set.mem_insert_iff, not_or] + exact ⟨Ne.symm hc.left, hu.right⟩ + · intro π x h + rw [Preterm.smul_app, Preterm.fv, Set.mem_union, not_or] at h + obtain ⟨t₁, ht₁⟩ := a_ih π x h.left + obtain ⟨t₂, ht₂⟩ := a_ih_1 π x h.right + use .app t₁ t₂ + constructor + · exact AlphaEq.cong_app ht₁.left ht₂.left + · rw [Preterm.vars, Set.mem_union, not_or] + exact ⟨ht₁.right, ht₂.right⟩ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by ext t u @@ -224,22 +245,19 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term { toFun t := Quotient.liftOn t (fun t => match t with | .var x => .inl x - | .abs x t' => .inr (.inl (⟪x⟫ Term.mk t')) - | .app t' u' => .inr (.inr ⟨(Term.mk t'), (Term.mk u')⟩)) + | .abs x t' => .inr (.inl (⟪x⟫ (⟦t'⟧ : Term))) + | .app t' u' => .inr (.inr ⟨(⟦t'⟧ : Term), (⟦u'⟧ : Term)⟩)) (by intro t u htu - cases htu - · sorry - · sorry - · sorry - · sorry - · sorry - · sorry) + rw [alpha_eq, alpha_eq_iff] at htu + cases htu <;> simp [*]) invFun | .inl x => .var x | .inr (.inl x) => Quotient.liftOn x (fun x => .abs x.atom x.body) - (by sorry) + (by + intro x y hxy + sorry) | .inr (.inr x) => .app x.fst x.snd left_inv := by sorry right_inv := by sorry @@ -258,7 +276,6 @@ lemma supp : NominalSet.supp Var = fv := by apply Quotient.ind intro t induction' t; all_goals - expose_names rw [EquivariantEquiv.supp_eq Var equiv] simp [fv, Preterm.fv, *] |