Documentation

Lean.Meta.Tactic.Grind.Arith.Offset.Proof

Helper functions for constructing proof terms in the offset constraint procedure.

Returns a proof for true = true

Equations
    Instances For

      Assume pi₁ is { w := u, k := k₁, proof := p₁ } and pi₂ is { w := w, k := k₂, proof := p₂ } p₁ is the proof for edge u -(k₁) → w and p₂ the proof for edge w -(k₂)-> v. Then, this function returns a proof for edge u -(k₁+k₂) -> v.

      Equations
        Instances For
          Equations
            Instances For
              def Lean.Meta.Grind.Arith.Offset.mkUnsatProof (u v : Expr) (kuv : Int) (huv : Expr) (kvu : Int) (hvu : Expr) :

              Returns a proof of False using a negative cycle composed of

              • u --(kuv)--> v with proof huv
              • v --(kvu)--> u with proof hvu
              Equations
                Instances For

                  Given a path u --(kuv)--> v justified by proof huv, construct a proof of e = True where e is a term corresponding to the edgen u --(k') --> v s.t. k ≤ k'

                  Equations
                    Instances For

                      Given a path u --(kuv)--> v justified by proof huv, construct a proof of e = False where e is a term corresponding to the edgen v --(k') --> u s.t. k+k' < 0

                      Equations
                        Instances For