Equality of vectors is injective

Stream: new members

[Cody Roux]

For various (perhaps bad) reasons, I have, in my context

fun i => Matrix.vecCons a ! [b] i = fun i =>Matrix.vecCons a' ![b'] i

(i is of type Fin 2) and I would like to deduce

a = a'

Is this true? I think it is. Is there an easy way to prove it?

[Eric Wieser]

Can you make a #mwe? (with imports etc)

[Cody Roux]

import Mathlib.ModelTheory.Satisfiability
import Mathlib.Data.Fintype.Card

open FirstOrder
open FirstOrder.Language
open FirstOrder.Language.Theory

section NonStandard

-- The naturals extended with a non-standard element
inductive NS :=
| standard : ℕ → NS
| omega : NS

-- The language with all of ℕ as constants, and a single binary relation.
def Arith : Language := Language.mk₂ ℕ Empty Empty Empty Unit

-- The language with all of NS as constants, and a single binary relation.
def OmegaArith : Language := Language.mk₂ NS Empty Empty Empty Unit


@[simp]
instance standardModel : Structure Arith ℕ :=
  Structure.mk₂ (λ c ↦ c)
    (λ h ↦ h.elim) (λ h ↦ h.elim) (λ h ↦ h.elim)
    (λ _ c₁ c₂ ↦ c₁ < c₂)


def lessThan : OmegaArith.Relations 2 := Unit.unit

def omegaGtN (n : ℕ) : Sentence OmegaArith :=
  lessThan.formula₂ (Constants.term (NS.standard n)) (Constants.term NS.omega)


lemma omegaGtN_inj : omegaGtN n = omegaGtN m → n = m :=
by
  intros eq
  injection eq
  -- -- This isn't well typed!
  -- let f := λ i ↦
  --  Term.relabel Sum.inl
  --  (Matrix.vecCons
  --    (Constants.term (NS.standard n)) ![Constants.term NS.omega])
  sorry

[Eric Wieser]

This doesn't answer your original question, but solves the issue:

lemma omegaGtN_inj : omegaGtN n = omegaGtN m → n = m :=
by
  intros eq
  injection eq with hn hl hR hts
  rw [Function.funext_iff] at hts
  have := hts 0
  simp at this  -- this is bad style; `simp?`'s output would be better
  injection this

[Eric Wieser]

If you turn your original question into a mwe without any of the language stuff, then I can answer that too

[Eric Wieser]

have := congr_fun hts 0 can also replace the rw and have line

[Cody Roux]

Neat, thanks! I'll dig deeper if I really have to.