internlm/Lean-Github huggingface dataset:
Theorem: AIG.denote.eq_of_aig_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
this✝ : entry.ref.gate < entry.aig.decls.size
this : entry.aig.decls.size ≤ newAIG.decls.size
⊢ entry.ref.gate < newAIG.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.denote.eq_of_aig_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ ⟦{ aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }, assign⟧ = ⟦entry, assign⟧
Tactic:
unfold denote
Proof state after:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ go { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.ref.gate
      { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ =
    go entry.ref.gate entry.aig.decls assign ⋯ ⋯
Theorem: AIG.denote.eq_of_aig_eq
Proof state before:
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ go { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.ref.gate
      { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ =
    go entry.ref.gate entry.aig.decls assign ⋯ ⋯
Tactic:
apply denote.go_eq_of_aig_eq
Proof state after:
case hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ IsPrefix entry.aig.decls { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls
Theorem: AIG.denote.eq_of_aig_eq
Proof state before:
case hprefix
α : Type
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : DecidableEq α
assign : α → Bool
entry : Entrypoint α
newAIG : AIG α
hprefix : IsPrefix entry.aig.decls newAIG.decls
⊢ IsPrefix entry.aig.decls { aig := newAIG, ref := { gate := entry.ref.gate, hgate := ⋯ } }.aig.decls
Tactic:
assumption
Proof state after:
no goals
Theorem: AIG.LawfulOperator.IsPrefix_aig
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ IsPrefix aig.decls (f aig input).aig.decls
Tactic:
apply IsPrefix.of
Proof state after:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]

case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Theorem: AIG.LawfulOperator.IsPrefix_aig
Proof state before:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]

case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. intro idx h
  apply decl_eq
Proof state after:
case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Theorem: AIG.LawfulOperator.IsPrefix_aig
Proof state before:
case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. apply le_size
Proof state after:
no goals
Theorem: AIG.LawfulOperator.IsPrefix_aig
Proof state before:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ ∀ (idx : Nat) (h : idx < aig.decls.size), (f aig input).aig.decls[idx] = aig.decls[idx]
Tactic:
intro idx h
Proof state after:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
idx : Nat
h : idx < aig.decls.size
⊢ (f aig input).aig.decls[idx] = aig.decls[idx]
Theorem: AIG.LawfulOperator.IsPrefix_aig
Proof state before:
case idx_eq
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
idx : Nat
h : idx < aig.decls.size
⊢ (f aig input).aig.decls[idx] = aig.decls[idx]
Tactic:
apply decl_eq
Proof state after:
no goals
Theorem: AIG.LawfulOperator.IsPrefix_aig
Proof state before:
case size_le
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
aig : AIG α
input : β aig
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
apply le_size
Proof state after:
no goals
Theorem: AIG.LawfulOperator.lt_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Tactic:
have h1 := entry.ref.hgate
Proof state after:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Theorem: AIG.LawfulOperator.lt_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Tactic:
have h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size := by
  apply le_size
Proof state after:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Theorem: AIG.LawfulOperator.lt_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
h2 : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ entry.ref.gate < (f entry.aig input).aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.LawfulOperator.lt_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
entry : Entrypoint α
input : β entry.aig
h1 : entry.ref.gate < entry.aig.decls.size
⊢ entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
Tactic:
apply le_size
Proof state after:
no goals
Theorem: AIG.LawfulOperator.lt_size_of_lt_aig_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ x < (f aig input).aig.decls.size
Tactic:
apply Nat.lt_of_lt_of_le
Proof state after:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ x < ?m

case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ Nat
Theorem: AIG.LawfulOperator.lt_size_of_lt_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ x < ?m

case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ Nat
Tactic:
. exact h
Proof state after:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Theorem: AIG.LawfulOperator.lt_size_of_lt_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. exact le_size aig input
Proof state after:
no goals
Theorem: AIG.LawfulOperator.lt_size_of_lt_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ x < ?m
Tactic:
exact h
Proof state after:
no goals
Theorem: AIG.LawfulOperator.lt_size_of_lt_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x < aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
exact le_size aig input
Proof state after:
no goals
Theorem: AIG.LawfulOperator.le_size_of_le_aig_size
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ x ≤ (f aig input).aig.decls.size
Tactic:
apply Nat.le_trans
Proof state after:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ x ≤ ?m

case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ Nat
Theorem: AIG.LawfulOperator.le_size_of_le_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ x ≤ ?m

case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ ?m ≤ (f aig input).aig.decls.size

case m
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ Nat
Tactic:
. exact h
Proof state after:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Theorem: AIG.LawfulOperator.le_size_of_le_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
. exact le_size aig input
Proof state after:
no goals
Theorem: AIG.LawfulOperator.le_size_of_le_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ x ≤ ?m
Tactic:
exact h
Proof state after:
no goals
Theorem: AIG.LawfulOperator.le_size_of_le_aig_size
Proof state before:
case a
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
x : Nat
aig : AIG α
input : β aig
h : x ≤ aig.decls.size
⊢ aig.decls.size ≤ (f aig input).aig.decls.size
Tactic:
exact le_size aig input
Proof state after:
no goals
Theorem: AIG.LawfulOperator.denote_input_entry
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
entry : Entrypoint α
input : β entry.aig
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ ⟦{ aig := (f entry.aig input).aig, ref := { gate := entry.ref.gate, hgate := h } }, assign⟧ = ⟦entry, assign⟧
Tactic:
apply denote.eq_of_aig_eq
Proof state after:
case hprefix
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
entry : Entrypoint α
input : β entry.aig
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ IsPrefix entry.aig.decls (f entry.aig input).aig.decls
Theorem: AIG.LawfulOperator.denote_input_entry
Proof state before:
case hprefix
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
entry : Entrypoint α
input : β entry.aig
h : entry.ref.gate < (f entry.aig input).aig.decls.size
⊢ IsPrefix entry.aig.decls (f entry.aig input).aig.decls
Tactic:
apply IsPrefix_aig
Proof state after:
no goals
Theorem: AIG.LawfulOperator.denote_cast_entry
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
assign : α → Bool
entry : Entrypoint α
input : β entry.aig
h : entry.aig.decls.size ≤ (f entry.aig input).aig.decls.size
⊢ ⟦{ aig := (f entry.aig input).aig, ref := entry.ref.cast h }, assign⟧ = ⟦entry, assign⟧
Tactic:
simp [Ref.cast]
Proof state after:
no goals
Theorem: AIG.LawfulOperator.denote_mem_prefix
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
start : Nat
assign : α → Bool
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ start < (f aig input).aig.decls.size
Tactic:
apply lt_size_of_lt_aig_size
Proof state after:
case h
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
start : Nat
assign : α → Bool
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ start < aig.decls.size
Theorem: AIG.LawfulOperator.denote_mem_prefix
Proof state before:
case h
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
start : Nat
assign : α → Bool
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ start < aig.decls.size
Tactic:
omega
Proof state after:
no goals
Theorem: AIG.LawfulOperator.denote_mem_prefix
Proof state before:
α : Type
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : DecidableEq α
β : AIG α → Type
f : (aig : AIG α) → β aig → Entrypoint α
inst✝ : LawfulOperator α β f
start : Nat
assign : α → Bool
aig : AIG α
input : β aig
h : start < aig.decls.size
⊢ ⟦{ aig := (f aig input).aig, ref := { gate := start, hgate := ⋯ } }, assign⟧ =
    ⟦{ aig := aig, ref := { gate := start, hgate := h } }, assign⟧
Tactic:
rw [denote_input_entry ⟨aig, start, h⟩]
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.assignments_invariant_of_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
⊢ f.strong_assignments_invariant → f.assignments_invariant
Tactic:
intro ⟨hsize, h⟩
Proof state after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ f.assignments_invariant
Theorem: LRAT.DefaultFormula.assignments_invariant_of_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ f.assignments_invariant
Tactic:
apply Exists.intro hsize
Proof state after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
Theorem: LRAT.DefaultFormula.assignments_invariant_of_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
⊢ ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
Tactic:
intro i b hb p pf
Proof state after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.assignments_invariant_of_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
h : ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → unit (i, b) ∈ f.toList
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ (i, b)
Tactic:
specialize h i b hb
Proof state after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
pf : p ⊨ f
h : unit (i, b) ∈ f.toList
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.assignments_invariant_of_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : ∀ (x : DefaultClause n), x ∈ f.toList → decide (Clause.instHSat.1 p x) = true
⊢ p ⊨ (i, b)
Tactic:
specialize pf (unit (i, b)) h
Proof state after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : decide (Clause.instHSat.1 p (unit (i, b))) = true
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.assignments_invariant_of_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : decide (Clause.instHSat.1 p (unit (i, b))) = true
⊢ p ⊨ (i, b)
Tactic:
simp [Clause.instHSat, unit_eq, Clause.toList] at pf
Proof state after:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : p ⊨ (i, b)
⊢ p ⊨ (i, b)
Theorem: LRAT.DefaultFormula.assignments_invariant_of_strong_assignments_invariant
Proof state before:
n : Nat
f : DefaultFormula n
hsize : f.assignments.size = n
i : PosFin n
b : Bool
hb : hasAssignment b f.assignments[i.val] = true
p : PosFin n → Bool
h : unit (i, b) ∈ f.toList
pf : p ⊨ (i, b)
⊢ p ⊨ (i, b)
Tactic:
exact pf
Proof state after:
no goals
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
⊢ limplies (PosFin n) f f.assignments
Tactic:
intro p pf
Proof state after:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.assignments
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
n : Nat
f : DefaultFormula n
f_assignments_invariant : f.assignments_invariant
p : PosFin n → Bool
pf : p ⊨ f
⊢ p ⊨ f.assignments
Tactic:
rcases f_assignments_invariant with ⟨hsize, f_assignments_invariant⟩
Proof state after:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_assignments_invariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
⊢ p ⊨ f.assignments
Theorem: LRAT.DefaultFormula.assignments_invariant_entails_limplies
Proof state before:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_assignments_invariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
⊢ ∀ (i : PosFin n), hasAssignment (decide (p i = false)) f.assignments[i.val]! = false
Tactic:
intro i
Proof state after:
case intro
n : Nat
f : DefaultFormula n
p : PosFin n → Bool
pf : p ⊨ f
hsize : f.assignments.size = n
f_assignments_invariant :
  ∀ (i : PosFin n) (b : Bool), hasAssignment b f.assignments[i.val] = true → limplies (PosFin n) f (i, b)
i : PosFin n
⊢ hasAssignment (decide (p i = false)) f.assignments[i.val]! = false