Definitional double negation in intuitionistic logic

Stream: lean4

[Trebor Huang]

I've written some Lean 4 code with this theorem:

theorem double_negation (P : Pprop) : -(-P) = P := rfl

that is purely intuitionistic. Apart from the ghastly reuse of negation as logical negation, is there anything I should know about Lean 4 that could improve the code? This implements the basics of https://arxiv.org/abs/1805.07518

[Trebor Huang]

And if I want to go further, is there some good way I can automate parts of the theorem proving? It is mostly intuitionistic propositional logic after you unfold all the definitions, and I would probably add first order logic as well.

[Mario Carneiro]

I have only minor stylistic changes to suggest, the proofs are all pretty trivial so there isn't much to golf

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 := ⟨P, ¬P, 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 := fun
      | h, .inl np => P.syn h.left np
      | h, .inr nq => 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 tensor_sym : P ⊗ Q ⊸ Q ⊗ P := by
  constructor <;> intro ⟨_, _⟩ <;> constructor <;> assumption

[Trebor Huang]

Ahh using where for instances should have been obvious, but somehow I didn't.. Maybe I'm just not familiar enough. Thanks!