namespace http://cds.omdoc.org/examples

// @_title Propositional Logic in MMT❙
// @_author Florian Rabe❙

/T   
Intuitionistic propositional logic with natural deduction rules and a few example proofs ❚

/T We use LF as the meta-theory for all theories in this file.❚
fixmeta http://cds.omdoc.org/urtheories?LF

/T    
We start with the syntax of propositional logic.❚

theory PL =

  # :types The Basic Concepts
  
  /T the type of propositions ❙
  prop  : type 
  
  /T Given [F:prop], the type $⊦ F$ holds the proofs of $F$.❙
  ded   : prop ⟶ type          #  1  prec -5role Judgment
  
  ## Abbreviations
  
  /T The type $contra$ abbreviates the judgment of inconsistency.
     If we can give an element of the type, then every proposition has a proof.❙
  contra : type  = {a} ⊦ a #              

  # Constructors

  /T The constructors provide the expressions of the types above.❙
  
  true  : prop                                   
  false : prop                                   
  and   : prop ⟶ prop ⟶ prop   # 1  2 prec 15
  or    : prop ⟶ prop ⟶ prop   # 1  2 prec 15
  impl  : prop ⟶ prop ⟶ prop   # 1  2 prec 10
  not   : prop ⟶ prop          # ¬ 1   prec 20

  /T Equivalence is taken as a non-primitive here and defined such that for [F:prop,G:prop] we define $F⇔G$ as $(F ⇒ G) ∧ (G ⇒ F)$.❙
  equiv : prop ⟶ prop ⟶ prop   # 1  2 prec 10
        = [x,y] (x ⇒ y) ∧ (y ⇒ x)


/T   Now we describe the proof theory.❚        

theory PLNatDed =
  include ?PL 
  
  /T We use natural ⊦uction proof rules that construct expressions of type $⊦ F$ for some [F:prop].
  {For example, assume two propositions [F: prop, G: prop].
    {If [p:⊦ F, q: ⊦ G], then $andI p q$ is a proof of $F∧G$.}
    {If [p:⊦ F∧G], then $andEl p$ is a proof of $F$.}
  }


  trueI : ⊦ true
  falseE : ⊦ false ⟶ ↯
  andI  : {A,B} ⊦ A ⟶ ⊦ B ⟶ ⊦ A ∧ B   
  andEl : {A,B} ⊦ A ∧ B ⟶ ⊦ A            role ForwardRule
  andEr : {A,B} ⊦ A ∧ B ⟶ ⊦ B            role ForwardRule

  orIl  : {A,B} ⊦ A ⟶ ⊦ A ∨ B           
  orIr  : {A,B} ⊦ B ⟶ ⊦ A ∨ B           
  orE   : {A,B,C} ⊦ A ∨ B ⟶ (⊦ A ⟶ ⊦ C) ⟶ (⊦ B ⟶ ⊦ C) ⟶ ⊦ C
  
  impI  : {A,B} (⊦ A ⟶ ⊦ B) ⟶ ⊦ A ⇒ B 
  impE  : {A,B} ⊦ A ⇒ B ⟶ ⊦ A ⟶ ⊦ B    role ForwardRule

  notI  : {A} (⊦ A ⟶ ↯) ⟶ ⊦ ¬ A# notI 2
  notE  : {A} ⊦ ¬ A ⟶ ⊦ A ⟶ ↯  # notE 2 3 role ForwardRule

  equivI : {A,B} (⊦ A ⟶ ⊦ B) ⟶ (⊦ B ⟶ ⊦ A) ⟶ ⊦ A ⇔ B  
         = [A,B,p,q] andI (impI [x] p x) (impI [x] q x)  
         
  equivEl : {A,B} ⊦ A ⇔ B ⟶ ⊦ A ⟶ ⊦ B  role ForwardRule
          = [A,B,p,a] impE (andEl p) a 
  equivEr : {A,B} ⊦ A ⇔ B ⟶ ⊦ B ⟶ ⊦ A  role ForwardRule
          = [A,B,p,b] impE (andEr p) b 
        
  imp2I : {A,B,C} (⊦ A ⟶ (⊦ B ⟶ ⊦ C)) ⟶ ⊦ A ⇒ (B ⇒ C) 
        = [A,B,C] [f] impI [p] (impI ([q] f p q))             
  
  imp2E : {A,B,C} ⊦ A ⇒ (B ⇒ C) ⟶ ⊦ A ⟶ ⊦ B ⟶ ⊦ C    
        = [A,B,C] [p,q,r] impE (impE p q) r                   

  example : {A} ⊦ A ⇒ (A ∧ A)  
          = [A]impI [p]andI p p


theory DeclarativeProofs =
  include ?PL

  cut : {A,B} ⊦A ⟶ (⊦A ⟶ ⊦B) ⟶ ⊦B
      = [A,B,p,q] q p # PROVE 1 BY 3 4
  
  have : {A} ⊦A ⟶ ⊦A = [A,p] p # HAVE 1 BY 2


theory Declarative_PL =
  include ?PLNatDed
  include ?DeclarativeProofs
  
  decl_trueI = trueI # TRIVIAL
  
  decl_falseE = falseE # EXFALSO 1 
  
  decl_andE : {A,B,C} ⊦ A∧B ⟶ (⊦A ⟶ ⊦B ⟶ ⊦C) ⟶ ⊦C
            = [A,B,C,p,q] q (andEl p) (andEr p) # FROM 4 OBTAIN 5   
  
  decl_orE  = orE # SPLIT 4 CASE 5 CASE 6 prec -10050
  
  decl_impI = impI  # SUPPOSE 1 3 prec 500
  
  example: {A,B,C} ⊦ A∧B ⇒ ((B⇒C)∨C ⇒ C)  = [A,B,C]
    SUPPOSE (A∧B) [ab]▪
    SUPPOSE ((B⇒C)∨C) [bc]▪
    PROVE B BY (
      FROM ab OBTAIN [a,b]▪
      HAVE B BY b
    )[b]▪
    SPLIT bc
      CASE [r] HAVE C BY ≪⊦C≫
      CASE [r] HAVE C BY r
  
  
  example2: {A,B,C} ⊦ A∧B ⇒ ((B⇒C)∨C ⇒ C) = [A,B,C] impI[p]impI[q]orE q ([r] impE r (andEr p)) ([r]r)


import rules scala://lf.mmt.kwarc.info
theory ProofIrrelevance =
  include ?PL
  /T a rule that makes all terms of type ded F equal❙
  rule rules?TermIrrelevanceRule ded