# Zulip Chat Archive

## 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

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

See also the playlist at https://www.youtube.com/watch?v=8mVOIGW5US4&list=PLlF-CfQhukNlxexiNJErGJd2dte_J1t1N

#### 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 `relation`

s 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 `relation`

s 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

`relation`

s 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,
rw add_comm,
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
```

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

@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))`

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

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?

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

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

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

#### 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