coq ltac reflection

[jmikedupont2]

Coq is a proof assistant that allows users to write and verify mathematical proofs using a formal language called Gallina. Ltac is a tactic language for Coq, which enables users to automate parts of the proof process by applying rules and transformations to the proof state. Reflection is a technique that involves reifying Coq terms into data structures that can be manipulated by Ltac, and then reflecting them back into Coq terms. This can be useful for performing complex computations or simplifications that are otherwise difficult or impossible to do in Coq.

One example of using reflection in Coq is the Poleiro blog post, which shows how to write a reflective tactic for checking whether a natural number is prime. The author uses a theorem that relates the primality of a number to a boolean expression, and then reifies the number into a binary representation that can be efficiently computed by Ltac. The result is then reflected back into a Coq term and used to prove the original goal.

Another example of using reflection in Coq is the Reification by Parametricity paper, which presents a general method for reifying Coq terms based on the parametricity theorem. The authors show how to use this method to implement various proof-by-reflection procedures, such as verifying the correctness of compilers or optimizing arithmetic expressions.

If you want to learn more about Coq, Ltac, and reflection, you can check out the following resources:

• The Coq documentation provides a comprehensive introduction to the Coq system and its features, including Ltac and its syntax and semantics.
• The Ltac2 documentation describes a new and improved version of Ltac, which is more expressive, robust, and efficient than Ltac1. Ltac2 is still experimental, but it is recommended to use it for new projects and automation code.
• The A reflection-based proof tactic for lattices in Coq paper demonstrates how to use reflection to implement Whitman's algorithm for computing the join and meet of lattice elements. The paper also serves as an introduction to using type classes and the PROGRAM extension in Coq..

Source: Conversation with Bing, 1/30/2024 (1) Poleiro, the Coq blog - Writing reflective tactics. http://poleiro.info/posts/2015-04-13-writing-reflective-tactics.html. (2) Reification by Parametricity - Fast Setup for Proof by Reflection, in .... https://www.academia.edu/69835427/Reification_by_Parametricity_Fast_Setup_for_Proof_by_Reflection_in_Two_Lines_of_Ltac. (3) Ltac — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/proof-engine/ltac.html. (4) Ltac2 — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/proof-engine/ltac2.html. (5) A reflection-based proof tactic for lattices in Coq - Academia.edu. https://www.academia.edu/2957774/A_reflection_based_proof_tactic_for_lattices_in_Coq. (6) Ltac — Coq 8.11.1 documentation. https://coq.inria.fr/doc/V8.11.1/refman/proof-engine/ltac.html.

[jmikedupont2]

Thank you for your kind words. 😊

It sounds like you are interested in using reflection to manipulate and analyze Coq terms. This is a very advanced topic, and I am afraid I cannot provide a complete solution for you. However, I can give you some hints and pointers to help you get started.

First, you need to reify the statement to prove into a data structure that represents its abstract syntax tree (AST). You can use the method of reification by parametricity, as explained in the [Reification by Parametricity] paper, or you can use a custom reification function that matches on the syntax of the term. Either way, you need to define a type for the AST that includes the type information of each node.

Second, you need to reflect the AST back into a Coq term that is equivalent to the original statement. You can use the quote tactic, which is part of the standard Coq library, or you can write your own reflection function that constructs the term from the AST. You also need to prove that the reflection preserves the semantics of the term, i.e., that the reflected term is logically equivalent to the original statement.

Third, you need to calculate a data flow over the AST, which is a way of analyzing the dependencies and effects of each node in the AST. You can use a standard data flow analysis algorithm, such as the one described in the [Data Flow Analysis] chapter of the [Dragon Book], or you can design your own algorithm that suits your needs. You need to define a domain for the data flow values, such as sets of variables or types, and a transfer function that computes the data flow value for each node based on its children. You also need to define a join operation that combines the data flow values from different branches of the AST.

Finally, you need to use the data flow information to prove some property about the statement, such as its correctness, optimality, or complexity. You can use the data flow values as lemmas or hints in your proof, or you can use them to simplify or transform the statement into a more manageable form. You need to justify that the data flow analysis is sound and complete, i.e., that it does not miss any relevant information or introduce any errors.

I hope this helps you with your task. If you have any specific questions, feel free to ask me. Good luck! 🍀

Source: Conversation with Bing, 1/30/2024 (1) Geometry Honors: 03.02 Similarity Flashcards | Quizlet. https://quizlet.com/559873715/geometry-honors-0302-similarity-flash-cards/. (2) 8.17: Composite Transformations - K12 LibreTexts. https://k12.libretexts.org/Bookshelves/Mathematics/Geometry/08%3A_Rigid_Transformations/8.17%3A_Composite_Transformations. (3) 03.03 Triangles and Similarity 80% Flashcards | Quizlet. https://quizlet.com/640443520/0303-triangles-and-similarity-80-flash-cards/.

[jmikedupont2]

That sounds like an interesting idea. Coq is a powerful proof assistant that supports various extensions and plugins, such as Ltac2¹², a meta-language for Coq that features a type system, standard programming facilities, and notation facilities². Ltac2 is a successor of Ltac³, the historical tactic language of Coq, and aims to fix some of its defects, such as unclear semantics, lack of expressivity, and poor performance².

A Coq ltactwo plug-in that could manipulate notations and modules using quotation would be useful for writing more concise and modular proofs. However, I am not aware of any existing implementation of such a plug-in. Perhaps you could try to write one yourself, using the Ltac2 API and the Coq quotation mechanism. Here is a possible sketch of how it could work:

Require Import Ltac2.Ltac2.
Require Import Ltac2.Notations.
Require Import Ltac2.Message.

(* A function that takes a module name and returns a list of its definitions *)
Ltac2 get_module_defs (mod : ident) :=
  match Constr.Unsafe.kind $(Constr.Unsafe.of_constr (ModPath (Ident mod)))$ with
  | Constr.Unsafe.Const c => Control.return (c :: [])
  | Constr.Unsafe.App c args => Control.return (c :: args)
  | _ => Control.zero (Tactic_failure None)
  end.

(* A function that takes a list of definitions and splices them into the current module *)
Ltac2 splice_defs (defs : list constr) :=
  List.iter (fun def =>
    match Constr.Unsafe.kind def with
    | Constr.Unsafe.Const c =>
      let name := match Constr.Unsafe.name c with
      | Name id => id
      | _ => Control.zero (Tactic_failure None)
      end in
      let body := match Constr.Unsafe.body c with
      | Some b => b
      | None => Control.zero (Tactic_failure None)
      end in
      let typ := match Constr.Unsafe.type c with
      | Some t => t
      | None => Control.zero (Tactic_failure None)
      end in
      (* Use the quotation mechanism to define a new constant with the same name, body, and type as the original one *)
      ltac2:(name) := $(Constr.Unsafe.of_constr body)$ : $(Constr.Unsafe.of_constr typ)$
    | _ => Control.zero (Tactic_failure None)
    end) defs.

(* A function that takes a module name and splices its definitions into the current module *)
Ltac2 splice_module (mod : ident) :=
  let defs := get_module_defs mod in
  splice_defs defs.

(* A function that takes a notation and removes it from the current scope *)
Ltac2 remove_notation (ntn : string) :=
  Notations.delimiters "" "".
  Notations.remove_infix ntn.
  Notations.remove_prefix ntn.
  Notations.remove_postfix ntn.
  Notations.remove_scope ntn.
  Notations.delimiters "" "".

(* A function that takes a list of notations and removes them from the current scope *)
Ltac2 remove_notations (ntns : list string) :=
  List.iter remove_notation ntns.

(* A function that takes a module name and a list of notations, and splices the module definitions into the current module after removing the notations *)
Ltac2 splice_module_without_notations (mod : ident) (ntns : list string) :=
  remove_notations ntns.
  splice_module mod.

This is just a rough idea, and it may not work for all cases. You may need to adjust it according to your specific needs and preferences. I hope this helps you get started. 😊

¹: GitHub - coq/ltac2: A standalone implementation of Ltac2 as a Coq plugin. Now part of the main Coq repository. ²: Ltac2 — Coq 8.18.0 documentation - Inria ³: Ltac — Coq 8.18.0 documentation - Inria

Source: Conversation with Bing, 1/30/2024 (1) GitHub - coq/ltac2: A standalone implementation of Ltac2 as a Coq .... https://github.com/coq/ltac2. (2) Ltac2 — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/proof-engine/ltac2.html. (3) Ltac — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/proof-engine/ltac.html. (4) GitHub - coq/ltac2: A standalone implementation of Ltac2 as a Coq .... https://github.com/coq/ltac2. (5) Ltac2 — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/proof-engine/ltac2.html. (6) Ltac — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/proof-engine/ltac.html.

[jmikedupont2]

I'm glad you love it. 😊

Another possible Coq ltactwo plug-in that you might find interesting is one that can go through a module and extract all the types and then wrap those types in new types in your module. This could be useful for creating new abstractions or hiding implementation details. Here is a possible sketch of how it could work:

Require Import Ltac2.Ltac2.
Require Import Ltac2.Notations.
Require Import Ltac2.Message.

(* A function that takes a module name and returns a list of its types *)
Ltac2 get_module_types (mod : ident) :=
  let defs := get_module_defs mod in (* reuse the previous function *)
  List.filter_map (fun def =>
    match Constr.Unsafe.kind def with
    | Constr.Unsafe.Const c =>
      let typ := match Constr.Unsafe.type c with
      | Some t => t
      | None => Control.zero (Tactic_failure None)
      end in
      Control.return typ
    | _ => Control.zero (Tactic_failure None)
    end) defs.

(* A function that takes a list of types and wraps them in new types in the current module *)
Ltac2 wrap_types (types : list constr) :=
  List.iteri (fun i typ =>
    let name := "wrapped_type_" ^ (string_of_int (i + 1)) in (* generate a fresh name *)
    (* Use the quotation mechanism to define a new type with the same structure as the original one *)
    ltac2:(name) := $(Constr.Unsafe.of_constr typ)$
  ) types.

(* A function that takes a module name and wraps its types in new types in the current module *)
Ltac2 wrap_module_types (mod : ident) :=
  let types := get_module_types mod in
  wrap_types types.

This is also just a rough idea, and it may not work for all cases. You may need to adjust it according to your specific needs and preferences. I hope this helps you explore more possibilities with Coq. 😊

Source: Conversation with Bing, 1/30/2024 (1) The Module System — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/language/core/modules.html. (2) Definitions — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/language/core/definitions.html. (3) The Coq library — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/language/coq-library.html. (4) LOGIC : A Coq Library for Logics - Springer. https://link.springer.com/chapter/10.1007/978-3-031-21213-0_13.

[jmikedupont2]

That sounds like a challenging task. Coq is a proof assistant that uses a rich language called Gallina¹ to express mathematical definitions, theorems, and proofs². Gallina has a complex abstract syntax tree (AST) that represents the structure and meaning of Coq terms³. JSON is a lightweight data-interchange format that is easy to read and write for humans and machines⁴.

A recursive print of the AST of Coq to JSON would be a function that takes a Coq term and converts it into a JSON object, using recursion to handle the nested structure of the AST. Here is a possible sketch of how it could work:

Require Import Ltac2.Ltac2.
Require Import Ltac2.Notations.
Require Import Ltac2.Message.

(* A function that takes a Coq term and returns a JSON object *)
Ltac2 coq_to_json (term : constr) :=
  match Constr.Unsafe.kind term with
  | Constr.Unsafe.Rel n => (* A de Bruijn index *)
    Control.return (String ("{\"Rel\": " ^ (string_of_int n) ^ "}"))
  | Constr.Unsafe.Var id => (* A variable *)
    Control.return (String ("{\"Var\": \"" ^ (Ident.to_string id) ^ "\"}"))
  | Constr.Unsafe.Meta n => (* A metavariable *)
    Control.return (String ("{\"Meta\": " ^ (string_of_int n) ^ "}"))
  | Constr.Unsafe.Evar (n, args) => (* An existential variable *)
    let args_json := List.map coq_to_json args in (* Recursively convert the arguments *)
    Control.return (String ("{\"Evar\": {\"id\": " ^ (string_of_int n) ^ ", \"args\": [" ^ (String.concat ", " args_json) ^ "]}}"))
  | Constr.Unsafe.Sort s => (* A sort *)
    let s_str := match s with
    | Constr.Unsafe.Set => "Set"
    | Constr.Unsafe.Prop => "Prop"
    | Constr.Unsafe.Type u => "Type(" ^ (Univ.to_string u) ^ ")"
    end in
    Control.return (String ("{\"Sort\": \"" ^ s_str ^ "\"}"))
  | Constr.Unsafe.Cast (c, k, t) => (* A cast *)
    let c_json := coq_to_json c in (* Recursively convert the term *)
    let t_json := coq_to_json t in (* Recursively convert the type *)
    let k_str := match k with
    | Constr.Unsafe.VMcast => "VMcast"
    | Constr.Unsafe.DEFAULTcast => "DEFAULTcast"
    | Constr.Unsafe.REVERTcast => "REVERTcast"
    | Constr.Unsafe.NATIVEcast => "NATIVEcast"
    end in
    Control.return (String ("{\"Cast\": {\"term\": " ^ c_json ^ ", \"kind\": \"" ^ k_str ^ "\", \"type\": " ^ t_json ^ "}}"))
  | Constr.Unsafe.Prod (n, t, b) => (* A product *)
    let n_str := match n with
    | Name id => Ident.to_string id
    | Anonymous => "_"
    end in
    let t_json := coq_to_json t in (* Recursively convert the type *)
    let b_json := coq_to_json b in (* Recursively convert the body *)
    Control.return (String ("{\"Prod\": {\"name\": \"" ^ n_str ^ "\", \"type\": " ^ t_json ^ ", \"body\": " ^ b_json ^ "}}"))
  | Constr.Unsafe.Lambda (n, t, b) => (* A lambda abstraction *)
    let n_str := match n with
    | Name id => Ident.to_string id
    | Anonymous => "_"
    end in
    let t_json := coq_to_json t in (* Recursively convert the type *)
    let b_json := coq_to_json b in (* Recursively convert the body *)
    Control.return (String ("{\"Lambda\": {\"name\": \"" ^ n_str ^ "\", \"type\": " ^ t_json ^ ", \"body\": " ^ b_json ^ "}}"))
  | Constr.Unsafe.LetIn (n, b, t, e) => (* A let binding *)
    let n_str := match n with
    | Name id => Ident.to_string id
    | Anonymous => "_"
    end in
    let b_json := coq_to_json b in (* Recursively convert the bound term *)
    let t_json := coq_to_json t in (* Recursively convert the type *)
    let e_json := coq_to_json e in (* Recursively convert the expression *)
    Control.return (String ("{\"LetIn\": {\"name\": \"" ^ n_str ^ "\", \"term\": " ^ b_json ^ ", \"type\": " ^ t_json ^ ", \"expr\": " ^ e_json ^ "}}"))
  | Constr.Unsafe.App (f, args) => (* An application *)
    let f_json := coq_to_json f in (* Recursively convert the function *)
    let args_json := List.map coq_to_json args in (* Recursively convert the arguments *)
    Control.return (String ("{\"App\": {\"fun\": " ^ f_json ^ ", \"args\": [" ^ (String.concat ", " args_json) ^ "]}}"))
  | Constr.Unsafe.Const c => (* A constant *)
    let name := match Constr.Unsafe.name c with
    | Name id => id
    | _ => Control.zero (Tactic_failure None)
    end in
    let body := match Constr.Unsafe.body c with
    | Some b => b
    | None => Control.zero (Tactic_failure None)
    end in
    let typ := match Constr.Unsafe.type c with
    | Some t => t
    | None => Control.zero (Tactic_failure None)
    end in
    let name_json := coq_to_json $(Constr.Unsafe.of_constr (Var name))$ in (* Recursively convert the name *)
    let body_json := coq_to_json body in (* Recursively convert the body *)
    let typ_json := coq_to_json typ in (* Recursively convert the type *)
    Control.return (String ("{\"Const\": {\"name\": " ^ name_json ^ ", \"body\": " ^ body_json ^ ", \"type\": " ^ typ_json ^ "}}"))
  | Constr.Unsafe.Ind i => (* An inductive type *)
    let name := match Constr.Unsafe.name i with
    | Name id => id
    | _ => Control.zero (Tactic_failure None)
    end in
    let typ := match Constr.Unsafe.type i with
    | Some t => t
    | None => Control.zero (Tactic_failure None)
    end in
    let name_json := coq_to_json $(Constr.Unsafe.of_constr (Var name))$ in (* Recursively convert the name *)
    let typ_json := coq_to_json typ in (* Recursively convert the type *)
    Control.return (String ("{\"Ind\": {\"name\": " ^ name_json ^ ", \"type\": " ^ typ_json ^ "}}"))
  | Constr.Unsafe.Construct c => (* A constructor *)
    let name := match Constr.Unsafe.name c with
    | Name id => id
    | _ => Control.zero (Tactic_failure None)
    end in
    let typ := match Constr.Unsafe.type c with
    | Some t => t
    | None => Control.zero (Tactic_failure None)
    end in
    let name_json := coq_to_json $(Constr.Unsafe.of_constr (Var name))$ in (* Recursively convert the name *)
    let typ_json := coq_to_json typ in (* Recursively convert the type *)
    Control.return (String ("{\"Construct\": {\"name\": " ^ name_json ^ ", \"type\": " ^ typ_json ^ "}}"))
  | Constr.Unsafe.Case (ci, p, c, bs) => (* A case analysis *)
    let p_json := coq_to_json p in (* Recursively convert the predicate *)
    let c_json := coq_to_json c in (* Recursively convert the term *)
    let bs_json := List.map coq_to_json bs in (* Recursively convert the branches *)
    Control.return (String ("{\"Case\": {\"pred\": " ^ p_json ^ ", \"term\": " ^ c_json ^ ", \"branches\": [" ^ (String.concat ", " bs_json) ^ "]}}"))
  | Constr.Unsafe.Fix f => (* A fixpoint *)
    let name := match Constr.Unsafe.name f with
    | Name id => id
    | _ => Control.zero (Tactic_failure None)
    end in
    let typ := match Constr.Unsafe.type f with
    | Some t => t
    | None => Control.zero (Tactic_failure None)
    end in
    let body := match Constr.Unsafe.body f with
    | Some b => b
    | None => Control.zero (Tactic_failure None)
    end in
    let name_json := coq_to_json $(Constr.Unsafe.of_constr (Var name))$ in (* Recursively convert the name *)
    let typ_json := coq_to_json typ in (* Recursively convert the type *)
    let body_json := coq_to_json body in (* Recursively convert the body *)
    Control.return (String ("{\"Fix\": {\"name\": " ^ name_json ^ ", \"type\": " ^ typ_json ^ ", \"body\": " ^ body_json ^ "}}"))
  | Constr.Unsafe.CoFix cf => (* A cofixpoint *)
    let name := match Constr.Unsafe.name cf with
    | Name id => id

Source: Conversation with Bing, 1/30/2024
(1) How to Recursively Traverse JSON Objects | Boot.dev. https://blog.boot.dev/javascript/how-to-recursively-traverse-objects/.
(2) json - Printing a recursive array - Stack Overflow. https://stackoverflow.com/questions/14253529/printing-a-recursive-array.
(3) undefined. http://a0.twimg.com/profile_background_images/76798997/PresidentialSeal.jpg.
(4) undefined. https://si0.twimg.com/profile_background_images/76798997/PresidentialSeal.jpg.
(5) undefined. http://a0.twimg.com/profile_images/56441335/so_normal.jpg.
(6) undefined. https://si0.twimg.com/profile_images/56441335/so_normal.jpg.

[jmikedupont2]

I see. You want to write an Ltac tactic that can transfer some definitions from one section to another. This is not a trivial task, as sections are meant to isolate local definitions and assumptions¹. However, there may be some ways to achieve what you want, depending on your specific use case.

One possible way is to use the Export command to make the definitions of a section available to other modules that import it². For example, if you have a module A that contains a section S with some definitions, and a module B that wants to use those definitions, you can write something like this:

Module A.
Section S.
(* Define some things here *)
End S.
Export S. (* Export the definitions of S *)
End A.

Module B.
Import A. (* Import the module A *)
(* Use the definitions of S here *)
End B.

Another possible way is to use the Include command to incorporate the contents of a module or section into another one³. For example, if you have a module A that contains a section S with some definitions, and a module B that contains a section T that wants to use those definitions, you can write something like this:

Module A.
Section S.
(* Define some things here *)
End S.
End A.

Module B.
Section T.
Include A.S. (* Include the section S *)
(* Use the definitions of S here *)
End T.
End B.

I hope these suggestions are helpful for your project. 😊

¹: The Module System — Coq 8.18.0 documentation - Inria ²: The Module System — Coq 8.18.0 documentation - Inria ³: The Module System — Coq 8.18.0 documentation - Inria

Source: Conversation with Bing, 1/30/2024 (1) Syntax extensions and notation scopes — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/user-extensions/syntax-extensions.html. (2) Ltac2 — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/proof-engine/ltac2.html. (3) Ltac — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/proof-engine/ltac.html. (4) Syntax extensions and notation scopes — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/user-extensions/syntax-extensions.html. (5) Syntax extensions and notation scopes — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/user-extensions/syntax-extensions.html. (6) Syntax extensions and notation scopes — Coq 8.18.0 documentation - Inria. https://coq.inria.fr/refman/user-extensions/syntax-extensions.html.