Documentation

Mathlib.Tactic.ITauto

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:

The intuitionistic logic rules are separated into three groups:

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

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

Instances For
    @[match_pattern]

    Constructor for ¬ p.

    Equations
    Instances For
      @[match_pattern]

      Constructor for xor p q.

      Equations
      • a.xor b = (a.and b.not).or (b.and a.not)
      Instances For

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

        Equations
        Instances For

          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

            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

              A reified inductive proof type for intuitionistic propositional logic.

              Instances For

                Debugging printer for proof objects.

                Equations
                Instances For

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

                  Equations
                  Instances For

                    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
                    Instances For
                      @[inline]

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

                      Equations
                      Instances For

                        Debug printer for the context.

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

                          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]

                          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
                          Instances For

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

                            Equations
                            Instances For

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

                              Equations
                              Instances For

                                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.

                                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.

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

                                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) :

                                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

                                  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

                                    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