Abstract
1
Introduction
▶
1.1
Organization of the Blueprint
1.2
Automation in Lean
1.3
Polynomials in Lean
2
Reflection by Inference
▶
2.1
Representation Inference
2.2
Reflection Model
2.3
Sensitive Inference Procedure
3
Univariate System
▶
3.1
Inference Rules
3.2
Reflection Classes
3.3
Representations
3.4
Tactics
▶
3.4.1
Utility tactics
3.4.2
Reflection tactics
4
Multivariate System
5
References
Dependency graph
Automate Polynomial: An Experiment in Reflection for Polynomials
Liam Schilling and Quang Dao
Abstract
1
Introduction
1.1
Organization of the Blueprint
1.2
Automation in Lean
1.3
Polynomials in Lean
2
Reflection by Inference
2.1
Representation Inference
2.2
Reflection Model
2.3
Sensitive Inference Procedure
3
Univariate System
3.1
Inference Rules
3.2
Reflection Classes
3.3
Representations
3.4
Tactics
3.4.1
Utility tactics
3.4.2
Reflection tactics
4
Multivariate System
5
References