Added basic ntac tactics and tests from Software Foundations

wilbowma / cur

A less devious proof assistant

BSD 2-Clause "Simplified" License

222 stars 18 forks source link

Closed wilbowma closed 6 years ago

wilbowma commented 6 years ago

Implemented basic tactics including
- destruct
- induction
- simpl
Implemented equality tactics, for both Martin-Löf (ML-=) equality and Paulin-Mohring equality (PM-= aka ==)
- rewrite, and friends
- reflexivity
Added tests based on working through Software Foundations Ch. 1--3, using PM equality (per Software Foundations), and testing ML equality when convenient.

wilbowma commented 6 years ago

This PR replaces #79

wilbowma commented 6 years ago

This is blocked:

[ ] Documentation (@stchang working on it)
[ ] A few broken abstractions (e.g. use of typed-lambda and \Pi as datum in some macros) (@wilbowma working on it)
[ ] Notes on lessons learned

I may also want to separate the software foundations stuff into a tutorial instead of a test suite, but... maybe I'll leave that to future work.