pawer_core

A rust library to work with the Calculus of Construction. Made for the PAWER (Proof Assistant Web Embeded in Rust) project.

The original project is at https://gitlab.aliens-lyon.fr/pawer/pawer_core but is severly outdated

Usage

Be sure to have cargo installed ! You can do cargo run to start a simple console version of the tool. You can run the tests using cargo test

Documentation

You can generate the documentation of the library by using the make doc command (it's an alias for cargo doc --lib --open). The file will be generated under ./target/doc/pawer_core/index.html

Commands

Generic commands:

• Check: Check <lambda>. tries to type <lambda> and prints the output.
• Reduce: Reduce <lambda>. reduce to a beta normal-form the lambda. Alias: Compute <lambda>.
• Search: Search <string>. search in the list of defined contants / inductive types the ones that contains <string>. If <string> is empty, returns all defined function / types.
• Print: Print <lambda>. print <lambda> (will remove syntaxic sugar)
• PrintProof: PrintProof. will print the current lambda-term of the proof, with hole if they are some.
• Cancel: Cancel. will cancel the current proof.

Commands abouts constants:

• Goal: Goal <prop>. will start a new proof of <prop>. Upon completion, nothing will happen.
• Theorem: Theorem <name> : <prop>. will start a new proof of <prop>. Upon completion, the theorem wil be added to the constant to be used, under the name <name>.
• Definition: Definition <name> : <lambda>. will try to type <lambda>. If sucessful, it will add <lambda> to the constants under the name <name>. It is the same as doing Theorem <name> : <type>. exact <lambda>. Qed.
• Qed: Qed. is used to finish a proof. Will calculate the beta normal-form, and then tries to type the term.
• Inductive: Inductive name (arg1:type1) ... (argN:typeN) : arity := <list of constructor>. will define an inductive type.
• Fixpoint: Fixpoint name (arg1:type1) ... (argN:typeN) {struct <struct>} : <type> := <code> is syntaxic sugar for Definition <name> := fix <name> (arg1:type1) ... (argN:typeN) {struct <struct>} : <type> := <code>

Tactics:

• Apply: apply <lambda>. if <lambda>: A1 -> ... -> AN -> Goal, will ask for a proof of A1, ..., AN
• Exact: exact <lambda>. will try to solve the goal by using the term <lambda> directly
• Cut: cut <prop>. will split the goal in two subgoals: proving <prop> and <prop> -> Goal
• Intro: intro <name>. on a goal of the form A -> B or forall x:A, B with intro either an hypothesis or an element named <name>. The <name> can be ommited, and the prover will generate a proper unused name.
• Intros: intros <name1> <name2> ... <nameN>. will perform multiple intro. If no name were given, it will do as many intro as possible, generating brand new name for each.
• Unfold: unfold <name>. will unfold a constant in the goal and every hypothesis.
• Simpl: simpl. will beta reduce the goal.
• Induction: induction <var>. if <var>:<inductive>:Set, will perform a proof by induction on the goal. It is still very buggy and might not work /!\

Project structure and codebase informations

We used the pest crate for the parsing. The pest grammar file can be seen in pest/grammar.pest. We do not have an incremental parsing.

There is two version of the lambda-terms:

• The LambdaTerm are a tree-like way to represent lambda, used only for parsing reasons.
• The LambdaNode are store in an array, with the 'pointors' that are an index to the next elements. This will allow of optimisations (hash-consing) and a memoized version of the beta-reduction

The """standard library""" is loaded at the function utils::load_prelude. The code used for the showcase can be seen in presentation.v

Status

The project devellopement will be considerably slow down, but Coda B is still looking at hosting a version of it on her website.

License

MIT -- see the LICENCE file