Zulip Chat Archive

Stream: general

Topic: evaluating proofs?

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?

Mario Carneiro (Dec 12 2018 at 01:21):

the axiom of choice is definitely nonconstructive

Mario Carneiro (Dec 12 2018 at 01:21):

You can evaluate proofs by using #reduce

Kenny Lau (Dec 12 2018 at 01:21):

the axiom of choice is definitely nonconstructive

even unsound?

Mario Carneiro (Dec 12 2018 at 01:22):

no...

Mario Carneiro (Dec 12 2018 at 01:22):

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

Mario Carneiro (Dec 12 2018 at 01:22):

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

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)

Mario Carneiro (Dec 12 2018 at 01:23):

Not in the VM

Kenny Lau (Dec 12 2018 at 01:23):

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

Kenny Lau (Dec 12 2018 at 01:23):

why not?

Mario Carneiro (Dec 12 2018 at 01:23):

because that term has no representation in the VM

Mario Carneiro (Dec 12 2018 at 01:23):

it is a neutral value, a "unit"

Kenny Lau (Dec 12 2018 at 01:24):

so reduce is not VM?

Mario Carneiro (Dec 12 2018 at 01:24):

it is kernel reduction

Kenny Lau (Dec 12 2018 at 01:24):

interesting

Last updated: Dec 20 2023 at 11:08 UTC