Louise Dubois de Prisque (Oct 05 2022 at 15:53): Louise Dubois de Prisque (Oct 05 2022 at 15:53):Hello, I would like to create a quoted term from two Gallina terms as inputs, unquote it, and assert it as a lemma. I know that the TemplateMonad can create proof obligations whenever the Lemma is not proved, thanks to the tmLemma constructor. But I cannot make this typecheck because the monad cannot resolve the implicit arguments. Here is a minimal example:
From MetaCoq Require Import All.
From MetaCoq.Template Require Import utils.
Import MCMonadNotation.
Require Import List.
Import ListNotations.
Definition mkEq A t t' := tApp <% @eq %> [A; t ; t'].
Definition assert_equality {A : Type}
(t: A) (t': A) :=
tquote <- tmQuote t ;;
t'quote <- tmQuote t' ;;
A_quote <- tmQuote A ;;
let st := mkEq A_quote tquote t'quote in
st_unq <- tmUnquoteTyped Prop st;;
na <- tmFreshName "new_lemma";;
tmLemma na st_unq.
Do you know how I can do it? I use MetaCoq version 1.1-8.14. Thanks in advance !
Yannick Forster (Oct 05 2022 at 16:01):The error message is misleading :) The problem is the return type of your function. What would you say it is?
Yannick Forster (Oct 05 2022 at 16:01):(It depends on t and t' I think
Yannick Forster (Oct 05 2022 at 16:10):the problem becomes more apparent when you write everything using tmBind explicitly
Yannick Forster (Oct 05 2022 at 16:14):Definition assert_equality {A : Type}
(t: A) (t': A) : TemplateMonad unit :=
tmBind (tquote <- tmQuote t ;;
t'quote <- tmQuote t' ;;
A_quote <- tmQuote A ;;
let st := mkEq A_quote tquote t'quote in
tmUnquoteTyped Prop st) (fun st_unq : Prop =>
na <- tmFreshName "new_lemma" ;;
_ <- tmLemma na st_unq;;
tmPrint "ok").
I easily get confused with monadic notations but I can see more clearly the problem. Thank you very much Yannick :)
Last updated: May 31 2023 at 02:31 UTC