internlm/Lean-Github huggingface dataset:
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (i, true) = toOrder (zip a b) { val := q, property := hv }
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rw [toOrder, Eq.comm, Prod.ext_iff] at h
Proof state after:
case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h :
  ((zip a b).index { val := q, property := hv }, (zip a b).ready { val := q, property := hv }).1 = (i, true).1 ∧
    ((zip a b).index { val := q, property := hv }, (zip a b).ready { val := q, property := hv }).2 = (i, true).2
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h :
  ((zip a b).index { val := q, property := hv }, (zip a b).ready { val := q, property := hv }).1 = (i, true).1 ∧
    ((zip a b).index { val := q, property := hv }, (zip a b).ready { val := q, property := hv }).2 = (i, true).2
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
simp only [zip_σ, zip_valid, Bool.and_eq_true, decide_eq_true_eq] at h
Proof state after:
case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (zip a b).index { val := q, property := hv } = i ∧ (zip a b).ready { val := q, property := hv } = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inr.inl
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : (zip a b).index { val := q, property := hv } = i ∧ (zip a b).ready { val := q, property := hv } = true
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rcases h with ⟨rfl, hr⟩
Proof state after:
case pos.inr.inl.intro
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
hv : (zip a b).valid q = true
hr : (zip a b).ready { val := q, property := hv } = true
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q →
      evalOption (zip a b) y ((zip a b).index { val := q, property := hv }) =
        Option.map₂ Prod.mk (evalOption a y.1 ((zip a b).index { val := q, property := hv }))
          (evalOption b y.2 ((zip a b).index { val := q, property := hv }))
⊢ evalOption (zip a b) q ((zip a b).index { val := q, property := hv }) =
    Option.map₂ Prod.mk (evalOption a q.1 ((zip a b).index { val := q, property := hv }))
      (evalOption b q.2 ((zip a b).index { val := q, property := hv }))
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inr.inl.intro
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
hv : (zip a b).valid q = true
hr : (zip a b).ready { val := q, property := hv } = true
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q →
      evalOption (zip a b) y ((zip a b).index { val := q, property := hv }) =
        Option.map₂ Prod.mk (evalOption a y.1 ((zip a b).index { val := q, property := hv }))
          (evalOption b y.2 ((zip a b).index { val := q, property := hv }))
⊢ evalOption (zip a b) q ((zip a b).index { val := q, property := hv }) =
    Option.map₂ Prod.mk (evalOption a q.1 ((zip a b).index { val := q, property := hv }))
      (evalOption b q.2 ((zip a b).index { val := q, property := hv }))
Tactic:
rw [zip_ready_eq hr, (zip_ready_eq'' hr).1, (zip_ready_eq'' hr).2]
Proof state after:
case pos.inr.inl.intro
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
hv : (zip a b).valid q = true
hr : (zip a b).ready { val := q, property := hv } = true
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q →
      evalOption (zip a b) y ((zip a b).index { val := q, property := hv }) =
        Option.map₂ Prod.mk (evalOption a y.1 ((zip a b).index { val := q, property := hv }))
          (evalOption b y.2 ((zip a b).index { val := q, property := hv }))
⊢ some
      (a.value (mul.ready.fst { val := { val := q, property := hv }, property := hr }),
        b.value (mul.ready.snd { val := { val := q, property := hv }, property := hr })) =
    Option.map₂ Prod.mk (some (a.value (mul.ready.fst { val := { val := q, property := hv }, property := hr })))
      (some (b.value (mul.ready.snd { val := { val := q, property := hv }, property := hr })))
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inr.inl.intro
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
hv : (zip a b).valid q = true
hr : (zip a b).ready { val := q, property := hv } = true
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q →
      evalOption (zip a b) y ((zip a b).index { val := q, property := hv }) =
        Option.map₂ Prod.mk (evalOption a y.1 ((zip a b).index { val := q, property := hv }))
          (evalOption b y.2 ((zip a b).index { val := q, property := hv }))
⊢ some
      (a.value (mul.ready.fst { val := { val := q, property := hv }, property := hr }),
        b.value (mul.ready.snd { val := { val := q, property := hv }, property := hr })) =
    Option.map₂ Prod.mk (some (a.value (mul.ready.fst { val := { val := q, property := hv }, property := hr })))
      (some (b.value (mul.ready.snd { val := { val := q, property := hv }, property := hr })))
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } < (i, true)
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
have not_ready := not_ready_of_toOrder_lt h
Proof state after:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } < (i, true)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } < (i, true)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rw [Prod.Lex.lt_mk_true_iff] at h
Proof state after:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
have := left_right_eval_eq_of_toOrder_le h
Proof state after:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
this :
  evalOption a (advance (zip a b) ↑{ val := q, property := hv }).1 i =
      evalOption a (↑(mul.valid.fst { val := q, property := hv })) i ∧
    evalOption b (advance (zip a b) ↑{ val := q, property := hv }).2 i =
      evalOption b (↑(mul.valid.snd { val := q, property := hv })) i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
this :
  evalOption a (advance (zip a b) ↑{ val := q, property := hv }).1 i =
      evalOption a (↑(mul.valid.fst { val := q, property := hv })) i ∧
    evalOption b (advance (zip a b) ↑{ val := q, property := hv }).2 i =
      evalOption b (↑(mul.valid.snd { val := q, property := hv })) i
⊢ evalOption (zip a b) q i = Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rw [(a.zip b).evalOption_not_ready ⟨q, hv⟩ _ not_ready, ih _ ((a.zip b).next_wf ⟨q, hv⟩), this.1, this.2]
Proof state after:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
this :
  evalOption a (advance (zip a b) ↑{ val := q, property := hv }).1 i =
      evalOption a (↑(mul.valid.fst { val := q, property := hv })) i ∧
    evalOption b (advance (zip a b) ↑{ val := q, property := hv }).2 i =
      evalOption b (↑(mul.valid.snd { val := q, property := hv })) i
⊢ Option.map₂ Prod.mk (evalOption a (↑(mul.valid.fst { val := q, property := hv })) i)
      (evalOption b (↑(mul.valid.snd { val := q, property := hv })) i) =
    Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Theorem: Etch.Verification.Stream.zip_spec
Proof state before:
case pos.inr.inr
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
i : ι
q : (zip a b).σ
ih :
  ∀ (y : (zip a b).σ),
    WfRel (zip a b) y q → evalOption (zip a b) y i = Option.map₂ Prod.mk (evalOption a y.1 i) (evalOption b y.2 i)
hv : (zip a b).valid q = true
h : toOrder (zip a b) { val := q, property := hv } ≤ (i, false)
not_ready : ¬(zip a b).ready { val := q, property := hv } = true ∨ (zip a b).index { val := q, property := hv } ≠ i
this :
  evalOption a (advance (zip a b) ↑{ val := q, property := hv }).1 i =
      evalOption a (↑(mul.valid.fst { val := q, property := hv })) i ∧
    evalOption b (advance (zip a b) ↑{ val := q, property := hv }).2 i =
      evalOption b (↑(mul.valid.snd { val := q, property := hv })) i
⊢ Option.map₂ Prod.mk (evalOption a (↑(mul.valid.fst { val := q, property := hv })) i)
      (evalOption b (↑(mul.valid.snd { val := q, property := hv })) i) =
    Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i)
Tactic:
rfl
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_spec'
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : (zip a b).σ
i : ι
⊢ (evalMultiset (zip a b) q) i =
    Option.getD (Option.map (fun x => {x}) (Option.map₂ Prod.mk (evalOption a q.1 i) (evalOption b q.2 i))) 0
Tactic:
rw [(zip_strict_mono a.strictMono b.strictMono ).evalMultiset_eq_evalOption, zip_spec]
Proof state after:
no goals
Theorem: Etch.Verification.Stream.zip_seek_spec
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
j : ι
h : i ≤ (j, false)
⊢ (evalMultiset (zip a b) ((zip a b).seek q i)) j = (evalMultiset (zip a b) ↑q) j
Tactic:
simp only [zip_spec', evalOption, zip_seek]
Proof state after:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
j : ι
h : i ≤ (j, false)
⊢ Option.getD
      (Option.map (fun x => {x})
        (Option.map₂ Prod.mk (Multiset.get ((evalMultiset a (a.seek (mul.valid.fst q) i)) j))
          (Multiset.get ((evalMultiset b (b.seek (mul.valid.snd q) i)) j))))
      0 =
    Option.getD
      (Option.map (fun x => {x})
        (Option.map₂ Prod.mk (Multiset.get ((evalMultiset a (↑q).1) j)) (Multiset.get ((evalMultiset b (↑q).2) j))))
      0
Theorem: Etch.Verification.Stream.zip_seek_spec
Proof state before:
ι : Type
inst✝² : LinearOrder ι
α : Type u
β : Type v
a : Stream ι α
b : Stream ι β
inst✝¹ : IsStrictLawful a
inst✝ : IsStrictLawful b
q : { q // (zip a b).valid q = true }
i : StreamOrder ι
j : ι
h : i ≤ (j, false)
⊢ Option.getD
      (Option.map (fun x => {x})
        (Option.map₂ Prod.mk (Multiset.get ((evalMultiset a (a.seek (mul.valid.fst q) i)) j))
          (Multiset.get ((evalMultiset b (b.seek (mul.valid.snd q) i)) j))))
      0 =
    Option.getD
      (Option.map (fun x => {x})
        (Option.map₂ Prod.mk (Multiset.get ((evalMultiset a (↑q).1) j)) (Multiset.get ((evalMultiset b (↑q).2) j))))
      0
Tactic:
congr 4 <;>
  apply IsLawful.seek_spec _ _ _ h
Proof state after:
no goals
Theorem: Option.isNone_eq_true
Proof state before:
α : Type u_1
o : Option α
⊢ isNone o = true ↔ o = none
Tactic:
cases o <;> simp
Proof state after:
no goals
Theorem: RegMachine.Config.is_halted_haltedOn
Proof state before:
R L : Type
o : ℕ
r : R → ℕ
⊢ is_halted (haltedOn o r) = true
Tactic:
simp [is_halted, haltedOn]
Proof state after:
no goals
Theorem: RegMachine.Config.io_reg_haltedOn
Proof state before:
R L : Type
o : ℕ
r : R → ℕ
⊢ regs (haltedOn o r) WithIO.io = o
Tactic:
simp [Config.haltedOn]
Proof state after:
no goals
Theorem: RegMachine.stepsTo_functional
Proof state before:
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d1 d2 : Config R L
h1 : c [P]==> d1
h2 : c [P]==> d2
⊢ d1 = d2
Tactic:
match c with
| {ip,regs} =>
  cases ip <;>
    (simp [step] at h1 h2; cases h1; cases h2; rfl)
Proof state after:
no goals
Theorem: RegMachine.stepsTo_functional
Proof state before:
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d1 d2 : Config R L
ip : Option L
regs : R → ℕ
h1 : { ip := ip, regs := regs } [P]==> d1
h2 : { ip := ip, regs := regs } [P]==> d2
⊢ d1 = d2
Tactic:
cases ip <;>
  (simp [step] at h1 h2; cases h1; cases h2; rfl)
Proof state after:
no goals
Theorem: RegMachine.stepsTo_functional
Proof state before:
case some
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d1 d2 : Config R L
regs : R → ℕ
val✝ : L
h1 : { ip := some val✝, regs := regs } [P]==> d1
h2 : { ip := some val✝, regs := regs } [P]==> d2
⊢ d1 = d2
Tactic:
simp [step] at h1 h2
Proof state after:
case some
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d1 d2 : Config R L
regs : R → ℕ
val✝ : L
h1 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d1
h2 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
⊢ d1 = d2
Theorem: RegMachine.stepsTo_functional
Proof state before:
case some
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d1 d2 : Config R L
regs : R → ℕ
val✝ : L
h1 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d1
h2 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
⊢ d1 = d2
Tactic:
cases h1
Proof state after:
case some.refl
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d2 : Config R L
regs : R → ℕ
val✝ : L
h2 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
⊢ (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
Theorem: RegMachine.stepsTo_functional
Proof state before:
case some.refl
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c d2 : Config R L
regs : R → ℕ
val✝ : L
h2 :
  (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
⊢ (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    d2
Tactic:
cases h2
Proof state after:
case some.refl.refl
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c : Config R L
regs : R → ℕ
val✝ : L
⊢ (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }
Theorem: RegMachine.stepsTo_functional
Proof state before:
case some.refl.refl
R✝ L✝ : Type
Start✝ : ?m.35746
P✝ : Prog R✝ L✝
inst✝¹ : DecidableEq R✝
S✝ : sorryAx (Sort ?u.35760) true
R L : Type
x✝ : Sort ?u.35745
Start : x✝
P : Prog R L
inst✝ : DecidableEq R
S : sorryAx (Sort ?u.35760) true
c : Config R L
regs : R → ℕ
val✝ : L
⊢ (match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }) =
    match P val✝ with
    | Instr.inc r l => { ip := l, regs := Function.update regs r (regs r + 1) }
    | Instr.dec r l k =>
      match regs r with
      | Nat.succ n => { ip := l, regs := Function.update regs r n }
      | 0 => { ip := k, regs := regs }
Tactic:
rfl
Proof state after:
no goals