Parametrize Var by type

Author: Will Bradley

LogicFormalization/Chapter2/Section4/Homework.lean

@@ -5,7 +5,9 @@ import Mathlib.Tactic.Ring
 
 namespace Homeworks
 
-open Term HasVar
+universe u
+
+open Term
 
 section Problem1
 /-! TODO -/
@@ -33,6 +35,8 @@ def 𝒩 : Structure .Rig ℕ where
   | .add,  a => a 0 + a 1
   | .mul,  a => a 0 * a 1
 
+variable {V: Type u} [DecidableEq V]
+
 section a
 variable (f: ℕ → ℕ)
 @[simp] abbrev isConstant := ∃ y, ∀ n, f n = y
@@ -76,7 +80,7 @@ lemma isConstant_or_isGe_of_mul:
 
 
 /-- 2.4 #5 (a) -/
-theorem not_exists_nat_rig_term₁ : ¬∃ (t: Term .Rig) (x: Var) (hx: AreVarsFor ![x] t),
+theorem not_exists_nat_rig_term₁ : ¬∃ (t: Term .Rig V) (x: V) (hx: AreVarsFor ![x] t),
     interp t 𝒩 hx ![0] = 1 ∧ interp t 𝒩 hx ![1] = 0 := by
   push_neg
   intro t x hx
@@ -229,7 +233,7 @@ where
         omega
 
 /-- Convert one of the `L`-terms to a `Poly`. -/
-def ofTerm (t: Term .Rig) {x: Var} (hx: AreVarsFor ![x] t):
+def ofTerm (t: Term .Rig V) {x: V} (hx: AreVarsFor ![x] t):
     { p // ∀ n, interp t 𝒩 hx ![n] = eval p n } :=
   match t with
   | .var _ => ⟨.var, fun n => by simp [interp, eval]⟩
@@ -248,7 +252,7 @@ end Poly
 
 
 /-- 2.4 #5 (b) -/
-theorem not_exists_nat_rig_term₂ : ¬∃ (t: Term .Rig) (x: Var) (hx: AreVarsFor ![x] t),
+theorem not_exists_nat_rig_term₂ : ¬∃ (t: Term .Rig V) (x: V) (hx: AreVarsFor ![x] t),
     ∀ n, interp t 𝒩 hx ![n] = 2^n :=
   fun ⟨t, x, hx, h⟩ =>
     let ⟨p, hp⟩ := Poly.ofTerm t hx

LogicFormalization/Chapter2/Section4/Term.lean

@@ -1,17 +1,17 @@
 import LogicFormalization.Chapter2.Section3.Basic
 import LogicFormalization.Chapter2.Section4.Var
 
-universe u v w
-variable [HasVar]
+universe u
+variable {V: Type u}
 
-inductive Term (L: Language)
+inductive Term (L: Language) (V: Type u := ULift ℕ)
 /-- `var v` represents the variable `v`, viewed as a word of length `1`-/
-| var (v: Var)
+| var (v: V)
 /-- `app F ts` represents the concatenation `Ft₁...tₙ`-/
-| app (F: L.ϝ) (ts: Fin (arity F) → Term L)
+| app (F: L.ϝ) (ts: Fin (arity F) → Term L V)
 
 
-example : Term Language.Ring :=
+example : Term Language.Ring ℕ :=
   .app .mul fun | 0 => .app .add fun
                   | 0 => .var x
                   | 1 => .app .neg fun
@@ -23,19 +23,19 @@ namespace Term
 variable {L: Language}
 
 /-- Predicate for a variable occurring in a term. -/
-def occursIn (v: Var) : Term L → Prop
+def occursIn (v: V) : Term L V → Prop
 | .var v' => v = v'
 | .app _ ts => ∃ i, occursIn v (ts i)
 
-lemma occursIn_app {v: Var} {F} {ts: Fin (arity F) → Term L}
+lemma occursIn_app {v: V} {F} {ts: Fin (arity F) → Term L V}
     {i} (h: occursIn v (ts i)): occursIn v (.app F ts) :=
   ⟨i, h⟩
 
-lemma occursIn_of_occursIn_app {v: Var} {F} {ts: Fin (arity F) → Term L}
+lemma occursIn_of_occursIn_app {v: V} {F} {ts: Fin (arity F) → Term L V}
     (h: occursIn v (.app F ts)): ∃ i, occursIn v (ts i) :=
   h
 
-instance instDecidableOccursIn (v) (t: Term L) :
+instance instDecidableOccursIn [DecidableEq V] (v: V) (t: Term L V) :
     Decidable (occursIn v t) :=
   match t with
   | .var v' => if h: v = v' then .isTrue h else .isFalse h
@@ -50,13 +50,13 @@ instance instDecidableOccursIn (v) (t: Term L) :
       have := Fin.find_eq_none_iff.mp h
       .isFalse fun ⟨i, hi⟩ => this i hi
 
-/- N.B.: Here, we use an injective mapping from `Fin m` instead of a `Finset Var` so
+/- N.B.: Here, we use an injective mapping from `Fin m` instead of a `Finset V` so
 that we can easily talk about the index of a variable (see `idx`),
 which is used in `interp`. -/
 
 /-- `AreVarsFor x t` means that `t = t(x₁, ..., xₘ)`, i.e. the `xᵢ` are
 unique and contain (possibly not strictly) all the variables in `t`. -/
-structure AreVarsFor {m: ℕ} (x: Fin m → Var) (t: Term L) where
+structure AreVarsFor {m: ℕ} (x: Fin m → V) (t: Term L V) where
   inj': Function.Injective x
   occursIn': ∀ {v}, occursIn v t → v ∈ Set.range x
 
@@ -67,12 +67,12 @@ variable {t: Term L} {m: ℕ}
 /-- If all the variables in a function application are in `x`, then
 then the variables in each subterm remain in `x`. -/
 @[simp]
-lemma ofApp {F} {m} {ts: Fin (arity F) → Term L} {x: Fin m → Var} (hx: AreVarsFor x (app F ts)):
+lemma ofApp {F} {m} {ts: Fin (arity F) → Term L V} {x: Fin m → V} (hx: AreVarsFor x (app F ts)):
     (i: Fin (arity F)) → AreVarsFor x (ts i) :=
   fun _i => ⟨hx.inj', fun h => hx.occursIn' (occursIn_app h)⟩
 
 /-- The (unique) `index` of a variable `xᵢ` in a set `x₁, ..., xₘ` is just `i`. -/
-def index {t: Term L} {v: Var} {x: Fin m → Var}
+def index [DecidableEq V] {t: Term L V} {v: V} {x: Fin m → V}
     (hx: AreVarsFor x t) (h: occursIn v t): { i : Fin m // x i = v } :=
   match t with
   | .var _v' =>
@@ -89,13 +89,14 @@ def index {t: Term L} {v: Var} {x: Fin m → Var}
 
 end AreVarsFor
 
-variable {A: Type u} [Nonempty A]
+universe v
+variable {A: Type v} [Nonempty A]
 
 open Structure
 
 /-- The interpretation `t^𝒜` of a term `t` with variables `x₁, ..., xₘ`
 (which may not actually appear in `t`) is a function from `A^m` to `A`. -/
-def interp (t: Term L) (𝒜: Structure L A) {m} {x: Fin m → Var} (hx: AreVarsFor x t):
+def interp [DecidableEq V] (t: Term L V) (𝒜: Structure L A) {m} {x: Fin m → V} (hx: AreVarsFor x t):
     (Fin m → A) → A :=
   match t with
   | .var _xᵢ => fun as => as (hx.index rfl)
@@ -105,9 +106,9 @@ def interp (t: Term L) (𝒜: Structure L A) {m} {x: Fin m → Var} (hx: AreVars
 open Structure in
 /-- If `𝒜 ⊆ ℬ` are `L`-structures and `t` is an `L`-term with variables `x₁, ..., xₘ`,
 then for all `a ∈ A^m`, `t^𝒜(a) = t^ℬ(a)`. -/
-lemma interp_substructure {B: Type v} {A: Set B} [Nonempty A]
+lemma interp_substructure [DecidableEq V] {B: Type v} {A: Set B} [Nonempty A]
     {𝒜: Structure L A} {ℬ: Structure L B}
-    (h: 𝒜 ⊆ ℬ) {t: Term L} {m} {x: Fin m → Var} (hx: AreVarsFor x t):
+    (h: 𝒜 ⊆ ℬ) {t: Term L V} {m} {x: Fin m → V} (hx: AreVarsFor x t):
     ∀ (a: Fin m → A), interp t 𝒜 hx a = interp t ℬ hx (a ·) :=
   match t with
   | .var v => fun a => rfl
@@ -119,12 +120,12 @@ lemma interp_substructure {B: Type v} {A: Set B} [Nonempty A]
     exact substructure_isSubstructure
 
 /-- "A term is said to be *variable-free* if no variables occur in it." -/
-def varFree : Term L → Prop
+def varFree : Term L V → Prop
 | .var _ => False
 | .app _ ts => ∀ i, varFree (ts i)
 
 @[simp]
-lemma not_varFree_var {v: Var}: ¬varFree (.var v: Term L) :=
+lemma not_varFree_var {v: V}: ¬varFree (.var v: Term L V) :=
   False.elim
 
 @[simp]
@@ -133,30 +134,30 @@ lemma varFree_of_varFree_app {F} {ts: Fin (arity F) → Term L}
   @h
 
 @[simp]
-lemma varFree_iff: ∀ {t: Term L}, varFree t ↔ ∀ v, ¬occursIn v t
+lemma varFree_iff: ∀ {t: Term L V}, varFree t ↔ ∀ v, ¬occursIn v t
 | .var _ => by simp [varFree, occursIn]
 | .app F ts => by
   simp only [varFree, occursIn, not_exists, varFree_iff]
   apply forall_comm
 
-def AreVarsFor.empty {t: Term L} (ht: varFree t): AreVarsFor Fin.elim0 t where
+def AreVarsFor.empty {t: Term L V} (ht: varFree t): AreVarsFor Fin.elim0 t where
   inj' := Function.injective_of_subsingleton _
   occursIn' := by simp [varFree_iff.mp ht _]
 
 /-- If `t` is variable-free, we can identify its
 interpretation with a single value. -/
-def interpConst (t: Term L) (ht: varFree t) (𝒜: Structure L A): A :=
+def interpConst [DecidableEq V] (t: Term L V) (ht: varFree t) (𝒜: Structure L A): A :=
   interp t 𝒜 (.empty ht) Fin.elim0
 
 /-- The more natural way of expressing `interpConst`.
 See `interpConst_eq_spec`. -/
-def interpConst.spec (t: Term L) (ht: varFree t) (𝒜: Structure L A): A :=
+def interpConst.spec (t: Term L V) (ht: varFree t) (𝒜: Structure L A): A :=
   match t with
   | .var _ => False.elim ht
   | .app F ts =>
     (F^𝒜) (fun i => spec (t := ts i) (ht i) 𝒜)
 
-lemma interpConst_eq_spec {t: Term L} (ht: varFree t) {𝒜: Structure L A} :
+lemma interpConst_eq_spec [DecidableEq V] {t: Term L V} (ht: varFree t) {𝒜: Structure L A} :
     interpConst t ht 𝒜 = interpConst.spec t ht 𝒜 :=
   match t with
   | .var _ => rfl
@@ -166,7 +167,7 @@ lemma interpConst_eq_spec {t: Term L} (ht: varFree t) {𝒜: Structure L A} :
     rfl
 
 /-- `replace t τ x` is `t(τ₁/x₁, ..., τₙ/xₙ)`. Note that `x` must be injective. -/
-def replace (t: Term L) {m} (τ: Fin m → Term L) (x: Fin m ↪ Var): Term L :=
+def replace [DecidableEq V] (t: Term L V) {m} (τ: Fin m → Term L V) (x: Fin m ↪ V): Term L V :=
   match t with
   | .var v =>
     match Fin.find (fun j => x j = v) with
@@ -175,8 +176,8 @@ def replace (t: Term L) {m} (τ: Fin m → Term L) (x: Fin m ↪ Var): Term L :=
   | .app F ts => .app F (fun i => replace (ts i) τ x)
 
 /-- Lemma 2.4.1 -/
-theorem replace_varFree {t: Term L} {m} {τ: Fin m → Term L}
-    {x: Fin m → Var} (hx: AreVarsFor x t) (h: ∀ i, varFree (τ i)):
+theorem replace_varFree [DecidableEq V] {t: Term L V} {m} {τ: Fin m → Term L V}
+    {x: Fin m → V} (hx: AreVarsFor x t) (h: ∀ i, varFree (τ i)):
     varFree (replace t τ ⟨x, hx.inj'⟩) :=
   match t with
   | .var v =>

LogicFormalization/Chapter2/Section4/Var.lean

@@ -1,39 +1,29 @@
 import Mathlib.Data.Fintype.EquivFin
 import Mathlib.Data.Real.Basic
 
-class HasVar.{u} where
-  Var: Type u
-  [emb: Function.Embedding ℕ Var]
-  [decidable: DecidableEq Var]
+universe u
 
-export HasVar (Var)
+class Var (V: Type u) where
+  var : ℕ ↪ V
 
-variable [HasVar]
+variable {V: Type u} [Var V]
 
-def var (n: ℕ) : Var :=
-  HasVar.emb n
+export Var (var)
 
-lemma var_inj: ∀ {m n}, var m = var n → m = n :=
-  @HasVar.emb.inj'
+lemma var_inj: ∀ {m n: ℕ}, var (V := V) m = var n → m = n :=
+  @var.inj'
 
-instance [HasVar] : DecidableEq Var :=
-  HasVar.decidable
+abbrev v₀: V := var 0
+abbrev v₁: V := var 1
+abbrev v₂: V := var 2
+abbrev v₃: V := var 3
 
-abbrev v₀ := var 0
-abbrev v₁ := var 1
-abbrev v₂ := var 2
-abbrev v₃ := var 3
+abbrev x: V := var 100
+abbrev y: V := var 101
+abbrev z: V := var 102
 
-abbrev x := var 100
-abbrev y := var 101
-abbrev z := var 102
+instance : Var ℝ where
+  var := ⟨(↑), CharZero.cast_injective⟩
 
-namespace HasVar
-
-noncomputable scoped instance (priority := low) instReal : HasVar where
-  Var := ℝ
-  emb := ⟨(↑), CharZero.cast_injective⟩
-
-scoped instance (priority := high) instNat : HasVar where
-  Var := ℕ
-  emb := ⟨id, Function.injective_id⟩
+instance : Var ℕ where
+  var := ⟨id, Function.injective_id⟩