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

inductive Mathlib.Tactic.ITauto.AndKind : Type

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

• and: Mathlib.Tactic.ITauto.AndKind
• iff: Mathlib.Tactic.ITauto.AndKind
• eq: Mathlib.Tactic.ITauto.AndKind

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

Equations

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

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

Equations

• Mathlib.Tactic.ITauto.instDecidableEqAndKind x y = if h : x.toCtorIdx = y.toCtorIdx then isTrue ⋯ else isFalse ⋯

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

Equations

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

inductive Mathlib.Tactic.ITauto.IProp : Type

A reified inductive type for propositional logic.

• var: ℕ → Mathlib.Tactic.ITauto.IProp
• true: Mathlib.Tactic.ITauto.IProp
• false: Mathlib.Tactic.ITauto.IProp
• and': Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp
• or: Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp
• imp: Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp

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

Equations

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

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

Equations

• Mathlib.Tactic.ITauto.instDecidableEqIProp = Mathlib.Tactic.ITauto.decEqIProp✝

@[match_pattern]

def Mathlib.Tactic.ITauto.IProp.and : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp

Constructor for p ∧ q.

Equations

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

@[match_pattern]

def Mathlib.Tactic.ITauto.IProp.iff : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp

Constructor for p ↔ q.

Equations

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

@[match_pattern]

def Mathlib.Tactic.ITauto.IProp.eq : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp

Constructor for p = q.

Equations

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

@[match_pattern]

def Mathlib.Tactic.ITauto.IProp.not (a : Mathlib.Tactic.ITauto.IProp) : Mathlib.Tactic.ITauto.IProp

Constructor for ¬ p.

Equations

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

@[match_pattern]

def Mathlib.Tactic.ITauto.IProp.xor (a : Mathlib.Tactic.ITauto.IProp) (b : Mathlib.Tactic.ITauto.IProp) : Mathlib.Tactic.ITauto.IProp

Constructor for xor p q.

Equations

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

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

Equations

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

def Mathlib.Tactic.ITauto.AndKind.sides : Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.IProp × Mathlib.Tactic.ITauto.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✝)

def Mathlib.Tactic.ITauto.IProp.format : Mathlib.Tactic.ITauto.IProp → Lean.Format

Debugging printer for propositions.

Equations

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

instance Mathlib.Tactic.ITauto.instToFormatIProp : Lean.ToFormat Mathlib.Tactic.ITauto.IProp

Equations

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

def Mathlib.Tactic.ITauto.AndKind.cmp (p : Mathlib.Tactic.ITauto.AndKind) (q : Mathlib.Tactic.ITauto.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.

def Mathlib.Tactic.ITauto.IProp.cmp (p : Mathlib.Tactic.ITauto.IProp) (q : Mathlib.Tactic.ITauto.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.

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

Equations

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

instance Mathlib.Tactic.ITauto.instDecidableRelIPropLt : DecidableRel LT.lt

Equations

• Mathlib.Tactic.ITauto.instDecidableRelIPropLt x✝ x = inferInstanceAs (Decidable (x✝.cmp x = Ordering.lt))

inductive Mathlib.Tactic.ITauto.Proof : Type

A reified inductive proof type for intuitionistic propositional logic.

• sorry: Mathlib.Tactic.ITauto.Proof

  ⊢ A, causes failure during reconstruction

• hyp: Lean.Name → Mathlib.Tactic.ITauto.Proof

  (n: A) ⊢ A

• triv: Mathlib.Tactic.ITauto.Proof

  ⊢ ⊤

• exfalso': Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof

  (p: ⊥) ⊢ A

• intro: Lean.Name → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof

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

• andLeft: Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
  • ak = .and: (p: A ∧ B) ⊢ A
  • ak = .iff: (p: A ↔ B) ⊢ A → B
  • ak = .eq: (p: A = B) ⊢ A → B
• andRight: Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof
  • ak = .and: (p: A ∧ B) ⊢ B
  • ak = .iff: (p: A ↔ B) ⊢ B → A
  • ak = .eq: (p: A = B) ⊢ B → A
• andIntro: Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.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: Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.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₂: Mathlib.Tactic.ITauto.AndKind → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.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': Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof

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

• orImpL: Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof

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

• orImpR: Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof

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

• orInL: Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof

  (p: A) ⊢ A ∨ B

• orInR: Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof

  (p: B) ⊢ A ∨ B

• orElim': Mathlib.Tactic.ITauto.Proof → Lean.Name → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof

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

• decidableElim: Bool → Lean.Name → Lean.Name → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof

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

• em: Bool → Lean.Name → Mathlib.Tactic.ITauto.Proof
  • classical = false: (p: Decidable A) ⊢ A ∨ ¬A
  • classical = true: (p: Prop) ⊢ p ∨ ¬p
• impImpSimp: Lean.Name → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof

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

  • (p: ((x:A) → B) → C) ⊢ B → C

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

Equations

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

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

Equations

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

def Mathlib.Tactic.ITauto.Proof.format : Mathlib.Tactic.ITauto.Proof → Lean.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 = Lean.format i
• Mathlib.Tactic.ITauto.Proof.triv.format = Std.Format.text "triv"
• p.exfalso'.format = Lean.format "(exfalso " ++ Lean.format p.format ++ Lean.format ")"
• (Mathlib.Tactic.ITauto.Proof.intro x_1 p).format = Lean.format "(fun " ++ Lean.format x_1 ++ Lean.format " ↦ " ++ Lean.format p.format ++ Lean.format ")"
• (Mathlib.Tactic.ITauto.Proof.andLeft ak p).format = Lean.format "" ++ Lean.format p.format ++ Lean.format " .1"
• (Mathlib.Tactic.ITauto.Proof.andRight ak p).format = Lean.format "" ++ Lean.format p.format ++ Lean.format " .2"
• (Mathlib.Tactic.ITauto.Proof.andIntro ak p q).format = Lean.format "⟨" ++ Lean.format p.format ++ Lean.format ", " ++ Lean.format q.format ++ Lean.format "⟩"
• (Mathlib.Tactic.ITauto.Proof.curry ak p).format = Lean.format "(curry " ++ Lean.format p.format ++ Lean.format ")"
• (Mathlib.Tactic.ITauto.Proof.curry₂ ak p q).format = Lean.format "(curry " ++ Lean.format p.format ++ Lean.format " " ++ Lean.format q.format ++ Lean.format ")"
• (p.app' q).format = Lean.format "(" ++ Lean.format p.format ++ Lean.format " " ++ Lean.format q.format ++ Lean.format ")"
• p.orImpL.format = Lean.format "(orImpL " ++ Lean.format p.format ++ Lean.format ")"
• p.orImpR.format = Lean.format "(orImpR " ++ Lean.format p.format ++ Lean.format ")"
• p.orInL.format = Lean.format "(Or.inl " ++ Lean.format p.format ++ Lean.format ")"
• p.orInR.format = Lean.format "(Or.inr " ++ Lean.format p.format ++ Lean.format ")"
• (Mathlib.Tactic.ITauto.Proof.em false p).format = Lean.format "(Decidable.em " ++ Lean.format p ++ Lean.format ")"
• (Mathlib.Tactic.ITauto.Proof.em true p).format = Lean.format "(Classical.em " ++ Lean.format p ++ Lean.format ")"
• (Mathlib.Tactic.ITauto.Proof.impImpSimp x_1 p).format = Lean.format "(impImpSimp " ++ Lean.format p.format ++ Lean.format ")"

instance Mathlib.Tactic.ITauto.instToFormatProof : Lean.ToFormat Mathlib.Tactic.ITauto.Proof

Equations

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

def Mathlib.Tactic.ITauto.Proof.exfalso : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.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'

def Mathlib.Tactic.ITauto.Proof.orElim : Mathlib.Tactic.ITauto.Proof → Lean.Name → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.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

def Mathlib.Tactic.ITauto.Proof.app : Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.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

@[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 ++ toString ""), n + 1)

def Mathlib.Tactic.ITauto.Context : Type

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

Equations

• Mathlib.Tactic.ITauto.Context = Lean.RBMap Mathlib.Tactic.ITauto.IProp Mathlib.Tactic.ITauto.Proof Mathlib.Tactic.ITauto.IProp.cmp

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

Debug printer for the context.

Equations

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

instance Mathlib.Tactic.ITauto.instToFormatContext : Lean.ToFormat Mathlib.Tactic.ITauto.Context

Equations

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

partial def Mathlib.Tactic.ITauto.Context.add : Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Context → Except (Mathlib.Tactic.ITauto.IProp → Mathlib.Tactic.ITauto.Proof) Mathlib.Tactic.ITauto.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).

@[inline]

def Mathlib.Tactic.ITauto.Context.withAdd (Γ : Mathlib.Tactic.ITauto.Context) (A : Mathlib.Tactic.ITauto.IProp) (p : Mathlib.Tactic.ITauto.Proof) (B : Mathlib.Tactic.ITauto.IProp) (f : Mathlib.Tactic.ITauto.Context → Mathlib.Tactic.ITauto.IProp → StateM ℕ (Bool × Mathlib.Tactic.ITauto.Proof)) : StateM ℕ (Bool × Mathlib.Tactic.ITauto.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)

def Mathlib.Tactic.ITauto.mapProof (f : Mathlib.Tactic.ITauto.Proof → Mathlib.Tactic.ITauto.Proof) : Bool × Mathlib.Tactic.ITauto.Proof → Bool × Mathlib.Tactic.ITauto.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)

def Mathlib.Tactic.ITauto.isOk : (Bool × Mathlib.Tactic.ITauto.Proof) × ℕ → Option (Mathlib.Tactic.ITauto.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)

def Mathlib.Tactic.ITauto.whenOk : Bool → Mathlib.Tactic.ITauto.IProp → StateM ℕ (Bool × Mathlib.Tactic.ITauto.Proof) → StateM ℕ (Bool × Mathlib.Tactic.ITauto.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

partial def Mathlib.Tactic.ITauto.search (Γ : Mathlib.Tactic.ITauto.Context) (B : Mathlib.Tactic.ITauto.IProp) : StateM ℕ (Bool × Mathlib.Tactic.ITauto.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.

partial def Mathlib.Tactic.ITauto.prove (Γ : Mathlib.Tactic.ITauto.Context) (B : Mathlib.Tactic.ITauto.IProp) : StateM ℕ (Bool × Mathlib.Tactic.ITauto.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.

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

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

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

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

def Mathlib.Tactic.ITauto.itautoCore (g : Lean.MVarId) (useDec : Bool) (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.

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.

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.