Posted: Apr 14, 2012 12:45 pm
by VazScep
mizvekov 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'
Ah, yeah. There's loads of other stuff in my Bootstrap.hs file. I provided matchMP a few posts back

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
I can just send you the whole file if you'd like, though I had some fun getting these proofs.