how to avoid `axiom` command

Stream: Is there code for X?

[Asei Inoue]

This code is a formalization of SKI combinator.

Can we show this theorem without axiom command?

inductive Lam : Type where
  | S : Lam
  | K : Lam
  | app : Lam → Lam → Lam

instance : CoeFun Lam (fun _ => Lam → Lam) where
  coe lambda := Lam.app lambda

namespace Lam

axiom K_def {a b : Lam} : (K a) b = a
axiom S_def {a b c : Lam} : ((S a) b) c = (a c) (b c)

theorem eta_simp {a b : Lam} : (∀(c : Lam), a c = b c) → a = b := by
  intro h
  specialize h S
  injection h

def I := (S K) K

theorem I_def {a : Lam} : I a = a := by rw [I, S_def, K_def]

example {a : Lam} : (S K) a = I := by
  apply eta_simp
  intro c
  rw [I_def, S_def, K_def]

end Lam

[Eric Wieser]

Your axiom is false:

example : False := by
  refine absurd @K_def ?_
  intro h
  cases @h S S

[Asei Inoue]

oh no…

[Damiano Testa]

Technically, this does not mean that you cannot show your theorem without the axiom, though...

[Eric Wieser]

Well, the theorems are also false

[Giacomo Stevanato]

The built-in equality is the wrong one for your usecase as its meaning is that two lambda terms have the same "structure" (i.e. they are written the same), not that they reduce to the same "value" in your calculus. You'll instead want to define your own equality relation that's inhabited when that happens. For example:

inductive Lam : Type where
  | S : Lam
  | K : Lam
  | app : Lam → Lam → Lam

instance : CoeFun Lam (fun _ => Lam → Lam) where
  coe lambda := Lam.app lambda

namespace Lam

-- Note: you might want to define this differently.
inductive LEq : Lam → Lam → Prop where
  | refl : LEq a a
  | symm : LEq a b → LEq b a
  | trans : (LEq a b) → (LEq b c) → LEq a c
  | lamext : (∀ c, LEq (a c) (b c)) → LEq a b
  | lam_left : LEq a b → LEq (a c) (b c)
  | lam_right : {c : Lam} → LEq a b → LEq (c a) (c b)
  | K : LEq ((Lam.K a) b) a
  | S : LEq (((Lam.S a) b) c) ((a c) (b c))
infix:50    " ≈ " => LEq

-- Needed to use calc
instance : Trans LEq LEq LEq where
  trans := LEq.trans

-- This is useless if you use `LEq`, as it is just `LEq.funext`. You might try to remove it from `LEq`'s definition and try to prove it, I don't know if it's possible.
theorem eta_simp {a b : Lam} : (∀(c : Lam), a c = b c) → a = b := by
  intro h
  specialize h S
  injection h

def I := (S K) K

theorem I_def {a : Lam} : I a ≈ a := by
  rw [I]
  apply LEq.trans
  apply LEq.S
  apply LEq.K

example {a : Lam} : (S K) a ≈ I := by
  rw [I]
  apply LEq.lamext
  intro c
  calc
    (S K) a c ≈ (K c) (a c) := LEq.S
    _ ≈ c                   := LEq.K
    _ ≈ (K c) (K c)         := LEq.symm LEq.K
    _ ≈ I c                 := LEq.symm LEq.S

example {a : Lam} : (S K) a ≈ I := by
  apply LEq.lamext
  intro c
  have left : (S K) a c ≈ c := LEq.trans LEq.S LEq.K
  have right : I c ≈ c := LEq.trans LEq.S LEq.K
  exact LEq.trans left (LEq.symm right)

end Lam

[Asei Inoue]

@Giacomo Stevanato Thank you!! But I wonder is there nicer definition of LEq. is this idiomatic way?

[Giacomo Stevanato]

I'm not sure if this is the most ideomatic way, but you will want some kind of relation anyway, though LEq is not necessarily the one you want. You'll need to think about what the concept of "equality" (though equality is probably the wrong term) between your Lams. Does it mean that they reduce to the same "value"? Then you'll need to express what is a reduction and a term. In that case some constructors of LEq (e.g. refl, symm and trans) will likely become replaceable by theorems, however others like lamext may become harder to express.

[Daniel Weber]

It might be nicer to define this as a docs#Setoid and take a docs#Quotient, although it will not be pleasant to show this is transitive, and that apply can lift to it

[Daniel Weber]

Although I imagine that's also something you'll want to prove eventually regardless