Zulip Chat Archive

Stream: general

Topic: evaluating proofs?


view this post on Zulip Kenny Lau (Dec 12 2018 at 01:20):

@Mario Carneiro I think you said that it is possible to evaluate proofs... do you have an example? can we also break proof irrelevance? maybe have an unsound but computable non-classical.some?

view this post on Zulip Mario Carneiro (Dec 12 2018 at 01:21):

the axiom of choice is definitely nonconstructive

view this post on Zulip Mario Carneiro (Dec 12 2018 at 01:21):

You can evaluate proofs by using #reduce

view this post on Zulip Kenny Lau (Dec 12 2018 at 01:21):

the axiom of choice is definitely nonconstructive

even unsound?

view this post on Zulip Mario Carneiro (Dec 12 2018 at 01:22):

no...

view this post on Zulip Mario Carneiro (Dec 12 2018 at 01:22):

wait, I don't think I understand what you are asking

view this post on Zulip Mario Carneiro (Dec 12 2018 at 01:22):

it's easy to compute a value if you are allowed to be wrong

view this post on Zulip Kenny Lau (Dec 12 2018 at 01:23):

so I want a function that reduces to 0 when given the input (⟨0, rfl⟩ : ∃ n, n = n)

view this post on Zulip Mario Carneiro (Dec 12 2018 at 01:23):

Not in the VM

view this post on Zulip Kenny Lau (Dec 12 2018 at 01:23):

#reduce (0, rfl :  n, n = n) -- Exists.intro 0 (eq.refl 0)

view this post on Zulip Kenny Lau (Dec 12 2018 at 01:23):

why not?

view this post on Zulip Mario Carneiro (Dec 12 2018 at 01:23):

because that term has no representation in the VM

view this post on Zulip Mario Carneiro (Dec 12 2018 at 01:23):

it is a neutral value, a "unit"

view this post on Zulip Kenny Lau (Dec 12 2018 at 01:24):

so reduce is not VM?

view this post on Zulip Mario Carneiro (Dec 12 2018 at 01:24):

no

view this post on Zulip Mario Carneiro (Dec 12 2018 at 01:24):

it is kernel reduction

view this post on Zulip Kenny Lau (Dec 12 2018 at 01:24):

interesting


Last updated: May 14 2021 at 06:16 UTC