Struggling to understand Lean's type inference and coercions

Stream: new members

[Rick van Oosterhout]

I am working on my thesis on formalizing relational algebra in Lean. I managed to implement and proof some basic theorems on the union and rename operation already. However, whilst working on the join operation, I ran into a few issues regarding Lean's type inference. I was able to resolve some using coercions, but this resulted in different issues later on, so I am wondering whether the coercions are the right approach?

Below is the complete relevant code (merged in a single file to make for an easy mwe). Please let me know whether my approach using coercions is right, whether you see any other critical mistakes I am making or if you have other suggestions on the code. I would also greatly appreciate it if those more familiar with the existing parts in Lean/mathlib would point out parts that are similar or deal with similar issues, such that I can use those when I encounter problems in the future. All advice is welcome, since I really want to improve my knowledge of Lean.

import Mathlib.Data.Set.Basic

-- Relational Model definitions
abbrev Attribute := Type

abbrev RelationName := Type

abbrev Value := Type

abbrev RelationSchema := Set Attribute

abbrev Tuple (relSch : RelationSchema) := relSch → Value

abbrev RelationInstance (relSch : RelationSchema) := Set (Tuple relSch)



-- Coercion for relation schema union (construction)
@[simp]
def schema_union_right (s1 s2 : RelationSchema) : s1 → {a // a ∈ s1 ∪ s2} := by
  intro a
  obtain ⟨val, property⟩ := a
  exact Subtype.mk val (Or.inl property)

instance schema_union_right_cast {s1 s2 : RelationSchema} :
  Coe s1 {a // a ∈ s1 ∪ s2} := ⟨schema_union_right s1 s2⟩

-- Coercion for relation schema union commutativity
@[simp]
def schema_union_comm (s1 s2 : RelationSchema) : {a // a ∈ s1 ∪ s2} ≃ {a // a ∈ s2 ∪ s1} := by rw [Set.union_comm]

instance schema_union_comm_cast (s1 s2 : RelationSchema) : Coe {a // a ∈ s1 ∪ s2} {a // a ∈ s2 ∪ s1} := ⟨schema_union_comm s1 s2⟩

-- -- Coercion for relation schema intersection (destruction)
@[simp]
noncomputable def schema_inter_left {s1 s2 : RelationSchema} (a : {a // a ∈ s1 ∩ s2}) : s1 :=
  ⟨a.val, Set.mem_of_mem_inter_left a.property⟩

@[simp]
noncomputable def schema_inter_right {s1 s2 : RelationSchema} (a : {a // a ∈ s1 ∩ s2}) : s2 :=
  ⟨a.val, Set.mem_of_mem_inter_right a.property⟩

noncomputable instance schema_inter_left_cast (s1 s2 : RelationSchema) :
  CoeOut {a // a ∈ s1 ∩ s2} s1 where
  coe := schema_inter_left

noncomputable instance schema_inter_right_cast (s1 s2 : RelationSchema) :
  CoeOut {a // a ∈ s1 ∩ s2} s2 where
  coe := schema_inter_right

-- Join operation (and theorems)
def join {s1 s2 : RelationSchema} (inst1 : RelationInstance s1) (inst2 : RelationInstance s2) :
  RelationInstance (s1 ∪ s2) :=
    { t | ∃ t1 ∈ inst1, ∃ t2 ∈ inst2,
      -- Attributes in both s1 and s2
      (∀ a : ↑(s1 ∩ s2), t1 a = t2 a) ∧ -- @Problem these lines require coercion(s)
      -- Attributes in s1
      (∀ a : s1, t a = t1 a) ∧ -- @Problem these lines require coercion(s)
      -- Attributes in s2
      (∀ a : s2, t a = t2 a) -- @Problem these lines require coercion(s)
    }

theorem join_empty {s1 s2 : RelationSchema} (inst1 : RelationInstance s1) :
  join inst1 (∅ : RelationInstance s2) = (∅ : RelationInstance (s1 ∪ s2)) := by
    simp only [join, Set.mem_empty_iff_false, false_and, exists_const, and_false, Set.setOf_false]



@[simp]
def instance_union_comm (s1 s2 : RelationSchema) : RelationInstance (s1 ∪ s2) ≃ RelationInstance (s2 ∪ s1) := by rw [Set.union_comm]

instance instance_union_comm_cast (s1 s2 : RelationSchema) :
  Coe (RelationInstance (s1 ∪ s2)) (RelationInstance (s2 ∪ s1)) := ⟨instance_union_comm s1 s2⟩

theorem join_comm {s1 s2 : RelationSchema} (inst1 : RelationInstance s1) (inst2 : RelationInstance s2) :
  join inst1 inst2 = join inst2 inst1 := by -- @Problem coercion is required, otherwise I get a type error on this line
    -- @Problem: I cannot get instance_union_comm out of this proof
    sorry



-- Coercion for relation instance schema union self
def instance_union_self (s1 : RelationSchema) : RelationInstance (s1 ∪ s1) ≃ RelationInstance s1 := by rw [Set.union_self]

instance instance_union_self_cast (s1 : RelationSchema) : CoeOut (RelationInstance (s1 ∪ s1)) (RelationInstance s1) := ⟨instance_union_self s1⟩

theorem join_self {s1 : RelationSchema} (inst1 : RelationInstance s1) :
  join inst1 inst1 = inst1 := by -- @Problem coercion is required, otherwise I get a type error on this line
    -- @Problem: I cannot get instance_union_self out of this proof
    sorry

[Aaron Liu]

Usually, using tactics to construct data is a bad idea, if you expect to prove things about the resulting definition.

-- Coercion for relation schema union (construction)
@[simp]
def schema_union_right (s1 s2 : RelationSchema) : s1 → {a // a ∈ s1 ∪ s2} := by
  intro a
  obtain ⟨val, property⟩ := a
  exact Subtype.mk val (Or.inl property)

[Aaron Liu]

I think this is not how you should be using coercions. Instead, you should write out the casts explicitly.

[Rick van Oosterhout]

Thanks for the feedback! I understand how this would work (and help) for the join definition, but I cannot find out how to do this in the theorems. Could you show me an example on how to do this?

[Kevin Buzzard]

Your definition of schema_union_comm will be unusable because rw will stick an Eq.rec into your definition. Don't use tactics to make data. You should just define the fields manually; to make a term of a subtype is to give a pair consisting of a term of the type and a proof that it satisfies the predicate, and you can use tactics when constructing the proof but you should use term mode when constructing the data or you'll end up with definitions which are very hard to work with.

[Kevin Buzzard]

eg

noncomputable def schema_union_right (s1 s2 : RelationSchema) (a : s1) : {a // a ∈ s1 ∪ s2} := ⟨a.1, Or.inl a.2⟩

noncomputable def schema_union_comm (s1 s2 : RelationSchema) : {a // a ∈ s1 ∪ s2} ≃ {a // a ∈ s2 ∪ s1} where
  toFun a := ⟨a.1, Or.symm a.2⟩
  invFun a := ⟨a.1, Or.symm a.2⟩
  left_inv a := by simp
  right_inv a := by ext; simp

I also think it's a dubious design decision to have s1 : Set Attribute and then to treat s1 as a type with things like s1 → {a // a ∈ s1 ∪ s2}. Do you want s1 to be a type or a term? You might want to think hard about some design decisions here before you get started.