internlm/Lean-Github huggingface dataset:
Theorem: Schema.get_map_nths_eq_get_get
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
i : Nat
hi : Nat.succ i < List.length (n :: ns)
ih :
  List.get (List.map Prod.fst (nths xs ns))
      { val := i, isLt := (_ : i < List.length (List.map Prod.fst (nths xs ns))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get ns { val := i, isLt := (_ : i < List.length ns) }).val,
        isLt :=
          (_ : (List.get ns { val := i, isLt := (_ : i < List.length ns) }).val < List.length (List.map Prod.fst xs)) }
⊢ List.get
      (List.map Prod.fst
        (nth xs n.val (_ : n.val < length xs) :: map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := Nat.succ i, isLt := (_ : Nat.succ i < List.length (List.map Prod.fst (nths xs (n :: ns)))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val,
        isLt := (_ : (List.get (n :: ns) { val := Nat.succ i, isLt := hi }).val < List.length (List.map Prod.fst xs)) }
Tactic:
simp only [List.get]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
i : Nat
hi : Nat.succ i < List.length (n :: ns)
ih :
  List.get (List.map Prod.fst (nths xs ns))
      { val := i, isLt := (_ : i < List.length (List.map Prod.fst (nths xs ns))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get ns { val := i, isLt := (_ : i < List.length ns) }).val,
        isLt :=
          (_ : (List.get ns { val := i, isLt := (_ : i < List.length ns) }).val < List.length (List.map Prod.fst xs)) }
⊢ List.get (List.map Prod.fst (map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := i,
        isLt :=
          (_ :
            Nat.succ i ≤ List.length (List.map Prod.fst (map (fun n => nth xs n.val (_ : n.val < length xs)) ns))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get ns { val := i, isLt := (_ : Nat.succ i ≤ List.length ns) }).val,
        isLt :=
          (_ :
            (List.get ns { val := i, isLt := (_ : Nat.succ i ≤ List.length ns) }).val <
              List.length (List.map Prod.fst xs)) }
Theorem: Schema.get_map_nths_eq_get_get
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
α : Type u_1
β : Type u_2
xs : List (α × β)
n : Fin (length xs)
ns : List (Fin (length xs))
i : Nat
hi : Nat.succ i < List.length (n :: ns)
ih :
  List.get (List.map Prod.fst (nths xs ns))
      { val := i, isLt := (_ : i < List.length (List.map Prod.fst (nths xs ns))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get ns { val := i, isLt := (_ : i < List.length ns) }).val,
        isLt :=
          (_ : (List.get ns { val := i, isLt := (_ : i < List.length ns) }).val < List.length (List.map Prod.fst xs)) }
⊢ List.get (List.map Prod.fst (map (fun n => nth xs n.val (_ : n.val < length xs)) ns))
      { val := i,
        isLt :=
          (_ :
            Nat.succ i ≤ List.length (List.map Prod.fst (map (fun n => nth xs n.val (_ : n.val < length xs)) ns))) } =
    List.get (List.map Prod.fst xs)
      { val := (List.get ns { val := i, isLt := (_ : Nat.succ i ≤ List.length ns) }).val,
        isLt :=
          (_ :
            (List.get ns { val := i, isLt := (_ : Nat.succ i ≤ List.length ns) }).val <
              List.length (List.map Prod.fst xs)) }
Tactic:
rw [←ih]
Proof state after:
no goals
Theorem: Schema.lookup_eq_lookup_append
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
⊢ ∀ (s t : Schema) (c : η) (h : HasName c s),
    lookup s { fst := c, snd := h } = lookup (append s t) { fst := c, snd := hasNameOfAppend h }
Tactic:
intros s t c h
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
h : HasName c s
⊢ lookup s { fst := c, snd := h } = lookup (append s t) { fst := c, snd := hasNameOfAppend h }
Theorem: Schema.lookup_eq_lookup_append
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
h : HasName c s
⊢ lookup s { fst := c, snd := h } = lookup (append s t) { fst := c, snd := hasNameOfAppend h }
Tactic:
induction h with
| hd =>
  simp only [Schema.hasNameOfAppend]
  rw [Schema.lookup_eq_1, Schema.lookup_eq_1]
| tl h' ih =>
  simp only [Schema.hasNameOfAppend]
  rw [Schema.lookup_eq_2, Schema.lookup_eq_2]
  exact ih
Proof state after:
no goals
Theorem: Schema.lookup_eq_lookup_append
Proof state before:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd } =
    lookup (append ((c✝, τ✝) :: rs✝) t) { fst := c✝, snd := hasNameOfAppend HasName.hd }
Tactic:
simp only [Schema.hasNameOfAppend]
Proof state after:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd } =
    lookup (append ((c✝, τ✝) :: rs✝) t) { fst := c✝, snd := HasName.hd }
Theorem: Schema.lookup_eq_lookup_append
Proof state before:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ lookup ((c✝, τ✝) :: rs✝) { fst := c✝, snd := HasName.hd } =
    lookup (append ((c✝, τ✝) :: rs✝) t) { fst := c✝, snd := HasName.hd }
Tactic:
rw [Schema.lookup_eq_1, Schema.lookup_eq_1]
Proof state after:
no goals
Theorem: Schema.lookup_eq_lookup_append
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h' } =
    lookup (append (r✝ :: rs✝) t) { fst := c✝, snd := hasNameOfAppend (HasName.tl h') }
Tactic:
simp only [Schema.hasNameOfAppend]
Proof state after:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h' } =
    lookup (append (r✝ :: rs✝) t) { fst := c✝, snd := HasName.tl (hasNameOfAppend h') }
Theorem: Schema.lookup_eq_lookup_append
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup (r✝ :: rs✝) { fst := c✝, snd := HasName.tl h' } =
    lookup (append (r✝ :: rs✝) t) { fst := c✝, snd := HasName.tl (hasNameOfAppend h') }
Tactic:
rw [Schema.lookup_eq_2, Schema.lookup_eq_2]
Proof state after:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
Theorem: Schema.lookup_eq_lookup_append
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
s t : Schema
c : η
r✝ : Header
c✝ : η
rs✝ : Schema
h' : HasName c✝ rs✝
ih : lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
⊢ lookup rs✝ { fst := c✝, snd := h' } = lookup (append rs✝ t) { fst := c✝, snd := hasNameOfAppend h' }
Tactic:
exact ih
Proof state after:
no goals
Theorem: Schema.mem_map_of_HasName
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
⊢ ∀ (sch : Schema) (nm : η), HasName nm sch → nm ∈ map Prod.fst sch
Tactic:
intro sch nm h
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
h : HasName nm sch
⊢ nm ∈ map Prod.fst sch
Theorem: Schema.mem_map_of_HasName
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
h : HasName nm sch
⊢ nm ∈ map Prod.fst sch
Tactic:
induction h with
| hd =>
  apply List.Mem.head
| tl _ ih =>
  apply List.Mem.tail
  apply ih
Proof state after:
no goals
Theorem: Schema.mem_map_of_HasName
Proof state before:
case hd
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm c✝ : η
rs✝ : Schema
τ✝ : Type u_1
⊢ c✝ ∈ map Prod.fst ((c✝, τ✝) :: rs✝)
Tactic:
apply List.Mem.head
Proof state after:
no goals
Theorem: Schema.mem_map_of_HasName
Proof state before:
case tl
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
a✝ : HasName c✝ rs✝
ih : c✝ ∈ map Prod.fst rs✝
⊢ c✝ ∈ map Prod.fst (r✝ :: rs✝)
Tactic:
apply List.Mem.tail
Proof state after:
case tl.a
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
a✝ : HasName c✝ rs✝
ih : c✝ ∈ map Prod.fst rs✝
⊢ List.Mem c✝ (map Prod.fst rs✝)
Theorem: Schema.mem_map_of_HasName
Proof state before:
case tl.a
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
r✝ : Header
c✝ : η
rs✝ : Schema
a✝ : HasName c✝ rs✝
ih : c✝ ∈ map Prod.fst rs✝
⊢ List.Mem c✝ (map Prod.fst rs✝)
Tactic:
apply ih
Proof state after:
no goals
Theorem: Schema.retypedFromSubschema_preserves_names
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
⊢ names (retypedFromSubschema ({ fst := (nm, τ), snd := pf } :: rs)) = names ((fst✝, snd✝) :: ss)
Tactic:
simp only [retypedFromSubschema]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
⊢ names (retypedFromSubschema (map (fun x => { fst := x.fst, snd := hasRetypedName x.snd }) rs)) =
    names ((fst✝, snd✝) :: ss)
Theorem: Schema.retypedFromSubschema_preserves_names
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
⊢ names (retypedFromSubschema (map (fun x => { fst := x.fst, snd := hasRetypedName x.snd }) rs)) =
    names ((fst✝, snd✝) :: ss)
Tactic:
have := retypedFromSubschema_preserves_names (Schema.retypeColumn _ pf τ)
  (Schema.map (fun ⟨h, pf⟩ => ⟨h, hasRetypedName pf⟩) rs)
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
this :
  names
      (retypedFromSubschema
        (map
          (fun x =>
            match x with
            | { fst := h, snd := pf_1 } => { fst := h, snd := hasRetypedName pf_1 })
          rs)) =
    names (retypeColumn ((fst✝, snd✝) :: ss) pf τ)
⊢ names (retypedFromSubschema (map (fun x => { fst := x.fst, snd := hasRetypedName x.snd }) rs)) =
    names ((fst✝, snd✝) :: ss)
Theorem: Schema.retypedFromSubschema_preserves_names
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
this :
  names
      (retypedFromSubschema
        (map
          (fun x =>
            match x with
            | { fst := h, snd := pf_1 } => { fst := h, snd := hasRetypedName pf_1 })
          rs)) =
    names (retypeColumn ((fst✝, snd✝) :: ss) pf τ)
⊢ names (retypedFromSubschema (map (fun x => { fst := x.fst, snd := hasRetypedName x.snd }) rs)) =
    names ((fst✝, snd✝) :: ss)
Tactic:
rw [this]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
this :
  names
      (retypedFromSubschema
        (map
          (fun x =>
            match x with
            | { fst := h, snd := pf_1 } => { fst := h, snd := hasRetypedName pf_1 })
          rs)) =
    names (retypeColumn ((fst✝, snd✝) :: ss) pf τ)
⊢ names (retypeColumn ((fst✝, snd✝) :: ss) pf τ) = names ((fst✝, snd✝) :: ss)
Theorem: Schema.retypedFromSubschema_preserves_names
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
fst✝ : η
snd✝ : Type u_1
ss : List Header
nm : η
τ : Type u_1
pf : HasName (nm, τ).fst ((fst✝, snd✝) :: ss)
rs : List ((h : Header) × HasName h.fst ((fst✝, snd✝) :: ss))
this :
  names
      (retypedFromSubschema
        (map
          (fun x =>
            match x with
            | { fst := h, snd := pf_1 } => { fst := h, snd := hasRetypedName pf_1 })
          rs)) =
    names (retypeColumn ((fst✝, snd✝) :: ss) pf τ)
⊢ names (retypeColumn ((fst✝, snd✝) :: ss) pf τ) = names ((fst✝, snd✝) :: ss)
Tactic:
simp only [retypeColumn_preserves_names]
Proof state after:
no goals
Theorem: Schema.hasNameOfFromCHeaders_eq_1
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
nm : η
τ : Type u_1
hpf : HasCol (nm, τ) sch
cs : List (CertifiedHeader sch)
⊢ hasNameOfFromCHeaders HasName.hd = colImpliesName hpf
Tactic:
cases sch with
| nil => contradiction
| cons s ss => simp [hasNameOfFromCHeaders]
Proof state after:
no goals
Theorem: Schema.hasNameOfFromCHeaders_eq_1
Proof state before:
case nil
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hpf : HasCol (nm, τ) []
cs : List (CertifiedHeader [])
⊢ hasNameOfFromCHeaders HasName.hd = colImpliesName hpf
Tactic:
contradiction
Proof state after:
no goals
Theorem: Schema.hasNameOfFromCHeaders_eq_1
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
s : Header
ss : List Header
hpf : HasCol (nm, τ) (s :: ss)
cs : List (CertifiedHeader (s :: ss))
⊢ hasNameOfFromCHeaders HasName.hd = colImpliesName hpf
Tactic:
simp [hasNameOfFromCHeaders]
Proof state after:
no goals
Theorem: Schema.hasNameOfFromCHeaders_eq_2
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
sch : Schema
hdr : Header
hpf : HasCol hdr sch
cs : List (CertifiedHeader sch)
nm : η
h : HasName nm (map Sigma.fst cs)
⊢ hasNameOfFromCHeaders (HasName.tl h) = hasNameOfFromCHeaders h
Tactic:
cases sch with
| nil => contradiction
| cons s ss => simp [hasNameOfFromCHeaders]
Proof state after:
no goals
Theorem: Schema.hasNameOfFromCHeaders_eq_2
Proof state before:
case nil
η : Type u_η
dec_η : DecidableEq η
schema : Schema
hdr : Header
nm : η
hpf : HasCol hdr []
cs : List (CertifiedHeader [])
h : HasName nm (map Sigma.fst cs)
⊢ hasNameOfFromCHeaders (HasName.tl h) = hasNameOfFromCHeaders h
Tactic:
contradiction
Proof state after:
no goals
Theorem: Schema.hasNameOfFromCHeaders_eq_2
Proof state before:
case cons
η : Type u_η
dec_η : DecidableEq η
schema : Schema
hdr : Header
nm : η
s : Header
ss : List Header
hpf : HasCol hdr (s :: ss)
cs : List (CertifiedHeader (s :: ss))
h : HasName nm (map Sigma.fst cs)
⊢ hasNameOfFromCHeaders (HasName.tl h) = hasNameOfFromCHeaders h
Tactic:
simp [hasNameOfFromCHeaders]
Proof state after:
no goals
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs)
      { fst := { fst := nm, snd := HasName.hd }.fst,
        snd := hasNameOfFromCHeaders { fst := nm, snd := HasName.hd }.snd } =
    lookupType (fromCHeaders ({ fst := (nm, τ), snd := HasCol.hd } :: cs)) { fst := nm, snd := HasName.hd }
Tactic:
simp only [lookupType]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := hasNameOfFromCHeaders HasName.hd } = τ
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := hasNameOfFromCHeaders HasName.hd } = τ
Tactic:
simp only [hasNameOfFromCHeaders_eq_1]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := colImpliesName HasCol.hd } = τ
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := colImpliesName HasCol.hd } = τ
Tactic:
rw [@colImpliesName_eq_1 η hs (nm, τ)]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := HasName.hd } = τ
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := nm, snd := HasName.hd } = τ
Tactic:
simp only [lookupType]
Proof state after:
no goals
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs)
      { fst := { fst := ch_nm, snd := HasName.hd }.fst,
        snd := hasNameOfFromCHeaders { fst := ch_nm, snd := HasName.hd }.snd } =
    lookupType (fromCHeaders ({ fst := (ch_nm, ch_τ), snd := HasCol.tl h } :: cs)) { fst := ch_nm, snd := HasName.hd }
Tactic:
simp only [lookupType]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := hasNameOfFromCHeaders HasName.hd } = ch_τ
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := hasNameOfFromCHeaders HasName.hd } = ch_τ
Tactic:
simp only [hasNameOfFromCHeaders_eq_1]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := colImpliesName (HasCol.tl h) } = ch_τ
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := colImpliesName (HasCol.tl h) } = ch_τ
Tactic:
rw [@colImpliesName_eq_2 η hs (nm, τ) (ch_nm, ch_τ) h]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := HasName.tl (colImpliesName h) } = ch_τ
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType ((nm, τ) :: hs) { fst := ch_nm, snd := HasName.tl (colImpliesName h) } = ch_τ
Tactic:
simp only [lookupType]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType hs { fst := ch_nm, snd := colImpliesName h } = ch_τ
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
ch_nm : η
ch_τ : Type u_1
h : HasCol (ch_nm, ch_τ) hs
cs : List (CertifiedHeader ((nm, τ) :: hs))
⊢ lookupType hs { fst := ch_nm, snd := colImpliesName h } = ch_τ
Tactic:
apply lookupType_of_colImpliesName
Proof state after:
no goals
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
fst✝ : Header
pf : HasCol fst✝ ((nm, τ) :: hs)
cs : List (CertifiedHeader ((nm, τ) :: hs))
s_nm : η
hn : HasName s_nm (map Sigma.fst cs)
⊢ lookupType ((nm, τ) :: hs)
      { fst := { fst := s_nm, snd := HasName.tl hn }.fst,
        snd := hasNameOfFromCHeaders { fst := s_nm, snd := HasName.tl hn }.snd } =
    lookupType (fromCHeaders ({ fst := fst✝, snd := pf } :: cs)) { fst := s_nm, snd := HasName.tl hn }
Tactic:
simp only [lookupType]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
fst✝ : Header
pf : HasCol fst✝ ((nm, τ) :: hs)
cs : List (CertifiedHeader ((nm, τ) :: hs))
s_nm : η
hn : HasName s_nm (map Sigma.fst cs)
⊢ lookupType ((nm, τ) :: hs) { fst := s_nm, snd := hasNameOfFromCHeaders (HasName.tl hn) } =
    lookupType (map Sigma.fst cs) { fst := s_nm, snd := hn }
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
fst✝ : Header
pf : HasCol fst✝ ((nm, τ) :: hs)
cs : List (CertifiedHeader ((nm, τ) :: hs))
s_nm : η
hn : HasName s_nm (map Sigma.fst cs)
⊢ lookupType ((nm, τ) :: hs) { fst := s_nm, snd := hasNameOfFromCHeaders (HasName.tl hn) } =
    lookupType (map Sigma.fst cs) { fst := s_nm, snd := hn }
Tactic:
simp only [hasNameOfFromCHeaders_eq_2]
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
fst✝ : Header
pf : HasCol fst✝ ((nm, τ) :: hs)
cs : List (CertifiedHeader ((nm, τ) :: hs))
s_nm : η
hn : HasName s_nm (map Sigma.fst cs)
⊢ lookupType ((nm, τ) :: hs) { fst := s_nm, snd := hasNameOfFromCHeaders hn } =
    lookupType (map Sigma.fst cs) { fst := s_nm, snd := hn }
Theorem: Schema.lookupTypeFromCHeadersUnique
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
nm : η
τ : Type u_1
hs : List Header
fst✝ : Header
pf : HasCol fst✝ ((nm, τ) :: hs)
cs : List (CertifiedHeader ((nm, τ) :: hs))
s_nm : η
hn : HasName s_nm (map Sigma.fst cs)
⊢ lookupType ((nm, τ) :: hs) { fst := s_nm, snd := hasNameOfFromCHeaders hn } =
    lookupType (map Sigma.fst cs) { fst := s_nm, snd := hn }
Tactic:
exact lookupTypeFromCHeadersUnique cs ⟨s_nm, hn⟩
Proof state after:
no goals
Theorem: Schema.hasNameEqHeadOrTail_inl
Proof state before:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
h : HasName nm ((nm, τ) :: hs)
⊢ hasNameEqHeadOrTail h ≡ Sum.inl (EqT.refl nm) → h = HasName.hd
Tactic:
intro eqt
Proof state after:
η : Type u_η
dec_η : DecidableEq η
schema : Schema
η✝ : Type u_1
nm : η✝
τ : Type u_2
hs : List Header
h : HasName nm ((nm, τ) :: hs)
eqt : hasNameEqHeadOrTail h ≡ Sum.inl (EqT.refl nm)
⊢ h = HasName.hd