Theorem: mapDenoteRegion_equiv (MLIR/Semantics/Semantics.lean)

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
⊢ denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ regions)
Tactic:
match REGIONS: regions with
| .nil =>
  intros region HregIn args env res env' H env₂ Henv₂
  contradiction
| .cons head tail =>
  intros region HregIn args env res env' H env₂ Henv₂
  simp [TopM.mapDenoteRegion] at HregIn
  cases HregIn
  case inl HXX =>
    subst HXX;
    sorry
    case inr HXX =>
    apply mapDenoteRegion_equiv <;> assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
REGIONS : regions = []
⊢ denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ [])
Tactic:
intros region HregIn args env res env' H env₂ Henv₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
REGIONS : regions = []
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
HregIn : region ∈ TopM.mapDenoteRegion Δ []
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
REGIONS : regions = []
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
HregIn : region ∈ TopM.mapDenoteRegion Δ []
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
contradiction
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
⊢ denoteRegionsEquivInvariant (TopM.mapDenoteRegion Δ (head :: tail))
Tactic:
intros region HregIn args env res env' H env₂ Henv₂
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
HregIn : region ∈ TopM.mapDenoteRegion Δ (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
HregIn : region ∈ TopM.mapDenoteRegion Δ (head :: tail)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
simp [TopM.mapDenoteRegion] at HregIn
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HregIn : region = TopM.scoped ∘ denoteRegion Δ head ∨ region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HregIn : region = TopM.scoped ∘ denoteRegion Δ head ∨ region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
cases HregIn
State after:
case inl
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
h✝ : region = TopM.scoped ∘ denoteRegion Δ head
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')

case inr
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
h✝ : region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HXX : region = TopM.scoped ∘ denoteRegion Δ head
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
case inl HXX =>
  subst HXX;
  sorry
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HXX : region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
case inr HXX =>
  apply mapDenoteRegion_equiv <;> assumption
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HXX : region = TopM.scoped ∘ denoteRegion Δ head
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
subst HXX
State after:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : Function.comp TopM.scoped (denoteRegion Δ head) args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ Function.comp TopM.scoped (denoteRegion Δ head) args env₂ = Except.ok (res, env₂')

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
H : Function.comp TopM.scoped (denoteRegion Δ head) args env = Except.ok (res, env')
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ Function.comp TopM.scoped (denoteRegion Δ head) args env₂ = Except.ok (res, env₂')
Tactic:
sorry
State after:
no goals

State before:
α₁ σ₁ : Type
ε₁ : σ₁ → Type
δ₁ : Dialect α₁ σ₁ ε₁
α₂ σ₂ : Type
ε₂ : σ₂ → Type
δ₂ : Dialect α₂ σ₂ ε₂
α σ : Type
ε : σ → Type
Δ : Dialect α σ ε
S : Semantics Δ
regions : List (Region Δ)
head : Region Δ
tail : List (Region Δ)
REGIONS : regions = head :: tail
region : TypedArgs Δ → TopM Δ (TypedArgs Δ)
args : TypedArgs Δ
env : SSAEnv Δ
res : TypedArgs Δ
env' : SSAEnv Δ
H : region args env = Except.ok (res, env')
env₂ : SSAEnv Δ
Henv₂ : SSAEnv.equiv env env₂
HXX : region ∈ TopM.mapDenoteRegion Δ tail
⊢ ∃ env₂', SSAEnv.equiv env' env₂' ∧ region args env₂ = Except.ok (res, env₂')
Tactic:
apply mapDenoteRegion_equiv <;> assumption
State after:
no goals