Computation with dfinsupp and multisets

Stream: new members

[Tej Chajed]

I'm doing some work that involves a theory over dfinsupp (functions with finite support), which I'm using over finsupp specifically for computation. It looks like I can reduce dfinsupp.support fine, but I was having trouble with multiset.sort. For example, the following theorem doesn't work:

import data.multiset.sort

lemma reduce_multiset_sort :
  multiset.sort (≤) {1, 2, 3} = [1, 2, 3] := rfl.

and furthermore #reduce doesn't work (after a while it produces "(deterministic) timeout"):

#reduce multiset.sort (≤) {1, 2, 3}.

Am I doing something wrong?

[Tej Chajed]

I did just discover that #eval works, which I guess uses the VM instead. Is there a way to access that from tactics (along with other forms of normalization)?

[Mario Carneiro]

when you run code in a tactic it's using the equivalent of #eval

[Mario Carneiro]

if you have access only to the expression you need to use eval_expr to turn it into a multiset and evaluate it

[Tej Chajed]

What I want to do is make one definition be the normalization of another, and ideally I'd know how to do that with unfold/simp/#eval. I thought I'd use a tactic block to do this, but I'm not sure how that would work. I'm basically trying to mimic Coq's eval compute in ....

[Tej Chajed]

I may want to do more metaprogramming in Lean 3, but I'm not able to find much in the way of resources. There is the mathlib generated documentation (eg, https://leanprover-community.github.io/mathlib_docs/init/meta/interactive.html#tactic.interactive.simp), which is helpful, but I'm wondering if there's a resource I don't know about.

[Junyan Xu]

As a subproblem I figured out how to evaluate list.merge_sort:

lemma reduce_list_sort : list.merge_sort (≤) [3,2,1] = [1,2,3] :=
begin
  iterate 2 { rw list.merge_sort_cons_cons, swap, refl },
  simp only [list.merge_sort],
  /- `refl` should work here if `list.merge` reduces nicely -/
  rw [list.merge, if_neg],
  simp only [list.merge],
  { refl },
  { dec_trivial },
end

I understand that docs#list.merge_sort is defined using well-founded recursion so we need to rewrite by non-defeq equational lemmas, but I'm surprised that docs#list.merge also behave similarly. Indeed when I #print list.merge._main._pack I see has_well_founded.wf.fix in it. Surely we can redefine list.merge to have good reduction behavior?

[Junyan Xu]

For reduce_multiset_sort you can start with change list.merge_sort (≤) [1,2,3] = _, but I haven't found a short and automatic way to do it.

[Eric Rodriguez]

does dec_trivial not work?

[Junyan Xu]

It doesn't.

[Mario Carneiro]

IIRC there is a set_option you can use to force unfolding lemmas to make dec_trivial work on wf recursions

[Junyan Xu]

By the way when I do simp [list.merge_sort, list.merge], dsimp,it reduces to something involving and.rec that doesn't seem to reduce further.

[Mario Carneiro]

I think it would be simpler to just prove the result is sorted and a permutation of the input

[Eric Rodriguez]

lemma reduce_list_sort : list.merge_sort (≤) [3,2,1] = [1,2,3] :=
begin
  refine list.eq_of_perm_of_sorted _ (list.sorted_merge_sort (≤) [3, 2, 1]) _,
  refine (list.perm_merge_sort _ _).trans _,
  dec_trivial,
  dec_trivial,
end

[Eric Rodriguez]

works for me

[Mario Carneiro]

^ that

[Junyan Xu]

Oh I see that wf.fix is used essentially, because in | (a :: l) (b :: l') := if r a b then a :: merge' l (b :: l') else b :: merge' (a :: l) l' only one of the two arguments becomes smaller, so maybe we can't make list.merge reduce nicely.

Eric's solution is nice, but docs#list.decidable_perm seems to be quadratic rather than linear, so it would be nicer if list.merge_sort could compute.

[Junyan Xu]

I forgot that double induction is actually easy to make computable; the following works:

namespace list

variables {α : Type*} (r : α → α → Prop) [decidable_rel r]
include r
def merge' (l : list α) : list α → list α :=
begin
  induction l with a l fl,
  { exact id },
  { intro l',
    induction l' with b l' fl',
    { exact a :: l },
    { exact if r a b then a :: fl (b :: l') else b :: fl' } },
end

lemma merge'_nil_left (l : list α) : merge' r [] l = l := rfl
lemma merge'_nil_right (l : list α) : merge' r l [] = l := by cases l; refl
lemma merge'_cons_cons (a b) (l l' : list α) : merge' r (a :: l) (b :: l') =
  if r a b then a :: merge' r l (b :: l') else b :: merge' r (a :: l) l' := rfl

#print merge'
/- list.rec id
    (λ (a : α) (l : list α) (fl : list α → list α) (l' : list α),
       list.rec (a :: l) (λ (b : α) (l' fl' : list α), ite (r a b) (a :: fl (b :: l')) (b :: fl')) l')
    l -/

end list

[Junyan Xu]

I've found some old discussions about stuck terms involving acc.rec and about acc being inefficient to compute with in the kernel of Lean and Coq. Presumably the stuck term makes docs#well_founded.fix_F_eq not a rfl lemma. Maybe there's something in Mario's thesis as well. So there's still no satisfying solution to this?

[Junyan Xu]

Interestingly, Lean can realize that fix_F_eq is defeq if we insert an id:

namespace well_founded
universes u v
variables {α : Sort u} {r : α → α → Prop}
local infix `≺`:50    := r
variable {C : α → Sort v}
variable F : Π x, (Π y, y ≺ x → C y) → C x

lemma fix_F_eq' (x : α) (acx : acc r x) :
  fix_F F x acx = F x (λ (y : α) (p : y ≺ x), fix_F F y (acc.inv acx p)) :=
by { change fix_F F x (acc.intro x $ λ y, acx.inv) = _, refl }
/- The original proof: acc.drec (λ x r ih, rfl) acx -/
/- by { dsimp only [← acc.eq_intro_inv], refl } doesn't work, where
  lemma acc.eq_intro_inv (x : α) (acx : acc r x) : acc.intro x (λ y, acx.inv) = acx := rfl -/

#print fix_F_eq' /- id (eq.refl (fix_F F x (acc.intro x (λ (y : α), acx.inv)))) -/

end well_founded

[Junyan Xu]

I'm confused upon reading issue 1803. From the discussion it seems well-founded recursion should actually compute, contrary to what I observed in fix_F_eq, which doesn't seem to involve anything like propext or choice that causes a term to be stuck. Has anything changed since then? It seems to be a fairly recent issue (as far as official Lean3 is concerned).
(Update: from this other issue it seems computation isn't supposed to work: "a function application f a b cannot be reduced definitionally (using the equational lemmas) if f was defined by well founded recursion.")

[Junyan Xu]

Another example of defeq non-transitivity could be extracted from my previous post:

namespace well_founded
universes u v
variables {α : Sort u} {r : α → α → Prop}
local infix `≺`:50    := r
variable {C : α → Sort v}
variable F : Π x, (Π y, y ≺ x → C y) → C x

lemma fix_F_eq0 (x : α) (acx : acc r x) :
  fix_F F x acx = fix_F F x (acc.intro x $ λ y, acx.inv) := rfl

lemma fix_F_eq1 (x : α) (acx : acc r x) :
  fix_F F x (acc.intro x $ λ y, acx.inv) = F x (λ y p, fix_F F y $ acx.inv p) := rfl

lemma fix_F_eq2 (x : α) (acx : acc r x) :
  fix_F F x acx = F x (λ y p, fix_F F y $ acx.inv p) := rfl /- fails -/

end well_founded

[Junyan Xu]

It's a bit mysterious why the following doesn't work; is it because of some special support for acc.rec?

namespace acc
variables {α : Sort*} {r : α → α → Prop} {C : α → Sort*} (x : α) (acx : acc r x)
variable F : Π x, (Π y, r y x → C y) → C x
lemma rec_eq0 : acx.rec (λ y _, F y) = (acc.intro x $ λ y, acx.inv).rec (λ y _, F y) := rfl /- fails -/
end acc

set_option pp.all true show the two sides agree except for the proof of acc r x.
lemma eq_intro : acx = acc.intro x (λ y, acx.inv) := rfl works without problem.