A mechanized proof of soundness of calculus defined in A Theory of Quoted Code Patterns which is a formalization of pattern matching on code available in Scala 3 as part of its new macro system.
One of the first things I wanted to learn to be able to specify the theorems in a more readable way was Coq notation mechanism.
By looking at examples and some trial and error I found how to define constants and simple notational shortcuts.
Example constant definition: Notation "∅" := emptyEnvironment. which allows to use the unicode ∅ for an empty environment.
One can also have arguments in the defined notation, so for example a function call can be translated into pretty infix operators like I did for extending the environment:
Notation "G ';' x ':' T" := (Textend G x T) (at level 40, x at level 59).
A more complex example is defining typing judgements using the well known syntax instead of a traditional inductive type syntax.
First I have to "reserve" the notation and then I can use it in the definition at the end "explaining" how the new notation relates to the original inductive type definition:
Reserved Notation "G '⊢' t ':' T" (at level 40, t at level 59).
Inductive term_typing : TypCtx -> Term -> TType -> Prop :=
| ty_lit : forall G n, G ⊢ (Lit n) : TNat
| ty_var : forall G x t, Tcontains G x t -> G ⊢ Var x : t
| ty_lam : forall G arg argT body bodyT, (G; arg : argT) ⊢ body : bodyT -> G ⊢ (Lam arg argT body) : (TLam argT bodyT)
| ty_app : forall G f arg argT retT, G ⊢ f : (TLam argT retT) -> G ⊢ arg : argT -> G ⊢ (App f arg) : retT
where "G '⊢' t ':' T" := (term_typing G t T).
(the where at the end of the definition is what actually binds the notation to the internal construct).
For now I haven't learned how to use the levels correctly - I know that they relate to operator precedence, but I haven't gotten into detail there - I just try to set them intuitively and prefer to use parentheses in unclear situations to avoid ambiguity.
One of the first things I wanted to learn to be able to specify the theorems in a more readable way was Coq notation mechanism. By looking at examples and some trial and error I found how to define constants and simple notational shortcuts.
Example constant definition:
Notation "∅" := emptyEnvironment.which allows to use the unicode ∅ for an empty environment.One can also have arguments in the defined notation, so for example a function call can be translated into pretty infix operators like I did for extending the environment:
A more complex example is defining typing judgements using the well known syntax instead of a traditional inductive type syntax. First I have to "reserve" the notation and then I can use it in the definition at the end "explaining" how the new notation relates to the original inductive type definition:
(the
whereat the end of the definition is what actually binds the notation to the internal construct).For now I haven't learned how to use the
levels correctly - I know that they relate to operator precedence, but I haven't gotten into detail there - I just try to set them intuitively and prefer to use parentheses in unclear situations to avoid ambiguity.