Stream: MetaCoq

Topic: Use of tmLemma


view this post on Zulip 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 !

view this post on Zulip 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?

view this post on Zulip Yannick Forster (Oct 05 2022 at 16:01):

(It depends on t and t' I think

view this post on Zulip Yannick Forster (Oct 05 2022 at 16:10):

the problem becomes more apparent when you write everything using tmBind explicitly

view this post on Zulip 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").

view this post on Zulip Louise Dubois de Prisque (Oct 05 2022 at 21:12):

I easily get confused with monadic notations but I can see more clearly the problem. Thank you very much Yannick :)


Last updated: Jan 30 2023 at 17:03 UTC