Theorem: BVExpr.bitblast.go_denote_eq_eval_getLsb
Proof state before:
w : Nat
aig : AIG BVBit
expr : BVExpr w
assign : Assignment
idx : Nat
hidx : idx < w
⊢ ⟦{ aig := (go aig expr).val.aig, ref := (go aig expr).val.stream.getRef idx hidx }, assign.toAIGAssignment⟧ =
    (eval assign expr).getLsb idx
Tactic:
induction expr generalizing aig idx with
| const =>
  simp [go, blastConst_eq_eval_getLsb]
| var =>
  simp [go, hidx, blastVar_eq_eval_getLsb]
| zeroExtend v inner ih =>
  simp only [go, blastZeroExtend_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right,
    eval_zeroExtend, BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and,
    Bool.and_iff_right_iff_imp, decide_eq_true_eq]
  apply BitVec.lt_of_getLsb
| append lhs rhs lih rih =>
  rename_i lw rw
  simp only [go, blastAppend_eq_eval_getLsb, RefStream.getRef_cast, Ref_cast', eval_append,
    BitVec.getLsb_append]
  split
  . next hsplit =>
    simp only [hsplit, decide_True, cond_true]
    rw [rih]
  . next hsplit =>
    simp only [hsplit, decide_False, cond_false]
    rw [go_denote_mem_prefix, lih]
| signExtend v inner ih =>
  rename_i originalWidth
  generalize hgo : (go aig (signExtend v inner)).val = res
  unfold go at hgo
  dsimp at hgo
  have : 0 ≤ originalWidth := by omega
  cases Nat.eq_or_lt_of_le this with
  | inl heq =>
    rw [blastSignExtend_empty_eq_zeroExtend] at hgo
    . rw [← hgo]
      simp only [eval_signExtend]
      rw [BitVec.signExtend_eq_not_zeroExtend_not_of_msb_false]
      . simp only [blastZeroExtend_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right,
          BitVec.getLsb_zeroExtend, hidx, decide_True, Bool.true_and, Bool.and_iff_right_iff_imp,
          decide_eq_true_eq]
        apply BitVec.lt_of_getLsb
      . subst heq
        rw [BitVec.msb_zero_length]
    . simp [heq]
  | inr hlt =>
    rw [← hgo]
    rw [blastSignExtend_eq_eval_getLsb]
    simp only [eval_signExtend]
    rw [BitVec.getLsb_signExtend]
    . simp only [hidx, decide_True, Bool.true_and]
      split
      . rw [ih]
      . rw [BitVec.msb_eq_getLsb_last]
        rw [ih]
        simp [hlt]
| extract hi lo inner ih =>
  simp only [go, blastExtract_eq_eval_getLsb, Bool.if_false_right, eval_extract,
    BitVec.getLsb_extract]
  have : idx ≤ hi - lo := by omega
  simp only [this, decide_True, Bool.true_and]
  split
  . next hsplit =>
    rw [ih]
  . apply Eq.symm
    apply BitVec.getLsb_ge
    omega
| bin lhs op rhs lih rih =>
  cases op with
  | and =>
    simp only [go, RefStream.denote_zip, denote_mkAndCached, rih, eval_bin, BVBinOp.eval_and,
      BitVec.getLsb_and]
    simp only [go_val_eq_bitblast, RefStream.getRef_cast]
    rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
    rw [← go_val_eq_bitblast]
    rw [lih]
  | or =>
    simp only [go, RefStream.denote_zip, denote_mkOrCached, rih, eval_bin, BVBinOp.eval_or,
      BitVec.getLsb_or]
    simp only [go_val_eq_bitblast, RefStream.getRef_cast]
    rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
    rw [← go_val_eq_bitblast]
    rw [lih]
  | xor =>
    simp only [go, RefStream.denote_zip, denote_mkXorCached, rih, eval_bin, BVBinOp.eval_xor,
      BitVec.getLsb_xor]
    simp only [go_val_eq_bitblast, RefStream.getRef_cast]
    rw [AIG.LawfulStreamOperator.denote_input_stream (f := bitblast)]
    rw [← go_val_eq_bitblast]
    rw [lih]
  | add =>
    simp only [go, eval_bin, BVBinOp.eval_add]
    apply blastAdd_eq_eval_getLsb
    . intros
      dsimp
      rw [go_denote_mem_prefix]
      rw [← lih (aig := aig)]
      . simp
      . assumption
      . simp [Ref.hgate]
    . intros
      rw [← rih]
| un op expr ih =>
  cases op with
  | not => simp [go, ih, hidx]
  | shiftLeftConst => simp [go, ih, hidx]
  | shiftRightConst =>
    simp only [go, blastShiftRight_eq_eval_getLsb, ih, dite_eq_ite, Bool.if_false_right, eval_un,
      BVUnOp.eval_shiftRightConst, BitVec.getLsb_ushiftRight, Bool.and_iff_right_iff_imp,
      decide_eq_true_eq]
    intro h
    apply BitVec.lt_of_getLsb
    assumption
  | rotateLeft => simp [go, ih, hidx]
  | rotateRight => simp [go, ih, hidx]
  | arithShiftRightConst n =>
    rename_i w
    have : ¬(w ≤ idx) := by omega
    simp [go, ih, this, BitVec.getLsb_sshiftRight, BitVec.msb_eq_getLsb_last ]
Proof state after:
no goals