finish initial lambda terms modulo alpha-equivalence

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