# Intuitionistic tautology (`itauto`) decision procedure #

The `itauto` tactic will prove any intuitionistic tautology. It implements the well-known `G4ip` algorithm: [Dyckhoff, Contraction-free sequent calculi for intuitionistic logic][dyckhoff_1992].

All built in propositional connectives are supported: `True`, `False`, `And`, `Or`, `→`, `Not`, `Iff`, `Xor'`, as well as `Eq` and `Ne` on propositions. Anything else, including definitions and predicate logical connectives (`∀` and `∃`), are not supported, and will have to be simplified or instantiated before calling this tactic.

The resulting proofs will never use any axioms except possibly `propext`, and `propext` is only used if the input formula contains an equality of propositions `p = q`. Using `itauto!`, one can enable the selective use of LEM for case splitting on specified propositions.

## Implementation notes #

The core logic of the prover is in three functions:

- `prove : Context → IProp → StateM Nat (Bool × Proof)`: The main entry point. Gets a context and a goal, and returns a `proof` object or fails, using `StateM Nat` for the name generator.
- `search : Context → IProp → StateM Nat (Bool × Proof)`: Same meaning as `proof`, called during the search phase (see below).
- `Context.add : IProp → Proof → Context → Except (IProp → Proof) Context`: Adds a proposition with its proof into the context, but it also does some simplifications on the spot while doing so. It will either return the new context, or if it happens to notice a proof of false, it will return a function to compute a proof of any proposition in the original context.

The intuitionistic logic rules are separated into three groups:

- level 1: No splitting, validity preserving: apply whenever you can. Left rules in `Context.add`, right rules in `prove`.
  - `Context.add`:
    - simplify `Γ, ⊤ ⊢ B` to `Γ ⊢ B`
    - `Γ, ⊥ ⊢ B` is true
    - simplify `Γ, A ∧ B ⊢ C` to `Γ, A, B ⊢ C`
    - simplify `Γ, ⊥ → A ⊢ B` to `Γ ⊢ B`
    - simplify `Γ, ⊤ → A ⊢ B` to `Γ, A ⊢ B`
    - simplify `Γ, A ∧ B → C ⊢ D` to `Γ, A → B → C ⊢ D`
    - simplify `Γ, A ∨ B → C ⊢ D` to `Γ, A → C, B → C ⊢ D`
  - `prove`:
    - `Γ ⊢ ⊤` is true
    - simplify `Γ ⊢ A → B` to `Γ, A ⊢ B`
  - `search`:
    - `Γ, P ⊢ P` is true
    - simplify `Γ, P, P → A ⊢ B` to `Γ, P, A ⊢ B`
- level 2: Splitting rules, validity preserving: apply after level 1 rules. Done in `prove`
  - simplify `Γ ⊢ A ∧ B` to `Γ ⊢ A` and `Γ ⊢ B`
  - simplify `Γ, A ∨ B ⊢ C` to `Γ, A ⊢ C` and `Γ, B ⊢ C`
- level 3: Splitting rules, not validity preserving: apply only if nothing else applies. Done in `search`
  - `Γ ⊢ A ∨ B` follows from `Γ ⊢ A`
  - `Γ ⊢ A ∨ B` follows from `Γ ⊢ B`
  - `Γ, (A₁ → A₂) → C ⊢ B` follows from `Γ, A₂ → C, A₁ ⊢ A₂` and `Γ, C ⊢ B`

This covers the core algorithm, which only handles `True`, `False`, `And`, `Or`, and `→`. For `Iff` and `Eq`, we treat them essentially the same as `(p → q) ∧ (q → p)`, although we use a different `IProp` representation because we have to remember to apply different theorems during replay. For definitions like `Not` and `Xor'`, we just eagerly unfold them. (This could potentially cause a blowup issue for `Xor'`, but it isn't used very often anyway. We could add it to the `IProp` grammar if it matters.)

## Tags #

propositional logic, intuitionistic logic, decision procedure

source
inductive Mathlib.Tactic.ITauto.AndKind :
Type

Different propositional constructors that are variants of "and" for the purposes of the theorem prover.

- and : AndKind
- iff : AndKind
- eq : AndKind

Instances For

source
instance Mathlib.Tactic.ITauto.instToExprAndKind :
Lean.ToExpr AndKind
Equations

- Mathlib.Tactic.ITauto.instToExprAndKind = { toExpr := Mathlib.Tactic.ITauto.instToExprAndKind.toExpr, toTypeExpr := Lean.Expr.const `Mathlib.Tactic.ITauto.AndKind [] }

source
def Mathlib.Tactic.ITauto.instToExprAndKind.toExpr :
AndKind → Lean.Expr
Equations

- Mathlib.Tactic.ITauto.instToExprAndKind.toExpr Mathlib.Tactic.ITauto.AndKind.and = Lean.Expr.const `Mathlib.Tactic.ITauto.AndKind.and []
- Mathlib.Tactic.ITauto.instToExprAndKind.toExpr Mathlib.Tactic.ITauto.AndKind.iff = Lean.Expr.const `Mathlib.Tactic.ITauto.AndKind.iff []
- Mathlib.Tactic.ITauto.instToExprAndKind.toExpr Mathlib.Tactic.ITauto.AndKind.eq = Lean.Expr.const `Mathlib.Tactic.ITauto.AndKind.eq []

Instances For

source
instance Mathlib.Tactic.ITauto.instDecidableEqAndKind :
DecidableEq AndKind
Equations

- Mathlib.Tactic.ITauto.instDecidableEqAndKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

source
instance Mathlib.Tactic.ITauto.instInhabitedAndKind :
Inhabited AndKind
Equations

- Mathlib.Tactic.ITauto.instInhabitedAndKind = { default := Mathlib.Tactic.ITauto.AndKind.and }

source
inductive Mathlib.Tactic.ITauto.IProp :
Type

A reified inductive type for propositional logic.

- var : ℕ → IProp
- true : IProp
- false : IProp
- and' : AndKind → IProp → IProp → IProp
- or : IProp → IProp → IProp
- imp : IProp → IProp → IProp

Instances For

source
instance Mathlib.Tactic.ITauto.instToExprIProp :
Lean.ToExpr IProp
Equations

- Mathlib.Tactic.ITauto.instToExprIProp = { toExpr := Mathlib.Tactic.ITauto.instToExprIProp.toExpr, toTypeExpr := Lean.Expr.const `Mathlib.Tactic.ITauto.IProp [] }

source
def Mathlib.Tactic.ITauto.instToExprIProp.toExpr :
IProp → Lean.Expr
Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.ITauto.instToExprIProp.toExpr (Mathlib.Tactic.ITauto.IProp.var a) = (Lean.Expr.const `Mathlib.Tactic.ITauto.IProp.var []).app (Lean.toExpr a)
- Mathlib.Tactic.ITauto.instToExprIProp.toExpr Mathlib.Tactic.ITauto.IProp.true = Lean.Expr.const `Mathlib.Tactic.ITauto.IProp.true []
- Mathlib.Tactic.ITauto.instToExprIProp.toExpr Mathlib.Tactic.ITauto.IProp.false = Lean.Expr.const `Mathlib.Tactic.ITauto.IProp.false []

Instances For

source
def Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (x✝ x✝¹ : IProp) :
Decidable (x✝ = x✝¹)
Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.var a) (Mathlib.Tactic.ITauto.IProp.var b) = if h : a = b then h ▸ isTrue ⋯ else isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.var a) Mathlib.Tactic.ITauto.IProp.true = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.var a) Mathlib.Tactic.ITauto.IProp.false = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.var a) (Mathlib.Tactic.ITauto.IProp.and' a_1 a_2 a_3) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.var a) (a_1.or a_2) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.var a) (a_1.imp a_2) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.true (Mathlib.Tactic.ITauto.IProp.var a) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.true Mathlib.Tactic.ITauto.IProp.true = isTrue ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.true Mathlib.Tactic.ITauto.IProp.false = isFalse Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq._proof_9
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.true (Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.true (a.or a_1) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.true (a.imp a_1) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.false (Mathlib.Tactic.ITauto.IProp.var a) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.false Mathlib.Tactic.ITauto.IProp.true = isFalse Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq._proof_14
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.false Mathlib.Tactic.ITauto.IProp.false = isTrue ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.false (Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.false (a.or a_1) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq Mathlib.Tactic.ITauto.IProp.false (a.imp a_1) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2) (Mathlib.Tactic.ITauto.IProp.var a_3) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2) Mathlib.Tactic.ITauto.IProp.true = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2) Mathlib.Tactic.ITauto.IProp.false = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2) (a_3.or a_4) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (Mathlib.Tactic.ITauto.IProp.and' a a_1 a_2) (a_3.imp a_4) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (a.or a_1) (Mathlib.Tactic.ITauto.IProp.var a_2) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (a.or a_1) Mathlib.Tactic.ITauto.IProp.true = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (a.or a_1) Mathlib.Tactic.ITauto.IProp.false = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (a.or a_1) (Mathlib.Tactic.ITauto.IProp.and' a_2 a_3 a_4) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (a.or a_1) (a_2.imp a_3) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (a.imp a_1) (Mathlib.Tactic.ITauto.IProp.var a_2) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (a.imp a_1) Mathlib.Tactic.ITauto.IProp.true = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (a.imp a_1) Mathlib.Tactic.ITauto.IProp.false = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (a.imp a_1) (Mathlib.Tactic.ITauto.IProp.and' a_2 a_3 a_4) = isFalse ⋯
- Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq (a.imp a_1) (a_2.or a_3) = isFalse ⋯

Instances For

source
instance Mathlib.Tactic.ITauto.instDecidableEqIProp :
DecidableEq IProp
Equations

- Mathlib.Tactic.ITauto.instDecidableEqIProp = Mathlib.Tactic.ITauto.instDecidableEqIProp.decEq

source
@[match_pattern]
def Mathlib.Tactic.ITauto.IProp.and :
IProp → IProp → IProp

Constructor for `p ∧ q`.

Equations

- Mathlib.Tactic.ITauto.IProp.and = Mathlib.Tactic.ITauto.IProp.and' Mathlib.Tactic.ITauto.AndKind.and

Instances For

source
@[match_pattern]
def Mathlib.Tactic.ITauto.IProp.iff :
IProp → IProp → IProp

Constructor for `p ↔ q`.

Equations

- Mathlib.Tactic.ITauto.IProp.iff = Mathlib.Tactic.ITauto.IProp.and' Mathlib.Tactic.ITauto.AndKind.iff

Instances For

source
@[match_pattern]
def Mathlib.Tactic.ITauto.IProp.eq :
IProp → IProp → IProp

Constructor for `p = q`.

Equations

- Mathlib.Tactic.ITauto.IProp.eq = Mathlib.Tactic.ITauto.IProp.and' Mathlib.Tactic.ITauto.AndKind.eq

Instances For

source
@[match_pattern]
def Mathlib.Tactic.ITauto.IProp.not (a : IProp) :
IProp

Constructor for `¬ p`.

Equations

- a.not = a.imp Mathlib.Tactic.ITauto.IProp.false

Instances For

source
@[match_pattern]
def Mathlib.Tactic.ITauto.IProp.xor (a b : IProp) :
IProp

Constructor for `xor p q`.

Equations

- a.xor b = (a.and b.not).or (b.and a.not)

Instances For

source
instance Mathlib.Tactic.ITauto.instInhabitedIProp :
Inhabited IProp
Equations

- Mathlib.Tactic.ITauto.instInhabitedIProp = { default := Mathlib.Tactic.ITauto.IProp.true }

source
def Mathlib.Tactic.ITauto.AndKind.sides :
AndKind → IProp → IProp → IProp × IProp

Given the contents of an `And` variant, return the two conjuncts.

Equations

- Mathlib.Tactic.ITauto.AndKind.and.sides x✝¹ x✝ = (x✝¹, x✝)
- x✝².sides x✝¹ x✝ = (x✝¹.imp x✝, x✝.imp x✝¹)

Instances For

source
def Mathlib.Tactic.ITauto.IProp.format :
IProp → Std.Format

Debugging printer for propositions.

Equations

- (Mathlib.Tactic.ITauto.IProp.var i).format = Std.format "v" ++ Std.format i
- Mathlib.Tactic.ITauto.IProp.true.format = Std.format "⊤"
- Mathlib.Tactic.ITauto.IProp.false.format = Std.format "⊥"
- (Mathlib.Tactic.ITauto.IProp.and' Mathlib.Tactic.ITauto.AndKind.and p q).format = Std.format "(" ++ Std.format p.format ++ Std.format " ∧ " ++ Std.format q.format ++ Std.format ")"
- (Mathlib.Tactic.ITauto.IProp.and' Mathlib.Tactic.ITauto.AndKind.iff p q).format = Std.format "(" ++ Std.format p.format ++ Std.format " ↔ " ++ Std.format q.format ++ Std.format ")"
- (Mathlib.Tactic.ITauto.IProp.and' Mathlib.Tactic.ITauto.AndKind.eq p q).format = Std.format "(" ++ Std.format p.format ++ Std.format " = " ++ Std.format q.format ++ Std.format ")"
- (p.or q).format = Std.format "(" ++ Std.format p.format ++ Std.format " ∨ " ++ Std.format q.format ++ Std.format ")"
- (p.imp q).format = Std.format "(" ++ Std.format p.format ++ Std.format " → " ++ Std.format q.format ++ Std.format ")"

Instances For

source
instance Mathlib.Tactic.ITauto.instToFormatIProp :
Std.ToFormat IProp
Equations

- Mathlib.Tactic.ITauto.instToFormatIProp = { format := Mathlib.Tactic.ITauto.IProp.format }

source
def Mathlib.Tactic.ITauto.AndKind.cmp (p q : AndKind) :
Ordering

A comparator for `AndKind`. (There should really be a derive handler for this.)

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.ITauto.IProp.cmp (p q : IProp) :
Ordering

A comparator for propositions. (There should really be a derive handler for this.)

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Mathlib.Tactic.ITauto.instLTIProp :
LT IProp
Equations

- Mathlib.Tactic.ITauto.instLTIProp = { lt := fun (p q : Mathlib.Tactic.ITauto.IProp) => p.cmp q = Ordering.lt }

source
instance Mathlib.Tactic.ITauto.instDecidableLTIProp :
DecidableLT IProp
Equations

- Mathlib.Tactic.ITauto.instDecidableLTIProp x✝¹ x✝ = inferInstanceAs (Decidable (x✝¹.cmp x✝ = Ordering.lt))

source
inductive Mathlib.Tactic.ITauto.Proof :
Type

A reified inductive proof type for intuitionistic propositional logic.

- sorry : Proof

  `⊢ A`, causes failure during reconstruction

- hyp (n : Lean.Name) : Proof

  `(n: A) ⊢ A`

- triv : Proof

  `⊢ ⊤`

- exfalso' (p : Proof) : Proof

  `(p: ⊥) ⊢ A`

- intro (x : Lean.Name) (p : Proof) : Proof

  `(p: (x: A) ⊢ B) ⊢ A → B`

- andLeft (ak : AndKind) (p : Proof) : Proof
  - `ak = .and`: `(p: A ∧ B) ⊢ A`
  - `ak = .iff`: `(p: A ↔ B) ⊢ A → B`
  - `ak = .eq`: `(p: A = B) ⊢ A → B`
- andRight (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`
- andIntro (ak : AndKind) (p₁ 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`
- curry (ak : AndKind) (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 q : 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`
- app' : Proof → Proof → Proof

  `(p: A → B) (q: A) ⊢ B`

- orImpL (p : Proof) : Proof

  `(p: A ∨ B → C) ⊢ A → C`

- orImpR (p : Proof) : Proof

  `(p: A ∨ B → C) ⊢ B → C`

- orInL (p : Proof) : Proof

  `(p: A) ⊢ A ∨ B`

- orInR (p : Proof) : Proof

  `(p: B) ⊢ A ∨ B`

- orElim' (p₁ : Proof) (x : Lean.Name) (p₂ p₃ : Proof) : Proof

  `(p₁: A ∨ B) (p₂: (x: A) ⊢ C) (p₃: (x: B) ⊢ C) ⊢ C`

- decidableElim (classical : Bool) (p₁ x : Lean.Name) (p₂ p₃ : Proof) : Proof

  `(p₁: Decidable A) (p₂: (x: A) ⊢ C) (p₃: (x: ¬ A) ⊢ C) ⊢ C`

- em (classical : Bool) (p : Lean.Name) : Proof
  - `classical = false`: `(p: Decidable A) ⊢ A ∨ ¬A`
  - `classical = true`: `(p: Prop) ⊢ p ∨ ¬p`
- impImpSimp (x : Lean.Name) (p : Proof) : Proof

  The variable `x` here names the variable that will be used in the elaborated proof.

  - `(p: ((x:A) → B) → C) ⊢ B → C`

Instances For

source
instance Mathlib.Tactic.ITauto.instToExprProof :
Lean.ToExpr Proof
Equations

- Mathlib.Tactic.ITauto.instToExprProof = { toExpr := Mathlib.Tactic.ITauto.instToExprProof.toExpr, toTypeExpr := Lean.Expr.const `Mathlib.Tactic.ITauto.Proof [] }

source
def Mathlib.Tactic.ITauto.instToExprProof.toExpr :
Proof → Lean.Expr
Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.ITauto.instToExprProof.toExpr Mathlib.Tactic.ITauto.Proof.sorry = Lean.Expr.const `Mathlib.Tactic.ITauto.Proof.sorry []
- Mathlib.Tactic.ITauto.instToExprProof.toExpr (Mathlib.Tactic.ITauto.Proof.hyp a) = (Lean.Expr.const `Mathlib.Tactic.ITauto.Proof.hyp []).app (Lean.toExpr a)
- Mathlib.Tactic.ITauto.instToExprProof.toExpr Mathlib.Tactic.ITauto.Proof.triv = Lean.Expr.const `Mathlib.Tactic.ITauto.Proof.triv []
- Mathlib.Tactic.ITauto.instToExprProof.toExpr a.exfalso' = (Lean.Expr.const `Mathlib.Tactic.ITauto.Proof.exfalso' []).app (Mathlib.Tactic.ITauto.instToExprProof.toExpr a)
- Mathlib.Tactic.ITauto.instToExprProof.toExpr a.orImpL = (Lean.Expr.const `Mathlib.Tactic.ITauto.Proof.orImpL []).app (Mathlib.Tactic.ITauto.instToExprProof.toExpr a)
- Mathlib.Tactic.ITauto.instToExprProof.toExpr a.orImpR = (Lean.Expr.const `Mathlib.Tactic.ITauto.Proof.orImpR []).app (Mathlib.Tactic.ITauto.instToExprProof.toExpr a)
- Mathlib.Tactic.ITauto.instToExprProof.toExpr a.orInL = (Lean.Expr.const `Mathlib.Tactic.ITauto.Proof.orInL []).app (Mathlib.Tactic.ITauto.instToExprProof.toExpr a)
- Mathlib.Tactic.ITauto.instToExprProof.toExpr a.orInR = (Lean.Expr.const `Mathlib.Tactic.ITauto.Proof.orInR []).app (Mathlib.Tactic.ITauto.instToExprProof.toExpr a)
- Mathlib.Tactic.ITauto.instToExprProof.toExpr (Mathlib.Tactic.ITauto.Proof.em a a_1) = ((Lean.Expr.const `Mathlib.Tactic.ITauto.Proof.em []).app (Lean.toExpr a)).app (Lean.toExpr a_1)

Instances For

source
instance Mathlib.Tactic.ITauto.instInhabitedProof :
Inhabited Proof
Equations

- Mathlib.Tactic.ITauto.instInhabitedProof = { default := Mathlib.Tactic.ITauto.Proof.triv }

source
def Mathlib.Tactic.ITauto.Proof.format :
Proof → Std.Format

Debugging printer for proof objects.

Equations

- One or more equations did not get rendered due to their size.
- Mathlib.Tactic.ITauto.Proof.sorry.format = Std.Format.text "sorry"
- (Mathlib.Tactic.ITauto.Proof.hyp i).format = Std.format i
- Mathlib.Tactic.ITauto.Proof.triv.format = Std.Format.text "triv"
- p.exfalso'.format = Std.format "(exfalso " ++ Std.format p.format ++ Std.format ")"
- (Mathlib.Tactic.ITauto.Proof.intro x_1 p).format = Std.format "(fun " ++ Std.format x_1 ++ Std.format " ↦ " ++ Std.format p.format ++ Std.format ")"
- (Mathlib.Tactic.ITauto.Proof.andLeft ak p).format = Std.format p.format ++ Std.format " .1"
- (Mathlib.Tactic.ITauto.Proof.andRight ak p).format = Std.format p.format ++ Std.format " .2"
- (Mathlib.Tactic.ITauto.Proof.andIntro ak p q).format = Std.format "⟨" ++ Std.format p.format ++ Std.format ", " ++ Std.format q.format ++ Std.format "⟩"
- (Mathlib.Tactic.ITauto.Proof.curry ak p).format = Std.format "(curry " ++ Std.format p.format ++ Std.format ")"
- (Mathlib.Tactic.ITauto.Proof.curry₂ ak p q).format = Std.format "(curry " ++ Std.format p.format ++ Std.format " " ++ Std.format q.format ++ Std.format ")"
- (p.app' q).format = Std.format "(" ++ Std.format p.format ++ Std.format " " ++ Std.format q.format ++ Std.format ")"
- p.orImpL.format = Std.format "(orImpL " ++ Std.format p.format ++ Std.format ")"
- p.orImpR.format = Std.format "(orImpR " ++ Std.format p.format ++ Std.format ")"
- p.orInL.format = Std.format "(Or.inl " ++ Std.format p.format ++ Std.format ")"
- p.orInR.format = Std.format "(Or.inr " ++ Std.format p.format ++ Std.format ")"
- (Mathlib.Tactic.ITauto.Proof.em false p).format = Std.format "(Decidable.em " ++ Std.format p ++ Std.format ")"
- (Mathlib.Tactic.ITauto.Proof.em true p).format = Std.format "(Classical.em " ++ Std.format p ++ Std.format ")"
- (Mathlib.Tactic.ITauto.Proof.impImpSimp x_1 p).format = Std.format "(impImpSimp " ++ Std.format p.format ++ Std.format ")"

Instances For

source
instance Mathlib.Tactic.ITauto.instToFormatProof :
Std.ToFormat Proof
Equations

- Mathlib.Tactic.ITauto.instToFormatProof = { format := Mathlib.Tactic.ITauto.Proof.format }

source
def Mathlib.Tactic.ITauto.Proof.exfalso :
IProp → Proof → Proof

A variant on `Proof.exfalso'` that performs opportunistic simplification.

Equations

- Mathlib.Tactic.ITauto.Proof.exfalso Mathlib.Tactic.ITauto.IProp.false x✝ = x✝
- Mathlib.Tactic.ITauto.Proof.exfalso x✝¹ x✝ = x✝.exfalso'

Instances For

source
def Mathlib.Tactic.ITauto.Proof.orElim :
Proof → Lean.Name → Proof → Proof → Proof

A variant on `Proof.orElim'` that performs opportunistic simplification.

Equations

- (Mathlib.Tactic.ITauto.Proof.em cl p).orElim x✝² x✝¹ x✝ = Mathlib.Tactic.ITauto.Proof.decidableElim cl p x✝² x✝¹ x✝
- x✝³.orElim x✝² x✝¹ x✝ = x✝³.orElim' x✝² x✝¹ x✝

Instances For

source
def Mathlib.Tactic.ITauto.Proof.app :
Proof → Proof → Proof

A variant on `Proof.app'` that performs opportunistic simplification. (This doesn't do full normalization because we don't want the proof size to blow up.)

Equations

- (Mathlib.Tactic.ITauto.Proof.curry ak p).app x✝ = Mathlib.Tactic.ITauto.Proof.curry₂ ak p x✝
- (Mathlib.Tactic.ITauto.Proof.curry₂ ak p q).app x✝ = p.app (Mathlib.Tactic.ITauto.Proof.andIntro ak q x✝)
- p.orImpL.app x✝ = p.app x✝.orInL
- p.orImpR.app x✝ = p.app x✝.orInR
- (Mathlib.Tactic.ITauto.Proof.impImpSimp x_2 p).app x✝ = p.app (Mathlib.Tactic.ITauto.Proof.intro x_2 x✝)
- x✝¹.app x✝ = x✝¹.app' x✝

Instances For

source
@[inline]
def Mathlib.Tactic.ITauto.freshName :
StateM ℕ Lean.Name

Get a new name in the pattern `h0, h1, h2, ...`

Equations

- Mathlib.Tactic.ITauto.freshName n = (Lean.Name.mkSimple (toString "h" ++ toString n), n + 1)

Instances For

source
@[reducible, inline]
abbrev Mathlib.Tactic.ITauto.Context :
Type

The context during proof search is a map from propositions to proof values.

Equations

- Mathlib.Tactic.ITauto.Context = Std.TreeMap Mathlib.Tactic.ITauto.IProp Mathlib.Tactic.ITauto.Proof Mathlib.Tactic.ITauto.IProp.cmp

Instances For

source
def Mathlib.Tactic.ITauto.Context.format (Γ : Context) :
Std.Format

Debug printer for the context.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
instance Mathlib.Tactic.ITauto.instToFormatContext :
Std.ToFormat Context
Equations

- Mathlib.Tactic.ITauto.instToFormatContext = { format := Mathlib.Tactic.ITauto.Context.format }

source
partial def Mathlib.Tactic.ITauto.Context.add :
IProp → Proof → Context → Except (IProp → Proof) Context

Insert a proposition and its proof into the context, as in `have : A := p`. This will eagerly apply all level 1 rules on the spot, which are rules that don't split the goal and are validity preserving: specifically, we drop `⊤` and `A → ⊤` hypotheses, close the goal if we find a `⊥` hypothesis, split all conjunctions, and also simplify `⊥ → A` (drop), `⊤ → A` (simplify to `A`), `A ∧ B → C` (curry to `A → B → C`) and `A ∨ B → C` (rewrite to `(A → C) ∧ (B → C)` and split).

source
@[inline]
def Mathlib.Tactic.ITauto.Context.withAdd (Γ : Context) (A : IProp) (p : Proof) (B : IProp) (f : Context → IProp → StateM ℕ (Bool × Proof)) :
StateM ℕ (Bool × Proof)

Add `A` to the context `Γ` with proof `p`. This version of `Context.add` takes a continuation and a target proposition `B`, so that in the case that `⊥` is found we can skip the continuation and just prove `B` outright.

Equations

- Γ.withAdd A p B f = match Mathlib.Tactic.ITauto.Context.add A p Γ with | Except.ok Γ_A => f Γ_A B | Except.error p => pure (true, p B)

Instances For

source
def Mathlib.Tactic.ITauto.mapProof (f : Proof → Proof) :
Bool × Proof → Bool × Proof

Map a function over the proof (regardless of whether the proof is successful or not).

Equations

- Mathlib.Tactic.ITauto.mapProof f (b, p) = (b, f p)

Instances For

source
def Mathlib.Tactic.ITauto.isOk :
(Bool × Proof) × ℕ → Option (Proof × ℕ)

Convert a value-with-success to an optional value.

Equations

- Mathlib.Tactic.ITauto.isOk ((false, snd), snd_1) = none
- Mathlib.Tactic.ITauto.isOk ((true, p), n) = some (p, n)

Instances For

source
def Mathlib.Tactic.ITauto.whenOk :
Bool → IProp → StateM ℕ (Bool × Proof) → StateM ℕ (Bool × Proof)

Skip the continuation and return a failed proof if the Boolean is false.

Equations

- Mathlib.Tactic.ITauto.whenOk false x✝¹ x✝ = pure (false, Mathlib.Tactic.ITauto.Proof.sorry)
- Mathlib.Tactic.ITauto.whenOk true x✝¹ x✝ = x✝

Instances For

source
partial def Mathlib.Tactic.ITauto.search (Γ : Context) (B : IProp) :
StateM ℕ (Bool × Proof)

The search phase, which deals with the level 3 rules, which are rules that are not validity preserving and so require proof search. One obvious one is the or-introduction rule: we prove `A ∨ B` by proving `A` or `B`, and we might have to try one and backtrack.

There are two rules dealing with implication in this category: `p, p → C ⊢ B` where `p` is an atom (which is safe if we can find it but often requires the right search to expose the `p` assumption), and `(A₁ → A₂) → C ⊢ B`. We decompose the double implication into two subgoals: one to prove `A₁ → A₂`, which can be written `A₂ → C, A₁ ⊢ A₂` (where we used `A₁` to simplify `(A₁ → A₂) → C`), and one to use the consequent, `C ⊢ B`. The search here is that there are potentially many implications to split like this, and we have to try all of them if we want to be complete.

source
partial def Mathlib.Tactic.ITauto.prove (Γ : Context) (B : IProp) :
StateM ℕ (Bool × Proof)

The main prover. This receives a context of proven or assumed lemmas and a target proposition, and returns a proof or `none` (with state for the fresh variable generator). The intuitionistic logic rules are separated into three groups:

- level 1: No splitting, validity preserving: apply whenever you can. Left rules in `Context.add`, right rules in `prove`
- level 2: Splitting rules, validity preserving: apply after level 1 rules. Done in `prove`
- level 3: Splitting rules, not validity preserving: apply only if nothing else applies. Done in `search`

The level 1 rules on the right of the turnstile are `Γ ⊢ ⊤` and `Γ ⊢ A → B`, these are easy to handle. The rule `Γ ⊢ A ∧ B` is a level 2 rule, also handled here. If none of these apply, we try the level 2 rule `A ∨ B ⊢ C` by searching the context and splitting all ors we find. Finally, if we don't make any more progress, we go to the search phase.

source
partial def Mathlib.Tactic.ITauto.reify (e : Q(Prop)) :
AtomM IProp

Reify an `Expr` into a `IProp`, allocating anything non-propositional as an atom in the `AtomM` state.

source
partial def Mathlib.Tactic.ITauto.applyProof (g : Lean.MVarId) (Γ : Lean.NameMap Lean.Expr) (p : Proof) :
Lean.MetaM Unit

Once we have a proof object, we have to apply it to the goal.

source
def Mathlib.Tactic.ITauto.itautoCore (g : Lean.MVarId) (useDec useClassical : Bool) (extraDec : Array Lean.Expr) :
Lean.MetaM Unit

A decision procedure for intuitionistic propositional logic.

- `useDec` will add `a ∨ ¬ a` to the context for every decidable atomic proposition `a`.
- `useClassical` will allow `a ∨ ¬ a` to be added even if the proposition is not decidable, using classical logic.
- `extraDec` will add `a ∨ ¬ a` to the context for specified (not necessarily atomic) propositions `a`.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.ITauto.itauto :
Lean.ParserDescr

A decision procedure for intuitionistic propositional logic. Unlike `finish` and `tauto!` this tactic never uses the law of excluded middle (without the `!` option), and the proof search is tailored for this use case. (`itauto!` will work as a classical SAT solver, but the algorithm is not very good in this situation.)

    example (p : Prop) : ¬ (p ↔ ¬ p) := by itauto

`itauto [a, b]` will additionally attempt case analysis on `a` and `b` assuming that it can derive `Decidable a` and `Decidable b`. `itauto *` will case on all decidable propositions that it can find among the atomic propositions, and `itauto! *` will case on all propositional atoms. Warning: This can blow up the proof search, so it should be used sparingly.

Equations

- One or more equations did not get rendered due to their size.

Instances For

source
def Mathlib.Tactic.ITauto.itauto! :
Lean.ParserDescr

A decision procedure for intuitionistic propositional logic. Unlike `finish` and `tauto!` this tactic never uses the law of excluded middle (without the `!` option), and the proof search is tailored for this use case. (`itauto!` will work as a classical SAT solver, but the algorithm is not very good in this situation.)

    example (p : Prop) : ¬ (p ↔ ¬ p) := by itauto

`itauto [a, b]` will additionally attempt case analysis on `a` and `b` assuming that it can derive `Decidable a` and `Decidable b`. `itauto *` will case on all decidable propositions that it can find among the atomic propositions, and `itauto! *` will case on all propositional atoms. Warning: This can blow up the proof search, so it should be used sparingly.

Equations

- One or more equations did not get rendered due to their size.

Instances For