Skip to content

[main] Don't use unguarded assumption #1276

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
JasonGross wants to merge 2 commits into
base: main
Choose a base branch
from
Open

[main] Don't use unguarded assumption #1276

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
dd073aa
Don't use unguarded `assumption`
JasonGross Jun 7, 2026
1c34182
Add quotation_of instances for ondecl, onctx, tCasePredProp, tCaseBrs…
JasonGross Jun 7, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
7 changes: 6 additions & 1 deletion quotation/theories/ToPCUIC/Common/BasicAst.v
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
From MetaRocq.Quotation.ToPCUIC Require Import Init.
From MetaRocq.Quotation.ToPCUIC Require Import (hints) Stdlib.Init Stdlib.Floats Stdlib.Numbers.
From MetaRocq.Quotation.ToPCUIC.Utils Require Import (hints) utils.
From MetaRocq.Quotation.ToPCUIC.Utils Require Import (hints) utils MROption.
From MetaRocq.Quotation.ToPCUIC.Common Require Import (hints) Kernames.
From MetaRocq.Common Require Import BasicAst.
From MetaRocq.Utils Require Import MRUtils.
Expand All @@ -18,9 +18,14 @@ From MetaRocq.Template Require Import AstUtils (* for tFixType *).
#[export] Instance quote_def {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (def term) := ltac:(destruct 1; exact _).
#[export] Instance quote_judgment_ {term univ} {qterm : quotation_of term} {uterm : quotation_of univ} {quote_term : ground_quotable term} {quote_univ : ground_quotable univ} : ground_quotable (judgment_ term univ) := ltac:(destruct 1; exact _).
#[export] Instance quote_context_decl {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (context_decl term) := ltac:(destruct 1; exact _).
#[export] Instance quotation_of_context_decl {term} {qterm : quotation_of term} {d : context_decl term} {qd : ondecl quotation_of d} : quotation_of d := ltac:(destruct d; cbv [ondecl BasicAst.decl_body BasicAst.decl_type] in qd; destruct_head'_prod; exact _).
#[export] Hint Extern 0 (ondecl quotation_of _) => assumption : typeclass_instances.
#[export] Instance quotation_of_context {term} {qterm : quotation_of term} {ctx : list (context_decl term)} {qctx : onctx quotation_of ctx} : quotation_of ctx := ltac:(induction qctx; exact _).
#[export] Hint Extern 0 (onctx quotation_of _) => assumption : typeclass_instances.
#[export] Hint Unfold mfixpoint : quotation.
#[export] Typeclasses Transparent mfixpoint.
#[local] Hint Unfold dtype dbody : quotation.
#[export] Instance quotation_of_mfixpoint {term} {m : mfixpoint term} {qterm : quotation_of term} {qm : tFixType quotation_of quotation_of m} : quotation_of m := ltac:(induction qm; destruct_head'_prod; destruct_head' def; exact _).
#[export] Hint Extern 0 (tFixType quotation_of quotation_of ?m) => assumption : typeclass_instances.
#[export] Hint Unfold eq_binder_annot : quotation.
#[export] Typeclasses Transparent eq_binder_annot.
8 changes: 7 additions & 1 deletion quotation/theories/ToPCUIC/PCUIC/PCUICAst.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -6,10 +6,16 @@ From MetaRocq.Quotation.ToPCUIC.Common Require Import Environment EnvironmentTyp
From MetaRocq.Quotation.ToPCUIC.PCUIC Require Import (hints) utils.PCUICPrimitive.
From MetaRocq.Quotation.ToPCUIC.QuotationOf.Common Require Import Environment.Sig EnvironmentTyping.Sig.
From MetaRocq.Quotation.ToPCUIC.QuotationOf.PCUIC Require Import PCUICAst.Instances Syntax.PCUICReflect.Instances.
From MetaRocq.Utils Require Import MRUtils.

#[export] Instance quote_predicate {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (predicate term) := ltac:(destruct 1; exact _).
#[export] Instance quote_branch {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (branch term) := ltac:(destruct 1; exact _).
#[local] Hint Extern 1 => assumption : typeclass_instances.

#[local] Instance quotation_of_predicate {term} {p : predicate term} {qterm : quotation_of term} {qp : tCasePredProp quotation_of quotation_of p} : quotation_of p := ltac:(induction p; cbv [tCasePredProp PCUICAst.pparams PCUICAst.pcontext PCUICAst.preturn] in *; destruct_head'_prod; exact _).
#[export] Hint Extern 0 (@tCasePredProp ?term quotation_of quotation_of ?p) => assumption : typeclass_instances.
#[local] Instance quotation_of_branch {term} {qterm : quotation_of term} {b : branch term} {qctx : onctx quotation_of b.(bcontext)} {qbody : quotation_of b.(bbody)} : quotation_of b := ltac:(destruct b; cbv [PCUICAst.bcontext PCUICAst.bbody] in *; exact _).
#[local] Instance quotation_of_branches {term} {qterm : quotation_of term} {l : list (branch term)} {ql : tCaseBrsProp quotation_of l} : quotation_of l := ltac:(cbv [tCaseBrsProp] in ql; induction ql; destruct_head'_prod; exact _).
#[export] Hint Extern 0 (@tCaseBrsProp _ quotation_of _) => assumption : typeclass_instances.

#[export] Instance quote_term : ground_quotable term := ltac:(induction 1 using term_forall_list_ind; exact _).

Expand Down
1 change: 1 addition & 0 deletions quotation/theories/ToPCUIC/PCUIC/utils/PCUICPrimitive.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,6 +13,7 @@ From MetaRocq.Quotation.ToPCUIC.Utils Require Import (hints) All_Forall.
#[export] Hint Extern 0 (@tPrimProp ?term quotation_of ?a)
=> lazymatch goal with
| [ H : @tPrimProp _ quotation_of _ |- _ ] => assumption
| [ H : @tPrimProp _ (fun x => quotation_of x) _ |- _ ] => assumption
end : typeclass_instances.

#[export] Instance quote_prim_model {term tag} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (prim_model term tag) := ltac:(destruct 1; eauto).
Expand Down
5 changes: 1 addition & 4 deletions quotation/theories/ToPCUIC/Stdlib/Init.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,10 +36,7 @@ Defined.
#[export] Polymorphic Instance quote_prod {A B} {qA : quotation_of A} {qB : quotation_of B} {quoteA : ground_quotable A} {quoteB : ground_quotable B} : ground_quotable (prod A B) := (ltac:(induction 1; exact _)).
#[export] Polymorphic Instance quote_list {A} {qA : quotation_of A} {quoteA : ground_quotable A} : ground_quotable (list A) := (ltac:(induction 1; exact _)).
#[export] Polymorphic Instance quotation_of_list {A ls} {qA : quotation_of A} {qls : @All A quotation_of ls} : quotation_of ls := ltac:(induction qls; exact _).
#[export] Hint Extern 0 (@All ?A quotation_of ?ls)
=> lazymatch goal with
| [ H : @All _ quotation_of _ |- _ ] => assumption
end : typeclass_instances.
#[export] Hint Extern 0 (@All ?A quotation_of ?ls) => assumption : typeclass_instances.
#[export] Instance quote_comparison : ground_quotable comparison := ltac:(destruct 1; exact _).
#[export] Instance quote_CompareSpec {Peq Plt Pgt : Prop} {qPeq : quotation_of Peq} {qPlt : quotation_of Plt} {qPgt : quotation_of Pgt} {quote_Peq : ground_quotable Peq} {quote_Plt : ground_quotable Plt} {quote_Pgt : ground_quotable Pgt} {c} : ground_quotable (CompareSpec Peq Plt Pgt c).
Proof.
Expand Down
3 changes: 3 additions & 0 deletions quotation/theories/ToPCUIC/Utils/MROption.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,9 @@ Defined.
#[export] Polymorphic Instance quote_option_default {A P o b} {quoteP : forall x, o = Some x -> ground_quotable (P x)} {quoteP' : o = None -> ground_quotable b} : ground_quotable (@option_default A Type P o b) := ltac:(destruct o; cbv [option_default]; exact _).
#[export] Polymorphic Instance quote_option_defaultP {A o} {P : A -> Prop} {b : Prop} {quoteP : forall x, o = Some x -> ground_quotable (P x)} {quoteP' : o = None -> ground_quotable b} : ground_quotable (@option_default A Prop P o b) := ltac:(destruct o; cbv [option_default]; exact _).

#[export] Polymorphic Instance quotation_of_option_default {A} {qA : quotation_of A} {o : option A} {b} {qb : ground_quotable b} {qo : option_default quotation_of o b} : quotation_of o := ltac:(destruct o; cbv [option_default] in qo; exact _).
#[export] Hint Extern 0 (option_default quotation_of _ _) => assumption : typeclass_instances.

#[export] Instance quote_on_Some {A P o} {quoteP : forall x, o = Some x -> ground_quotable (P x:Prop)} : ground_quotable (@on_Some A P o) := ltac:(destruct o; cbv [on_Some]; exact _).
#[export] Typeclasses Opaque on_Some.
#[export] Instance quote_on_Some_or_None {A P o} {quoteP : forall x, o = Some x -> ground_quotable (P x:Prop)} : ground_quotable (@on_Some_or_None A P o) := ltac:(destruct o; cbv [on_Some_or_None]; exact _).
Expand Down
1 change: 1 addition & 0 deletions quotation/theories/ToTemplate/Common/BasicAst.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -22,5 +22,6 @@ From MetaRocq.Template Require Import AstUtils (* for tFixType *).
#[export] Typeclasses Transparent mfixpoint.
#[local] Hint Unfold dtype dbody : quotation.
#[export] Instance quotation_of_mfixpoint {term} {m : mfixpoint term} {qterm : quotation_of term} {qm : tFixType quotation_of quotation_of m} : quotation_of m := ltac:(induction qm; destruct_head'_prod; destruct_head' def; exact _).
#[export] Hint Extern 0 (tFixType quotation_of quotation_of ?m) => assumption : typeclass_instances.
#[export] Hint Unfold eq_binder_annot : quotation.
#[export] Typeclasses Transparent eq_binder_annot.
5 changes: 1 addition & 4 deletions quotation/theories/ToTemplate/Stdlib/Init.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -36,10 +36,7 @@ Defined.
#[export] Polymorphic Instance quote_prod {A B} {qA : quotation_of A} {qB : quotation_of B} {quoteA : ground_quotable A} {quoteB : ground_quotable B} : ground_quotable (prod A B) := (ltac:(induction 1; exact _)).
#[export] Polymorphic Instance quote_list {A} {qA : quotation_of A} {quoteA : ground_quotable A} : ground_quotable (list A) := (ltac:(induction 1; exact _)).
#[export] Polymorphic Instance quotation_of_list {A ls} {qA : quotation_of A} {qls : @All A quotation_of ls} : quotation_of ls := ltac:(induction qls; exact _).
#[export] Hint Extern 0 (@All ?A quotation_of ?ls)
=> lazymatch goal with
| [ H : @All _ quotation_of _ |- _ ] => assumption
end : typeclass_instances.
#[export] Hint Extern 0 (@All ?A quotation_of ?ls) => assumption : typeclass_instances.
#[export] Instance quote_comparison : ground_quotable comparison := ltac:(destruct 1; exact _).
#[export] Instance quote_CompareSpec {Peq Plt Pgt : Prop} {qPeq : quotation_of Peq} {qPlt : quotation_of Plt} {qPgt : quotation_of Pgt} {quote_Peq : ground_quotable Peq} {quote_Plt : ground_quotable Plt} {quote_Pgt : ground_quotable Pgt} {c} : ground_quotable (CompareSpec Peq Plt Pgt c).
Proof.
Expand Down
6 changes: 5 additions & 1 deletion quotation/theories/ToTemplate/Template/Ast.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -5,12 +5,16 @@ From MetaRocq.Quotation.ToTemplate.Common Require Import (hints) Universes Basic
From MetaRocq.Quotation.ToTemplate.Common Require Import Environment EnvironmentTyping.
From MetaRocq.Quotation.ToTemplate.QuotationOf.Common Require Import Environment.Sig EnvironmentTyping.Sig.
From MetaRocq.Quotation.ToTemplate.QuotationOf.Template Require Import Ast.Instances ReflectAst.Instances.
From MetaRocq.Utils Require Import MRUtils.

#[export] Instance quote_pstring : ground_quotable PrimString.string := fun s => Ast.tString s.

#[export] Instance quote_predicate {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (predicate term) := ltac:(destruct 1; exact _).
#[export] Instance quote_branch {term} {qterm : quotation_of term} {quote_term : ground_quotable term} : ground_quotable (branch term) := ltac:(destruct 1; exact _).
#[local] Hint Extern 1 => assumption : typeclass_instances.

#[local] Instance quotation_of_predicate {term} {p : predicate term} {qterm : quotation_of term} {qp : tCasePredProp quotation_of quotation_of p} : quotation_of p := ltac:(induction p; cbv [tCasePredProp Ast.pparams Ast.preturn] in *; destruct_head'_prod; exact _).
#[export] Hint Extern 0 (@tCasePredProp ?term quotation_of quotation_of ?p) => assumption : typeclass_instances.

#[export] Instance quote_term : ground_quotable term := ltac:(induction 1 using term_forall_list_rect; exact _).

Module QuoteTemplateTerm <: QuoteTerm TemplateTerm.
Expand Down
Loading