Showing wellfoundedness

Stream: new members

[Patrick Stevens]

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?

[Kevin Buzzard]

Does this help?

[Patrick Stevens]

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.

[Patrick Stevens]

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)⟩],
}

[Patrick Stevens]

(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)

[Kenny Lau]

the first def is called finset.image

[Kenny Lau]

swap i and m

[Patrick Stevens]

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

[Patrick Stevens]

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