tstp2agda-0.1.0.0: Proof-term reconstruction from TSTP to Agda

T2A

Synopsis

# How to use tstp2agda

Let use an example, given this problem

```  \$ cat problem.tstp
fof(a1,axiom,a).
fof(a2,conjecture,a).
```

and the corresponding Metis proof

```  \$ cat proof.tstp
---------------------------------------------------------------------------
SZS status Theorem for examplesproblemTest-1.tstp
SZS output start CNFRefutation for examplesproblemTest-1.tstp
fof(a1, axiom, (a)).
fof(a2, conjecture, (a)).
fof(subgoal_0, plain, (a), inference(strip, [], [a2])).
fof(negate_0_0, plain, (~ a), inference(negate, [], [subgoal_0])).
fof(normalize_0_0, plain, (~ a),
inference(canonicalize, [], [negate_0_0])).
fof(normalize_0_1, plain, (a), inference(canonicalize, [], [a1])).
fof(normalize_0_2, plain, (\$false),
inference(simplify, [], [normalize_0_0, normalize_0_1])).
cnf(refute_0_0, plain, (\$false),
inference(canonicalize, [], [normalize_0_2])).
SZS output end CNFRefutation for examplesproblemTest-1.tstp
```

we create some requiered data structures

```main ∷ IO ()
main = do
formulas ← `parseFile` "proof.tstp"
-- create a map
proofmap ← `buildProofMap` formulas
-- get subgoals,refutes,axioms, and the conjecture
let subgoals    = `getSubGoals` formulas
let refutes     = `getRefutes` formulas
let axioms      = `getAxioms` formulas
let (Just conj) = `getConjeture` formulas
-- build a `proofTree` for each subgoal (using his associated refute)
let prooftree = `map` (`buildProofTree` proofmap) refutes
```

and then print the actual Agda code

```  -- PREAMBLE: module definitions and imports
`printPreamble` "BaseProof"
-- STEP 1: Print auxiliary functions
`printAuxSignatures` proofmap prooftree
-- STEP 2: Subgoal handling
`printSubGoals` subgoals conj "goals"
-- STEP 3: Print main function signature
`printProofBody` axioms conj "proof" subgoals "goals"
-- STEP 4: Print all the step of the proof as local definitions
`mapM_` (`printProofWhere` proofmap  prooftree
```

and then get

```  module BaseProof where
open import Data.FOL.Shallow
postulate fun-normalize-0-0 : { a : Set} → ¬ a → ¬ a
postulate fun-normalize-0-1 : { a : Set} → a → a
postulate fun-normalize-0-2 : { a : Set} → ¬ a → a → ⊥
postulate fun-refute-0-0 :  ⊥ → ⊥
postulate goals : { a : Set} → a → a
proof : { a : Set} → a → a
proof {a} a1 = goals subgoal-0
where
fun-negate-0-0 : ¬ a → ⊥
fun-negate-0-0 negate-0-0 = refute-0-0
where
normalize-0-0 = fun-normalize-0-0 negate-0-0
normalize-0-1 = fun-normalize-0-1 a1
normalize-0-2 = fun-normalize-0-2 normalize-0-0 normalize-0-1
refute-0-0 = fun-refute-0-0 normalize-0-2
```

# Getters

getSubGoals :: [F] -> [F]

Extract subgoals from a list of formulae.

getRefutes :: [F] -> [F]

Extract refuting steps from a list of formulae.

getAxioms :: [F] -> [F]

Extract axioms from a list of formulae.

getConjeture :: [F] -> Maybe F

Try to extract a conjecture from a list of formulae and checks for uniqueness.

# Agda translation

printPreamble

Arguments

 :: String Module name -> IO ()

printAuxSignatures

Arguments

 :: ProofMap map of formulas -> [ProofTree] list of subgoals -> IO ()

Print a series of auxiliary functions required to perform most of the steps of the proof. Every `Formula` has a corresponding function which has its parents as arguments and the current function as return value. Since a proof is split in various subgoals, this function receives a list of sub-`ProofTree`s

```   fun-stepₘ_ₙ : { ν₀ ... νᵢ : Set } → stepₘ_ₙ₁ → ... → stepₘ_ₙⱼ → stepₘ_ₙ
```

printSubGoals

Arguments

 :: [F] Subgoals -> F Conjecture -> String Function name (`subGoalImplName`) -> IO ()

Print the main subgoal implication function

```  subGoalImplName : subgoal₀ → ... → subgoalₙ → conjecture
```

printProofBody

Arguments

 :: [F] Axioms -> F Conjecture -> String Function name (`proofName`) -> [F] Subgoals -> String Name of `subGoalImplName` -> IO ()

Print main proof type signature, and top level LHS ans RHS of the form

```  proofName : axiom₀ → ... → axiomₙ → conjecture
proofName axiomName₀ ... axiomNameₙ = subGoalImplName subgoal₀ ... subgoalₙ
where
```

For a given subgoal print each formula definition in reverse order of dependencies

```      negation₀ : ¬ τ₀ → ⊥
negation₀ negate₀ = refute₀
where
step₀_ᵢ = fun-step₀_ᵢ step₀_ᵢ₁ .. step₀_ᵢⱼ
...
step₀_₀ = fun-step₀_₀ step₀_₀₁ .. step₀_₀ₖ
...
negationₙ : ¬ τₙ → ⊥
negationₙ negateₙ = refuteₙ
where
stepₙ_ₜ = fun-stepₙ_ₜ stepₙ__ₜ₁ .. stepₙ_ₜₒ
...
stepₙ_₀ = fun-stepₙ_₀ stepₙ_₀₁ .. stepₙ_₀ᵤ
```

This is perhaps the most important step and the one that does the "actual" proof translation. The basic principle is to define each `subgoal` in terms of its parents which for most (if not all) cases implies a `negation` of the `subgoal` and a corresponding `refute` term.

buildProofMap

Arguments

 :: [F] List of functions -> ProofMap Map of the given functions indexed by its names

`buildProofMap` `lf`, given a list of functions `lf` builds a `ProofMap`

buildProofTree

Arguments

 :: ProofMap `Map` for resolving dependencies -> F Root formula -> ProofTree Tree of formulas with the given formula as root

`buildProofTree` `m` `f`, build a `ProofTree` with `f` as root, and using `m` for dependencies resolution. Depending on the root, not all values in `m` are used.

# TSTP parsing

Similar to `parse` but reading directly from a file or stdin.