Zulip Chat Archive

Stream: new members

Topic: best way to prove


view this post on Zulip Arjun Pitchanathan (Mar 03 2020 at 02:49):

What's the best way to prove this? I have a proof (strong induction on l1.length) but it's upwards of a hundred lines...

import data.list
noncomputable theory
open_locale classical
universe u
variables (α β : Type u)
example {l₁ l₂ : list β} {r : α  β  Prop} (nodup :  (x y : α) (b : β),
    x  y  ¬ (r x b  r y b)) : ( a : α, l₁.countp (r a) = l₂.countp (r a)) 
    l₁.countp (λ b,  a, r a b) = l₂.countp (λ b,  a, r a b) := sorry

view this post on Zulip Bryan Gin-ge Chen (Mar 03 2020 at 19:56):

I took a crack at this but I wasn't able to succeed. Can you post your proof or link to a gist?

view this post on Zulip Arjun Pitchanathan (Mar 03 2020 at 20:33):

Here it is. I'm not sure how readable it is. I tried to add some explanatory comments.


Last updated: May 08 2021 at 19:11 UTC