## Stream: new members

### Topic: Showing wellfoundedness

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

Does this help?

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

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


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

#### Kenny Lau (May 13 2020 at 07:48):

the first def is called finset.image

#### Kenny Lau (May 13 2020 at 07:49):

swap i and m

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

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