Zulip Chat Archive

Stream: new members

Topic: Showing wellfoundedness


view this post on Zulip Patrick Stevens (May 12 2020 at 06:03):

I've got the following definition of the set of all powers of a given prime dividing a given n (where I have actually filled in the sorry but I don't think it's relevant to my question):

def powers_dividing (p : nat) [is_prime : nat.prime p] : Π (n : nat) (pos : 0 < n), finset nat
| n n_pos :=
  let p_pos : 1 < p := nat.prime.one_lt is_prime in
  have n / p < n, from nat.div_lt_self n_pos p_pos,
  dite (p  n)
    (λ p_div_n,
      have pos : 0 < n / p, by sorry,
      insert 1 (finset.map (times_p p (nat.prime.pos is_prime)) (powers_dividing (n / p) pos))
    )
    (λ _, finset.singleton 1)

Lean complains that it can't prove the powers_dividing recursive call to be following a wellfounded relation; it ends up trying to show that 0 < 0, which I think I agree is not possible. But I don't see why it's trying to show that; I may have just woken up, but I think I've shown everything that's required for this function to be well-defined (namely that in the recursive case, we have strictly decreased the first argument while still providing a term pos for the second argument). Have I missed something?

view this post on Zulip Kevin Buzzard (May 12 2020 at 06:37):

Does this help?

view this post on Zulip Patrick Stevens (May 12 2020 at 06:43):

Witchcraft, thanks - this was the "Conjecture : this is because the type of h depends on n and the equation compiler can only synthesize useful relations on non dependent products" case.

view this post on Zulip Patrick Stevens (May 13 2020 at 07:43):

What's my quickest path to victory with the following wellfounded induction that Lean can't prove is wellfounded? It refuses both recursive calls, because it gets stuck trying to prove e.g. that m + succ i < succ m + succ i. Writing inside this tactic context is quite a bit harder than writing in a normal context, I seem to be getting no help from Lean at all.

def freely_map {A B : Type*} [decidable_eq B] (f : A  B) : finset A  finset B
| s :=
  finset.fold (λ a b, a  b) finset.empty (λ a, finset.singleton (f a)) s

def subs_of_size : Π (m : nat) (i : nat), finset (finset nat)
| 0 i := finset.singleton finset.empty
| (nat.succ m) 0 := finset.singleton finset.empty
| (nat.succ m) (nat.succ i) :=
    let from_lower := (subs_of_size m (nat.succ i)) in
    let from_upper := (freely_map (λ j, insert i.succ j) (subs_of_size (nat.succ m) i)) in
    from_lower  from_upper
using_well_founded {
  rel_tac := λ _ _, `[exact  _, measure_wf (λ  x1, x2  , x1 + x2)],
}

view this post on Zulip Patrick Stevens (May 13 2020 at 07:47):

(I'm aware that my definition is not actually the subsets of [0..m] of size i - I'll cross that bridge when I come to it)

view this post on Zulip Kenny Lau (May 13 2020 at 07:48):

the first def is called finset.image

view this post on Zulip Kenny Lau (May 13 2020 at 07:49):

swap i and m

view this post on Zulip Patrick Stevens (May 13 2020 at 07:57):

Ah, and there I was with fifty lines of proof that

lemma freely_map_is_map
  {A B : Type*} [decidable_eq A] [decidable_eq B]
  {f : A  B}
  (x : B)
  :  (s : finset A), ( (x : B), x  (freely_map f s)   y, y  s  f y = x)
  := by sorry

Good practice, probably

view this post on Zulip Patrick Stevens (May 13 2020 at 07:58):

In fact when I get the definition of subs_of_size expressing what I actually intended it to express, Lean is able to show that it's wellfounded


Last updated: May 15 2021 at 00:39 UTC