Proof — Mathlib

Lean4
/-- A reified inductive proof type for intuitionistic propositional logic. -/
inductive Proof/-- `⊢ A`, causes failure during reconstruction -/

  | sorry : Proof/-- `(n: A) ⊢ A` -/

  | hyp (n : Name) : Proof/-- `⊢ ⊤` -/

  | triv : Proof/-- `(p: ⊥) ⊢ A` -/

  | exfalso' (p : Proof) : Proof/-- `(p: (x: A) ⊢ B) ⊢ A → B` -/

  | intro (x : Name) (p : Proof) : Proof/-- * `ak = .and`: `(p: A ∧ B) ⊢ A`
  * `ak = .iff`: `(p: A ↔ B) ⊢ A → B`
  * `ak = .eq`: `(p: A = B) ⊢ A → B`
  -/

  | andLeft (ak : AndKind) (p : Proof) : Proof/-- * `ak = .and`: `(p: A ∧ B) ⊢ B`
  * `ak = .iff`: `(p: A ↔ B) ⊢ B → A`
  * `ak = .eq`: `(p: A = B) ⊢ B → A`
  -/

  | andRight (ak : AndKind) (p : Proof) : Proof/-- * `ak = .and`: `(p₁: A) (p₂: B) ⊢ A ∧ B`
  * `ak = .iff`: `(p₁: A → B) (p₁: B → A) ⊢ A ↔ B`
  * `ak = .eq`: `(p₁: A → B) (p₁: B → A) ⊢ A = B`
  -/

  | andIntro (ak : AndKind) (p₁ p₂ : Proof) : Proof/-- * `ak = .and`: `(p: A ∧ B → C) ⊢ A → B → C`
  * `ak = .iff`: `(p: (A ↔ B) → C) ⊢ (A → B) → (B → A) → C`
  * `ak = .eq`: `(p: (A = B) → C) ⊢ (A → B) → (B → A) → C`
  -/

  | curry (ak : AndKind) (p : Proof) : Proof/-- This is a partial application of curry.
  * `ak = .and`: `(p: A ∧ B → C) (q : A) ⊢ B → C`
  * `ak = .iff`: `(p: (A ↔ B) → C) (q: A → B) ⊢ (B → A) → C`
  * `ak = .eq`: `(p: (A ↔ B) → C) (q: A → B) ⊢ (B → A) → C`
  -/

  | curry₂ (ak : AndKind) (p q : Proof) : Proof/-- `(p: A → B) (q: A) ⊢ B` -/

  | app' : Proof → Proof → Proof/-- `(p: A ∨ B → C) ⊢ A → C` -/

  | orImpL (p : Proof) : Proof/-- `(p: A ∨ B → C) ⊢ B → C` -/

  | orImpR (p : Proof) : Proof/-- `(p: A) ⊢ A ∨ B` -/

  | orInL (p : Proof) : Proof/-- `(p: B) ⊢ A ∨ B` -/

  | orInR (p : Proof) : Proof/-- `(p₁: A ∨ B) (p₂: (x: A) ⊢ C) (p₃: (x: B) ⊢ C) ⊢ C` -/

  | orElim' (p₁ : Proof) (x : Name) (p₂ p₃ : Proof) : Proof/--
`(p₁: Decidable A) (p₂: (x: A) ⊢ C) (p₃: (x: ¬ A) ⊢ C) ⊢ C` -/

  | decidableElim (classical : Bool) (p₁ x : Name) (p₂ p₃ : Proof) : Proof/--
* `classical = false`: `(p: Decidable A) ⊢ A ∨ ¬A`
  * `classical = true`: `(p: Prop) ⊢ p ∨ ¬p`
  -/

  | em (classical : Bool) (p : Name) : Proof/--
The variable `x` here names the variable that will be used in the elaborated proof.
  * `(p: ((x:A) → B) → C) ⊢ B → C`
  -/

  | impImpSimp (x : Name) (p : Proof) : Proof
  deriving Lean.ToExpr
Похожие утверждения