relation between Inference Rules in the Physics Derivation Graph and Proofs in Lean

Published 2023-06-18T13:56:00.001Z by Physics Derivation Graph

In this post I explore the concept that each derivation can be phrased as a proof of the initial declaration and the final result. Also, each step in a derivation can be phrased as a proof.

Lean Proofs of Derivation Steps

As per https://stackoverflow.com/questions/41946310/how-to-prove-a-b-%E2%86%92-a-1-b-1-in-lean Lean can prove that 

(a=b) -> (a+1=b+1)

In comparison, a PDG Inference Rule is more generic: 

add __ to both sides of (LHS=RHS) to get (LHS+__=RHS+__)

The PDG Inference Rule is generic because the types of LHS and RHS are undefined. Are they Real? Complex? Matrices?

The relevance of types for inference rules is because mixing types may not work. "Add 1 to both sides of (LHS=RHS)" won't work if LHS and RHS are 2x2 matrices.  

Example Step

To leverage Lean, a PDG derivation step involves

  1. Select the relevant PDG Inference Rule.
  2. Prove the application of the inference rule specific to the expressions associated with the step

As an example, the derivation step 

  (T = 1/f) -> (T f = 1)
is a provable instance of the PDG Inference Rule 
multiply both sides of (LHS=RHS) by __ to get (LHS*__=RHS*__)

Generalizability for an Inference Rule 

The proofs of each application of each inference rule follow a similar structure. Once I've shown

(a=b) -> (a*c=b*c) for all (a, b, c) in Complex
then I can later substitute 
a=LHS
b=RHS
c=__

and re-run the same proof tactics. The proof tactics should be agnostic to the specific contents of LHS and RHS as long as LHS, RHS, and __ are Real or Complex.

If I've proven

(a=b) -> (a*c=b*c) for all (a, b, c) in Complex
then the proof tactics will the same for 
(a+d=b*f) -> ((a+d)*c=(b*f)*c) for all (a, b, c, d, f) in Complex



Lean Proofs of Derivations


What about more complicated derivations that have multiple predicates, like 

A    B
\   /
 \ /  
  F   C
  \   /
   \ /
    D
where A and B and C are initial assumptions and D is the final expression in the derivation?

In Lean the top-level summary would be 

  (A ^ B ^ C) -> D
and the derivation steps expressed in Lean would be 
(A ^ B) -> F
and 
(F ^ C) -> D

This decomposition also applies to derivations with branches and joins. A derivation like 
A    B
\   /
 \ / 
  F
 / \
/   \
D   C 
|   |
E   |
\   /
 \ /
  G
expressed in Lean would be 
(A ^ B) -> F
and 
F -> (D ^ C)
and
D -> E
and
(E ^ C) -> G

with a top-level description in Lean being

(A ^ B) -> G