Can someone explain the difference between Ltac2 preterms and terms constructed via Constr.Unsafe?

The documentation states that preterms are untyped syntactic Coq expressions. Is that different from constructing terms through the Constr.Unsafe API? Would it make sense to have a `Constr.Unsafe.from_preterm : preterm -> kind`

function?

For context: I am manipulating some terms under an arbitrary number of binders. My goal is to decompose for example `input := fun x y z => op (g x y) (h y z)`

into `left := fun x y z => g x y`

and `right := fun x y z => h y z`

for some operator `op`

, along with a proof that `∀ x y z, input x y z = op (left x y z) (right x y z)`

.

I use `Constr.Unsafe.kind`

to look beneath an arbitrary number of `Lambda`

s. This allows me to `match!`

on the head of the function (i.e. check that it is `op`

), and get the arguments (i.e. `g _ _`

and `h _ _`

in this case). The arguments to `g`

and `h`

will mention de Bruijn variables, however, so I need to put lambdas around these again---and the same applies for the proof term.

The proof term is somewhat annoying: I'd like to write something like `'(my_proof_term $left $right)`

and then rebind this under the binders. But there are situations where I get an `Anomaly: "in retyping: Unbound local variable".`

---I think when a de Bruijn variable is the head term of `left`

or `right`

. I can write `preterm:(my_proof_term $left $right)`

without these complaints, but then I cannot rebind this: I can only `Constr.pretype`

preterms. The one thing that works is to use `Constr.Unsafe.App`

to explicitly write the term I want, but this is much more verbose than using `preterm`

s.

preterm is before elaboration

for instance `preterm:(_)`

is not an evar, it's a preterm which generates an evar when given to pretyping. So for instance `let c := preterm:(_) in let c1 := pretype c in let c2 := pretype c in Constr.equal c1 c2`

returns `false`

because c1 and c2 are 2 unrelated evars

since it's not an evar there's no appropriate kind to return from an hypothetical preterm -> kind function

going from the string you type to a constr goes

- string
- parsing -> constr_expr
- intern -> preterm (glob_constr in the ocaml)
- pretype -> term

(BTW printing goes through those stages in the opposite direction, detyping/extern/printing)

intern does things like expanding notations, inserting holes for implicit arguments, resolving global names (so eg `fun x => id x`

is internalized to `fun x : _ => @whatever.id _ x`

)

pretype does things like inserting coercions, match compilation, turning holes into evars and resolving evars through unification as required for typechecking

I can only Constr.pretype preterms

you can also build more preterms, eg `let c := preterm:(_) in preterm:(0 : $preterm:c)`

(`$preterm:x`

is like `$x`

but for preterm variables) (`constr:(bla $preterm:x)`

will run pretyping on the preterm bound to `x`

)

not sure how well building preterms with unbound rels and later closing them to pretype works but you can try

Cannot we go to kind by generating evars? Or is the problem that there might not be enough information to do so?

I can indeed manually build what I want with the `$preterm:c`

quotation:

```
From Ltac2 Require Import Ltac2 Printf.
Section test.
Notation f := (fun (x : nat) P => x = 0 /\ P).
Lemma as_and_trivial (P Q : Prop) : (P /\ Q) = (P /\ Q).
Proof. reflexivity. Qed.
Goal True.
match Constr.Unsafe.kind 'f with
| Constr.Unsafe.Lambda b1 t1 =>
match Constr.Unsafe.kind t1 with
| Constr.Unsafe.Lambda b2 t2 =>
lazy_match! t2 with
| and ?l ?r =>
printf "left: %t right: %t" l r;
let proto_preterm := preterm:(as_and_trivial $l $r) in
(* let proto_open_constr := '(as_and_trivial $l $r) in *)
(* above produces: Anomaly "in retyping: Unbound local variable." *)
let b1_type := Constr.Binder.type b1 in
let b2_type := Constr.Binder.type b2 in
let result := '(fun (x : $b1_type) (P : $b2_type) => $preterm:proto_preterm) in
printf "result: %t" result
end
| _ => Control.throw Not_found
end
| _ => Control.throw Not_found
end.
Abort.
End test.
```

but I wouldn't know how to make `result`

when all I have is a `bs : binder list`

.

maybe something like

```
Ltac2 wrap_binder (c:preterm) b :=
let t := Constr.Binder.type b in
preterm:(fun (x : $t) => $preterm:c).
(* or fold_right depending on which order the list is in *)
Ltac2 wrap_binders bs c := List.fold_left wrap_binder c bs.
Ltac2 make_result bs c := let c := wrap_binders bs c in pretype c.
```

?

But if you want to put a variable number of binders with different naming in the rel context I don't think we have the APIs

Ah, of course, one can just stay in `preterm`

. Yes, so the only downside is that this loses the naming information, the rest works out.

Completed example

Thanks!

Last updated: Oct 12 2024 at 13:01 UTC