internlm/Lean-Github huggingface dataset:
Theorem: SSAScope.get_some_getT
Proof state before:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
x✝ : Option ((τ : MLIRType δ) × MLIRType.eval τ)
v'✝ : MLIRType.eval τ
Hget : getT name scope = some { fst := τ, snd := v'✝ }
H :
  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)
      v'✝ =
    v
⊢ some { fst := τ, snd := v'✝ } =
    some
      { fst := τ,
        snd :=
          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)
            v'✝ }
Tactic:
rfl
Proof state after:
no goals
Theorem: SSAScope.getT_none_get
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
⊢ getT name scope = none → ∀ (τ : MLIRType δ), get name scope τ = none
Tactic:
induction scope <;> simp
Proof state after:
case cons
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head✝ : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail✝ : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT name tail✝ = none → ∀ (τ : MLIRType δ), get name tail✝ τ = none
⊢ (if head✝.fst = name then some head✝.2 else getT name tail✝) = none →
    ∀ (τ : MLIRType δ),
      (if head✝.fst = name then
          if h : head✝.2.fst = τ then
            some
              (cast
                (_ :
                  (match head✝.2.fst 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)
                head✝.2.snd)
          else none
        else get name tail✝ τ) =
        none
Theorem: SSAScope.getT_none_get
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : getT name tail = none → ∀ (τ : MLIRType δ), get name tail τ = none
⊢ (if head.fst = name then some head.2 else getT name tail) = none →
    ∀ (τ : MLIRType δ),
      (if head.fst = name then
          if h : head.2.fst = τ then
            some
              (cast
                (_ :
                  (match head.2.fst 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)
                head.2.snd)
          else none
        else get name tail τ) =
        none
Tactic:
case cons head tail HInd =>
byCases Hname: head.fst = name <;> assumption
Proof state after:
no goals
Theorem: SSAScope.getT_none_get
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : getT name tail = none → ∀ (τ : MLIRType δ), get name tail τ = none
⊢ (if head.fst = name then some head.2 else getT name tail) = none →
    ∀ (τ : MLIRType δ),
      (if head.fst = name then
          if h : head.2.fst = τ then
            some
              (cast
                (_ :
                  (match head.2.fst 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)
                head.2.snd)
          else none
        else get name tail τ) =
        none
Tactic:
byCases Hname: head.fst = name <;> assumption
Proof state after:
no goals
Theorem: SSAScope.getT_some_get
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
⊢ getT name scope = some { fst := τ, snd := v } → get name scope τ = some v
Tactic:
induction scope <;> simp
Proof state after:
case cons
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
head✝ : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail✝ : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
tail_ih✝ : getT name tail✝ = some { fst := τ, snd := v } → get name tail✝ τ = some v
⊢ (if head✝.fst = name then some head✝.2 else getT name tail✝) = some { fst := τ, snd := v } →
    (if head✝.fst = name then
        if h : head✝.2.fst = τ then
          some
            (cast
              (_ :
                (match head✝.2.fst 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)
              head✝.2.snd)
        else none
      else get name tail✝ τ) =
      some v
Theorem: SSAScope.getT_some_get
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : getT name tail = some { fst := τ, snd := v } → get name tail τ = some v
⊢ (if head.fst = name then some head.2 else getT name tail) = some { fst := τ, snd := v } →
    (if head.fst = name then
        if h : head.2.fst = τ then
          some
            (cast
              (_ :
                (match head.2.fst 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)
              head.2.snd)
        else none
      else get name tail τ) =
      some v
Tactic:
case cons head tail HInd =>
byCases Hname: head.fst = name <;> try assumption
have ⟨headName, headτ, headVal⟩ := head; simp at *
intros H; cases H
simp;
Proof state after:
no goals
Theorem: SSAScope.getT_some_get
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : getT name tail = some { fst := τ, snd := v } → get name tail τ = some v
⊢ (if head.fst = name then some head.2 else getT name tail) = some { fst := τ, snd := v } →
    (if head.fst = name then
        if h : head.2.fst = τ then
          some
            (cast
              (_ :
                (match head.2.fst 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)
              head.2.snd)
        else none
      else get name tail τ) =
      some v
Tactic:
byCases Hname: head.fst = name <;> try assumption
Proof state after:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : getT head.fst tail = some { fst := τ, snd := v } → get head.fst tail τ = some v
⊢ head.2 = { fst := τ, snd := v } →
    (if h : head.2.fst = τ then
        some
          (cast
            (_ :
              (match head.2.fst 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)
            head.2.snd)
      else none) =
      some v
Theorem: SSAScope.getT_some_get
Proof state before:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd : getT head.fst tail = some { fst := τ, snd := v } → get head.fst tail τ = some v
⊢ head.2 = { fst := τ, snd := v } →
    (if h : head.2.fst = τ then
        some
          (cast
            (_ :
              (match head.2.fst 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)
            head.2.snd)
      else none) =
      some v
Tactic:
have ⟨headName, headτ, headVal⟩ := head
Proof state after:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
headName : SSAVal
headτ : MLIRType δ
headVal : MLIRType.eval headτ
HInd :
  getT (headName, { fst := headτ, snd := headVal }).fst tail = some { fst := τ, snd := v } →
    get (headName, { fst := headτ, snd := headVal }).fst tail τ = some v
⊢ (headName, { fst := headτ, snd := headVal }).2 = { fst := τ, snd := v } →
    (if h : (headName, { fst := headτ, snd := headVal }).2.fst = τ then
        some
          (cast
            (_ :
              (match (headName, { fst := headτ, snd := headVal }).2.fst 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)
            (headName, { fst := headτ, snd := headVal }).2.snd)
      else none) =
      some v
Theorem: SSAScope.getT_some_get
Proof state before:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
headName : SSAVal
headτ : MLIRType δ
headVal : MLIRType.eval headτ
HInd : getT headName tail = some { fst := τ, snd := v } → get headName tail τ = some v
⊢ headτ = τ →
    HEq headVal v →
      (if h : headτ = τ then
          some
            (cast
              (_ :
                (match (headName, { fst := headτ, snd := headVal }).2.fst 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)
              headVal)
        else none) =
        some v
Tactic:
intros H
Proof state after:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
headName : SSAVal
headτ : MLIRType δ
headVal : MLIRType.eval headτ
HInd : getT headName tail = some { fst := τ, snd := v } → get headName tail τ = some v
H : headτ = τ
⊢ HEq headVal v →
    (if h : headτ = τ then
        some
          (cast
            (_ :
              (match (headName, { fst := headτ, snd := headVal }).2.fst 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)
            headVal)
      else none) =
      some v
Theorem: SSAScope.getT_some_get
Proof state before:
case h1
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
headName : SSAVal
headτ : MLIRType δ
headVal : MLIRType.eval headτ
HInd : getT headName tail = some { fst := τ, snd := v } → get headName tail τ = some v
H : headτ = τ
⊢ HEq headVal v →
    (if h : headτ = τ then
        some
          (cast
            (_ :
              (match (headName, { fst := headτ, snd := headVal }).2.fst 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)
            headVal)
      else none) =
      some v
Tactic:
cases H
Proof state after:
case h1.refl
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
τ : MLIRType δ
v : MLIRType.eval τ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
headName : SSAVal
HInd : getT headName tail = some { fst := τ, snd := v } → get headName tail τ = some v
headVal : MLIRType.eval τ
⊢ HEq headVal v →
    (if h : τ = τ then
        some
          (cast
            (_ :
              (match (headName, { fst := τ, snd := headVal }).2.fst 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)
            headVal)
      else none) =
      some v