Documentation

VCVio.ProgramLogic.Tactics.Relational.Internals

Relational VCGen Internals #

Implementation details for the relational VCGen planner and step selection.

source
def OracleComp.ProgramLogic.TacticInternals.Relational.tryCloseRelGoalImmediate :
Lean.Elab.Tactic.TacticM Bool
Instances For
    source
    def OracleComp.ProgramLogic.TacticInternals.Relational.tryCloseLeadingRelGoalImmediate :
    Lean.Elab.Tactic.TacticM Unit
    Instances For
      source
      def OracleComp.ProgramLogic.TacticInternals.Relational.reorderRelBindGoals :
      Lean.Elab.Tactic.TacticM Unit
      Instances For
        source
        def OracleComp.ProgramLogic.TacticInternals.Relational.tryLowerRelGoal :
        Lean.Elab.Tactic.TacticM Bool
        Instances For
          source
          def OracleComp.ProgramLogic.TacticInternals.Relational.runERelPureRule :
          Lean.Elab.Tactic.TacticM Bool
          Instances For
            source
            def OracleComp.ProgramLogic.TacticInternals.Relational.runERelBindRule :
            Lean.Elab.Tactic.TacticM Bool
            Instances For
              source
              def OracleComp.ProgramLogic.TacticInternals.Relational.runERelBindRuleUsing (cut : Lean.TSyntax `term) :
              Lean.Elab.Tactic.TacticM Bool
              Instances For
                source
                def OracleComp.ProgramLogic.TacticInternals.Relational.runRelBindRule :
                Lean.Elab.Tactic.TacticM Bool
                Instances For
                  source
                  def OracleComp.ProgramLogic.TacticInternals.Relational.runRelBindRuleUsing (R : Lean.TSyntax `term) :
                  Lean.Elab.Tactic.TacticM Bool
                  Instances For
                    source
                    def OracleComp.ProgramLogic.TacticInternals.Relational.runRelMapRule :
                    Lean.Elab.Tactic.TacticM Bool
                    Instances For
                      source
                      def OracleComp.ProgramLogic.TacticInternals.Relational.runRelReplicateRule :
                      Lean.Elab.Tactic.TacticM Bool
                      Instances For
                        source
                        def OracleComp.ProgramLogic.TacticInternals.Relational.runRelMapMRule :
                        Lean.Elab.Tactic.TacticM Bool
                        Instances For
                          source
                          def OracleComp.ProgramLogic.TacticInternals.Relational.runRelMapMRuleUsing (R : Lean.TSyntax `term) :
                          Lean.Elab.Tactic.TacticM Bool
                          Instances For
                            source
                            def OracleComp.ProgramLogic.TacticInternals.Relational.runRelFoldlMRule :
                            Lean.Elab.Tactic.TacticM Bool
                            Instances For
                              source
                              def OracleComp.ProgramLogic.TacticInternals.Relational.runRelFoldlMRuleUsing (R : Lean.TSyntax `term) :
                              Lean.Elab.Tactic.TacticM Bool
                              Instances For
                                source
                                def OracleComp.ProgramLogic.TacticInternals.Relational.runRelRndRuleUsing (f : Lean.TSyntax `term) :
                                Lean.Elab.Tactic.TacticM Bool
                                Instances For
                                  source
                                  def OracleComp.ProgramLogic.TacticInternals.Relational.runRelRndRuleWithContextBijection :
                                  Lean.Elab.Tactic.TacticM Bool
                                  Instances For
                                    source
                                    def OracleComp.ProgramLogic.TacticInternals.Relational.runRelRndRule :
                                    Lean.Elab.Tactic.TacticM Bool
                                    Instances For
                                      source
                                      def OracleComp.ProgramLogic.TacticInternals.Relational.runRelCondRule :
                                      Lean.Elab.Tactic.TacticM Bool
                                      Instances For
                                        source
                                        def OracleComp.ProgramLogic.TacticInternals.Relational.runByUptoRule (bad : Lean.TSyntax `term) :
                                        Lean.Elab.Tactic.TacticM Bool
                                        Instances For
                                          source
                                          def OracleComp.ProgramLogic.TacticInternals.Relational.runRelSimRule :
                                          Lean.Elab.Tactic.TacticM Bool
                                          Instances For
                                            source
                                            def OracleComp.ProgramLogic.TacticInternals.Relational.runRelSimRuleUsing (R : Lean.TSyntax `term) :
                                            Lean.Elab.Tactic.TacticM Bool
                                            Instances For
                                              source
                                              def OracleComp.ProgramLogic.TacticInternals.Relational.runRelSimDistRule :
                                              Lean.Elab.Tactic.TacticM Bool
                                              Instances For
                                                source
                                                def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenCore :
                                                Lean.Elab.Tactic.TacticM Bool
                                                Instances For
                                                  source
                                                  def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenCoreUsing (hint : Lean.TSyntax `term) :
                                                  Lean.Elab.Tactic.TacticM Bool
                                                  Instances For
                                                    source
                                                    def OracleComp.ProgramLogic.TacticInternals.Relational.findRelHintCandidates :
                                                    Lean.Elab.Tactic.TacticM (Array Lean.Name)

                                                    Find the local hypotheses that work as relational using hints.

                                                    Instances For
                                                      source
                                                      def OracleComp.ProgramLogic.TacticInternals.Relational.findUniqueRelHint? :
                                                      Lean.Elab.Tactic.TacticM (Option Lean.Name)

                                                      Find the unique local hypothesis that works as a relational using hint. Returns none if there are 0 or ≥ 2 viable hints (keeping ambiguity explicit).

                                                      Instances For
                                                        source
                                                        def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenStepUsingWithNames (hint : Lean.TSyntax `term) (names : Array Lean.Name) :
                                                        Lean.Elab.Tactic.TacticM Bool
                                                        Instances For
                                                          source
                                                          def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenStepWithTheorem (thm : Lean.TSyntax `term) (requireClosed : Bool := false) :
                                                          Lean.Elab.Tactic.TacticM Bool

                                                          Apply an explicit relational theorem/assumption step and try to close any easy side goals.

                                                          Instances For
                                                            source
                                                            def OracleComp.ProgramLogic.TacticInternals.Relational.findRegisteredRVCGenRuleCandidates :
                                                            Lean.Elab.Tactic.TacticM (Array CompiledRelationalVCSpecRule)

                                                            Find the registered compiled relational rules whose bounded application makes progress.

                                                            Instances For
                                                              source
                                                              def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenStructuralCore :
                                                              Lean.Elab.Tactic.TacticM Bool

                                                              Structural/default relational VCGen step, excluding explicit using-hint fallbacks.

                                                              Instances For
                                                                source
                                                                def OracleComp.ProgramLogic.TacticInternals.Relational.planRVCGenStep? :
                                                                Lean.Elab.Tactic.TacticM (Option PlannedStep)

                                                                Choose one relational VCGen step and remember how to replay it explicitly.

                                                                Instances For
                                                                  source
                                                                  def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenPlannedStep? :
                                                                  Lean.Elab.Tactic.TacticM (Option PlannedStep)

                                                                  Execute one planned relational VCGen step, returning the chosen step for replay/trace.

                                                                  Instances For
                                                                    source
                                                                    def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenStep :
                                                                    Lean.Elab.Tactic.TacticM Bool

                                                                    One step of relational VCGen.

                                                                    Instances For
                                                                      source
                                                                      def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenStepUsing (hint : Lean.TSyntax `term) :
                                                                      Lean.Elab.Tactic.TacticM Bool
                                                                      Instances For
                                                                        source
                                                                        def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenPassPlanned :
                                                                        Lean.Elab.Tactic.TacticM (Array PlannedStep)
                                                                        Instances For
                                                                          source
                                                                          def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenPass :
                                                                          Lean.Elab.Tactic.TacticM Bool
                                                                          Instances For
                                                                            source
                                                                            def OracleComp.ProgramLogic.TacticInternals.Relational.throwRVCGenStepError :
                                                                            Lean.Elab.Tactic.TacticM Unit
                                                                            Instances For
                                                                              source
                                                                              def OracleComp.ProgramLogic.TacticInternals.Relational.throwRVCGenStepUsingError (hint : Lean.TSyntax `term) :
                                                                              Lean.Elab.Tactic.TacticM Unit
                                                                              Instances For
                                                                                source
                                                                                def OracleComp.ProgramLogic.TacticInternals.Relational.tryCloseRelGoalConseq :
                                                                                Lean.Elab.Tactic.TacticM Bool

                                                                                Try to close a relational goal by applying postcondition monotonicity and closing both the inner triple and the implication from local hypotheses.

                                                                                Instances For
                                                                                  source
                                                                                  def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenCloseConseqPass :
                                                                                  Lean.Elab.Tactic.TacticM Bool
                                                                                  Instances For
                                                                                    source
                                                                                    def OracleComp.ProgramLogic.TacticInternals.Relational.runRVCGenFinish :
                                                                                    Lean.Elab.Tactic.TacticM Unit
                                                                                    Instances For