Theorem: QueueData.nonEmptyPull (Advent/Queue.lean)

State before:
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ toList q = x :: xs ↔ ∃ qt, toList qt = xs ∧ pull q = some (x, qt)
Tactic:
simp [toList, pull]
State after:
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ init ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match init with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)

State before:
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ init ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match init with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)
Tactic:
cases q.init
State after:
case nil
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ [] ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match [] with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)

case cons
α : Type u_1
q : QueueData α
x : α
xs : List α
head✝ : α
tail✝ : List α
⊢ head✝ :: tail✝ ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match head✝ :: tail✝ with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)

State before:
case nil
α : Type u_1
q : QueueData α
x : α
xs : List α
⊢ [] ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match [] with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)

case cons
α : Type u_1
q : QueueData α
x : α
xs : List α
head✝ : α
tail✝ : List α
⊢ head✝ :: tail✝ ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match head✝ :: tail✝ with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)
Tactic:
generalize p : q.tail.reverse = tr
State after:
case nil
α : Type u_1
q : QueueData α
x : α
xs tr : List α
p : List.reverse tail = tr
⊢ [] ++ tr = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match [] with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match tr with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)

case cons
α : Type u_1
q : QueueData α
x : α
xs : List α
head✝ : α
tail✝ : List α
⊢ head✝ :: tail✝ ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match head✝ :: tail✝ with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)

State before:
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ h = x ∧ t = xs ↔ ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt
Tactic:
constructor
State after:
case mp
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ h = x ∧ t = xs → ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt

case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt) → h = x ∧ t = xs

State before:
case mp
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ h = x ∧ t = xs → ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt

case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt) → h = x ∧ t = xs
Tactic:
. intro p1 
  exists ⟨ t , []⟩
  simp [*]
State after:
case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = qt) → h = x ∧ t = xs

State before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
⊢ h = x ∧ t = xs
Tactic:
simp [*]
State after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
⊢ t = xs

State before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
⊢ t = xs
Tactic:
let p2 := p1.right.right
State after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
⊢ t = xs

State before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
⊢ t = xs
Tactic:
simp at p1
State after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
⊢ t = xs

State before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
p3 : (fun x => init) { init := t, tail := [] } = (fun x => init) { init := qi, tail := qt } :=
  congrArg (fun x => init) p2
p4 : (fun x => tail) { init := t, tail := [] } = (fun x => tail) { init := qi, tail := qt } :=
  congrArg (fun x => tail) p2
⊢ t = xs
Tactic:
simp at p3 p4
State after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
⊢ t = xs

State before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1 : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
⊢ t = xs
Tactic:
rw [← p3, ← p4] at p1
State after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1✝ : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p1 : t ++ List.reverse [] = xs ∧ h = x ∧ { init := t, tail := [] } = { init := t, tail := [] }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1✝.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
⊢ t = xs

State before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1✝ : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p1 : t ++ List.reverse [] = xs ∧ h = x ∧ { init := t, tail := [] } = { init := t, tail := [] }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1✝.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
⊢ t = xs
Tactic:
simp at p1
State after:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1✝ : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1✝.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
p1 : t = xs ∧ h = x
⊢ t = xs

State before:
case mpr.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p : List.reverse tail = h :: t
qi qt : List α
p1✝ : qi ++ List.reverse qt = xs ∧ h = x ∧ { init := t, tail := [] } = { init := qi, tail := qt }
p2 : { init := t, tail := [] } = { init := qi, tail := qt } := p1✝.right.right
p3 : t = qi := congrArg (fun x => init) p2
p4 : [] = qt := congrArg (fun x => tail) p2
p1 : t = xs ∧ h = x
⊢ t = xs
Tactic:
simp [p1]
State after:
no goals

State before:
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h :: t ++ List.reverse tail = x :: xs ↔
    ∃ qt,
      init ++ List.reverse tail = xs ∧
        (match h :: t with
          | x :: xs => some (x, { init := xs, tail := tail })
          | [] =>
            match List.reverse tail with
            | x :: xs => some (x, { init := xs, tail := [] })
            | [] => none) =
          some (x, qt)
Tactic:
simp
State after:
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h = x ∧ t ++ List.reverse tail = xs ↔ ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt

State before:
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h = x ∧ t ++ List.reverse tail = xs ↔ ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt
Tactic:
constructor
State after:
case mp
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h = x ∧ t ++ List.reverse tail = xs → ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt

case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt) →
    h = x ∧ t ++ List.reverse tail = xs

State before:
case mp
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ h = x ∧ t ++ List.reverse tail = xs → ∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt

case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt) →
    h = x ∧ t ++ List.reverse tail = xs
Tactic:
. intro pp
  let qt: QueueData α := ⟨ t, q.tail ⟩
  exists qt
  simp
  rw [pp.left, pp.right]    
  simp
State after:
case mpr
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
⊢ (∃ qt, init ++ List.reverse tail = xs ∧ h = x ∧ { init := t, tail := tail } = qt) →
    h = x ∧ t ++ List.reverse tail = xs

State before:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
⊢ h = x ∧ t ++ List.reverse tail = xs
Tactic:
rw [p2, ← p1]
State after:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
⊢ x = x ∧ t ++ List.reverse tail = init ++ List.reverse tail

State before:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
⊢ x = x ∧ t ++ List.reverse tail = init ++ List.reverse tail
Tactic:
simp
State after:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
⊢ t ++ List.reverse tail = qti ++ List.reverse qtt

State before:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
p4 : (fun x => init) { init := t, tail := tail } = (fun x => init) { init := qti, tail := qtt } :=
  congrArg (fun x => init) p3
p5 : (fun x => tail) { init := t, tail := tail } = (fun x => tail) { init := qti, tail := qtt } :=
  congrArg (fun x => tail) p3
⊢ t ++ List.reverse tail = qti ++ List.reverse qtt
Tactic:
simp at p4 p5
State after:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
p4 : t = qti := congrArg (fun x => init) p3
p5 : tail = qtt := congrArg (fun x => tail) p3
⊢ t ++ List.reverse tail = qti ++ List.reverse qtt

State before:
case mpr.intro.intro.intro.mk
α : Type u_1
q : QueueData α
x : α
xs : List α
h : α
t : List α
p2 : h = x
qti qtt : List α
p1 : init ++ List.reverse tail = xs
p3 : { init := t, tail := tail } = { init := qti, tail := qtt }
p4 : t = qti := congrArg (fun x => init) p3
p5 : tail = qtt := congrArg (fun x => tail) p3
⊢ t ++ List.reverse tail = qti ++ List.reverse qtt
Tactic:
rw [p4, p5]
State after:
no goals