diff options
Diffstat (limited to 'Nominal/LambdaCalculus')
| -rw-r--r-- | Nominal/LambdaCalculus/Terms.lean | 75 |
1 files changed, 59 insertions, 16 deletions
diff --git a/Nominal/LambdaCalculus/Terms.lean b/Nominal/LambdaCalculus/Terms.lean index 0ca0418..5362e04 100644 --- a/Nominal/LambdaCalculus/Terms.lean +++ b/Nominal/LambdaCalculus/Terms.lean @@ -219,27 +219,44 @@ lemma alpha_eq_iff : AlphaEq = AlphaEq' := by /-- Alternative characterization of α-equivalence for variable preterms. -/ lemma alpha_eq_var {x y : Var} : Preterm.var x ≈ Preterm.var y ↔ x = y := by - sorry + rw [alpha_eq, alpha_eq_iff] + constructor + · intro h; cases h; rfl + · intro h; rw [h]; constructor @[inherit_doc alpha_eq_var] lemma eq_var {x y : Var} : Term.var x = Term.var y ↔ x = y := by - sorry + rw [var, var, mk, Quotient.eq_iff_equiv, alpha_eq_var] /-- Alternative characterization of α-equivalence for abstraction preterms. -/ -lemma alpha_eq_abs {x y : Var} {t u : Preterm} : Preterm.abs x t ≈ Preterm.abs y u ↔ ⟪x⟫ Term.mk t = ⟪y⟫ Term.mk u := by - sorry +lemma alpha_eq_abs {x y : Var} {t u : Preterm} : Preterm.abs x t ≈ Preterm.abs y u ↔ ⟪x⟫ (⟦t⟧ : Term) = ⟪y⟫ (⟦u⟧ : Term) := by + rw [alpha_eq, alpha_eq_iff] + constructor + · intro h; cases h; assumption + · intro h; constructor; assumption @[inherit_doc alpha_eq_abs] lemma eq_abs {x y : Var} {t u : Term} : Term.abs x t = Term.abs y u ↔ ⟪x⟫ t = ⟪y⟫ u := by - sorry + obtain ⟨t', ht'⟩ := t.exists_rep + obtain ⟨u', hu'⟩ := u.exists_rep + simp only [abs, mk, ← ht', Quotient.lift_mk, ← hu'] + rw [Quotient.eq_iff_equiv, alpha_eq_abs] /-- Alternative characterization of α-equivalence for application preterms. -/ lemma alpha_eq_app {t₁ t₂ u₁ u₂ : Preterm} : Preterm.app t₁ t₂ ≈ Preterm.app u₁ u₂ ↔ t₁ ≈ u₁ ∧ t₂ ≈ u₂ := by - sorry + rw [alpha_eq, alpha_eq_iff] + constructor + · intro h; cases h; rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv]; constructor <;> assumption + · rw [← Quotient.eq_iff_equiv, ← Quotient.eq_iff_equiv]; intro ⟨h₁, h₂⟩; constructor <;> assumption @[inherit_doc alpha_eq_app] lemma eq_app {t₁ t₂ u₁ u₂ : Term} : Term.app t₁ t₂ = Term.app u₁ u₂ ↔ t₁ = u₁ ∧ t₂ = u₂ := by - sorry + obtain ⟨t₁', ht₁'⟩ := t₁.exists_rep + obtain ⟨t₂', ht₂'⟩ := t₂.exists_rep + obtain ⟨u₁', hu₁'⟩ := u₁.exists_rep + obtain ⟨u₂', hu₂'⟩ := u₂.exists_rep + simp only [app, mk, ← ht₁', ← ht₂', Quotient.lift_mk, ← hu₁', ← hu₂'] + rw [Quotient.eq_iff_equiv, Quotient.eq_iff_equiv, Quotient.eq_iff_equiv, alpha_eq_app] private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term) ⊕ (Term × Term)) := { toFun t := Quotient.liftOn t @@ -257,27 +274,53 @@ private def equiv : EquivariantEquiv Var Term (Var ⊕ (NameAbstraction Var Term (fun x => .abs x.atom x.body) (by intro x y hxy - sorry) + simp only [eq_abs] + exact Quotient.sound hxy) | .inr (.inr x) => .app x.fst x.snd - left_inv := by sorry - right_inv := by sorry - toFun_equivariant := by sorry + left_inv := by + apply Quotient.ind; intro t + cases t <;> rfl + right_inv := by + intro x + cases x with + | inl x => rfl + | inr x => + cases x with + | inl x => + obtain ⟨x', hx'⟩ := x.exists_rep + obtain ⟨body, hbody⟩ := x'.body.exists_rep + simp only [← hx', abs, mk, Quotient.lift_mk, ← hbody, Sum.inr.injEq, Sum.inl.injEq] + rw [hbody]; rfl + | inr x => + obtain ⟨x', hx'⟩ := x.fst.exists_rep + obtain ⟨y', hy'⟩ := x.snd.exists_rep + simp only [app, mk, ← hx', ← hy', Quotient.lift_mk, Sum.inr.injEq] + rw [hx', hy'] + toFun_equivariant := by + intro t π + obtain ⟨t', ht'⟩ := t.exists_rep + rw [← ht'] + cases t' <;> all_goals rfl } @[simp] private lemma equiv_var {x : Var} : equiv.toFun ⟦.var x⟧ = .inl x := rfl @[simp] private lemma equiv_abs {x : Var} {t : Preterm} : equiv.toFun ⟦.abs x t⟧ = .inr (.inl (⟪x⟫ ⟦t⟧)) := rfl @[simp] private lemma equiv_app {t u : Preterm} : equiv.toFun ⟦.app t u⟧ = .inr (.inr (⟦t⟧, ⟦u⟧)) := rfl -def fv : Term → Set Var := Quotient.lift Preterm.fv - (by sorry) +private lemma supp' (t : Preterm) : NominalSet.supp Var (⟦t⟧ : Term) = t.fv := by + induction' t; all_goals + rw [EquivariantEquiv.supp_eq Var equiv] + simp [Preterm.fv, *] + +def fv : Term → Set Var := Quotient.lift Preterm.fv (by + intro t u htu + rw [← supp', ← supp', Quotient.sound htu]) lemma supp : NominalSet.supp Var = fv := by apply funext apply Quotient.ind intro t - induction' t; all_goals - rw [EquivariantEquiv.supp_eq Var equiv] - simp [fv, Preterm.fv, *] + rw [supp']; rfl end Term |