Theorem: DimList.dim_known_refines_inv (MLIR/Semantics/TensorElem.lean)

State before:
D : DimList
S : List ℕ
⊢ known D = true → shapeRefines S D = true → D = List.map Dimension.Known S
Tactic:
intros Hknown
State after:
D : DimList
S : List ℕ
Hknown : known D = true
⊢ shapeRefines S D = true → D = List.map Dimension.Known S

State before:
D : DimList
S : List ℕ
Hknown : known D = true
⊢ shapeRefines S D = true → D = List.map Dimension.Known S
Tactic:
revert S
State after:
D : DimList
Hknown : known D = true
⊢ ∀ {S : List ℕ}, shapeRefines S D = true → D = List.map Dimension.Known S

State before:
D : DimList
Hknown : known D = true
⊢ ∀ {S : List ℕ}, shapeRefines S D = true → D = List.map Dimension.Known S
Tactic:
induction D <;> intros S Hrefines
State after:
case nil
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ [] = List.map Dimension.Known S

case cons
head✝ : Dimension
tail✝ : List Dimension
tail_ih✝ : known tail✝ = true → ∀ {S : List ℕ}, shapeRefines S tail✝ = true → tail✝ = List.map Dimension.Known S
Hknown : known (head✝ :: tail✝) = true
S : List ℕ
Hrefines : shapeRefines S (head✝ :: tail✝) = true
⊢ head✝ :: tail✝ = List.map Dimension.Known S

State before:
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ [] = List.map Dimension.Known S
Tactic:
case nil =>
  cases S; simp [List.map]; simp at Hrefines
State after:
no goals

State before:
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
S : List ℕ
Hrefines : shapeRefines S (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known S
Tactic:
case cons head tail ih =>
  cases S; simp at Hrefines
  simp [List.map]; cases head <;> simp at *
  rw [Hrefines.1, ←ih Hknown]; apply Hrefines.2
State after:
no goals

State before:
Hknown : known [] = true
S : List ℕ
Hrefines : shapeRefines S [] = true
⊢ [] = List.map Dimension.Known S
Tactic:
cases S
State after:
case nil
Hknown : known [] = true
Hrefines : shapeRefines [] [] = true
⊢ [] = List.map Dimension.Known []

case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ [] = List.map Dimension.Known (head✝ :: tail✝)

State before:
case nil
Hknown : known [] = true
Hrefines : shapeRefines [] [] = true
⊢ [] = List.map Dimension.Known []

case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ [] = List.map Dimension.Known (head✝ :: tail✝)
Tactic:
simp [List.map]
State after:
case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ [] = List.map Dimension.Known (head✝ :: tail✝)

State before:
case cons
Hknown : known [] = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) [] = true
⊢ [] = List.map Dimension.Known (head✝ :: tail✝)
Tactic:
simp at Hrefines
State after:
no goals

State before:
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
S : List ℕ
Hrefines : shapeRefines S (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known S
Tactic:
cases S
State after:
case nil
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
Hrefines : shapeRefines [] (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known []

case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known (head✝ :: tail✝)

State before:
case nil
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
Hrefines : shapeRefines [] (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known []

case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known (head✝ :: tail✝)
Tactic:
simp at Hrefines
State after:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known (head✝ :: tail✝)

State before:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = List.map Dimension.Known (head✝ :: tail✝)
Tactic:
simp [List.map]
State after:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = Dimension.Known head✝ :: List.map Dimension.Known tail✝

State before:
case cons
head : Dimension
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
Hknown : known (head :: tail) = true
head✝ : ℕ
tail✝ : List ℕ
Hrefines : shapeRefines (head✝ :: tail✝) (head :: tail) = true
⊢ head :: tail = Dimension.Known head✝ :: List.map Dimension.Known tail✝
Tactic:
cases head <;> simp at *
State after:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ Dimension.Known a✝ :: tail = Dimension.Known head✝ :: List.map Dimension.Known tail✝

State before:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ Dimension.Known a✝ :: tail = Dimension.Known head✝ :: List.map Dimension.Known tail✝
Tactic:
rw [Hrefines.1, ←ih Hknown]
State after:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ shapeRefines tail✝ tail = true

State before:
case cons.Known
tail : List Dimension
ih : known tail = true → ∀ {S : List ℕ}, shapeRefines S tail = true → tail = List.map Dimension.Known S
head✝ : ℕ
tail✝ : List ℕ
a✝ : ℕ
Hknown : known tail = true
Hrefines : head✝ = a✝ ∧ shapeRefines tail✝ tail = true
⊢ shapeRefines tail✝ tail = true
Tactic:
apply Hrefines.2
State after:
no goals