Theorem: length_backtrack (ReckonLean/Dpll.lean)

State before:
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
⊢ ∀ (tr : Trail α), List.length (backtrack tr) ≤ List.length tr
Tactic:
intro t
State after:
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
t : Trail α
⊢ List.length (backtrack t) ≤ List.length t

State before:
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
t : Trail α
⊢ List.length (backtrack t) ≤ List.length t
Tactic:
induction t with
| nil => unfold backtrack; apply Nat.le_refl
| cons d ds ih =>
  simp [backtrack]
  cases d.decision == .Deduced
  . simp
  . simp; apply Nat.le_succ_of_le; assumption
State after:
no goals

State before:
case nil
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
⊢ List.length (backtrack []) ≤ List.length []
Tactic:
unfold backtrack
State after:
case nil
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
⊢ List.length [] ≤ List.length []

State before:
case nil
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
⊢ List.length [] ≤ List.length []
Tactic:
apply Nat.le_refl
State after:
no goals

State before:
case cons
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (backtrack (d :: ds)) ≤ List.length (d :: ds)
Tactic:
simp [backtrack]
State after:
case cons
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if (d.decision == LitState.Deduced) = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)

State before:
case cons
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if (d.decision == LitState.Deduced) = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Tactic:
cases d.decision == .Deduced
State after:
case cons.false
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if false = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)

case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if true = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)

State before:
case cons.false
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if false = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)

case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if true = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Tactic:
. simp
State after:
case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if true = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)

State before:
case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if true = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Tactic:
. simp; apply Nat.le_succ_of_le; assumption
State after:
no goals

State before:
case cons.false
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if false = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Tactic:
simp
State after:
no goals

State before:
case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (if true = true then backtrack ds else d :: ds) ≤ Nat.succ (List.length ds)
Tactic:
simp
State after:
case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (backtrack ds) ≤ Nat.succ (List.length ds)

State before:
case cons.true
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (backtrack ds) ≤ Nat.succ (List.length ds)
Tactic:
apply Nat.le_succ_of_le
State after:
case cons.true.h
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (backtrack ds) ≤ List.length ds

State before:
case cons.true.h
α : Type
inst✝³ : BEq α
inst✝² : Ord α
inst✝¹ : Repr α
inst✝ : Hashable α
d : Decision α
ds : List (Decision α)
ih : List.length (backtrack ds) ≤ List.length ds
⊢ List.length (backtrack ds) ≤ List.length ds
Tactic:
assumption
State after:
no goals