internlm/Lean-Github huggingface dataset:
Theorem: SSAEnv.equiv_set
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)
Tactic:
byCases Hname: name = name'
Proof state after:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
⊢ get name' τ' (set name' τ v env₁) = get name' τ' (set name' τ v env₂)

case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)
Theorem: SSAEnv.equiv_set
Proof state before:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
⊢ get name' τ' (set name' τ v env₁) = get name' τ' (set name' τ v env₂)

case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)
Tactic:
. simp [get_set_eq_val]
Proof state after:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)
Theorem: SSAEnv.equiv_set
Proof state before:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' (set name τ v env₁) = get name' τ' (set name τ v env₂)
Tactic:
. repeat rw [get_set_ne_val] <;> try assumption
  apply HEnv
Proof state after:
no goals
Theorem: SSAEnv.equiv_set
Proof state before:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' env₁ = get name' τ' (set name τ v env₂)
Tactic:
rw [get_set_ne_val] <;> try assumption
Proof state after:
case h2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ get name' τ' env₁ = get name' τ' env₂
Theorem: SSAEnv.equiv_set
Proof state before:
case h2.a
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
env₁ env₂ : SSAEnv δ
HEnv : equiv env₁ env₂
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
name' : SSAVal
τ' : MLIRType δ
Hname : ¬name = name'
⊢ name ≠ name'
Tactic:
assumption
Proof state after:
no goals
Theorem: SSAEnv.set_commutes
Proof state before:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
⊢ v' ≠ v →
    ∀ ⦃env : SSAEnv δ⦄ ⦃τ τ' : MLIRType δ⦄ ⦃val : MLIRType.eval τ⦄ ⦃val' : MLIRType.eval τ'⦄,
      equiv (set v τ val (set v' τ' val' env)) (set v' τ' val' (set v τ val env))
Tactic:
intros Hne env τ τ' val val' v₂ τ₂
Proof state after:
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
v₂ : SSAVal
τ₂ : MLIRType δ
⊢ get v₂ τ₂ (set v τ val (set v' τ' val' env)) = get v₂ τ₂ (set v' τ' val' (set v τ val env))
Theorem: SSAEnv.set_commutes
Proof state before:
case inr
α σ : Type
ε : σ → Type
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ : Dialect α✝ σ✝ ε✝
v v' : SSAVal
Hne : v' ≠ v
env : SSAEnv δ
τ τ' : MLIRType δ
val : MLIRType.eval τ
val' : MLIRType.eval τ'
v₂ : SSAVal
τ₂ : MLIRType δ
h✝ : ¬v = v₂
⊢ (if v' = v₂ then
      if H : τ' = τ₂ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ₂ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            val')
      else none
    else get v₂ τ₂ env) =
    if v' = v₂ then
      if H : τ' = τ₂ then
        some
          (cast
            (_ :
              (match τ' with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit) =
                match τ₂ with
                | MLIRType.float a => Float
                | MLIRType.int signedness sz => FinInt sz
                | MLIRType.tensor1d => Tensor1D
                | MLIRType.tensor2d => Tensor2D
                | MLIRType.tensor4d => Tensor4D
                | MLIRType.index => ℤ
                | MLIRType.undefined a => Unit
                | MLIRType.extended σ => ε✝ σ
                | MLIRType.erased => Unit)
            val')
      else none
    else get v₂ τ₂ env
Tactic:
. split <;> simp
Proof state after:
no goals
Theorem: interpSSA'_trigger_MemberSumL
Proof state before:
α σ : Type
ε : σ → Type
α' σ' : Type
ε' : σ' → Type
T : Type
E : Type → Type
Δ : Dialect α' σ' ε'
e : SSAEnvE Δ T
s₁ : SSAEnv Δ
⊢ interpSSA' (Fitree.trigger e) s₁ = SSAEnvE.handle T e s₁
Tactic:
simp [Fitree.trigger, pair_eta]
Proof state after:
no goals
Theorem: interpSSA'_bind
Proof state before:
α σ : Type
ε : σ → Type
E : Type → Type
T R : Type
δ : Dialect α σ ε
t : Fitree (SSAEnvE δ +' E) T
k : T → Fitree (SSAEnvE δ +' E) R
s₁ : SSAEnv δ
⊢ interpSSA' (Fitree.bind t k) s₁ =
    Fitree.bind (interpSSA' t s₁) fun x =>
      match x with
      | (x, s₂) => interpSSA' (k x) s₂
Tactic:
apply Fitree.interpState_bind
Proof state after:
no goals
Theorem: BubbleUpExtractSlice.bubble_up_extract_slice
Proof state before:
M : Type → Type
len : ℕ
MM : Monad M
LM : LawfulMonad M
t : Tensor1D
f : FinInt 32 → M (FinInt 32)
⊢ (fun s => Tensor1D.extract s len) <$> Tensor1D.mapM t f = Tensor1D.mapM (Tensor1D.extract t len) f
Tactic:
cases t
Proof state after:
case mk
M : Type → Type
len : ℕ
MM : Monad M
LM : LawfulMonad M
f : FinInt 32 → M (FinInt 32)
size0✝ : ℕ
data✝ : List (FinInt 32)
h_data_size✝ : List.length data✝ = size0✝
⊢ (fun s => Tensor1D.extract s len) <$>
      Tensor1D.mapM { size0 := size0✝, data := data✝, h_data_size := h_data_size✝ } f =
    Tensor1D.mapM (Tensor1D.extract { size0 := size0✝, data := data✝, h_data_size := h_data_size✝ } len) f
Theorem: BubbleUpExtractSlice.bubble_up_extract_slice
Proof state before:
case mk
M : Type → Type
len : ℕ
MM : Monad M
LM : LawfulMonad M
f : FinInt 32 → M (FinInt 32)
size0✝ : ℕ
data✝ : List (FinInt 32)
h_data_size✝ : List.length data✝ = size0✝
⊢ (fun s => Tensor1D.extract s len) <$>
      Tensor1D.mapM { size0 := size0✝, data := data✝, h_data_size := h_data_size✝ } f =
    Tensor1D.mapM (Tensor1D.extract { size0 := size0✝, data := data✝, h_data_size := h_data_size✝ } len) f
Tactic:
sorry
Proof state after:
no goals
Theorem: ExtractSliceFillCommuteOneD.extract_fill_commute
Proof state before:
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ Tensor1D.fill (Tensor1D.extract t extractlen) fillval = Tensor1D.extract (Tensor1D.fill t fillval) extractlen
Tactic:
simp [Tensor1D.fill, Tensor1D.extract]
Proof state after:
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.replicate (min extractlen t.size0) fillval = List.take extractlen (List.replicate t.size0 fillval)
Theorem: ExtractSliceFillCommuteOneD.extract_fill_commute
Proof state before:
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.replicate (min extractlen t.size0) fillval = List.take extractlen (List.replicate t.size0 fillval)
Tactic:
apply List.extF
Proof state after:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ ∀ (n : ℕ) (h : n < List.length (List.replicate (min extractlen t.size0) fillval)),
    List.getF (List.replicate (min extractlen t.size0) fillval) n h =
      List.getF (List.take extractlen (List.replicate t.size0 fillval)) n
        (_ : n < List.length (List.take extractlen (List.replicate t.size0 fillval)))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Theorem: ExtractSliceFillCommuteOneD.extract_fill_commute
Proof state before:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ ∀ (n : ℕ) (h : n < List.length (List.replicate (min extractlen t.size0) fillval)),
    List.getF (List.replicate (min extractlen t.size0) fillval) n h =
      List.getF (List.take extractlen (List.replicate t.size0 fillval)) n
        (_ : n < List.length (List.take extractlen (List.replicate t.size0 fillval)))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Tactic:
intros n h
Proof state after:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h : n < List.length (List.replicate (min extractlen t.size0) fillval)
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h =
    List.getF (List.take extractlen (List.replicate t.size0 fillval)) n
      (_ : n < List.length (List.take extractlen (List.replicate t.size0 fillval)))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Theorem: ExtractSliceFillCommuteOneD.extract_fill_commute
Proof state before:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h : n < List.length (List.replicate (min extractlen t.size0) fillval)
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h =
    List.getF (List.take extractlen (List.replicate t.size0 fillval)) n
      (_ : n < List.length (List.take extractlen (List.replicate t.size0 fillval)))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Tactic:
simp
Proof state after:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h : n < List.length (List.replicate (min extractlen t.size0) fillval)
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h =
    List.getF (List.replicate t.size0 fillval) n (_ : n < List.length (List.replicate t.size0 fillval))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Theorem: ExtractSliceFillCommuteOneD.extract_fill_commute
Proof state before:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h : n < List.length (List.replicate (min extractlen t.size0) fillval)
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h =
    List.getF (List.replicate t.size0 fillval) n (_ : n < List.length (List.replicate t.size0 fillval))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Tactic:
simp at h
Proof state after:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h✝ : n < List.length (List.replicate (min extractlen t.size0) fillval)
h : n < extractlen ∧ n < t.size0
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h✝ =
    List.getF (List.replicate t.size0 fillval) n (_ : n < List.length (List.replicate t.size0 fillval))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Theorem: ExtractSliceFillCommuteOneD.extract_fill_commute
Proof state before:
case a
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
n : ℕ
h✝ : n < List.length (List.replicate (min extractlen t.size0) fillval)
h : n < extractlen ∧ n < t.size0
⊢ List.getF (List.replicate (min extractlen t.size0) fillval) n h✝ =
    List.getF (List.replicate t.size0 fillval) n (_ : n < List.length (List.replicate t.size0 fillval))

case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Tactic:
sorry
Proof state after:
case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Theorem: ExtractSliceFillCommuteOneD.extract_fill_commute
Proof state before:
case h_len
t : Tensor1D
extractlen : ℕ
fillval : FinInt 32
⊢ List.length (List.replicate (min extractlen t.size0) fillval) =
    List.length (List.take extractlen (List.replicate t.size0 fillval))
Tactic:
sorry
Proof state after:
no goals
Theorem: ExtractSliceGenericCommute1D.equiv
Proof state before:
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
⊢ validGenericRegion r rSpec →
    run ⟦ LHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
      run ⟦ RHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])
Tactic:
intros valid_r
Proof state after:
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
valid_r : validGenericRegion r rSpec
⊢ run ⟦ LHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
    run ⟦ RHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])
Theorem: ExtractSliceGenericCommute1D.equiv
Proof state before:
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
valid_r : validGenericRegion r rSpec
⊢ run ⟦ LHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
    run ⟦ RHS r ⟧ (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])
Tactic:
simp[LHS, RHS]
Proof state after:
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
valid_r : validGenericRegion r rSpec
⊢ run
      (denoteRegion linalg
        (Region.mk "entry" []
          [Op.mk "linalg.generic1d" [(SSAVal.SSAVal "x", MLIRType.tensor1d)] [(SSAVal.SSAVal "t", MLIRType.tensor1d)]
              [r] (AttrDict.mk [AttrEntry.mk "len" (AttrValue.int 10 MLIRType.index)]),
            Op.mk "linalg.fill1d" [(SSAVal.SSAVal "out", MLIRType.tensor1d)] [(SSAVal.SSAVal "x", MLIRType.tensor1d)] []
              (AttrDict.mk [AttrEntry.mk "cst" (AttrValue.int 42 MLIRType.index)])])
        [])
      (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
    run
      (denoteRegion linalg
        (Region.mk "entry" []
          [Op.mk "linalg.generic1d" [(SSAVal.SSAVal "x", MLIRType.tensor1d)] [(SSAVal.SSAVal "t", MLIRType.tensor1d)]
              [r] (AttrDict.mk [AttrEntry.mk "cst" (AttrValue.int 42 MLIRType.index)]),
            Op.mk "linalg.extractslice1d" [(SSAVal.SSAVal "out", MLIRType.tensor1d)]
              [(SSAVal.SSAVal "x", MLIRType.tensor1d)] []
              (AttrDict.mk [AttrEntry.mk "len" (AttrValue.int 10 MLIRType.index)])])
        [])
      (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])
Theorem: ExtractSliceGenericCommute1D.equiv
Proof state before:
r✝ : Region linalg
t : Tensor1D
r : Region linalg
rSpec : ℤ → FinInt 32 → FinInt 32
valid_r : validGenericRegion r rSpec
⊢ run
      (denoteRegion linalg
        (Region.mk "entry" []
          [Op.mk "linalg.generic1d" [(SSAVal.SSAVal "x", MLIRType.tensor1d)] [(SSAVal.SSAVal "t", MLIRType.tensor1d)]
              [r] (AttrDict.mk [AttrEntry.mk "len" (AttrValue.int 10 MLIRType.index)]),
            Op.mk "linalg.fill1d" [(SSAVal.SSAVal "out", MLIRType.tensor1d)] [(SSAVal.SSAVal "x", MLIRType.tensor1d)] []
              (AttrDict.mk [AttrEntry.mk "cst" (AttrValue.int 42 MLIRType.index)])])
        [])
      (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })]) =
    run
      (denoteRegion linalg
        (Region.mk "entry" []
          [Op.mk "linalg.generic1d" [(SSAVal.SSAVal "x", MLIRType.tensor1d)] [(SSAVal.SSAVal "t", MLIRType.tensor1d)]
              [r] (AttrDict.mk [AttrEntry.mk "cst" (AttrValue.int 42 MLIRType.index)]),
            Op.mk "linalg.extractslice1d" [(SSAVal.SSAVal "out", MLIRType.tensor1d)]
              [(SSAVal.SSAVal "x", MLIRType.tensor1d)] []
              (AttrDict.mk [AttrEntry.mk "len" (AttrValue.int 10 MLIRType.index)])])
        [])
      (SSAEnv.One [(SSAVal.SSAVal "t", { fst := MLIRType.tensor1d, snd := t })])
Tactic:
sorry
Proof state after:
no goals
Theorem: mapMCommute.mapM_cons
Proof state before:
m : Type u_1 → Type u_2
a : Type u_3
b : Type u_1
M : Monad m
LM : LawfulMonad m
x : a
xs : List a
f : a → m b
⊢ mapM f (x :: xs) = do
    let b_1 ← f x
    let bs ← mapM f xs
    pure (b_1 :: bs)
Tactic:
simp[List.mapM, List.mapM.loop]
Proof state after:
m : Type u_1 → Type u_2
a : Type u_3
b : Type u_1
M : Monad m
LM : LawfulMonad m
x : a
xs : List a
f : a → m b
⊢ (do
      let __do_lift ← f x
      List.mapM.loop f xs [__do_lift]) =
    do
    let b_1 ← f x
    let bs ← List.mapM.loop f xs []
    pure (b_1 :: bs)
Theorem: mapMCommute.mapM_cons
Proof state before:
m : Type u_1 → Type u_2
a : Type u_3
b : Type u_1
M : Monad m
LM : LawfulMonad m
x : a
xs : List a
f : a → m b
⊢ (do
      let __do_lift ← f x
      List.mapM.loop f xs [__do_lift]) =
    do
    let b_1 ← f x
    let bs ← List.mapM.loop f xs []
    pure (b_1 :: bs)
Tactic:
sorry
Proof state after:
no goals
Theorem: mapMCommute.commute_implies_mapM_commute
Proof state before:
m : Type → Type u_1
a b : Type
xs : List a
y : a
inst✝¹ : Monad m
inst✝ : LawfulMonad m
f g : a → m a
k : List a → a → m b
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
⊢ (do
      let r1 ← mapM f xs
      let r2 ← g y
      k r1 r2) =
    do
    let r2 ← g y
    let r1 ← mapM f xs
    k r1 r2
Tactic:
sorry
Proof state after:
no goals
Theorem: mapMCommute.mapM_commute
Proof state before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
⊢ fish (mapM f) (mapM g) = mapM (fish f g)
Tactic:
funext x
Proof state after:
case h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
x : List a
⊢ fish (mapM f) (mapM g) x = mapM (fish f g) x
Theorem: mapMCommute.mapM_commute
Proof state before:
case h
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
x : List a
⊢ fish (mapM f) (mapM g) x = mapM (fish f g) x
Tactic:
induction x
Proof state after:
case h.nil
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
⊢ fish (mapM f) (mapM g) [] = mapM (fish f g) []

case h.cons
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head✝ : a
tail✝ : List a
tail_ih✝ : fish (mapM f) (mapM g) tail✝ = mapM (fish f g) tail✝
⊢ fish (mapM f) (mapM g) (head✝ :: tail✝) = mapM (fish f g) (head✝ :: tail✝)
Theorem: mapMCommute.mapM_commute
Proof state before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
⊢ fish (mapM f) (mapM g) [] = mapM (fish f g) []
Tactic:
case nil => {
     simp[fish, List.mapM, List.mapM.loop];
}
Proof state after:
no goals
Theorem: mapMCommute.mapM_commute
Proof state before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ fish (mapM f) (mapM g) (head :: tail) = mapM (fish f g) (head :: tail)
Tactic:
case cons head tail IH => {
  rewrite [mapM_cons];
  simp[fish];
  simp [bind_assoc]
  simp[mapM_cons];
  congr; funext x';
  rewrite [commute_implies_mapM_commute];
  congr;
  funext x';
  simp [fish] at IH;
  rewrite [<- IH];
  simp[bind_assoc];
  apply COMMUTE;
}
Proof state after:
no goals
Theorem: mapMCommute.mapM_commute
Proof state before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
⊢ fish (mapM f) (mapM g) [] = mapM (fish f g) []
Tactic:
simp[fish, List.mapM, List.mapM.loop]
Proof state after:
no goals
Theorem: mapMCommute.mapM_commute
Proof state before:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ fish (mapM f) (mapM g) (head :: tail) = mapM (fish f g) (head :: tail)
Tactic:
rewrite [mapM_cons]
Proof state after:
m : Type → Type u_1
a : Type
M : Monad m
LM : LawfulMonad m
f g : a → m a
COMMUTE :
  ∀ {b : Type} (x y : a) (k : a → a → m b),
    (do
        let r1 ← f x
        let r2 ← g y
        k r1 r2) =
      do
      let r2 ← g y
      let r1 ← f x
      k r1 r2
head : a
tail : List a
IH : fish (mapM f) (mapM g) tail = mapM (fish f g) tail
⊢ fish (mapM f) (mapM g) (head :: tail) = do
    let b ← fish f g head
    let bs ← mapM (fish f g) tail
    pure (b :: bs)