Documentation

Mathlib.Tactic.Choose

choose tactic #

Performs Skolemization, that is, given h : ∀ a:α, ∃ b:β, p a b |- G produces f : α → β, hf: ∀ a, p a (f a) |- G.

TODO: switch to rcases syntax: choose ⟨i, j, h₁ -⟩ := expr.

Given α : Sort u, nonemp : Nonempty α, p : α → Prop, a context of free variables ctx, and a pair of an element val : α and spec : p val, mk_sometimes u α nonemp p ctx (val, spec) produces another pair val', spec' such that val' does not have any free variables from elements of ctx whose types are propositions. This is done by applying Function.sometimes to abstract over all the propositional arguments.

Equations
Instances For

    Results of searching for nonempty instances, to eliminate dependencies on propositions (choose!). success means we found at least one instance; failure ts means we didn't find instances for any t ∈ ts. (failure [] means we didn't look for instances at all.)

    Rationale: choose! means we are expected to succeed at least once in eliminating dependencies on propositions.

    Instances For

      mkFreshNameFrom orig base returns mkFreshUserName base if orig = `_ and orig otherwise.

      Equations
      Instances For

        Changes (h : ∀xs, ∃a:α, p a) ⊢ g to (d : ∀xs, a) ⊢ (s : ∀xs, p (d xs)) → g and (h : ∀xs, p xs ∧ q xs) ⊢ g to (d : ∀xs, p xs) ⊢ (s : ∀xs, q xs) → g. choose1 returns a tuple of

        • the error result (see ElimStatus)
        • the data new free variable that was "chosen"
        • the new goal (which contains the spec of the data as domain of an arrow type)

        If nondep is true and α is inhabited, then it will remove the dependency of d on all propositional assumptions in xs. For example if ys are propositions then (h : ∀xs ys, ∃a:α, p a) ⊢ g becomes (d : ∀xs, a) (s : ∀xs ys, p (d xs)) ⊢ g.

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

          A wrapper around choose1 that parses identifiers and adds variable info to new variables.

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

            A loop around choose1. The main entry point for the choose tactic.

            Equations
            Instances For
              • choose a b h h' using hyp takes a hypothesis hyp of the form ∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b for some P Q : X → Y → A → B → Prop and outputs into context a function a : X → Y → A, b : X → Y → B and two assumptions: h : ∀ (x : X) (y : Y), P x y (a x y) (b x y) and h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y). It also works with dependent versions.

              • choose! a b h h' using hyp does the same, except that it will remove dependency of the functions on propositional arguments if possible. For example if Y is a proposition and A and B are nonempty in the above example then we will instead get a : X → A, b : X → B, and the assumptions h : ∀ (x : X) (y : Y), P x y (a x) (b x) and h' : ∀ (x : X) (y : Y), Q x y (a x) (b x).

              The using hyp part can be omitted, which will effectively cause choose to start with an intro hyp.

              Examples:

              example (h : ∀ n m : ℕ, ∃ i j, m = n + i ∨ m + j = n) : True := by
                choose i j h using h
                guard_hyp i : ℕ → ℕ → ℕ
                guard_hyp j : ℕ → ℕ → ℕ
                guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n
                trivial
              
              example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : True := by
                choose! f h h' using h
                guard_hyp f : ℕ → ℕ
                guard_hyp h : ∀ (i : ℕ), i < 7 → i < f i
                guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + i
                trivial
              
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For
                • choose a b h h' using hyp takes a hypothesis hyp of the form ∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b for some P Q : X → Y → A → B → Prop and outputs into context a function a : X → Y → A, b : X → Y → B and two assumptions: h : ∀ (x : X) (y : Y), P x y (a x y) (b x y) and h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y). It also works with dependent versions.

                • choose! a b h h' using hyp does the same, except that it will remove dependency of the functions on propositional arguments if possible. For example if Y is a proposition and A and B are nonempty in the above example then we will instead get a : X → A, b : X → B, and the assumptions h : ∀ (x : X) (y : Y), P x y (a x) (b x) and h' : ∀ (x : X) (y : Y), Q x y (a x) (b x).

                The using hyp part can be omitted, which will effectively cause choose to start with an intro hyp.

                Examples:

                example (h : ∀ n m : ℕ, ∃ i j, m = n + i ∨ m + j = n) : True := by
                  choose i j h using h
                  guard_hyp i : ℕ → ℕ → ℕ
                  guard_hyp j : ℕ → ℕ → ℕ
                  guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n
                  trivial
                
                example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : True := by
                  choose! f h h' using h
                  guard_hyp f : ℕ → ℕ
                  guard_hyp h : ∀ (i : ℕ), i < 7 → i < f i
                  guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + i
                  trivial
                
                Equations
                • One or more equations did not get rendered due to their size.
                Instances For