Documentation

Std.Sat.AIG.RefVecOperator.Map

class Std.Sat.AIG.RefVec.LawfulMapOperator (α : Type) [Hashable α] [DecidableEq α] (f : (aig : Std.Sat.AIG α) → aig.RefStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] :
  • chainable : ∀ (aig : Std.Sat.AIG α) (input1 input2 : aig.Ref) (h : aig.decls.size (f aig input1).aig.decls.size) (assign : αBool), assign, f (f aig input1).aig (input2.cast h) = assign, f aig input2
Instances
    theorem Std.Sat.AIG.RefVec.LawfulMapOperator.chainable {α : Type} :
    ∀ {inst : Hashable α} {inst_1 : DecidableEq α} {f : (aig : Std.Sat.AIG α) → aig.RefStd.Sat.AIG.Entrypoint α} {inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f} [self : Std.Sat.AIG.RefVec.LawfulMapOperator α f] (aig : Std.Sat.AIG α) (input1 input2 : aig.Ref) (h : aig.decls.size (f aig input1).aig.decls.size) (assign : αBool), assign, f (f aig input1).aig (input2.cast h) = assign, f aig input2
    theorem Std.Sat.AIG.RefVec.LawfulMapOperator.denote_prefix_cast_ref {α : Type} [Hashable α] [DecidableEq α] {assign : αBool} {aig : Std.Sat.AIG α} {input1 : aig.Ref} {input2 : aig.Ref} {f : (aig : Std.Sat.AIG α) → aig.RefStd.Sat.AIG.Entrypoint α} [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [Std.Sat.AIG.RefVec.LawfulMapOperator α f] {h : aig.decls.size (f aig input1).aig.decls.size} :
    assign, f (f aig input1).aig (input2.cast h) = assign, f aig input2
    structure Std.Sat.AIG.RefVec.MapTarget {α : Type} [Hashable α] [DecidableEq α] (aig : Std.Sat.AIG α) (len : Nat) :
    Instances For
      theorem Std.Sat.AIG.RefVec.MapTarget.lawful {α : Type} [Hashable α] [DecidableEq α] {aig : Std.Sat.AIG α} {len : Nat} (self : Std.Sat.AIG.RefVec.MapTarget aig len) :
      Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref self.func
      @[specialize #[]]
      def Std.Sat.AIG.RefVec.map {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : Std.Sat.AIG α) (target : Std.Sat.AIG.RefVec.MapTarget aig len) :
      Equations
      Instances For
        @[irreducible, specialize #[]]
        def Std.Sat.AIG.RefVec.map.go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} (aig : Std.Sat.AIG α) (idx : Nat) (hidx : idx len) (s : aig.RefVec idx) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.RefStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [Std.Sat.AIG.RefVec.LawfulMapOperator α f] :
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For
          @[irreducible]
          theorem Std.Sat.AIG.RefVec.map.go_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (idx : Nat) (hidx : idx len) (s : aig.RefVec idx) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.RefStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [Std.Sat.AIG.RefVec.LawfulMapOperator α f] :
          aig.decls.size (Std.Sat.AIG.RefVec.map.go aig idx hidx s input f).aig.decls.size
          theorem Std.Sat.AIG.RefVec.map_le_size {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.MapTarget aig len) :
          aig.decls.size (Std.Sat.AIG.RefVec.map aig target).aig.decls.size
          @[irreducible]
          theorem Std.Sat.AIG.RefVec.map.go_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (i : Nat) (hi : i len) (s : aig.RefVec i) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.RefStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [Std.Sat.AIG.RefVec.LawfulMapOperator α f] (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Sat.AIG.RefVec.map.go aig i hi s input f).aig.decls.size) :
          (Std.Sat.AIG.RefVec.map.go aig i hi s input f).aig.decls[idx] = aig.decls[idx]
          theorem Std.Sat.AIG.RefVec.map_decl_eq {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.MapTarget aig len) (idx : Nat) (h1 : idx < aig.decls.size) (h2 : idx < (Std.Sat.AIG.RefVec.map aig target).aig.decls.size) :
          (Std.Sat.AIG.RefVec.map aig target).aig.decls[idx] = aig.decls[idx]
          instance Std.Sat.AIG.RefVec.instLawfulVecOperatorMapTargetMap {α : Type} [Hashable α] [DecidableEq α] :
          Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.RefVec.MapTarget fun {len : Nat} => Std.Sat.AIG.RefVec.map
          Equations
          • =
          @[irreducible]
          theorem Std.Sat.AIG.RefVec.map.go_get_aux {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr len) (s : aig.RefVec curr) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.RefStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [Std.Sat.AIG.RefVec.LawfulMapOperator α f] (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).aig.decls.size) :
          (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).vec.get idx = (s.get idx hidx).cast hfoo
          theorem Std.Sat.AIG.RefVec.map.go_get {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr len) (s : aig.RefVec curr) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.RefStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [Std.Sat.AIG.RefVec.LawfulMapOperator α f] (idx : Nat) (hidx : idx < curr) :
          (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).vec.get idx = (s.get idx hidx).cast
          theorem Std.Sat.AIG.RefVec.map.go_denote_mem_prefix {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : αBool} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr len) (s : aig.RefVec curr) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.RefStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [Std.Sat.AIG.RefVec.LawfulMapOperator α f] (start : Nat) (hstart : start < aig.decls.size) :
          assign, { aig := (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).aig, ref := { gate := start, hgate := } } = assign, { aig := aig, ref := { gate := start, hgate := hstart } }
          @[irreducible]
          theorem Std.Sat.AIG.RefVec.map.denote_go {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : αBool} {aig : Std.Sat.AIG α} (curr : Nat) (hcurr : curr len) (s : aig.RefVec curr) (input : aig.RefVec len) (f : (aig : Std.Sat.AIG α) → aig.RefStd.Sat.AIG.Entrypoint α) [Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref f] [Std.Sat.AIG.RefVec.LawfulMapOperator α f] (idx : Nat) (hidx1 : idx < len) :
          curr idxassign, { aig := (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).aig, ref := (Std.Sat.AIG.RefVec.map.go aig curr hcurr s input f).vec.get idx hidx1 } = assign, f aig (input.get idx hidx1)
          @[simp]
          theorem Std.Sat.AIG.RefVec.denote_map {α : Type} [Hashable α] [DecidableEq α] {len : Nat} {assign : αBool} {aig : Std.Sat.AIG α} (target : Std.Sat.AIG.RefVec.MapTarget aig len) (idx : Nat) (hidx : idx < len) :
          assign, { aig := (Std.Sat.AIG.RefVec.map aig target).aig, ref := (Std.Sat.AIG.RefVec.map aig target).vec.get idx hidx } = assign, target.func aig (target.vec.get idx hidx)