Theorem: LeanSAT.Model.PropForm.eval_ofFun (LeanSAT/Model/OfFun.lean)

State before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ eval τ (ofFun p L hc) = p τ
Tactic:
unfold ofFun
State after:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ eval τ (ofFun.aux p L fun v h => ⋯.elim) = p τ

State before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ eval τ (ofFun.aux p L fun v h => ⋯.elim) = p τ
Tactic:
suffices ∀ {rem passn},
  (∀ v h, passn v h = τ v ) →
  eval τ (ofFun.aux p rem passn) = p τ
  from this (fun v h => by have := h (hc v); contradiction)
State after:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ

State before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
⊢ ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ
Tactic:
intro rem passn ht
State after:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
rem : List V
passn : (v : V) → v ∉ rem → Bool
ht : ∀ (v : V) (h : v ∉ rem), passn v h = τ v
⊢ eval τ (ofFun.aux p rem passn) = p τ

State before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
rem : List V
passn : (v : V) → v ∉ rem → Bool
ht : ∀ (v : V) (h : v ∉ rem), passn v h = τ v
⊢ eval τ (ofFun.aux p rem passn) = p τ
Tactic:
induction rem with
| nil => simp [ofFun.aux]; congr; funext v; simp [*]
| cons head tail ih =>
  simp
  cases hhead : τ head <;> (simp; apply ih; intro v h; split <;> simp [*])
State after:
no goals

State before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
this :
  ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ
v : V
h : v ∉ L
⊢ (fun v h => ⋯.elim) v h = τ v
Tactic:
have := h (hc v)
State after:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
this✝ :
  ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ
v : V
h : v ∉ L
this : False
⊢ (fun v h => ⋯.elim) v h = τ v

State before:
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
this✝ :
  ∀ {rem : List V} {passn : (v : V) → v ∉ rem → Bool},
    (∀ (v : V) (h : v ∉ rem), passn v h = τ v) → eval τ (ofFun.aux p rem passn) = p τ
v : V
h : v ∉ L
this : False
⊢ (fun v h => ⋯.elim) v h = τ v
Tactic:
contradiction
State after:
no goals

State before:
case nil
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
⊢ eval τ (ofFun.aux p [] passn) = p τ
Tactic:
simp [ofFun.aux]
State after:
case nil
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
⊢ (p fun v => passn v ⋯) = p τ

State before:
case nil
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
⊢ (p fun v => passn v ⋯) = p τ
Tactic:
congr
State after:
case nil.e_a
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
⊢ (fun v => passn v ⋯) = τ

State before:
case nil.e_a
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
⊢ (fun v => passn v ⋯) = τ
Tactic:
funext v
State after:
case nil.e_a.h
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
v : V
⊢ passn v ⋯ = τ v

State before:
case nil.e_a.h
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
passn : (v : V) → v ∉ [] → Bool
ht : ∀ (v : V) (h : v ∉ []), passn v h = τ v
v : V
⊢ passn v ⋯ = τ v
Tactic:
simp [*]
State after:
no goals

State before:
case cons
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
⊢ eval τ (ofFun.aux p (head :: tail) passn) = p τ
Tactic:
simp
State after:
case cons
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
⊢ (τ head && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then true else passn v' ⋯) ||
      !τ head && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then false else passn v' ⋯)) =
    p τ

State before:
case cons
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
⊢ (τ head && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then true else passn v' ⋯) ||
      !τ head && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then false else passn v' ⋯)) =
    p τ
Tactic:
cases hhead : τ head <;> (simp; apply ih; intro v h; split <;> simp [*])
State after:
no goals

State before:
case cons.true
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
⊢ (true && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then true else passn v' ⋯) ||
      !true && eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then false else passn v' ⋯)) =
    p τ
Tactic:
simp
State after:
case cons.true
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
⊢ eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then true else passn v' ⋯) = p τ

State before:
case cons.true
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
⊢ eval τ (ofFun.aux p tail fun v' h' => if h : v' = head then true else passn v' ⋯) = p τ
Tactic:
apply ih
State after:
case cons.true.ht
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
⊢ ∀ (v : V) (h : v ∉ tail), (if h : v = head then true else passn v ⋯) = τ v

State before:
case cons.true.ht
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
⊢ ∀ (v : V) (h : v ∉ tail), (if h : v = head then true else passn v ⋯) = τ v
Tactic:
intro v h
State after:
case cons.true.ht
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
v : V
h : v ∉ tail
⊢ (if h : v = head then true else passn v ⋯) = τ v

State before:
case cons.true.ht
V : Type u_1
p : PropAssignment V → Bool
τ : PropAssignment V
inst✝ : DecidableEq V
L : List V
hc : ∀ (v : V), v ∈ L
head : V
tail : List V
ih :
  ∀ {passn : (v : V) → v ∉ tail → Bool},
    (∀ (v : V) (h : v ∉ tail), passn v h = τ v) → eval τ (ofFun.aux p tail passn) = p τ
passn : (v : V) → v ∉ head :: tail → Bool
ht : ∀ (v : V) (h : v ∉ head :: tail), passn v h = τ v
hhead : τ head = true
v : V
h : v ∉ tail
⊢ (if h : v = head then true else passn v ⋯) = τ v
Tactic:
split <;> simp [*]
State after:
no goals