Documentation

Std.Tactic.Do.Syntax

Theorems tagged with the spec attribute are used by the mspec and mvcgen tactics.

  • When used on a theorem foo_spec : Triple (foo a b c) P Q, then mspec and mvcgen will use foo_spec as a specification for calls to foo.
  • Otherwise, when used on a definition that @[simp] would work on, it is added to the internal simp set of mvcgen that is used within wp⟦·⟧ contexts to simplify match discriminants and applications of constants.
Equations
  • One or more equations did not get rendered due to their size.
Instances For

    massumption is like assumption, but operating on a stateful Std.Do.SPred goal.

    example (P Q : SPred σs) : Q ⊢ₛ P → Q := by
      mintro _ _
      massumption
    
    Equations
    Instances For

      mclear is like clear, but operating on a stateful Std.Do.SPred goal.

      example (P Q : SPred σs) : P ⊢ₛ Q → Q := by
        mintro HP
        mintro HQ
        mclear HP
        mexact HQ
      
      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

        mconstructor is like constructor, but operating on a stateful Std.Do.SPred goal.

        example (Q : SPred σs) : Q ⊢ₛ Q ∧ Q := by
          mintro HQ
          mconstructor <;> mexact HQ
        
        Equations
        Instances For

          mexact is like exact, but operating on a stateful Std.Do.SPred goal.

          example (Q : SPred σs) : Q ⊢ₛ Q := by
            mstart
            mintro HQ
            mexact HQ
          
          Equations
          • One or more equations did not get rendered due to their size.
          Instances For

            mexfalso is like exfalso, but operating on a stateful Std.Do.SPred goal.

            example (P : SPred σs) : ⌜False⌝ ⊢ₛ P := by
              mintro HP
              mexfalso
              mexact HP
            
            Equations
            Instances For

              mexists is like exists, but operating on a stateful Std.Do.SPred goal.

              example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
                mintro H
                mexists 42
              
              Equations
              • One or more equations did not get rendered due to their size.
              Instances For

                mframe infers which hypotheses from the stateful context can be moved into the pure context. This is useful because pure hypotheses "survive" the next application of modus ponens (Std.Do.SPred.mp) and transitivity (Std.Do.SPred.entails.trans).

                It is used as part of the mspec tactic.

                example (P Q : SPred σs) : ⊢ₛ ⌜p⌝ ∧ Q ∧ ⌜q⌝ ∧ ⌜r⌝ ∧ P ∧ ⌜s⌝ ∧ ⌜t⌝ → Q := by
                  mintro _
                  mframe
                  /- `h : p ∧ q ∧ r ∧ s ∧ t` in the pure context -/
                  mcases h with hP
                  mexact h
                
                Equations
                Instances For

                  Duplicate a stateful Std.Do.SPred hypothesis.

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

                    mhave is like have, but operating on a stateful Std.Do.SPred goal.

                    example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
                      mintro HP HPQ
                      mhave HQ : Q := by mspecialize HPQ HP; mexact HPQ
                      mexact HQ
                    
                    Equations
                    • One or more equations did not get rendered due to their size.
                    Instances For

                      mreplace is like replace, but operating on a stateful Std.Do.SPred goal.

                      example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
                        mintro HP HPQ
                        mreplace HPQ : Q := by mspecialize HPQ HP; mexact HPQ
                        mexact HPQ
                      
                      Equations
                      • One or more equations did not get rendered due to their size.
                      Instances For

                        mright is like right, but operating on a stateful Std.Do.SPred goal.

                        example (P Q : SPred σs) : P ⊢ₛ Q ∨ P := by
                          mintro HP
                          mright
                          mexact HP
                        
                        Equations
                        Instances For

                          mleft is like left, but operating on a stateful Std.Do.SPred goal.

                          example (P Q : SPred σs) : P ⊢ₛ P ∨ Q := by
                            mintro HP
                            mleft
                            mexact HP
                          
                          Equations
                          Instances For

                            mpure moves a pure hypothesis from the stateful context into the pure context.

                            example (Q : SPred σs) (ψ : φ → ⊢ₛ Q): ⌜φ⌝ ⊢ₛ Q := by
                              mintrompuremexact (ψ Hφ)
                            
                            Equations
                            • One or more equations did not get rendered due to their size.
                            Instances For

                              mpure_intro operates on a stateful Std.Do.SPred goal of the form P ⊢ₛ ⌜φ⌝. It leaves the stateful proof mode (thereby discarding P), leaving the regular goal φ.

                              theorem simple : ⊢ₛ (⌜True⌝ : SPred σs) := by
                                mpure_intro
                                exact True.intro
                              
                              Equations
                              Instances For

                                mrevert is like revert, but operating on a stateful Std.Do.SPred goal.

                                example (P Q R : SPred σs) : P ∧ Q ∧ R ⊢ₛ P → R := by
                                  mintro ⟨HP, HQ, HR⟩
                                  mrevert HR
                                  mrevert HP
                                  mintro HP'
                                  mintro HR'
                                  mexact HR'
                                
                                Equations
                                • One or more equations did not get rendered due to their size.
                                Instances For

                                  mspecialize is like specialize, but operating on a stateful Std.Do.SPred goal. It specializes a hypothesis from the stateful context with hypotheses from either the pure or stateful context or pure terms.

                                  example (P Q : SPred σs) : P ⊢ₛ (P → Q) → Q := by
                                    mintro HP HPQ
                                    mspecialize HPQ HP
                                    mexact HPQ
                                  
                                  example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) : ⊢ₛ Q → (∀ x, P → Q → Ψ x) → Ψ (y + 1) := by
                                    mintro HQ HΨ
                                    mspecialize HΨ (y + 1) hP HQ
                                    mexact
                                  Equations
                                  • One or more equations did not get rendered due to their size.
                                  Instances For

                                    mspecialize_pure is like mspecialize, but it specializes a hypothesis from the pure context with hypotheses from either the pure or stateful context or pure terms.

                                    example (y : Nat) (P Q : SPred σs) (Ψ : Nat → SPred σs) (hP : ⊢ₛ P) (hΨ : ∀ x, ⊢ₛ P → Q → Ψ x) : ⊢ₛ Q → Ψ (y + 1) := by
                                      mintro HQ
                                      mspecialize_pure (hΨ (y + 1)) hP HQ => HΨ
                                      mexact
                                    Equations
                                    • One or more equations did not get rendered due to their size.
                                    Instances For

                                      Start the stateful proof mode of Std.Do.SPred. This will transform a stateful goal of the form H ⊢ₛ T into ⊢ₛ H → T upon which mintro can be used to re-introduce H and give it a name. It is often more convenient to use mintro directly, which will try mstart automatically if necessary.

                                      Equations
                                      Instances For

                                        Stops the stateful proof mode of Std.Do.SPred. This will simply forget all the names given to stateful hypotheses and pretty-print a bit differently.

                                        Equations
                                        Instances For
                                          Equations
                                          • One or more equations did not get rendered due to their size.
                                          Instances For
                                            Equations
                                            • One or more equations did not get rendered due to their size.
                                            Instances For
                                              Equations
                                              • One or more equations did not get rendered due to their size.
                                              Instances For
                                                Equations
                                                • One or more equations did not get rendered due to their size.
                                                Instances For
                                                  Equations
                                                  • One or more equations did not get rendered due to their size.
                                                  Instances For
                                                    Instances For
                                                      Equations
                                                      • One or more equations did not get rendered due to their size.
                                                      Instances For
                                                        partial def Lean.Parser.Tactic.MCasesPat.parse.goAlts :
                                                        TSyntax `Lean.Parser.Tactic.mcasesPatAltsOption MCasesPat

                                                        Like rcases, but operating on stateful Std.Do.SPred goals. Example: Given a goal h : (P ∧ (Q ∨ R) ∧ (Q → R)) ⊢ₛ R, mcases h with ⟨-, ⟨hq | hr⟩, hqr⟩ will yield two goals: (hq : Q, hqr : Q → R) ⊢ₛ R and (hr : R) ⊢ₛ R.

                                                        That is, mcases h with pat has the following semantics, based on pat:

                                                        • pat=□h' renames h to h' in the stateful context, regardless of whether h is pure
                                                        • pat=⌜h'⌝ introduces h' : φ to the pure local context if h : ⌜φ⌝ (c.f. Lean.Elab.Tactic.Do.ProofMode.IsPure)
                                                        • pat=h' is like pat=⌜h'⌝ if h is pure (c.f. Lean.Elab.Tactic.Do.ProofMode.IsPure), otherwise it is like pat=□h'.
                                                        • pat=_ renames h to an inaccessible name
                                                        • pat=- discards h
                                                        • ⟨pat₁, pat₂⟩ matches on conjunctions and existential quantifiers and recurses via pat₁ and pat₂.
                                                        • ⟨pat₁ | pat₂⟩ matches on disjunctions, matching the left alternative via pat₁ and the right alternative via pat₂.
                                                        Equations
                                                        • One or more equations did not get rendered due to their size.
                                                        Instances For
                                                          Equations
                                                          • One or more equations did not get rendered due to their size.
                                                          Instances For
                                                            Equations
                                                            • One or more equations did not get rendered due to their size.
                                                            Instances For
                                                              Equations
                                                              • One or more equations did not get rendered due to their size.
                                                              Instances For
                                                                Equations
                                                                • One or more equations did not get rendered due to their size.
                                                                Instances For
                                                                  Equations
                                                                  • One or more equations did not get rendered due to their size.
                                                                  Instances For
                                                                    Instances For
                                                                      Equations
                                                                      • One or more equations did not get rendered due to their size.
                                                                      Instances For

                                                                        Like refine, but operating on stateful Std.Do.SPred goals.

                                                                        example (P Q R : SPred σs) : (P ∧ Q ∧ R) ⊢ₛ P ∧ R := by
                                                                          mintro ⟨HP, HQ, HR⟩
                                                                          mrefine ⟨HP, HR⟩
                                                                        
                                                                        example (ψ : Nat → SPred σs) : ψ 42 ⊢ₛ ∃ x, ψ x := by
                                                                          mintro H
                                                                          mrefine ⟨⌜42⌝, H⟩
                                                                        
                                                                        Equations
                                                                        • One or more equations did not get rendered due to their size.
                                                                        Instances For
                                                                          Equations
                                                                          • One or more equations did not get rendered due to their size.
                                                                          Instances For
                                                                            Equations
                                                                            Instances For

                                                                              Like intro, but introducing stateful hypotheses into the stateful context of the Std.Do.SPred proof mode. That is, given a stateful goal (hᵢ : Hᵢ)* ⊢ₛ P → T, mintro h transforms into (hᵢ : Hᵢ)*, (h : P) ⊢ₛ T.

                                                                              Furthermore, mintro ∀s is like intro s, but preserves the stateful goal. That is, mintro ∀s brings the topmost state variable s:σ in scope and transforms (hᵢ : Hᵢ)* ⊢ₛ T (where the entailment is in Std.Do.SPred (σ::σs)) into (hᵢ : Hᵢ s)* ⊢ₛ T s (where the entailment is in Std.Do.SPred σs).

                                                                              Beyond that, mintro supports the full syntax of mcases patterns (mintro pat = (mintro h; mcases h with pat), and can perform multiple introductions in sequence.

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

                                                                                mspec_no_simp $spec first tries to decompose Bind.binds before applying $spec. This variant of mspec_no_simp does not; mspec_no_bind $spec is defined as

                                                                                try with_reducible mspec_no_bind Std.Do.Spec.bind
                                                                                mspec_no_bind $spec
                                                                                
                                                                                Equations
                                                                                • One or more equations did not get rendered due to their size.
                                                                                Instances For

                                                                                  Like mspec, but does not attempt slight simplification and closing of trivial sub-goals. mspec $spec is roughly (the set of simp lemmas below might not be up to date)

                                                                                  mspec_no_simp $spec
                                                                                  all_goals
                                                                                    ((try simp only [SPred.true_intro_simp, SPred.true_intro_simp_nil, SVal.curry_cons,
                                                                                                     SVal.uncurry_cons, SVal.getThe_here, SVal.getThe_there]);
                                                                                     (try mpure_intro; trivial))
                                                                                  
                                                                                  Equations
                                                                                  • One or more equations did not get rendered due to their size.
                                                                                  Instances For

                                                                                    mspec is an apply-like tactic that applies a Hoare triple specification to the target of the stateful goal.

                                                                                    Given a stateful goal H ⊢ₛ wp⟦prog⟧.apply Q', mspec foo_spec will instantiate foo_spec : ... → ⦃P⦄ foo ⦃Q⦄, match foo against prog and produce subgoals for the verification conditions ?pre : H ⊢ₛ P and ?post : Q ⊢ₚ Q'.

                                                                                    • If prog = x >>= f, then mspec Specs.bind is tried first so that foo is matched against x instead. Tactic mspec_no_bind does not attempt to do this decomposition.
                                                                                    • If ?pre or ?post follow by .rfl, then they are discharged automatically.
                                                                                    • ?post is automatically simplified into constituent ⊢ₛ entailments on success and failure continuations.
                                                                                    • ?pre and ?post.* goals introduce their stateful hypothesis as h.
                                                                                    • Any uninstantiated MVar arising from instantiation of foo_spec becomes a new subgoal.
                                                                                    • If the goal looks like fun s => _ ⊢ₛ _ then mspec will first mintro ∀s.
                                                                                    • If P has schematic variables that can be instantiated by doing mintro ∀s, for example foo_spec : ∀(n:Nat), ⦃⌜n = ‹Nat›ₛ⌝⦄ foo ⦃Q⦄, then mspec will do mintro ∀s first to instantiate n = s.
                                                                                    • Right before applying the spec, the mframe tactic is used, which has the following effect: Any hypothesis Hᵢ in the goal h₁:H₁, h₂:H₂, ..., hₙ:Hₙ ⊢ₛ T that is pure (i.e., equivalent to some ⌜φᵢ⌝) will be moved into the pure context as hᵢ:φᵢ.

                                                                                    Additionally, mspec can be used without arguments or with a term argument:

                                                                                    • mspec without argument will try and look up a spec for x registered with @[spec].
                                                                                    • mspec (foo_spec blah ?bleh) will elaborate its argument as a term with expected type ⦃?P⦄ x ⦃?Q⦄ and introduce ?bleh as a subgoal. This is useful to pass an invariant to e.g., Specs.forIn_list and leave the inductive step as a hole.
                                                                                    Equations
                                                                                    • One or more equations did not get rendered due to their size.
                                                                                    Instances For

                                                                                      mvcgen will break down a Hoare triple proof goal like ⦃P⦄ prog ⦃Q⦄ into verification conditions, provided that all functions used in prog have specifications registered with @[spec].

                                                                                      A verification condition is an entailment in the stateful logic of Std.Do.SPred in which the original program prog no longer occurs. Verification conditions are introduced by the mspec tactic; see the mspec tactic for what they look like. When there's no applicable mspec spec, mvcgen will try and rewrite an application prog = f a b c with the simp set registered via @[spec].

                                                                                      When used like mvcgen +noLetElim [foo_spec, bar_def, instBEqFloat], mvcgen will additionally

                                                                                      • add a Hoare triple specification foo_spec : ... → ⦃P⦄ foo ... ⦃Q⦄ to spec set for a function foo occurring in prog,
                                                                                      • unfold a definition def bar_def ... := ... in prog,
                                                                                      • unfold any method of the instBEqFloat : BEq Float instance in prog.
                                                                                      • it will no longer substitute away let-expressions that occur at most once in P, Q or prog.

                                                                                      Furthermore, mvcgen tries to close trivial verification conditions by SPred.entails.rfl or the tactic sequence try (mpure_intro; trivial). The variant mvcgen_no_trivial does not do this.

                                                                                      For debugging purposes there is also mvcgen_step 42 which will do at most 42 VC generation steps. This is useful for bisecting issues with the generated VCs.

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

                                                                                        Like mvcgen, but does not attempt to prove trivial VCs via mpure_intro; trivial.

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

                                                                                          Like mvcgen_no_trivial, but mvcgen_step 42 will only do 42 steps of the VC generation procedure. This is helpful for bisecting bugs in mvcgen and tracing its execution.

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