internlm/Lean-Github huggingface dataset:
Theorem: SSAScope.equiv_trans
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ : SSAScope δ
H1 : equiv scope₁ scope₂
scope₃ : SSAScope δ
H2 : equiv scope₂ scope₃
name : SSAVal
τ : MLIRType δ
⊢ get name scope₁ τ = get name scope₃ τ
Tactic:
specialize H1 name τ
Proof state after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ scope₃ : SSAScope δ
H2 : equiv scope₂ scope₃
name : SSAVal
τ : MLIRType δ
H1 : get name scope₁ τ = get name scope₂ τ
⊢ get name scope₁ τ = get name scope₃ τ
Theorem: SSAScope.equiv_trans
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ scope₃ : SSAScope δ
H2 : equiv scope₂ scope₃
name : SSAVal
τ : MLIRType δ
H1 : get name scope₁ τ = get name scope₂ τ
⊢ get name scope₁ τ = get name scope₃ τ
Tactic:
specialize H2 name τ
Proof state after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ scope₃ : SSAScope δ
name : SSAVal
τ : MLIRType δ
H1 : get name scope₁ τ = get name scope₂ τ
H2 : get name scope₂ τ = get name scope₃ τ
⊢ get name scope₁ τ = get name scope₃ τ
Theorem: SSAScope.equiv_trans
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
scope₁ scope₂ scope₃ : SSAScope δ
name : SSAVal
τ : MLIRType δ
H1 : get name scope₁ τ = get name scope₂ τ
H2 : get name scope₂ τ = get name scope₃ τ
⊢ get name scope₁ τ = get name scope₃ τ
Tactic:
simp [H1, H2]
Proof state after:
no goals
Theorem: SSAScope.get_to_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ τ' : MLIRType δ
v' : MLIRType.eval τ'
H : τ' = τ
⊢ MLIRType.eval τ' = MLIRType.eval τ
Tactic:
simp [H]
Proof state after:
no goals
Theorem: SSAScope.get_to_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
⊢ get name [] τ =
    match getT name [] with
    | none => none
    | some { fst := τ', snd := v' } =>
      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)
            v')
      else none
Tactic:
case nil => simp
Proof state after:
no goals
Theorem: SSAScope.get_to_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd :
  get name tail τ =
    match getT name tail with
    | none => none
    | some { fst := τ', snd := v' } =>
      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)
            v')
      else none
⊢ get name (head :: tail) τ =
    match getT name (head :: tail) with
    | none => none
    | some { fst := τ', snd := v' } =>
      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)
            v')
      else none
Tactic:
case cons head tail HInd =>
unfold getT get
byCases Hname: head.fst = name
case h2 =>
  rw [HInd]
Proof state after:
no goals
Theorem: SSAScope.get_to_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
⊢ get name [] τ =
    match getT name [] with
    | none => none
    | some { fst := τ', snd := v' } =>
      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)
            v')
      else none
Tactic:
simp
Proof state after:
no goals
Theorem: SSAScope.get_to_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd :
  get name tail τ =
    match getT name tail with
    | none => none
    | some { fst := τ', snd := v' } =>
      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)
            v')
      else none
Hname : ¬head.fst = name
⊢ get name tail τ =
    match getT name tail with
    | none => none
    | some { fst := τ', snd := v' } =>
      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)
            v')
      else none
Tactic:
case h2 =>
  rw [HInd]
Proof state after:
no goals
Theorem: SSAScope.get_to_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
τ : MLIRType δ
head : SSAVal × (τ : MLIRType δ) × MLIRType.eval τ
tail : List (SSAVal × (τ : MLIRType δ) × MLIRType.eval τ)
HInd :
  get name tail τ =
    match getT name tail with
    | none => none
    | some { fst := τ', snd := v' } =>
      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)
            v')
      else none
Hname : ¬head.fst = name
⊢ get name tail τ =
    match getT name tail with
    | none => none
    | some { fst := τ', snd := v' } =>
      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)
            v')
      else none
Tactic:
rw [HInd]
Proof state after:
no goals
Theorem: SSAScope.get_some_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
⊢ get name scope τ = some v → getT name scope = some { fst := τ, snd := v }
Tactic:
rw [get_to_getT]
Proof state after:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
⊢ (match getT name scope with
      | none => none
      | some { fst := τ', snd := v' } =>
        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)
              v')
        else none) =
      some v →
    getT name scope = some { fst := τ, snd := v }
Theorem: SSAScope.get_some_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
⊢ (match getT name scope with
      | none => none
      | some { fst := τ', snd := v' } =>
        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)
              v')
        else none) =
      some v →
    getT name scope = some { fst := τ, snd := v }
Tactic:
split <;> simp at * <;> try contradiction
Proof state after:
case h_2
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
x✝ : Option ((τ : MLIRType δ) × MLIRType.eval τ)
τ'✝ : MLIRType δ
v'✝ : MLIRType.eval τ'✝
heq✝ : getT name scope = some { fst := τ'✝, snd := v'✝ }
⊢ (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)
            v'✝)
      else none) =
      some v →
    getT name scope = some { fst := τ, snd := v }
Theorem: SSAScope.get_some_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
x✝ : Option ((τ : MLIRType δ) × MLIRType.eval τ)
τ' : MLIRType δ
v'✝ : MLIRType.eval τ'
Hget : getT name scope = some { fst := τ', snd := v'✝ }
⊢ (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)
            v'✝)
      else none) =
      some v →
    getT name scope = some { fst := τ, snd := v }
Tactic:
case h_2 _ τ' _ Hget =>
byCases Hτ: τ' = τ
intros H
rw [←H, Hget]
rfl
Proof state after:
no goals
Theorem: SSAScope.get_some_getT
Proof state before:
α σ : Type
ε : σ → Type
δ : Dialect α σ ε
name : SSAVal
scope : SSAScope δ
τ : MLIRType δ
v : MLIRType.eval τ
x✝ : Option ((τ : MLIRType δ) × MLIRType.eval τ)
τ' : MLIRType δ
v'✝ : MLIRType.eval τ'
Hget : getT name scope = some { fst := τ', snd := v'✝ }
⊢ (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)
            v'✝)
      else none) =
      some v →
    getT name scope = some { fst := τ, snd := v }
Tactic:
byCases Hτ: τ' = τ
Proof state after:
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'✝ }
⊢ 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 →
    getT name scope = some { fst := τ, snd := v }
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'✝ }
⊢ 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 →
    getT name scope = some { fst := τ, snd := v }
Tactic:
intros H
Proof state after:
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
⊢ getT name scope = some { fst := τ, snd := v }