Function on equal types

Stream: new members

[Robert Brijder]

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]

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]

oh that looks like trouble coming

[Mario Carneiro]

equality of types is a Bad Thing

[Robert Brijder]

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]

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

[Kevin Buzzard]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kenny Lau]

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

[Kenny Lau]

instead of just avoiding it like the plague

[Kenny Lau]

is this infeasible?

[Kenny Lau]

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

[Robert Brijder]

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]

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]

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]

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]

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]

You might want to look at docs#holor

[Robert Brijder]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Reid Barton]

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]

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

[Robert Brijder]

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]

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]

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]

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

[Reid Barton]

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

[Robert Brijder]

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]

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

[Reid Barton]

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]

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]

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

[Reid Barton]

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]

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

[Robert Brijder]

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]

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]

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]

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]

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]

the solution to heq is not to use heq

[Robert Brijder]

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]

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

[Mario Carneiro]

@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]

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

[Simon Hudon]

Can you minimize it?

[Mario Carneiro]

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]

@Simon Hudon

[Simon Hudon]

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]

whoa that's new

[Simon Hudon]

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]

resolve_name returns a pexpr?

[Simon Hudon]

It does

[Mario Carneiro]

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

[Simon Hudon]

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]

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]

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

[Simon Hudon]

#4032

[Simon Hudon]

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]

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

[Robert Brijder]

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