internlm/Lean-Github huggingface dataset:
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length (flatten (nested l) Htype) = shapeProd (s_head :: s_tail)
Tactic:
simp [TensorElem.flatten_list, shapeProd, List.foldr]
Proof state after:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length (List.join (mapWithType l flatten Htype)) = s_head * List.foldr (fun x x_1 => x * x_1) 1 s_tail
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length (List.join (mapWithType l flatten Htype)) = s_head * List.foldr (fun x x_1 => x * x_1) 1 s_tail
Tactic:
simp [motive_2 s_tail Hshape.2 (hasType_list_1 Htype)]
Proof state after:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length l * shapeProd s_tail = s_head * List.foldr (fun x x_1 => x * x_1) 1 s_tail
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
l : List TensorElem
motive_2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ l → hasShape x s = true) →
      ∀ (h : (List.all l fun x => hasType x τ) = true),
        List.length (List.join (mapWithType l flatten (_ : hasType (nested l) τ = true))) = List.length l * shapeProd s
Htype : hasType (nested l) τ = true
s_head : ℕ
s_tail : List ℕ
Hshape : List.length l = s_head ∧ ∀ (x : TensorElem), x ∈ l → hasShape x s_tail = true
⊢ List.length l * shapeProd s_tail = s_head * List.foldr (fun x x_1 => x * x_1) 1 s_tail
Tactic:
simp [shapeProd, Nat.mul_comm, Hshape.1]
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ ∀ (s : List ℕ), hasShape empty s = true → ∀ (h : hasType empty τ = true), List.length (flatten empty h) = shapeProd s
Tactic:
intros s Hshape Htype
Proof state after:
τ : MLIRTy
s : List ℕ
Hshape : hasShape empty s = true
Htype : hasType empty τ = true
⊢ List.length (flatten empty Htype) = shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
s : List ℕ
Hshape : hasShape empty s = true
Htype : hasType empty τ = true
⊢ List.length (flatten empty Htype) = shapeProd s
Tactic:
simp [hasType] at Htype
Proof state after:
no goals
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
⊢ ∀ (head : TensorElem) (tail : List TensorElem),
    (∀ (s : List ℕ),
        hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s) →
      (∀ (s : List ℕ),
          (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
            ∀ (h : (List.all tail fun x => hasType x τ) = true),
              List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
                List.length tail * shapeProd s) →
        ∀ (s : List ℕ),
          hasShape head s = true →
            (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
              ∀ (h : (List.all (head :: tail) fun x => hasType x τ) = true),
                List.length (flatten head (_ : hasType head τ = true)) +
                    List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
                  Nat.succ (List.length tail) * shapeProd s
Tactic:
intros head tail motive_1 IH2 s Hshape1 Hshape2 Htype1
Proof state after:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
      ∀ (h : (List.all tail fun x => hasType x τ) = true),
        List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
          List.length tail * shapeProd s
s : List ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (flatten head (_ : hasType head τ = true)) +
      List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
    Nat.succ (List.length tail) * shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
      ∀ (h : (List.all tail fun x => hasType x τ) = true),
        List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
          List.length tail * shapeProd s
s : List ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (flatten head (_ : hasType head τ = true)) +
      List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
    Nat.succ (List.length tail) * shapeProd s
Tactic:
rw [Nat.add_comm]
Proof state after:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
      ∀ (h : (List.all tail fun x => hasType x τ) = true),
        List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
          List.length tail * shapeProd s
s : List ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    Nat.succ (List.length tail) * shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
      ∀ (h : (List.all tail fun x => hasType x τ) = true),
        List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
          List.length tail * shapeProd s
s : List ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    Nat.succ (List.length tail) * shapeProd s
Tactic:
simp [Nat.succ_eq_add_one, Nat.right_distrib]
Proof state after:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
      ∀ (h : (List.all tail fun x => hasType x τ) = true),
        List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
          List.length tail * shapeProd s
s : List ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    List.length tail * shapeProd s + shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
      ∀ (h : (List.all tail fun x => hasType x τ) = true),
        List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
          List.length tail * shapeProd s
s : List ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1 : (List.all (head :: tail) fun x => hasType x τ) = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    List.length tail * shapeProd s + shapeProd s
Tactic:
simp [List.all_cons] at Htype1
Proof state after:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
      ∀ (h : (List.all tail fun x => hasType x τ) = true),
        List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
          List.length tail * shapeProd s
s : List ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1✝ : (List.all (head :: tail) fun x => hasType x τ) = true
Htype1 : hasType head τ = true ∧ ∀ (x : TensorElem), x ∈ tail → hasType x τ = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    List.length tail * shapeProd s + shapeProd s
Theorem: MLIR.AST.TensorElem.flatten_size
Proof state before:
τ : MLIRTy
head : TensorElem
tail : List TensorElem
motive_1 :
  ∀ (s : List ℕ), hasShape head s = true → ∀ (h : hasType head τ = true), List.length (flatten head h) = shapeProd s
IH2 :
  ∀ (s : List ℕ),
    (∀ (x : TensorElem), x ∈ tail → hasShape x s = true) →
      ∀ (h : (List.all tail fun x => hasType x τ) = true),
        List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) =
          List.length tail * shapeProd s
s : List ℕ
Hshape1 : hasShape head s = true
Hshape2 : ∀ (x : TensorElem), x ∈ tail → hasShape x s = true
Htype1✝ : (List.all (head :: tail) fun x => hasType x τ) = true
Htype1 : hasType head τ = true ∧ ∀ (x : TensorElem), x ∈ tail → hasType x τ = true
⊢ List.length (List.join (mapWithType tail flatten (_ : hasType (nested tail) τ = true))) +
      List.length (flatten head (_ : hasType head τ = true)) =
    List.length tail * shapeProd s + shapeProd s
Tactic:
sorry
Proof state after:
no goals
Theorem: th1.equivalent
Proof state before:
n m : FinInt 32
⊢ run ⟦ LHS ⟧
      (SSAEnv.One
        [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }),
          (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m })]) =
    run ⟦ RHS ⟧
      (SSAEnv.One
        [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }),
          (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m })])
Tactic:
simp [LHS, RHS,
      run, StateT.run,
      denoteOp, bind, List.mapM, StateT.bind, denoteOpArgs, List.mapM,
      List.mapM.loop, Except.bind, TopM.get, StateT.get, pure, Except.pure,
      StateT.pure, TopM.mapDenoteRegion, OpM.toTopM, TopM.set, StateT.set, MLIRType.eval,
      SSAEnv.get, SSAEnv.getT, cast]
Proof state after:
n m : FinInt 32
⊢ FinInt.add n m = FinInt.add m n ∧
    [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }), (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m }),
        (SSAVal.SSAVal "r", { fst := MLIRType.int Signedness.Signless 32, snd := FinInt.add n m })] =
      [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }), (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m }),
        (SSAVal.SSAVal "r", { fst := MLIRType.int Signedness.Signless 32, snd := FinInt.add m n })]
Theorem: th1.equivalent
Proof state before:
n m : FinInt 32
⊢ FinInt.add n m = FinInt.add m n ∧
    [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }), (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m }),
        (SSAVal.SSAVal "r", { fst := MLIRType.int Signedness.Signless 32, snd := FinInt.add n m })] =
      [(SSAVal.SSAVal "n", { fst := MLIRType.i32, snd := n }), (SSAVal.SSAVal "m", { fst := MLIRType.i32, snd := m }),
        (SSAVal.SSAVal "r", { fst := MLIRType.int Signedness.Signless 32, snd := FinInt.add m n })]
Tactic:
simp [FinInt.add_comm']
Proof state after:
no goals
Theorem: FinInt.sub_add_dist
Proof state before:
sz : ℕ
⊢ ∀ (C X C2 : FinInt sz), C - (X + C2) = C - C2 - X
Tactic:
intros C X C2
Proof state after:
sz : ℕ
C X C2 : FinInt sz
⊢ C - (X + C2) = C - C2 - X
Theorem: FinInt.sub_add_dist
Proof state before:
sz : ℕ
C X C2 : FinInt sz
⊢ C - (X + C2) = C - C2 - X
Tactic:
apply eq_of_toUint_cong2
Proof state after:
case a
sz : ℕ
C X C2 : FinInt sz
⊢ toUint (C - (X + C2)) ≡ toUint (C - C2 - X) [2^sz]
Theorem: FinInt.sub_add_dist
Proof state before:
case a
sz : ℕ
C X C2 : FinInt sz
⊢ toUint (C - (X + C2)) ≡ toUint (C - C2 - X) [2^sz]
Tactic:
simp [cong2, FinInt.sub_toUint, FinInt.add_toUint]
Proof state after:
case a
sz : ℕ
C X C2 : FinInt sz
⊢ mod2 (toUint C - (toUint X + toUint C2)) sz = mod2 (toUint C - toUint C2 - toUint X) sz
Theorem: FinInt.sub_add_dist
Proof state before:
case a
sz : ℕ
C X C2 : FinInt sz
⊢ mod2 (toUint C - (toUint X + toUint C2)) sz = mod2 (toUint C - toUint C2 - toUint X) sz
Tactic:
apply FinInt.mod2_fequal
Proof state after:
case a.a
sz : ℕ
C X C2 : FinInt sz
⊢ toUint C - (toUint X + toUint C2) = toUint C - toUint C2 - toUint X
Theorem: FinInt.sub_add_dist
Proof state before:
case a.a
sz : ℕ
C X C2 : FinInt sz
⊢ toUint C - (toUint X + toUint C2) = toUint C - toUint C2 - toUint X
Tactic:
simp [Int.sub_add_dist, Int.sub_assoc]
Proof state after:
no goals
Theorem: P₁_tautology8
Proof state before:
⊢ isTautologyUpTo2 8 P₁ = true
Tactic:
native_decide
Proof state after:
no goals
Theorem: P₂_tautology8
Proof state before:
⊢ isTautologyUpTo2 8 P₂ = true
Tactic:
native_decide
Proof state after:
no goals
Theorem: P₃_tautology8
Proof state before:
⊢ isTautologyUpTo2 8 P₃ = true
Tactic:
native_decide
Proof state after:
no goals
Theorem: SSAEnv.refines_set
Proof state before:
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
⊢ refines env1 env2 → refines (set name τ val env1) (set name τ val env2)
Tactic:
simp [refines, SSAEnv.refines]
Proof state after:
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
⊢ (∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
      getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }) →
    ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
      getT v (set name τ val env2) = some { fst := a, snd := b } →
        getT v (set name τ val env1) = some { fst := a, snd := b }
Theorem: SSAEnv.refines_set
Proof state before:
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
⊢ (∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
      getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }) →
    ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
      getT v (set name τ val env2) = some { fst := a, snd := b } →
        getT v (set name τ val env1) = some { fst := a, snd := b }
Tactic:
intros Href name' val' Hget
Proof state after:
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }
Theorem: SSAEnv.refines_set
Proof state before:
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }
Tactic:
by_cases H: name = name'
Proof state after:
case pos
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }

case neg
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }
Theorem: SSAEnv.refines_set
Proof state before:
case pos
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }

case neg
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }
Tactic:
. subst H;
  rw [SSAEnv.getT_set_eq] <;> try assumption
  rw [SSAEnv.getT_set_eq] <;> try assumption
  intros K; assumption;
Proof state after:
case neg
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }
Theorem: SSAEnv.refines_set
Proof state before:
case neg
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ getT name' (set name τ val env2) = some { fst := val', snd := Hget } →
    getT name' (set name τ val env1) = some { fst := val', snd := Hget }
Tactic:
. rw [SSAEnv.getT_set_ne] <;> try assumption
  rw [SSAEnv.getT_set_ne] <;> try assumption
  intros K;
  apply Href; assumption;
Proof state after:
no goals
Theorem: SSAEnv.refines_set
Proof state before:
case neg.a
α✝ σ✝ : Type
ε✝ : σ✝ → Type
δ✝ : Dialect α✝ σ✝ ε✝
env1 env2 : SSAEnv δ✝
name : SSAVal
τ : MLIRType δ✝
val : MLIRType.eval τ
Href :
  ∀ (v : SSAVal) (a : MLIRType δ✝) (b : MLIRType.eval a),
    getT v env2 = some { fst := a, snd := b } → getT v env1 = some { fst := a, snd := b }
name' : SSAVal
val' : MLIRType δ✝
Hget : MLIRType.eval val'
H : ¬name = name'
⊢ name ≠ name'
Tactic:
assumption
Proof state after:
no goals
Theorem: TopM.get_unfold
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ get τ name env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)
Tactic:
simp [TopM.get]
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some v => pure v
        | none => pure default)
      env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)
Theorem: TopM.get_unfold
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ bind StateT.get
      (fun s =>
        match SSAEnv.get name τ s with
        | some v => pure v
        | none => pure default)
      env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)
Tactic:
simp_monad
Proof state after:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ (match SSAEnv.get name τ env with
      | some v => fun s => Except.ok (v, s)
      | none => fun s => Except.ok (default, s))
      env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)
Theorem: TopM.get_unfold
Proof state before:
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
τ : MLIRType Δ
name : SSAVal
env : SSAEnv Δ
⊢ (match SSAEnv.get name τ env with
      | some v => fun s => Except.ok (v, s)
      | none => fun s => Except.ok (default, s))
      env =
    Except.ok
      (match SSAEnv.get name τ env with
        | some v => v
        | none => default,
        env)
Tactic:
cases (env.get name τ) <;> rfl
Proof state after:
no goals