## Stream: new members

### Topic: Function on equal types

#### Robert Brijder (Aug 23 2020 at 09:17):

Why does the second example below not even type check?

import data.set

variables {α : Type} (s t : set α)

example : s ∪ t = t ∪ s := set.union_comm s t -- this works, of course

example : (s ∪ t) → nat = (t ∪ s) → nat := sorry -- why does this not even typecheck?


#### Robert Brijder (Aug 23 2020 at 09:22):

Ah, sorry, I see it now. It seems to be a parenthesis thing

example : ((s ∪ t) → nat) = ((t ∪ s) → nat) := sorry -- this typechecks


#### Mario Carneiro (Aug 23 2020 at 09:44):

oh that looks like trouble coming

#### Mario Carneiro (Aug 23 2020 at 09:44):

equality of types is a Bad Thing

#### Robert Brijder (Aug 23 2020 at 09:52):

Yes, I am beginning to realize that I am in trouble. Here is a MWE of the problem I faced when trying to formalize something

import data.set

variables {α : Type} (s t : set α)

lemma union_comm_func : ((s ∪ t) → nat) = ((t ∪ s) → nat) := by rw set.union_comm s t

@[reducible] def f_ones : s → nat := (λ x, 1)
example : f_ones (t ∪ s) = eq.mp (union_comm_func s t) (f_ones (s ∪ t)) := sorry


This example looks not very nice and I don't know how to prove it. I would just like to say

example : f_ones (t ∪ s) = f_ones (s ∪ t)


but I can't. What is the Good Thing to do?

#### Robert Brijder (Aug 23 2020 at 10:07):

And is there some documentation about good and bad practices for formalizing in Lean?

#### Kevin Buzzard (Aug 23 2020 at 10:07):

Don't talk about equality of functions between non-definitionally equal types I guess

#### Patrick Massot (Aug 23 2020 at 10:08):

This is a pretty vague question, but there are lots of resources listed at https://leanprover-community.github.io/learn.html

#### Kenny Lau (Aug 23 2020 at 11:08):

Actually, why don't we prove that eq.rec is a group hom etc?

#### Kenny Lau (Aug 23 2020 at 11:08):

instead of just avoiding it like the plague

#### Kenny Lau (Aug 23 2020 at 11:08):

is this infeasible?

#### Kenny Lau (Aug 23 2020 at 11:09):

I have a dream: that one day we will stop relying on definitional equality

#### Robert Brijder (Aug 23 2020 at 14:19):

Kenny Lau said:

instead of just avoiding it like the plague

OK, so the Good Thing is to avoid non-definitionally equal types like the plague. But how do I do this? Should I just refrain from proving certain mathematical statements or is there always a way around it? In particular, is there some alternative formalization of the (trivial) mathematical statement f_ones (t ∪ s) = f_ones (s ∪ t)in my example that avoids non-definitionally equal types?

#### Patrick Massot (Aug 23 2020 at 14:25):

There is a way. You are clearly fighting the system instead of playing with it, but we don't have enough context to understand what you are trying to do (see also #xy).

#### Robert Brijder (Aug 23 2020 at 16:03):

Oh, I didn't know I was fighting the system. I do think a problem similar to the MWE arised naturally.

Sure, I'll give some context. I want to formalize a result about a database query language in this paper. The theory is low-level and self-contained, so it seems doable. This lean code is what I have now. It is mostly definitions. The problem is the commutativity of the union operation for relations: theorem rel_union_comm.

#### Robert Brijder (Aug 24 2020 at 18:15):

From a mathematical point of view, it boils down to this: I am trying to define higher-dimensional matrices (tensors) and I am interested in formalizing a result about the expressivity of a certain set of operations on them (i.e., what kind of computations/queries I can do). If X is some finite set of dimensions of one tensor and Y of another, then union operation obtains a tensor with X \cup Y as the set of dimensions. I would like to show (as a first tiny step) that union is commutative, but now I run into the trouble that I have a tensor with X \cup Y as the set of dimensions and another with Y \cup X as the set of dimensions. In the case of an ordinary matrix X would be {row, col}, and in the case of a column vector X would be {col}, but in this case X is arbitrary. Now, just like in matrix multiplication, we also need to keep track of the sizes of each dimension (or, more generally, assign of set of indices to each dimension) for things to make sense. The notion of relation in the linked github repo captures this notion of a tensor (it is called a relation instead of a tensor because of the database context).

Any help on how to avoid non-definitionally equal types here is appreciated.

#### Kevin Buzzard (Aug 24 2020 at 18:22):

Instead of defining a function on s union t, why not define it on all of alpha and then ignore its values outside s union t?

#### Yakov Pechersky (Aug 24 2020 at 18:25):

You might want to look at docs#holor

#### Robert Brijder (Aug 24 2020 at 18:28):

Kevin Buzzard said:

Instead of defining a function on s union t, why not define it on all of alpha and then ignore its values outside s union t?

Perhaps that would work. So, I should store the "real" set of dimensions separately, say together as a structure?

#### Kevin Buzzard (Aug 24 2020 at 18:34):

I don't really know the type of the things you're talking about. I'm just saying that sets are terms and when you promote them to types, equal sets may become non-defeq types. On the other hand if you're only interested in equality of functions on these sets then you could define functions on a bigger type without doing the promotion which is causing the problem

#### Robert Brijder (Aug 24 2020 at 18:35):

Yakov Pechersky said:

You might want to look at docs#holor

Yes. The problem for me with that definition (and mine for that matter) is that the index set is baked-in the type, which apparently is something I should avoid.

#### Reid Barton (Aug 24 2020 at 18:39):

It seems like you already have a way of moving relations across subset inclusions, so one option is to move the two sides together using the inclusion of X \cup Y in Y \cup X

#### Reid Barton (Aug 24 2020 at 18:41):

Another option is to move the X index of the relation type into a structure field, so effectively work with \Sigma X, relation D X alpha

#### Robert Brijder (Aug 24 2020 at 18:42):

Kevin Buzzard said:

if you're only interested in equality of functions on these sets

Unfortunately, I am not only interested in this. I do want to keep track of the real set of dimensions. Like in linear algebra, where one would need to be able to distinguish a vector from a matrix.

#### Reid Barton (Aug 24 2020 at 18:42):

this can be awkward if you have operations which require two relations with the same X, for example, but your existing operations don't appear to be of this sort

#### Robert Brijder (Aug 24 2020 at 18:46):

Reid Barton said:

this can be awkward if you have operations which require two relations with the same X, for example, but your existing operations don't appear to be of this sort

Unfortunately, one such operation requires this! (Actually, it is the union operation; I didn't want to over-complicate my message by saying that union is actually only defined if the index sets are equal. Details are in the above mentioned lean repo and paper.)

#### Reid Barton (Aug 24 2020 at 18:47):

I'm actually looking at the repo and paper and I'm confused about this point

#### Reid Barton (Aug 24 2020 at 18:47):

def rel_union (r : relation D X α) (r' : relation D X' α) :
relation D (X ∪ X') α := (λ t, r(tuple_comp t (inclusion_compat (finset.subset_union_left X X'))) +
r'(tuple_comp t (inclusion_compat (finset.subset_union_right X X'))))


#### Reid Barton (Aug 24 2020 at 18:48):

Indeed, isn't this the very function which originated this topic?

#### Robert Brijder (Aug 24 2020 at 18:49):

Reid Barton said:

Indeed, isn't this the very function which originated this topic?

Yes, it is! I am defining it in the lean code in higher generality (thinking this might help in formalization), but the query language requires that X' = X. I have defined a notion of well-typed expressions in the lean code which says that the schemas should coincide.

#### Robert Brijder (Aug 24 2020 at 18:51):

def ARA_well_typed (e : ARAe rel att) (S : rel → finset att) : Prop :=
ARAe.rec_on e (λ R, true) -- relnm
(λ e1 e2 e1W e2W, e1W ∧ e2W ∧ (ARAschema e1 S = ARAschema e2 S)) -- union
(λ Y e1 e1W, e1W) -- proj
(λ Y hmutc e1 e1W, e1W) -- selection
(λ φ hinj hc e1 e1W, e1W) -- rename
(λ e1 e2 e1W e2W, e1W ∧ e2W) -- join


#### Reid Barton (Aug 24 2020 at 18:52):

If you have a relation with X as a structure field then you can still impose a propositional condition r.X = r'.X if you want to.

#### Reid Barton (Aug 24 2020 at 18:52):

It just might be less convenient than if you knew they were definitionally equal.

#### Reid Barton (Aug 24 2020 at 18:55):

It looks like you're halfway down that road already with this definition of ARA_well_typed

#### Robert Brijder (Aug 24 2020 at 18:56):

Reid Barton said:

It just might be less convenient than if you knew they were definitionally equal.

Whatever is most convenient. If restricting the definition of union is better, then great.

#### Robert Brijder (Aug 24 2020 at 18:58):

It is not yet clear to me how I should define the notion of a relation.

#### Reid Barton (Aug 24 2020 at 18:58):

so to be explicit, I am suggesting something like

structure relation (D : dom_assign) (α : Type) :=
(schema : finset att)
(rel : tuple D schema → α)

def rel_join (r : relation D α) (r' : relation D α) :     -- for example
relation D α :=
{ schema := r.schema ∪ r'.schema, rel := ... }

def rel_union (r : relation D α) (r' : relation D α) (h : r.schema = r'.schema) :
relation D α :=
{ schema := r.schema, --say
rel := ... }


#### Reid Barton (Aug 24 2020 at 18:59):

now that the schema is not exposed in the type of relations, it won't get in the way of formulating statements like commutativity

#### Robert Brijder (Aug 24 2020 at 19:02):

I see! By bundling the schema you make the types definitially equal. Thank you very much! I will try this.

#### Reid Barton (Aug 24 2020 at 19:04):

Another situation you might think about is an expression like

rel_union
(rel_join r r')
(rel_join r' r)


where rel_union has a type that enforces that the schemas agree.
This expression is valid, but only because of a theorem in propositional logic. So either you have to reject this expression, or extend rel_union to the situation where the schemas might not be equal, or explain to Lean somehow why the expression makes sense.

#### Reid Barton (Aug 24 2020 at 19:05):

This is just to point out that the issue is going to crop up other places besides rel_union_comm.

#### Robert Brijder (Aug 24 2020 at 19:09):

Oh dear, this is a valid expression in the language so I cannot reject this. It is the same problem of non-definitially-equal types again.

#### Reid Barton (Aug 24 2020 at 19:12):

You might also be interested in the CDGA challenge topic (where, probably not by coincidence, addition and multiplication play very similar roles to your union and join).

#### Robert Brijder (Aug 24 2020 at 19:20):

I see, a challenge for

Anyone who doesn't already believe that this will be a mess

And I was thinking formalizing this low-level self-contained paper would be a doable exercise for a beginner like me....

#### Robert Brijder (Sep 02 2020 at 08:57):

Bundling the domain indeed solved my problem: I can now prove that union on relations commutes. However, my proof is very slow using tactics congr' 3 and finish. This seems unnecessary because I can get in a sane and fast way to this state:

att dom : Type,
_inst_1 : setoid att,
D : dom_assign,
K : Type,
_inst_2 : semiring K,
r r' : relation D K,
a : tuple D (r.schema ∪ r'.schema),
a' : tuple D (r'.schema ∪ r.schema),
a_1 : a == a'
⊢ r'.rel (tuple_comp a _) + r.rel (tuple_comp a _) == r'.rel (tuple_comp a' _) + r.rel (tuple_comp a' _)


How do I finish such a goal in a proper way?

#### Robert Brijder (Sep 02 2020 at 08:58):

MWE

import data.set.finite
import init.data.quot
import data.setoid.partition

noncomputable theory
local attribute [instance] classical.prop_decidable

namespace ARA
section ARA

parameters {rel att dom : Type} [setoid att]

def dom_assign := quotient _inst_1 → finset dom
def tuple (D : dom_assign) (X : finset att) := Π (A : (↑X : set att)), (↑(D⟦A⟧) : set dom)
structure relation (D : dom_assign) (K : Type) :=
(schema : finset att)
(rel : tuple D schema → K)
def compat_func {att : Type} [setoid att] {X Y : set att} (φ : X → Y) : Prop :=
∀ x : X, (x : att) ≈ ((φ x) : att)

variables {D : dom_assign} {X X' : finset att} {K : Type} [semiring K]

theorem inclusion_compat (h : X ⊆ X') : compat_func (set.inclusion h) :=
begin
intro x,
refl,
end

theorem compat_att_eq_dom {A B : att} (h: ⟦A⟧ = ⟦B⟧) :
↥(↑(D⟦A⟧) : set dom) = ↥(↑(D⟦B⟧) : set dom) :=
congr rfl (congr_arg coe (congr_arg D h))

theorem func_compat_eq_dom {f : (↑X' : set att) → (↑X : set att)}
(h : compat_func f) (A : (↑X' : set att)) : ⟦(f A : att)⟧ = ⟦(A : att)⟧ :=
begin
apply quotient.eq_rel.mpr,
unfold compat_func at h,
rw set_coe.forall at h,
cases A,
exact setoid.symm' _inst_1 (h A_val A_property),
end

def tuple_comp {f : (↑X' : set att) → (↑X : set att)}
(t : tuple D X) (h : compat_func f) : tuple D X' :=
(λ A, (eq.mp (compat_att_eq_dom (func_compat_eq_dom h A)) (t (f A))))

def rel_union (r r' : relation D K) : relation D K :=
{
schema := r.schema ∪ r'.schema,
rel := (λ t, r.rel(tuple_comp t (inclusion_compat (finset.subset_union_left r.schema r'.schema))) +
r'.rel(tuple_comp t (inclusion_compat (finset.subset_union_right r.schema r'.schema))))
}

instance rel_has_union : has_union (relation D K) := ⟨rel_union⟩

theorem rel_union_comm (r r' : relation D K) : r ∪ r' = r' ∪ r :=
begin
unfold has_union.union,
unfold rel_union,
congr' 1,
rw finset.union_comm,
ext,
rw finset.union_comm,
intros,
conv
begin
to_lhs,
end,
sorry,
end

end ARA
end ARA


#### Kenny Lau (Sep 02 2020 at 10:04):

the solution to heq is not to use heq

#### Robert Brijder (Sep 02 2020 at 16:45):

Kenny Lau said:

the solution to heq is not to use heq

Right. But the problem is that I never use heq in my code. For some reason it is introduced by invoking tactic congr' 1 in my proof. Perhaps I should have used some alternative to congr' 1?

#### Mario Carneiro (Sep 03 2020 at 00:08):

the first step is to prove an extensionality lemma for relation, preferably one that doesn't involve heq

#### Mario Carneiro (Sep 03 2020 at 00:40):

@Robert Brijder

import data.set.finite

noncomputable theory
local attribute [instance] classical.prop_decidable

namespace ARA
section ARA

parameters {rel att dom : Type} [setoid att]

def dom_assign := quotient _inst_1 → finset dom
def tuple (D : dom_assign) (X : finset att) := ∀ A ∈ X, {x : dom // x ∈ D⟦A⟧}

def tuple.sub {D : dom_assign} {X Y : finset att} (H : X ⊆ Y) (T : tuple D Y) : tuple D X :=
λ a h, T a (H h)

-- @[ext]
theorem tuple.ext {D X} {t₁ t₂ : tuple D X}
(H : ∀ (A : att) (h : A ∈ X), (t₁ A h : dom) = t₂ A h) : t₁ = t₂ :=
by ext a h : 3; apply H

structure relation (D : dom_assign) (K : Type) :=
(schema : finset att)
(rel : tuple D schema → K)
def compat_func {att : Type} [setoid att] {X Y : set att} (φ : X → Y) : Prop :=
∀ x : X, (x : att) ≈ ((φ x) : att)

-- @[ext]
theorem relation_ext {D K} (r₁ r₂ : relation D K)
(h₁ : ∀ x, x ∈ r₁.schema ↔ x ∈ r₂.schema)
(h₂ : ∀ (T : tuple D r₂.schema), r₁.rel (T.sub (λ x, (h₁ x).1)) = r₂.rel T) :
r₁ = r₂ :=
begin
cases r₁ with S₁ R₁, cases r₂ with S₂ R₂,
obtain rfl : S₁ = S₂, {ext, apply h₁},
congr, ext T, apply h₂
end

variables {D : dom_assign} {X X' : finset att} {K : Type} [semiring K]

def rel_union (r r' : relation D K) : relation D K :=
{ schema := r.schema ∪ r'.schema,
rel := λ t, r.rel (t.sub $finset.subset_union_left r.schema r'.schema) + r'.rel (t.sub$ finset.subset_union_right r.schema r'.schema) }

instance rel_has_union : has_union (relation D K) := ⟨rel_union⟩

@[simp] theorem rel_union_mem {r r' : relation D K} {x} :
x ∈ (r ∪ r').schema ↔ x ∈ r.schema ∨ x ∈ r'.schema :=
by simp [(∪), rel_union]; refl

@[simp] theorem rel_union_rel {r r' : relation D K} {t} :
(r ∪ r').rel t =
r.rel (t.sub $finset.subset_union_left r.schema r'.schema) + r'.rel (t.sub$ finset.subset_union_right r.schema r'.schema) := rfl

theorem rel_union_comm (r r' : relation D K) : r ∪ r' = r' ∪ r :=
begin
fapply relation_ext,
{ simp [or_comm] },
{ intro, simp [add_comm], refl },
end

end ARA
end ARA


#### Mario Carneiro (Sep 03 2020 at 00:40):

@Simon Hudon The two commented @[ext] lemmas fail with match failed. Do you know what's happening?

#### Simon Hudon (Sep 03 2020 at 01:25):

Can you minimize it?

#### Mario Carneiro (Sep 03 2020 at 01:44):

It's a parameter problem.

import tactic.ext
section

parameters (A : Type)

def tuple (a : A) : Type := sorry

@[ext] theorem tuple.ext {a} {t₁ t₂ : tuple a} : t₁ = t₂ := sorry
-- match failed

end


@Simon Hudon

#### Simon Hudon (Sep 03 2020 at 02:25):

Yes I see. When we call resolve_constant, it calls resolve_name expecting that the result will be a const. Because of the parameter, we get this as a response instead: as_atomic ((«@» tuple) («@» A))

whoa that's new

#### Simon Hudon (Sep 03 2020 at 02:37):

Yeah. I think that's because pre-elaboration terms have much more annotations. What we can do is implement an alternative resolve_constant that checks if resolve_name gives a const and, if not, use e <- to_expr and then use e.get_app_fn.const_name

#### Mario Carneiro (Sep 03 2020 at 02:38):

resolve_name returns a pexpr?

It does

#### Mario Carneiro (Sep 03 2020 at 02:38):

but you already have an expr, don't you?

#### Simon Hudon (Sep 03 2020 at 02:41):

no, it's right after parsing the parameters of ext. They come as a list of names and they're not necessarily fully qualified. We need resolve_constant (and resolve_name) to figure out what their full name is

#### Mario Carneiro (Sep 03 2020 at 02:50):

This works:

meta def resolve_constant' (n : name) : tactic name :=
do e ← resolve_name n,
(expr.const_name ∘ expr.app_fn) <\$> to_expr e tt ff,


#### Mario Carneiro (Sep 03 2020 at 02:51):

resolve_constant is in core though so this will have to be a patch until the next version

#4032

#### Simon Hudon (Sep 03 2020 at 02:58):

I did something similar. In the normal case, we don't need to go through elaboration so I only call to_expr when resolve_constant would crash

#### Simon Hudon (Sep 03 2020 at 03:01):

Oh and I use expr.get_app_fn (which is recursive) instead of expr.app_fn

#### Robert Brijder (Sep 03 2020 at 06:08):

Wow, thank you very much Mario for the rewrite of my code! I am learning a lot from this.

Last updated: May 14 2021 at 06:16 UTC