internlm/Lean-Github huggingface dataset:
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
ratAddSuccess : f.performRatAdd c p rupHints ratHints = (f', true)
⊢ f' = f.insert c
Tactic:
rw [performRatAdd] at ratAddSuccess
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
ratAddSuccess :
  (if f.ratHintsExhaustive p ratHints = true then
      let negC := c.negate;
      match f.insertRupUnits negC with
      | (f, contradictionFound) =>
        if contradictionFound = true then (f, false)
        else
          match f.performRupCheck rupHints with
          | (f, derivedLits, derivedEmpty, encounteredError) =>
            if encounteredError = true then (f, false)
            else
              if derivedEmpty = true then (f, false)
              else
                let fold_fn := fun x ratHint =>
                  match x with
                  | (f, allChecksPassed) =>
                    if allChecksPassed = true then f.performRatCheck p.negateLiteral ratHint else (f, false);
                match Array.foldl fold_fn (f, true) ratHints 0 with
                | (f, allChecksPassed) =>
                  if (!allChecksPassed) = true then (f, false)
                  else
                    match f with
                    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
                      let assignments := restoreAssignments assignments derivedLits;
                      let f :=
                        { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits,
                            assignments := assignments }.clearRupUnits;
                      (f.insert c, true)
    else (f, false)) =
    (f', true)
⊢ f' = f.insert c
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝ : ¬f.ratHintsExhaustive p ratHints = true
ratAddSuccess : (f, false) = (f', true)
⊢ f' = f.insert c
Tactic:
. simp at ratAddSuccess
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
case isTrue.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝¹ : f.ratHintsExhaustive p ratHints = true
h✝ : (f.insertRupUnits c.negate).snd = true
ratAddSuccess : ((f.insertRupUnits c.negate).fst, false) = (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
case isTrue.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝² : f.ratHintsExhaustive p ratHints = true
h✝¹ : ¬(f.insertRupUnits c.negate).snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
case isTrue.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess : (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, false) = (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
case isTrue.isFalse.isFalse.isFalse.isTrue
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝⁴ : f.ratHintsExhaustive p ratHints = true
h✝³ : ¬(f.insertRupUnits c.negate).snd = true
h✝² : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
h✝ :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    false
ratAddSuccess :
  ((Array.foldl
          (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
          (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).fst,
      false) =
    (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
ratAddSuccess :
  ({
              clauses :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.clauses,
              rupUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.rupUnits,
              ratUnits :=
                (Array.foldl
                      (fun x ratHint =>
                        if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                      (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.ratUnits,
              assignments :=
                restoreAssignments
                  (Array.foldl
                        (fun x ratHint =>
                          if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
                        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).1.assignments
                  ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.fst }.clearRupUnits.insert
        c,
      true) =
    (f', true)
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
⊢ f.assignments.size = n
Tactic:
exact f_readyForRatAdd.2.2.1
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
⊢ performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n
Tactic:
have hsize : performRupCheck_res.assignments.size = n := by
  rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
Proof state after:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
hsize : performRupCheck_res.assignments.size = n
⊢ performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
hsize : performRupCheck_res.assignments.size = n
⊢ performRupCheck_res.ratUnits = #[] ∧ performRupCheck_res.assignments.size = n
Tactic:
exact And.intro f_readyForRatAdd.1 hsize
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝³ : f.ratHintsExhaustive p ratHints = true
h✝² : ¬(f.insertRupUnits c.negate).snd = true
h✝¹ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.snd = true
h✝ : ¬((f.insertRupUnits c.negate).fst.performRupCheck rupHints).2.2.fst = true
performRatCheck_fold_success :
  (Array.foldl (fun x ratHint => if x.snd = true then x.fst.performRatCheck p.negateLiteral ratHint else (x.fst, false))
        (((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst, true) ratHints 0).snd =
    true
fc : DefaultFormula n := (f.insertRupUnits c.negate).fst
fc_assignments_size : (f.insertRupUnits c.negate).fst.assignments.size = n
performRupCheck_res : DefaultFormula n := ((f.insertRupUnits c.negate).fst.performRupCheck rupHints).fst
⊢ performRupCheck_res.assignments.size = n
Tactic:
rw [performRupCheck_preserves_assignments_size, insertRupUnits_preserves_assignments_size, f_readyForRatAdd.2.2.1]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.ratAdd_result
Proof state before:
case isFalse
n : Nat
f : DefaultFormula n
c : DefaultClause n
p : Literal (PosFin n)
rupHints : Array Nat
ratHints : Array (Nat × Array Nat)
f' : DefaultFormula n
f_readyForRatAdd : f.readyForRatAdd
_pc : p ∈ Clause.toList c
h✝ : ¬f.ratHintsExhaustive p ratHints = true
ratAddSuccess : (f, false) = (f', true)
⊢ f' = f.insert c
Tactic:
simp at ratAddSuccess
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastConst.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
hfoo : aig.decls.size ≤ (go aig curr s c hcurr).aig.decls.size
⊢ idx < w
Tactic:
omega
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastConst.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
⊢ ∀ (idx : Nat) (hidx : idx < curr) (hfoo : aig.decls.size ≤ (go aig curr s c hcurr).aig.decls.size),
    (go aig curr s c hcurr).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
intro idx hidx
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ ∀ (hfoo : aig.decls.size ≤ (go aig curr s c hcurr).aig.decls.size),
    (go aig curr s c hcurr).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastConst.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
⊢ ∀ (hfoo : aig.decls.size ≤ (go aig curr s c hcurr).aig.decls.size),
    (go aig curr s c hcurr).stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
generalize hgo : go aig curr s c hcurr = res
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
hgo : go aig curr s c hcurr = res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastConst.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
hgo : go aig curr s c hcurr = res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
unfold go at hgo
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      let res := aig.mkConstCached (c.getLsb curr);
      let aig_1 := res.aig;
      let bitRef := res.ref;
      let s := s.cast ⋯;
      let s := s.pushRef bitRef;
      go aig_1 (curr + 1) s c ⋯
    else
      let_fun hidx := ⋯;
      { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastConst.go_getRef_aux
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
hgo :
  (if hidx : curr < w then
      let res := aig.mkConstCached (c.getLsb curr);
      let aig_1 := res.aig;
      let bitRef := res.ref;
      let s := s.cast ⋯;
      let s := s.pushRef bitRef;
      go aig_1 (curr + 1) s c ⋯
    else
      let_fun hidx := ⋯;
      { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
split at hgo
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : curr < w
hgo :
  (let res := aig.mkConstCached (c.getLsb curr);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go aig_1 (curr + 1) s c ⋯) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastConst.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : curr < w
hgo :
  (let res := aig.mkConstCached (c.getLsb curr);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go aig_1 (curr + 1) s c ⋯) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo

case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
. dsimp at hgo
  rw [← hgo]
  intro hfoo
  rw [go_getRef_aux]
  rw [AIG.RefStream.getRef_push_ref_lt]
  . simp only [Ref.cast, Ref.mk.injEq]
    rw [AIG.RefStream.getRef_cast]
    . simp
    . assumption
  . apply go_le_size
Proof state after:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastConst.go_getRef_aux
Proof state before:
case isFalse
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : ¬curr < w
hgo :
  (let_fun hidx := ⋯;
    { aig := aig, stream := hidx ▸ s }) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
. dsimp at hgo
  rw [← hgo]
  simp only [Nat.le_refl, RefStream.getRef, Ref_cast', Ref.mk.injEq, true_implies]
  congr
  . omega
  . simp
Proof state after:
no goals
Theorem: BVExpr.bitblast.blastConst.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : curr < w
hgo :
  (let res := aig.mkConstCached (c.getLsb curr);
    let aig_1 := res.aig;
    let bitRef := res.ref;
    let s := s.cast ⋯;
    let s := s.pushRef bitRef;
    go aig_1 (curr + 1) s c ⋯) =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
dsimp at hgo
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : curr < w
hgo :
  go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref) c
      ⋯ =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastConst.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : curr < w
hgo :
  go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref) c
      ⋯ =
    res
⊢ ∀ (hfoo : aig.decls.size ≤ res.aig.decls.size), res.stream.getRef idx ⋯ = (s.getRef idx hidx).cast hfoo
Tactic:
rw [← hgo]
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : curr < w
hgo :
  go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref) c
      ⋯ =
    res
⊢ ∀
    (hfoo :
      aig.decls.size ≤
        (go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1)
                ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref) c ⋯).aig.decls.size),
    (go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref)
              c ⋯).stream.getRef
        idx ⋯ =
      (s.getRef idx hidx).cast hfoo
Theorem: BVExpr.bitblast.blastConst.go_getRef_aux
Proof state before:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : curr < w
hgo :
  go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref) c
      ⋯ =
    res
⊢ ∀
    (hfoo :
      aig.decls.size ≤
        (go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1)
                ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref) c ⋯).aig.decls.size),
    (go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref)
              c ⋯).stream.getRef
        idx ⋯ =
      (s.getRef idx hidx).cast hfoo
Tactic:
intro hfoo
Proof state after:
case isTrue
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
w : Nat
aig : AIG α
c : BitVec w
curr : Nat
hcurr : curr ≤ w
s : aig.RefStream curr
idx : Nat
hidx : idx < curr
res : RefStreamEntry α w
h✝ : curr < w
hgo :
  go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref) c
      ⋯ =
    res
hfoo :
  aig.decls.size ≤
    (go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref)
            c ⋯).aig.decls.size
⊢ (go (aig.mkConstCached (c.getLsb curr)).aig (curr + 1) ((s.cast ⋯).pushRef (aig.mkConstCached (c.getLsb curr)).ref) c
            ⋯).stream.getRef
      idx ⋯ =
    (s.getRef idx hidx).cast hfoo