Quoting and denoting of universes is not an inverse

[gmalecha]

I wanted to experiment with the possibility of using template-coq as a tactic language to solve a "simple" problem with universes (which was the impetus for my initial question on slack). Here's the problem:

Monomorphic Universes x y z.

Goal TT@{x} /\ TT@{y} /\ TT@{z}.

I wrote the following:

Fixpoint prove_it (G : term) : option term :=
  match G with
  | tApp f (l :: r :: nil) =>
    if eq_term_dec f c_I then
      match prove_it l , prove_it r with
      | Some pfL , Some pfR =>
        Some (tApp c_conj (l :: r :: pfL :: pfR :: nil))
      | _ , _ =>
        None
      end
    else
      None
  | tInd _ inst =>
    if eq_term_dec G c_I then
      Some (tConstruct p_II 1 inst)
    else
      None
  | _ => None
  end.

(note that I just decided that eq_term_dec would be fun _ _ => true, but there is probably an implementation of it somewhere).

I plugged it in as follows:

  lazymatch goal with
  | |- ?G =>
      quote_term G ltac:(fun g =>
                           match eval compute in (prove_it g) with
                           | Some ?pf => denote_term pf ltac:(fun pf => exact pf)
                           end)
  end.

After the tactic runs (and it does), I get the following errors:

Show Proof.
(* Error: Anomaly "Uncaught exception Not_found." Please report at http://coq.inria.fr/bugs/. *)
Qed.
(* Error: Not enough constructors in the type. *)

[gmalecha]

Just as a note, the term generated is the following:

(tApp (tConstruct {| inductive_mind := "Coq.Init.Logic.and"; inductive_ind := 0 |} 0 nil)
   (tInd {| inductive_mind := "meta.TT"; inductive_ind := 0 |} (Level.Level "meta.234" :: nil)
    :: tApp (tInd {| inductive_mind := "Coq.Init.Logic.and"; inductive_ind := 0 |} nil)
         (tInd {| inductive_mind := "meta.TT"; inductive_ind := 0 |} (Level.Level "meta.235" :: nil)
          :: tInd {| inductive_mind := "meta.TT"; inductive_ind := 0 |} (Level.Level "meta.236" :: nil) :: nil)
       :: tConstruct {| inductive_mind := "meta.TT"; inductive_ind := 0 |} 1 (Level.Level "meta.234" :: nil)
          :: tApp (tConstruct {| inductive_mind := "Coq.Init.Logic.and"; inductive_ind := 0 |} 0 nil)
               (tInd {| inductive_mind := "meta.TT"; inductive_ind := 0 |} (Level.Level "meta.235" :: nil)
                :: tInd {| inductive_mind := "meta.TT"; inductive_ind := 0 |} (Level.Level "meta.236" :: nil)
                   :: tConstruct {| inductive_mind := "meta.TT"; inductive_ind := 0 |} 1 (Level.Level "meta.235" :: nil)
                      :: tConstruct {| inductive_mind := "meta.TT"; inductive_ind := 0 |} 1 (Level.Level "meta.236" :: nil) :: nil) :: nil))

There are no mentions of the universes x, y, and z anywhere, but I'm not sure if there should be, maybe that is done at the printing level?

[mattam82]

Yes, x, y and. z should be meta.234 etc...

[mattam82]

Maybe you can use Pretty.print_term to get a nicer output