Stream: Coq users

Topic: use Qed for Acc proofs?


view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:03):

https://github.com/coq/coq/pull/15254

Let's continue the discussion here.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:11):

re Opaque doesn’t work: Opaque foo is not equivalent to Qeding foo’s body (and it can’t be: removing the definitional equality could make existing terms ill-typed), and it doesn’t prevent all tactics from seeing through foo’s definition (and it could, except for backward compatibility).

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:12):

I think both reflexivity and apply ignore opacity; compute respects it, but vm_compute ignores it.

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:12):

But Opaque isn't meant to be a Qed.

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:12):

Sometimes people use Qed trickery inside proofs to stop unfolding

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:12):

Opaque allows this and to keep definitional equalities

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:13):

The performance however can be poor

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:13):

Qed isn't really any different to an axiom

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:13):

I’m not discussing performance, just information hiding.

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:13):

I'm not sure I fully understand Pierre-Marie's position though. Is it OK to be transparent everywhere for well_founded as long as you're not using tactics? For example, if I wrote all my proofs like this I could/should be transparent?

Theorem op_inv_r_ex
  :  forall x : E, exists y : E, op_is_inv_r x y.
Proof
  fun x
    => ex_ind
         (fun (y : E) (H : op_is_inv_l x y)
           => ex_intro
                (op_is_inv_r x)
                y
                (H || a = 0 @a by op_is_comm x y))
         (op_inv_l_ex x).

(https://github.com/llee454/functional-algebra/blob/master/abelian_group.v#L191-L201)

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:14):

@Ali Caglayan I agree Opaque isn’t Qed, but I challenge you to give a specification that is (a) reasonable (b) correct for the current implementation.

view this post on Zulip Gaëtan Gilbert (Nov 28 2021 at 14:16):

Proof with a term is Qed though ;)

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:17):

I was not aware that was even possible!

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:18):

OK, but let's say then:

Theorem op_inv_r_ex
  :  forall x : E, exists y : E, op_is_inv_r x y.
Proof.
 refine (fun x
    => ex_ind
         (fun (y : E) (H : op_is_inv_l x y)
           => ex_intro
                (op_is_inv_r x)
                y
                (H || a = 0 @a by op_is_comm x y))
         (op_inv_l_ex x)).
Defined.

Is this what we should be doing?

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:19):

You can also just make that a definition and inline it completely. The line between definition and theorem isn't so clear. Just an arbitrary syntactic restriction IMO

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:19):

indeed, the only downside is you can’t stick to the Theorem keyword (but there’s a CEP for that).

view this post on Zulip Gaëtan Gilbert (Nov 28 2021 at 14:19):

personnally I don't mind Defined with tactics

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:19):

Karl: at least, proof terms or safe tactics are necessary for Defined for information hiding. There might be performance questions.

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:20):

The performance issues don't really arise unless you are really unfolding the opaque terms.

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:21):

For example, in the HoTT library almost all our definitions/theorems etc. are Defined. There are a few places where we explicitly mark things as opaque to discourage coq from uselessly unfolding large proof terms.

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:21):

I think the main reason to even introduce Qed opaqueness was to lower memory use, i.e., don't keep proof terms in memory etc.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:22):

I was talking about Defined, not Defined + Opaque, Ali.

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:22):

Paolo Giarrusso said:

Ali Caglayan I agree Opaque isn’t Qed, but I challenge you to give a specification that is (a) reasonable (b) correct for the current implementation.

@Paolo Giarrusso Sorry I have misunderstood. What are you asking here?

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:22):

HoTT is special since Qed isn’t reasonable there, and even then Opaque is probably not the perfect tool.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:23):

@Ali Caglayan a formal semantics for Opaque :-)

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:24):

if I wanted to use features that work 50%, 70%, 90% of the time, I’d program PHP.

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:24):

Isn't it supposed to be an explicit flag for reductions that do delta, saying "please don't unfold me until you get stuck"?

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:24):

I'm just looking for some heuristics that work for most ordinary libraries / verification projects, HoTT is neither of those

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:25):

“until you get stuck”? that sounds like simpl never — which is misnamed since simpl never definitions will be unfolded by simpl if forced by a surrounding match.

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:25):

for example, if you don't use Qed you can't get the benefits of vio/vos/vok. And your memory use will be through the roof for long files, ruling out using x32 (32-bit pointer) Coq which is much faster in CI than regular 64-bit Coq.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:26):

just to clarify what I mean by “information hiding”:

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:27):

changes to Qed proofs are safe _because nobody else can depend on the details_. That’s information hiding, and that’s useful when maintaining large projects.

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:28):

a.k.a abstraction barrier

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:28):

Right but Qed has two uses:

  1. stopping definitions from being unfolded (because they simply can't)
  2. using proofs like an axiom

I think opaque is trying to do the first no?

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:29):

right, but then why can apply bar unfold foo if needed for typechecking? Answer: this is a bug, but it’s hard to fix for backward compatibility.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:30):

but I agree Opaque is _trying_ something like that, but it’s failing, and then my instinct is to reach for a flamethrower :-|.

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:31):

Do you have an example where apply unfold Qed?

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:31):

Also does this happen if the Qed is imported from a module or if it is in the same module?

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:31):

no it unfolds Opaque

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:32):

Yes that is intended

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:32):

Opaque just delays the priority of unfolding

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:32):

Which is great if you have some big fat proof terms that are useless during a proof

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:33):

But there are still real situations where this fat proof term needs to be compared later, which is where Qed doesn't fit the bill

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:35):

However coming back to the original topic, I don't have too much experience with Acc but since people have been coming up with tricks to hide large proof terms (for performance reasons). I suspect that using Qed for those parts is fine.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:35):

“delay priority” is what Strategy is for, AFAIK.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:36):

I wasn’t aware that eauto ignored Opaque https://github.com/coq/coq/issues/11502, I’m less surprised by inversion https://github.com/coq/coq/issues/10920…

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:36):

across MathComp itself, fourcolor and odd-order there are fewer than 10 Defined

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:36):

The question is, are these Props or Types?

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:36):

to me, this is a strong signal that Defined is mostly for foundational research stuff, not for formalizing math or program verification

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:37):

Since Prop is intended to be proof-irrelevant there is no harm in making every Prop Qed, until you start comparing proofs which is why UIP appears. This can be avoided (I think) with SProp.

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:38):

<s>On the other hand, Acc really isn't a Prop</s>

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:39):

so the question of using Qed seems to be a trial-and-error thing.

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:39):

that seems like Coq metatheory to me. Acc is a Prop inside Coq.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:39):

but it’s as much as Prop as eq, right? Both enjoy subsingleton elimination, which is why this question arises

view this post on Zulip Gaëtan Gilbert (Nov 28 2021 at 14:39):

Ali Caglayan said:

On the other hand, Acc really isn't a Prop

what

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:40):

Nevermind I misremembered

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:42):

I got confused with the Equations version. Anyhow, I don't know much about Acc. I just wanted to share some thoughts about Qed.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:43):

(here’s apply vs Opaque https://github.com/coq/coq/issues/9135#issue-387409471)

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:43):

unfortunately it's all connected. I try to use Qed whenever I can but well_founded and Qed prevents some simple reductions. But if Coq devs are blessing the well_founded reduction trick (2^32 unfoldings OK), then I think we can go (nearly) full Qed.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:43):

@Karl Palmskog but for a more radical question, do you have transparent well-founded definitions?

view this post on Zulip Gaëtan Gilbert (Nov 28 2021 at 14:43):

there's no general trick for eq though

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:44):

Paolo Giarrusso said:

(here’s apply vs Opaque https://github.com/coq/coq/issues/9135#issue-387409471)

Oh I remember reading that. It's weird that it's only for compatibility for CoRN

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:44):

so far I use Defined for well-founded definitions usually. But trying to figure out whether to change that.

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:45):

I think the eq opaque issue comes up less frequently than well-foundedness though?

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:46):

At least for eq there is a canonical proof

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:46):

Is there one for Acc? I don't think so...

view this post on Zulip Gaëtan Gilbert (Nov 28 2021 at 14:47):

Ali Caglayan said:

At least for eq there is a canonical proof

is there?

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:47):

reflexivity no?

view this post on Zulip Gaëtan Gilbert (Nov 28 2021 at 14:47):

but you can't plug in refl when reducing some arbitrary thing

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:49):

I don’t see anybody proposing that?

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:50):

in that respect, SProp is much better behaved

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:50):

For Acc, there’s the “unfolding trick” we’ve referenced without explaining, which works for concrete computations; I agree eq won’t block computation unless you really use indexed types, and even there you can often use a proof of K (for types with decidable equality).

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:50):

also, there is a trick for opaque equality but it's not universal

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:51):

if you only eliminate decidable equalities you're safe

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:51):

(so essentially use SProp undercover)

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:51):

some may recall this on the general problem of evaluation/opaqueness in program verification: http://gallium.inria.fr/blog/coq-eval/ ("Using Coq's evaluation mechanisms in anger")

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:51):

So let's say we had two vectors Vector.t (n + m) and Vector.t (m + n). We show that there is a conversion function, but we use a Qed commutativity proof. If we plug in a closed term, it won't compute since there is a Qed. But if your reduction could turn the Qed proof into refl would there be any problem?

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:52):

let's say we had two vectors

IMO you've already lost by tthat point

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:53):

I'm not following?

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:53):

using dependent types is frowned upon by a good chunk of the Coq community

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:53):

instead, the mathcomp way seems to scale much more

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:54):

can we remember Ali’s work has different tradeoffs?

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:54):

(and it will probably be even better when SProp is properly handled by tactics unification and whatnot)

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:54):

Pierre-Marie Pédrot said:

using dependent types is frowned upon by a good chunk of the Coq community

Honestly I am surprised anyone would claim this

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:55):

Ali: basically Coq-HoTT and Coq are disjoint ecosystems with somewhat disjoint heuristics.

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:56):

Indeed, HoTT (and even more unimath) are doing things that are very non-standard compared to your average Coq development

view this post on Zulip Ali Caglayan (Nov 28 2021 at 14:56):

Right, I do work a lot in HoTT where these things are important. But I do not agree that dependent types are useless in plain Coq.

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:56):

but the mathcomp approach could also be used in the HoTT world, it's not incompatible

view this post on Zulip Karl Palmskog (Nov 28 2021 at 14:57):

MathComp does not use much dependent/indexed types, and if I recall correctly Adam Chlipala wrote his nearly dependent/indexed types free book (http://adam.chlipala.net/frap/) partly in response to seeing student disasters with dependent types

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:57):

well, obviously you critically need dependent types to prove anything, but the point is that you should flee away from indexed types

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:57):

Back on track: the magical-refl stuff is essentially what SProp does

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:57):

(so my colorful comments against Opaque are not addressed at all at Coq-HoTT)

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:58):

but SProp (without the dreaded UIP flag) only lets you eliminate when the equality is decidable essentially

view this post on Zulip Kenji Maillard (Nov 28 2021 at 14:59):

Ali Caglayan said:

So let's say we had two vectors Vector.t (n + m) and Vector.t (m + n). We show that there is a conversion function, but we use a Qed commutativity proof. If we plug in a closed term, it won't compute since there is a Qed. But if your reduction could turn the Qed proof into refl would there be any problem?

You could achieve something along these lines using equality witnesses in SProp: once n,m are instantiated by concrete natural numbers your "non-reducing" equality proofs will become convertible.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 14:59):

@Pierre-Marie Pédrot could one use SAcc in SProp? I never learned the exact SProp restrictions…

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:59):

I love SProp because it clearly exposes the issues with Prop, namely singleton elimination

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:59):

@Paolo Giarrusso nope

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:59):

and that's not a bug but a feature

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:59):

there are three archetypal singleton in Prop: False, eq and Acc

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 14:59):

but in SProp only False is eliminable

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:00):

Acc breaks decidability of type-checking, and eq is sulphurous

view this post on Zulip Ali Caglayan (Nov 28 2021 at 15:00):

Pierre-Marie Pédrot said:

there are three archetypal singleton in Prop: False, eq and Acc

Are you saying there is a canonical proof of Acc?

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:00):

but then given an seq I can’t even subst it in Type

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:00):

@Ali Caglayan no, that you can eliminate a proof of Acc to produce something that lives in Type

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:01):

@Ali Caglayan because it has a single constructor, and that’s enough for subsingleton elimination

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:01):

@Paolo Giarrusso yes, you can precisely when the equality is decidable

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:01):

so SProp is a way to clearly delineate the stuff that is relevant

view this post on Zulip Karl Palmskog (Nov 28 2021 at 15:02):

so for regular Coq libraries, should one switch to SProp everywhere? Or how would Prop and SProp ideally coexist?

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:02):

Hard to tell, but there are people working on that.

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:02):

Prop does many things at the same time.

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:02):

For instance, for extraction you definitely want Acc to be erased

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:03):

Also the current support for SProp is terrible (and I can personally testify)

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:03):

is SProp not erasable?

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:03):

remember the good old 8.5 days when you would get random universe errors at Qed because of broken univpoly tactics? Basically that's where we're at with SProp.

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:04):

SProp is erasable indeed

view this post on Zulip Karl Palmskog (Nov 28 2021 at 15:04):

and SProp is not in MetaCoq yet, right? I was hoping to have erasure inside Coq.

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:04):

hm, it's at least partially there

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:05):

I don't know what you mean by "erasure inside Coq" but it's probably never going to satisfy you

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:05):

erasure is not -- and never will be -- type-preserving in CIC

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:05):

@Pierre-Marie Pédrot so don’t erase to CIC?

view this post on Zulip Karl Palmskog (Nov 28 2021 at 15:05):

I meant something very operational, defining a sigma type and then just getting a function that has the computational part and a separate lemma that the function output has the property

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:06):

so we’re talking of Eval untyped_vm_compute in foo I guess?

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:06):

well then this is not correct in general, you may write partial program translations for that but it will never be total

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:06):

I know Lean does that, but it's utter nonsense

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:06):

you can get real garbage, typically when going under inconsistent contexts

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:07):

but if you want to do it externally you already have extraction

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:07):

I am not sure what use case you have in mind, actually

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:07):

thanks for reminding me I’m talking about _evaluation_ not normalization :-)

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:08):

so, imagine foo is a closed term of “ground” type — say nat, but even a Coq/mathcomp Vector — and I want to get the concrete value.

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:08):

you mean head normalization? That's already problematic enough

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:09):

what's this value for exactly?

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:09):

I mean evaluation, as for OCaml. I’d be happy if this used extraction maybe, as long as it’s seamless.

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:10):

I repeat: what do you need this value for?

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:10):

just printing on the toplevel?

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:10):

Yes

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:10):

well, then probably you could hack something with the extraction or so

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:11):

but then the problem still holds that this value is essentially unrelated to the original term if you happened to erase anything there

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:11):

to be clear, the example use-case is that I wrote a program in Coq and I want to test it on a concrete input to look at the result :-)

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:11):

OK, so this is UI problem, not a kernel one

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:12):

we could even peek into Qed proofs for this evaluator

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:12):

yep! I never talked about the kernel… and I wonder if this is _one_ of the things that Lean does

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:15):

the only _other_ thing I can imagine (again, purely UX-level) is asserting the result coincides with some other value… Eval untyped_vm_compute (or whatever) in (foo =? expected) =? true.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:15):

as long as the command has hardcoded support for comparing booleans, it’s good.

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:16):

what if the program uses an axiom?

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:16):

and peeking into Qed or such would be nice if I wanted to look through locked terms.

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:17):

well, the semantics I’d hope for are (untyped/weakly typed) extraction + execution: the axiom would extract as throw “not_implemented” or such?

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:18):

I hope this means that axioms/Qed on Acc/eq aren’t a problem

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:18):

well not always, but a sensible variant

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:19):

hm, but then if you just had unfolding of Qed + clever evaluation of singleton eliminations, you'd also get what you want, am I wrong?

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:19):

Axiom nope : bool = nat probably wouldn’t work, but an axiom/admitted proof in the size of a vector should probably be erased first?

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:20):

(assuming you only care about Prop erasure)

view this post on Zulip Pierre-Marie Pédrot (Nov 28 2021 at 15:21):

obviously this would be incompatible with any fancy axiom like univalence but well you can't have it both ways

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:21):

depends on “clever evaluation” and details are tricky, but “extraction to realizers” should be the right spec…

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:22):

I agree the answer is (likely) yes if you’re willing to do the Lean thing here

view this post on Zulip Paolo Giarrusso (Nov 28 2021 at 15:24):

IMHO, if people want to replace n: a = b by refl automatically, they’re probably talking of CBV evaluation of realizers, even if they might not know any of those words.


Last updated: Jan 29 2023 at 06:02 UTC