internlm/Lean-Github huggingface dataset:
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign rhs).getLsb idx
Tactic:
intros
Proof state after:
case bin.eq.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
            idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign rhs).getLsb idx✝
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.eq.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
            idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign rhs).getLsb idx✝
Tactic:
simp
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦bitblast aig (bin lhs BVBinPred.ult rhs), assign.toAIGAssignment⟧ = eval assign (bin lhs BVBinPred.ult rhs)
Tactic:
simp only [bitblast, eval_bin, BVBinPred.eval_ult]
Proof state after:
case bin.ult
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦mkUlt (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
        { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
          rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).ult (BVExpr.eval assign rhs)
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ⟦mkUlt (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig
        { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
          rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).ult (BVExpr.eval assign rhs)
Tactic:
rw [mkUlt_denote_eq_eval_ult]
Proof state after:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign lhs).getLsb idx

case bin.ult.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign rhs).getLsb idx
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign lhs).getLsb idx

case bin.ult.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign rhs).getLsb idx
Tactic:
. intros
  rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast)]
  . simp
    rw [BVExpr.bitblast_denote_eq_eval_getLsb]
  . simp [Ref.hgate]
Proof state after:
case bin.ult.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign rhs).getLsb idx
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign rhs).getLsb idx
Tactic:
. intros
  simp
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign lhs).getLsb idx
Tactic:
intros
Proof state after:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
            idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
            idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Tactic:
rw [AIG.LawfulStreamOperator.denote_mem_prefix (f := BVExpr.bitblast)]
Proof state after:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref :=
          {
            gate :=
              ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                        rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
                  idx✝ hidx✝).gate,
            hgate := ?bin.ult.hleft } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝

case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref :=
          {
            gate :=
              ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                        rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
                  idx✝ hidx✝).gate,
            hgate := ?bin.ult.hleft } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝

case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
. simp
  rw [BVExpr.bitblast_denote_eq_eval_getLsb]
Proof state after:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
. simp [Ref.hgate]
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref :=
          {
            gate :=
              ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                        rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
                  idx✝ hidx✝).gate,
            hgate := ?bin.ult.hleft } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Tactic:
simp
Proof state after:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref := { gate := ((BVExpr.bitblast aig lhs).stream.getRef idx✝ hidx✝).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast aig lhs).aig,
        ref := { gate := ((BVExpr.bitblast aig lhs).stream.getRef idx✝ hidx✝).gate, hgate := ⋯ } },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign lhs).getLsb idx✝
Tactic:
rw [BVExpr.bitblast_denote_eq_eval_getLsb]
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hleft
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ({ lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
              rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.lhs.getRef
        idx✝ hidx✝).gate <
    (BVExpr.bitblast aig lhs).aig.decls.size
Tactic:
simp [Ref.hgate]
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
⊢ ∀ (idx : Nat) (hidx : idx < w✝),
    ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
          ref :=
            { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                    rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
              idx hidx },
        assign.toAIGAssignment⟧ =
      (BVExpr.eval assign rhs).getLsb idx
Tactic:
intros
Proof state after:
case bin.ult.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
            idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign rhs).getLsb idx✝
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case bin.ult.hright
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
lhs rhs : BVExpr w✝
idx✝ : Nat
hidx✝ : idx✝ < w✝
⊢ ⟦{ aig := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).aig,
        ref :=
          { lhs := (BVExpr.bitblast aig lhs).stream.cast ⋯,
                  rhs := (BVExpr.bitblast (BVExpr.bitblast aig lhs).aig rhs).stream }.rhs.getRef
            idx✝ hidx✝ },
      assign.toAIGAssignment⟧ =
    (BVExpr.eval assign rhs).getLsb idx✝
Tactic:
simp
Proof state after:
no goals
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case getLsb
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ ⟦bitblast aig (getLsb expr idx), assign.toAIGAssignment⟧ = eval assign (getLsb expr idx)
Tactic:
simp [bitblast]
Proof state after:
case getLsb
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (BVExpr.eval assign expr).getLsb idx = true → idx < w✝
Theorem: BVPred.bitblast_denote_eq_eval
Proof state before:
case getLsb
aig : AIG BVBit
assign : BVExpr.Assignment
w✝ : Nat
expr : BVExpr w✝
idx : Nat
⊢ (BVExpr.eval assign expr).getLsb idx = true → idx < w✝
Tactic:
apply BitVec.lt_of_getLsb
Proof state after:
no goals
Theorem: bitvec_AndOrXor_2658
Proof state before:
⊢ ∀ (a b : BitVec 64), a &&& (b ^^^ -1) ^^^ (a ^^^ -1) = a &&& b ^^^ -1
Tactic:
intros
Proof state after:
a✝ b✝ : BitVec 64
⊢ a✝ &&& (b✝ ^^^ -1) ^^^ (a✝ ^^^ -1) = a✝ &&& b✝ ^^^ -1
Theorem: bitvec_AndOrXor_2658
Proof state before:
a✝ b✝ : BitVec 64
⊢ a✝ &&& (b✝ ^^^ -1) ^^^ (a✝ ^^^ -1) = a✝ &&& b✝ ^^^ -1
Tactic:
bv_decide
Proof state after:
no goals
Theorem: Array.get_of_mem
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
⊢ a ∈ as → ∃ i, as[i] = a
Tactic:
intro ha
Proof state after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
ha : a ∈ as
⊢ ∃ i, as[i] = a
Theorem: Array.get_of_mem
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
ha : a ∈ as
⊢ ∃ i, as[i] = a
Tactic:
rcases List.get_of_mem ha.val with ⟨i, hi⟩
Proof state after:
case intro
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
ha : a ∈ as
i : Fin as.data.length
hi : as.data.get i = a
⊢ ∃ i, as[i] = a
Theorem: Array.get_of_mem
Proof state before:
case intro
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
a : α
as : Array α
ha : a ∈ as
i : Fin as.data.length
hi : as.data.get i = a
⊢ ∃ i, as[i] = a
Tactic:
exists i
Proof state after:
no goals
Theorem: AIG.RelabelNat.State.Inv2.upper_lt_size
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
upper : Nat
map : HashMap α Nat
decls : Array (Decl α)
hinv : Inv2 decls upper map
⊢ upper ≤ decls.size
Tactic:
cases hinv <;> omega
Proof state after:
no goals
Theorem: AIG.RelabelNat.State.ofAIG.Inv1
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ ∃ n, State.Inv1 n (ofAIG aig)
Tactic:
exists (ofAIGAux aig).max
Proof state after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIG aig)
Theorem: AIG.RelabelNat.State.ofAIG.Inv1
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIG aig)
Tactic:
dsimp [ofAIG]
Proof state after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIGAux aig).map
Theorem: AIG.RelabelNat.State.ofAIG.Inv1
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv1 (ofAIGAux aig).max (ofAIGAux aig).map
Tactic:
exact (ofAIGAux aig).inv1
Proof state after:
no goals
Theorem: AIG.RelabelNat.State.ofAIG.Inv2
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ State.Inv2 aig.decls aig.decls.size (ofAIG aig)
Tactic:
have := (ofAIGAux aig).inv2
Proof state after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
this : State.Inv2 aig.decls aig.decls.size (ofAIGAux aig).map
⊢ State.Inv2 aig.decls aig.decls.size (ofAIG aig)
Theorem: AIG.RelabelNat.State.ofAIG.Inv2
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
this : State.Inv2 aig.decls aig.decls.size (ofAIGAux aig).map
⊢ State.Inv2 aig.decls aig.decls.size (ofAIG aig)
Tactic:
simp [ofAIG, this]
Proof state after:
no goals
Theorem: AIG.RelabelNat.State.ofAIG_find_unique
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
n : Nat
aig : AIG α
a : α
ha : (ofAIG aig).find? a = some n
⊢ ∀ (a' : α), (ofAIG aig).find? a' = some n → a = a'
Tactic:
intro a' ha'
Proof state after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
n : Nat
aig : AIG α
a : α
ha : (ofAIG aig).find? a = some n
a' : α
ha' : (ofAIG aig).find? a' = some n
⊢ a = a'
Theorem: AIG.RelabelNat.State.ofAIG_find_unique
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
n : Nat
aig : AIG α
a : α
ha : (ofAIG aig).find? a = some n
a' : α
ha' : (ofAIG aig).find? a' = some n
⊢ a = a'
Tactic:
rcases ofAIG.Inv1 aig with ⟨n, hn⟩
Proof state after:
case intro
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
n✝ : Nat
aig : AIG α
a : α
ha : (ofAIG aig).find? a = some n✝
a' : α
ha' : (ofAIG aig).find? a' = some n✝
n : Nat
hn : Inv1 n (ofAIG aig)
⊢ a = a'
Theorem: AIG.RelabelNat.State.ofAIG_find_unique
Proof state before:
case intro
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
n✝ : Nat
aig : AIG α
a : α
ha : (ofAIG aig).find? a = some n✝
a' : α
ha' : (ofAIG aig).find? a' = some n✝
n : Nat
hn : Inv1 n (ofAIG aig)
⊢ a = a'
Tactic:
apply Inv1.property <;> assumption
Proof state after:
no goals
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
⊢ ∀ (a : α), a ∈ aig → ∃ n, (ofAIG aig).find? a = some n
Tactic:
intro a ha
Proof state after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : a ∈ aig
⊢ ∃ n, (ofAIG aig).find? a = some n
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : a ∈ aig
⊢ ∃ n, (ofAIG aig).find? a = some n
Tactic:
simp only [mem_def] at ha
Proof state after:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
⊢ ∃ n, (ofAIG aig).find? a = some n
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
⊢ ∃ n, (ofAIG aig).find? a = some n
Tactic:
rcases Array.get_of_mem ha with ⟨⟨i, isLt⟩, hi⟩
Proof state after:
case intro.mk
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ∃ n, (ofAIG aig).find? a = some n
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
case intro.mk
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ∃ n, (ofAIG aig).find? a = some n
Tactic:
apply Inv2.property
Proof state after:
case intro.mk.a
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.decls[?intro.mk.idx] = Decl.atom a

case intro.mk.decls
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Array (Decl α)

case intro.mk.idx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

case intro.mk.upper
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 ?intro.mk.decls ?intro.mk.upper (ofAIG aig)

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.idx < ?intro.mk.upper
Theorem: AIG.RelabelNat.State.ofAIG_find_some
Proof state before:
case intro.mk.a
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.decls[?intro.mk.idx] = Decl.atom a

case intro.mk.decls
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Array (Decl α)

case intro.mk.idx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

case intro.mk.upper
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 ?intro.mk.decls ?intro.mk.upper (ofAIG aig)

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ?intro.mk.idx < ?intro.mk.upper
Tactic:
. assumption
Proof state after:
case intro.mk.upper
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Nat

case intro.mk.hinv
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ Inv2 aig.decls ?intro.mk.upper (ofAIG aig)

case intro.mk.hidx
α : Type
inst✝¹ : BEq α
inst✝ : Hashable α
aig : AIG α
a : α
ha : Decl.atom a ∈ aig.decls
i : Nat
isLt : i < aig.decls.size
hi : aig.decls[⟨i, isLt⟩] = Decl.atom a
⊢ ↑⟨i, isLt⟩ < ?intro.mk.upper