Stream: Coq users

Topic: Print a term as Coq accepts it as input

view this post on Zulip Ambroise (Mar 31 2021 at 05:08):

Hi!

Is there a way to print a term as Coq would accept as input? I thought Print would do, but it fails on the the generated scheme for trees and forests, as described in the documentation (https://coq.inria.fr/distrib/current/refman/user-extensions/proof-schemes.html?highlight=scheme):

  Inductive tree : Set := node : A -> forest -> tree
with forest : Set :=
    leaf : B -> forest
  | cons : tree -> forest -> forest.
  Scheme tree_forest_rec := Induction for tree Sort Set
  with forest_tree_rec := Induction for forest Sort Set.

  Print tree_forest_rec.

When I copy and paste the printed term with Coq 8.13.1, I get the following error:

Error:
Syntax error: [term level 200] expected after '=>' (in [binder_constr]).

Below is the printed term:

tree_forest_rec =
fun (P : tree -> Set) (P0 : forest -> Set)
  (f : forall (a : A) (f : forest), P0 f -> P (node a f))
  (f0 : forall b : B, P0 (leaf b))
  (f1 : forall t : tree, P t -> forall f1 : forest, P0 f1 -> P0 (cons t f1))
=>
with F (t : tree) : P t :=
  match t as t0 return (P t0) with
  | node a f2 => f a f2 (F0 f2)
  end
with F0 (f2 : forest) : P0 f2 :=
  match f2 as f3 return (P0 f3) with
  | leaf b => f0 b
  | cons t f3 => f1 t (F t) f3 (F0 f3)
  end
for
F
     : forall (P : tree -> Set) (P0 : forest -> Set),
       (forall (a : A) (f : forest), P0 f -> P (node a f)) ->
       (forall b : B, P0 (leaf b)) ->
       (forall t : tree, P t -> forall f1 : forest, P0 f1 -> P0 (cons t f1)) ->
       forall t : tree, P t

view this post on Zulip Ambroise (Mar 31 2021 at 05:41):

hmm, I guess it is a printing bug in the case of mutually recursive functions

view this post on Zulip Matthieu Sozeau (Mar 31 2021 at 08:08):

Yes, that's a bug, if should not start with with

view this post on Zulip Emilio Jesús Gallego Arias (Mar 31 2021 at 11:30):

Indeed, that's a bug, please open a report. As of today it should be noted that in general, printing Coq programs won't produce output that can be parsed _and interpreted_ back; this is due to a complex set of issues, and may be hard to fix, but in particular printing is not injective w.r.t. AST.

Depending on the needs of your use case, you could be better off with actually using a faithful representation of the AST such as the one provided by SerAPI.

Last updated: Oct 12 2024 at 12:01 UTC