I'm interested in getting typing derivations that don't rely on the SN axiom (ideally that don't rely on axioms at all). Would it be reasonable to factor the checker into first a fueled version that returns a sum of either a typing derivation, or a function from Acc to typing derivations, with the idea being that it first uses fuel, and then used Acc when it runs out; and then a version that just plugs the axiom into this to merge the results?

I thought that the acc-intro hack (pile n acc-intro on top of the axiom) was basically providing a fueled version (in the sense that if you obtain a complete derivation then the axiom won't be present). Am I missing something ?

You need to reduce the derivation enough to make the axiom go away. If the derivation cannot be fully reduced in `vm_compute`

(because, e.g., there are `Qed`

-opaque intermediates, or functions present in the fully reduced term, or the fully reduced term is too big because inductives are quadratically-sized in their indices/parameters), then you have to very carefully reduce the right parts enough to see that the axiom goes away, but not so much that you blow up reduction

It also means you can't use the hack where you get a thing of type `T`

by having `f args : option T`

, proving that `g : (if f args then true else false) = true -> T`

and then getting a thing of type `T`

by doing `g (eq_refl true <: _)`

, because `g`

is still going to mention the axiom even if it's eventually computed away.

(This doesn't matter for type inference, but it does matter for accessing the typing derivation, which does not seem to actually be vm_computable)

Why use `vm_compute`

? I would use `lazy`

precisely not to unfold stuff I don't need to.

Because then I need to whitelist or blacklist the identifiers to be (not) unfolded, and this sort of stuff is in general near-impossible to debug when you're missing any identifier, because the intermediate terms are huge.

Can you do something like this and not implement the function twice? If so, I would say this is an improvement onto the acc-intro hack, by replacing the hidden, hardcoded fuel into a more transparent one

Yes, it should be possible

I'm not super-familiar with the infrastructure, and would appreciate some help figuring out where to start (somewhere around `reduce_stack_full`

?) and how to interface with Equations, but the basic idea is like this:

```
Require Import Coq.Program.Program.
Require Import Coq.micromega.Lia.
Require Import Coq.Init.Wf.
Local Set Implicit Arguments.
Variant PartiallyFueled (R : Prop) A := finished (_ : A) | needs_acc (_ : R -> A).
Arguments finished {_ _} _.
Definition ret {R A} : A -> PartiallyFueled R A := finished.
Definition bind {R A A'} (v : PartiallyFueled R A) (k : A -> PartiallyFueled R A') : PartiallyFueled R A'
:= match v with
| finished v => k v
| needs_acc f
=> needs_acc (fun acc => match k (f acc) with
| finished v => v
| needs_acc f' => f' acc
end)
end.
Definition fully_fuel {R : Prop} {A} (r : R) (v : PartiallyFueled R A) : A
:= match v with
| finished v => v
| needs_acc f => f r
end.
Notation "x <- c1 ;; c2" := (@bind _ _ _ c1 (fun x => c2))
(at level 100, c1 at next level, right associativity).
Definition Fix_fueled_F {A} {R : A -> A -> Prop} (P : A -> Type)
(F : forall x : A, (forall y : A, R y x -> PartiallyFueled (well_founded R) (P y)) -> PartiallyFueled (well_founded R) (P x))
: forall (x : A) (fuel : nat), PartiallyFueled (well_founded R) (P x)
:= fix Fix_fueled_F (x : A) (fuel : nat) : PartiallyFueled (well_founded R) (P x)
:= F x (fun y _ => match fuel with
| O => needs_acc (fun rwf => @Fix A R rwf P (fun x f => fully_fuel rwf (F x (fun y h => finished (f y h)))) y)
| S fuel' => Fix_fueled_F y fuel'
end).
#[program]
Definition fib (n : nat) : PartiallyFueled (well_founded lt) nat
:= @Fix_fueled_F
nat lt (fun _ => nat)
(fun n fib => match n with
| 0 => ret 1
| 1 => ret 1
| S (S n) => (fn <- fib n _;; fsn <- fib (S n) _;; ret (fn + fsn))
end)
n 100.
Axiom ltwf : well_founded lt.
Compute fully_fuel ltwf (fib 10). (* 89 *)
```

The idea is that you do everything inside this monad that tracks whether or not you need the well-founded proof. When you're doing the computational work, you use the monad to abstract away whether you're in fuel-land or acc-land. When you're tying everything together, there's a general fixpoint combinator that basically says "use fuel until you're out; then switch to using well-founded". It's a little bit ugly in that everything happens inside this monad, and I don't really see a way to make the fuel go away in extraction, but I think that's a small price to pay for being able to make use of the proofs without needing to depend on the SN axiom.

The main motivation for this implementation was to have no fuel at extraction so I'm not sure we'd like that.

Can you share a bit more of the design desires around extraction? What does avoiding fuel in extraction get you?

(If it's just about having a function that doesn't error out if it runs out of fuel, this methodology achieves that)

(And if matching on the fuel is too expensive, you can just pass in `0`

for the fuel and the extracted code will behave the same except for an extra branch at the top level)

I think we wanted to handwave that we were basically producing the same we would write in ocaml. It's anyway false. But anything that might drag performance down for something already not fast is something I guess we would like to avoid.

On my side I'm also afraid it will complicate an already very complicated definition. But it may well be that all my fears are unfounded.

I'm trying to code up an example change. How do I change

```
| @exist (Some (args, c, ρ)) eq2 with inspect (reduce c (Fix_app mfix idx args :: ρ) _) := {
| @exist (@exist (t, ρ') prf) eq3 with construct_viewc t := {
```

into something that does a monadic bind on `reduce`

either before or after the `inspect`

?

```
| @exist (Some (args, c, ρ)) eq2 :=
'(@exist (t, ρ') prf) <- reduce c (Fix_app mfix idx args :: ρ) _;;
with construct_viewc t := {
```

is a syntax error...

I guess you need to basically reimplement `bind`

manually…

Is there no way to add syntactic sugar for it? The bind of this monad is non-trivial and implementing it manually duplicates code in a way that seems pretty terrible to inline:

```
Definition partially_fueled_bind {R A A'} (v : PartiallyFueled R A) (k : A -> PartiallyFueled R A') : PartiallyFueled R A'
:= match v with
| finished v => k v
| needs_acc f
=> needs_acc (fun acc => match k (f acc) with
| finished v => v
| needs_acc f' => f' acc
end)
end.
```

Is inlining even enough? It seems you'd need `with`

inside a lambda, right? Since equations-based pattern-matching lambdas are not available in Coq, you probably need a named helper function using `where`

?

Last updated: Jun 10 2023 at 06:31 UTC