Posted:

**Apr 14, 2012 12:45 pm**Ah, yeah. There's loads of other stuff in my Bootstrap.hs file. I provided matchMP a few posts backmizvekov wrote:Hey, trying to give this one a go, but it fails to compile, several missing symbols:

- Code: Select all
`Conversions.hs:20:26: Not in scope: `matchMP'`

Conversions.hs:20:34: Not in scope: `eqMP'

Conversions.hs:26:32: Not in scope: `matchMP'

Conversions.hs:27:69: Not in scope: `substLeft'

Conversions.hs:33:32: Not in scope: `matchMP'

Conversions.hs:34:70: Not in scope: `substRight'

Conversions.hs:40:29: Not in scope: `matchMP'

Conversions.hs:40:37: Not in scope: `substNot'

Conversions.hs:62:27: Not in scope: `matchMP'

Conversions.hs:62:35: Not in scope: `trans'

Conversions.hs:63:18: Not in scope: `matchMP'

Conversions.hs:69:39: Not in scope: `reflEq'

- Code: Select all
`-- matchMP (P → Q) (Γ ⊢ P') attempts to match P with P', and then applies MP.`

matchMP :: Theorem String -> Proof -> Proof

matchMP imp ant =

let antT = concl ant in

case theoremTerm imp of

p :=>: q ->

case match p antT of

[insts] -> MP (UseTheorem $ instM Var insts imp) ant

_ -> error "MATCH MP"

_ -> error "MATCH MP"

The rest are all theorems:

- Code: Select all
`-- ⊢ (P → Q → R) ↔ (P ∧ Q → R)`

uncurry :: Theorem String

-- ⊢ ¬¬P → P

dblNegElim :: Theorem String

-- ⊢ P → ¬¬P

dblNegIntro :: Theorem String

-- ⊢ P → Q → P ∧ Q

conjI :: Theorem String

-- ⊢ (X ↔ Y) → X → Y

eqMP :: Theorem String

-- ⊢ (X ↔ X)

reflEq :: Theorem String

-- ⊢ (X ↔ Y) ↔ (Y ↔ X)

symEq :: Theorem String

-- ⊢ (X ↔ Y) → (Y ↔ Z) → (X ↔ Z)

trans :: Theorem String

-- ⊢ (X ↔ Y) → (X → P ↔ Y → P)

substLeft :: Theorem String

-- ⊢ (X ↔ Y) → (P → X ↔ P → Y)

substRight :: Theorem String

-- ⊢ (X ↔ Y) → (¬X ↔ ¬Y)

substNot :: Theorem String