Translating Martin-Löf's equality to low-level Lean

Stream: new members

[Eduardo Ochs]

Hi all,

the second rule in page 16 of Martin-Löf's "Intuitionistic Type Theory" looks like this:

martinlof1.png

Let's specialize it to a proof that a=c implies 2-a=2-c:

martinlof2.png

How do I write that proof of a=c → 2-a=2-c using low-level Lean? I guess that we have to use Eq.subst with the right (motive:=...), but I spent a long time on that and couldn't find the trick...

[Ruben Van de Velde]

This works:

variable (α : Type) (a b c : α) [Sub α]

example (h : a = b) : c - a = c - b := congrArg (c - ·) h

[Ruben Van de Velde]

Or

variable (α : Type) (a b c : α) [Sub α]

example (h : a = b) : c - a = c - b := h ▸ rfl

[Eduardo Ochs]

congrArg is exactly what I was looking for! Thanks!!! =)

[Giacomo Stevanato]

AFAIK Martin-Löf's = represents definitional equality, while Lean's = is just sugar for a propositional equality type, so they are not equivalent. I don't think there is a proper way to represent definitional equality in Lean's frontend.

[Eduardo Ochs]

@Giacomo Stevanato, thanks, I'm going to need that at some point... but right now I'm doing something much more basic - I still find some things in Martin-Löf's notation confusing, like the hypotheses written on top, and I'm just checking how to do a very rough translation of the rules and deductions in ITT to Lean, and I'm writing notes like this...

--   /          (x∈A)   \                 /            (x∈A) \
--   | a=c∈A  b(x)∈B(x) | [    A:=Nat ]   | a=c∈Nat  2-x∈Int |
--   | ---------------- | [ B(x):=Int ] = | ---------------- |
--   \ b(a)=b(c)∈B(a)   / [ b(x):=2-x ]   \   2-a=2-c∈Int    /

variable {a c : Nat}
axiom e1 : a = c
def b (x : Nat) : Int := 2 - x

#check  congrArg
#check  congrArg                 (f:=b)
#check  congrArg (a₁:=a) (a₂:=c) (f:=b)
#check  congrArg (a₁:=a) (a₂:=c) (f:=b) (h:=e1)
#check  congrArg                 (f:=b) (h:=e1)
#check (congrArg                 (f:=b) (h:=e1) : b a = b c)