In the blog post I try to figure out how all of those concepts map to features in Lean Theorem prover.
Concepts and relations of concepts in the Physics Derivation Graph
In the Physics Derivation Graph a derivation is comprised of steps. Each step has one inference rule. Inference rules can have
- zero or more input expressions
- zero or more output expressions
- zero or more feed values
Each expression is comprised of a LHS, RHS, and relation. "Relation" can be =, >, <, <=, >=.
The LHS and RHS and Feed values are comprised of symbols (e.g., a, b, x, y) and operators (e.g., *,+,/).
Symbols are variables (e.g., a, b, x, y) or constants (\pi, e).
How Physics Derivation Graph concepts map to Lean
I think a PDG input expression is a proposition in Lean.
I think a PDG step is a theorem in Lean.
Maybe the PDG output expression is a goal in Lean?
I think a PDG inference rule is a tactic in Lean. See https://leanprover.github.io/reference/tactics.html
"The type of a function that can inspect the proof state, modify it, and potentially return something of type A (or fail) is called tactic A.source: https://leanprover-community.github.io/extras/tactic_writing.html
Equivalence of the PDG derivation step "add 2 to both sides of a=b to get a+2=b+2" with using Lean for the proof "(a=b) -> (a+2=b+2)"
In the Physics Derivation Graph the expressions "
a=b" and "a+2=b+2" are related by the inference rule "add __ to both sides".In Lean, "
a=b" is a proposition. We have to specify that a is Real and b is Real. Then we can prove that(a=b) -> (a+2=b+2)
Work in progress -- try something like
see also
No comments:
Post a Comment