Classical affine logic for intuitionists.

Pprop.lean

structure Pprop : Type where
  pos : Prop
  neg : Prop
  syn : pos → neg → False := by intros; assumption
namespace Pprop

instance : CoeSort Pprop Prop := ⟨Pprop.pos⟩
instance : Coe Bool Pprop where
  coe
  | true => {pos := True, neg := False}
  | false => {pos := False, neg := True}
instance : Coe Prop Pprop where
  coe P := {
    pos := P
    neg := ¬P
    syn := fun p q => q p
  }

def Null : Pprop where
  pos := False
  neg := False

instance : AndOp Pprop where
  and P Q := {
    pos := P.pos ∧ Q.pos,
    neg := P.neg ∨ Q.neg,
    syn := by
      intros h h'
      cases h' with
      | inl np => exact P.syn h.left np
      | inr nq => exact Q.syn h.right nq
  }

instance : Neg Pprop where
  neg P := ⟨P.neg, P.pos, flip P.syn⟩
theorem double_negation (P : Pprop) : -(-P) = P := rfl

instance : OrOp Pprop where
  or P Q := -(-P &&& -Q)

def Tensor (P Q : Pprop) : Pprop where
  pos := P.pos ∧ Q.pos
  neg := (P.pos → Q.neg) ∧ (Q.pos → P.neg)
  syn h h' := P.syn h.left (h'.right h.right)
infixr:61 " ⊗ " => Tensor

def Par (P Q : Pprop) := -(-P ⊗ -Q)
infixr:54 " ⅋ " => Par

def Impl (P Q : Pprop) := -P ⅋ Q
infixr:53 " ⊸ " => Impl

theorem ppropext : P ⊸ Q → Q ⊸ P → P = Q := by
  intro ⟨pq, nqnp⟩ ⟨qp, npnq⟩
  have := propext ⟨pq, qp⟩
  have := propext ⟨npnq, nqnp⟩
  cases P; cases Q; simp
  constructor <;> assumption

theorem tensor_sym_aux : P ⊗ Q ⊸ Q ⊗ P := by
  constructor <;> intro ⟨_, _⟩ <;> constructor <;> assumption

theorem tensor_sym : P ⊗ Q = Q ⊗ P := by
  apply ppropext <;> apply tensor_sym_aux