chore(model_theory/encoding): Improve the encoding of terms (#13532)

Makes it so that the encoding of terms no longer requires the assumption `inhabited (L.term A)`.
Adjusts following lemmas to use the `encoding` API more directly.

src/model_theory/encoding.lean

@@ -20,8 +20,8 @@ import computability.encoding
 
 ## TODO
 * An encoding for formulas
-* `fin_encoding`s for terms and formulas, based on the `encoding`s
-* Computability facts about these `fin_encoding`s, to set up a computability approach to
+* `primcodable` instances for terms and formulas, based on the `encoding`s
+* Computability facts about term and formula operations, to set up a computability approach to
 incompleteness
 
 -/
@@ -46,86 +46,82 @@ def list_encode : L.term α → list (α ⊕ Σ i, L.functions i)
     ((list.fin_range _).bind (λ i, (ts i).list_encode)))
 
 /-- Decodes a list of variables and function symbols as a list of terms. -/
-def list_decode [inhabited (L.term α)] :
-  list (α ⊕ Σ i, L.functions i) → list (L.term α)
+def list_decode :
+  list (α ⊕ Σ i, L.functions i) → list (option (L.term α))
 | [] := []
-| ((sum.inl a) :: l) := var a :: list_decode l
-| ((sum.inr ⟨n, f⟩) :: l) := func f (λ i, ((list_decode l).nth i).iget) :: ((list_decode l).drop n)
-
-@[simp] theorem list_decode_encode_list [inhabited (L.term α)] (l : list (L.term α)) :
-  list_decode (l.bind list_encode) = l :=
+| ((sum.inl a) :: l) := some (var a) :: list_decode l
+| ((sum.inr ⟨n, f⟩) :: l) :=
+  if h : ∀ (i : fin n), ((list_decode l).nth i).join.is_some
+  then func f (λ i, option.get (h i)) :: ((list_decode l).drop n)
+  else [none]
+
+theorem list_decode_encode_list (l : list (L.term α)) :
+  list_decode (l.bind list_encode) = l.map option.some :=
 begin
   suffices h : ∀ (t : L.term α) (l : list (α ⊕ Σ i, L.functions i)),
-    list_decode (t.list_encode ++ l) = t :: list_decode l,
+    list_decode (t.list_encode ++ l) = some t :: list_decode l,
   { induction l with t l lih,
     { refl },
-    { rw [cons_bind, h t (l.bind list_encode), lih] } },
+    { rw [cons_bind, h t (l.bind list_encode), lih, list.map] } },
   { intro t,
     induction t with a n f ts ih; intro l,
     { rw [list_encode, singleton_append, list_decode] },
     { rw [list_encode, cons_append, list_decode],
       have h : list_decode ((fin_range n).bind (λ (i : fin n), (ts i).list_encode) ++ l) =
-        (fin_range n).map ts ++ list_decode l,
+        (fin_range n).map (option.some ∘ ts) ++ list_decode l,
       { induction (fin_range n) with i l' l'ih,
         { refl },
         { rw [cons_bind, append_assoc, ih, map_cons, l'ih, cons_append] } },
-      have h' : n ≤ (list_decode ((fin_range n).bind (λ (i : fin n),
-        (ts i).list_encode) ++ l)).length,
-      { rw [h, length_append, length_map, length_fin_range],
-        exact le_self_add, },
-      refine congr (congr rfl (congr rfl (funext (λ i, _)))) _,
-      { rw [nth_le_nth (lt_of_lt_of_le i.is_lt h'), option.iget_some, nth_le_of_eq h, nth_le_append,
-          nth_le_map, nth_le_fin_range, fin.eta],
-        { rw [length_fin_range],
-          exact i.is_lt },
-        { rw [length_map, length_fin_range],
-          exact i.is_lt } },
+      have h' : ∀ i, (list_decode ((fin_range n).bind (λ (i : fin n), (ts i).list_encode) ++ l)).nth
+        ↑i = some (some (ts i)),
+      { intro i,
+        rw [h, nth_append, nth_map],
+        { simp only [option.map_eq_some', function.comp_app, nth_eq_some],
+          refine ⟨i, ⟨lt_of_lt_of_le i.2 (ge_of_eq (length_fin_range _)), _⟩, rfl⟩,
+          rw [nth_le_fin_range, fin.eta] },
+        { refine lt_of_lt_of_le i.2 _,
+          simp } },
+      refine (dif_pos (λ i, option.is_some_iff_exists.2 ⟨ts i, _⟩)).trans _,
+      { rw [option.join_eq_some, h'] },
+      refine congr (congr rfl (congr rfl (congr rfl (funext (λ i, option.get_of_mem _ _))))) _,
+      { simp [h'] },
       { rw [h, drop_left'],
         rw [length_map, length_fin_range] } } }
 end
 
 /-- An encoding of terms as lists. -/
-@[simps] protected def encoding [inhabited (L.term α)] : encoding (L.term α) :=
+@[simps] protected def encoding : encoding (L.term α) :=
 { Γ := α ⊕ Σ i, L.functions i,
   encode := list_encode,
-  decode := λ l, (list_decode l).head',
+  decode := λ l, (list_decode l).head'.join,
   decode_encode := λ t, begin
     have h := list_decode_encode_list [t],
     rw [bind_singleton] at h,
-    rw [h, head'],
+    simp only [h, option.join, head', list.map, option.some_bind, id.def],
   end }
 
 lemma list_encode_injective :
   function.injective (list_encode : L.term α → list (α ⊕ Σ i, L.functions i)) :=
-begin
-  casesI is_empty_or_nonempty (L.term α) with he hne,
-  { exact he.elim },
-  { inhabit (L.term α),
-    exact term.encoding.encode_injective }
-end
+term.encoding.encode_injective
 
-theorem card_le : # (L.term α) ≤ # (α ⊕ Σ i, L.functions i) + ω :=
-begin
-  have h := (mk_le_of_injective list_encode_injective),
-  refine h.trans _,
-  casesI fintype_or_infinite (α ⊕ Σ i, L.functions i) with ft inf,
-  { haveI := fintype.to_encodable (α ⊕ Σ i, L.functions i),
-    exact le_add_left mk_le_omega },
-  { rw mk_list_eq_mk,
-    exact le_self_add }
-end
+theorem card_le : # (L.term α) ≤ max ω (# (α ⊕ Σ i, L.functions i)) :=
+lift_le.1 (trans term.encoding.card_le_card_list (lift_le.2 (mk_list_le_max _)))
 
-instance [encodable α] [encodable ((Σ i, L.functions i))] [inhabited (L.term α)] :
+instance [encodable α] [encodable ((Σ i, L.functions i))] :
   encodable (L.term α) :=
-encodable.of_left_injection list_encode (λ l, (list_decode l).head')
-  (λ t, by rw [← bind_singleton list_encode, list_decode_encode_list, head'])
+encodable.of_left_injection list_encode (λ l, (list_decode l).head'.join)
+  (λ t, begin
+    rw [← bind_singleton list_encode, list_decode_encode_list],
+    simp only [option.join, head', list.map, option.some_bind, id.def],
+  end)
 
 lemma card_le_omega [h1 : nonempty (encodable α)] [h2 : L.countable_functions] :
   # (L.term α) ≤ ω :=
 begin
   refine (card_le.trans _),
-  rw [add_le_omega, mk_sum, add_le_omega, lift_le_omega, lift_le_omega, ← encodable_iff],
-  exact ⟨⟨h1, L.card_functions_le_omega⟩, refl _⟩,
+  rw [max_le_iff],
+  simp only [le_refl, mk_sum, add_le_omega, lift_le_omega, true_and],
+  exact ⟨encodable_iff.1 h1, L.card_functions_le_omega⟩,
 end
 
 instance small [small.{u} α] :

src/model_theory/substructures.lean

@@ -263,7 +263,7 @@ begin
 end
 
 theorem lift_card_closure_le : cardinal.lift.{(max u w) w} (# (closure L s)) ≤
-  cardinal.lift.{(max u w) w} (#s) + cardinal.lift.{(max u w) u} (#(Σ i, L.functions i)) + ω :=
+  max ω (cardinal.lift.{(max u w) w} (#s) + cardinal.lift.{(max u w) u} (#(Σ i, L.functions i))) :=
 begin
   refine lift_card_closure_le_card_term.trans (term.card_le.trans _),
   rw [mk_sum, lift_umax', lift_umax],