Zulip Chat Archive
Stream: metaprogramming / tactics
Topic: down to the axioms
Ping J (Jul 11 2025 at 10:42):
I'm lookng for a 'pure axiomatic' representation of proofs, where proofs and tactics can be traced down to basic type-theoretic reductions.
I need this for a non-language environment to test various ML algorithms.
Perhaps a clever use of Elaborator / Compiler can get me just that? but i was confused if i should use Lean.Expr, Infotree, or sth else
Ping J (Jul 11 2025 at 10:42):
help & guidance greatly appreciated~
perhaps i just missed the right doc/book?
metakuntyyy (Jul 11 2025 at 11:01):
try
set_option pp.proofs true
#print theorem_you_want
metakuntyyy (Jul 11 2025 at 11:02):
Although this won't be very nice.
protected theorem Nat.add_comm : ∀ (n m : Nat),
@Eq.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n m)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m n) :=
fun (x x_1 : Nat) ↦
@Nat.brecOn.{0}
(fun (x : Nat) ↦
∀ (x_2 : Nat),
@Eq.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x_2 x)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x x_2))
x_1
(fun (x : Nat)
(f :
@Nat.below.{0}
(fun (x : Nat) ↦
∀ (x_2 : Nat),
@Eq.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x_2 x)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x x_2))
x)
(x_2 : Nat) ↦
Nat.add_comm.match_1_1
(fun (x x_3 : Nat) ↦
∀
(x_4 :
@Nat.below.{0}
(fun (x : Nat) ↦
∀ (x_4 : Nat),
@Eq.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x_4 x)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x x_4))
x_3),
@Eq.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x x_3)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x_3 x))
x_2 x
(fun (n : Nat)
(x :
@Nat.below.{0}
(fun (x : Nat) ↦
∀ (x_3 : Nat),
@Eq.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x_3 x)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x x_3))
(@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0)))) ↦
@Eq.symm.{1} Nat
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
(@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))) n)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n
(@OfNat.ofNat.{0} Nat (nat_lit 0) (instOfNatNat (nat_lit 0))))
(Nat.zero_add n))
(fun (n m : Nat)
(x :
@Nat.below.{0}
(fun (x : Nat) ↦
∀ (x_3 : Nat),
@Eq.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x_3 x)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) x x_3))
(Nat.succ m)) ↦
@letFun.{0, 0}
(@Eq.{1} Nat (Nat.succ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n m))
(Nat.succ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m n)))
(fun
(this :
@Eq.{1} Nat (Nat.succ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n m))
(Nat.succ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m n))) ↦
@Eq.{1} Nat
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m
(@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m
(@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n))
(@congrArg.{1, 1} Nat Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n m)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m n) Nat.succ (x.1 n))
fun
(this :
@Eq.{1} Nat (Nat.succ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n m))
(Nat.succ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m n))) ↦
@Eq.mpr.{0}
(@Eq.{1} Nat
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m
(@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m
(@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n))
(@Eq.{1} Nat
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m
(@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Nat.succ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m n)))
(@id.{0}
(@Eq.{1} Prop
(@Eq.{1} Nat
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m
(@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat)
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m
(@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1))))
n))
(@Eq.{1} Nat
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m
(@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
(Nat.succ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m n))))
(@congrArg.{1, 1} Nat Prop
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (Nat.succ m) n)
(Nat.succ (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m n))
(fun (_a : Nat) ↦
@Eq.{1} Nat
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) n
(@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) m
(@OfNat.ofNat.{0} Nat (nat_lit 1) (instOfNatNat (nat_lit 1)))))
_a)
(Nat.succ_add m n)))
this)
f)
x
metakuntyyy (Jul 11 2025 at 11:03):
Here's the code.
import Mathlib
set_option pp.all true
#print Nat.add_comm
metakuntyyy (Jul 11 2025 at 11:03):
If you replace pp.all with pp.proofs you get something much more manageable.
protected theorem Nat.add_comm : ∀ (n m : ℕ), n + m = m + n :=
fun x x_1 ↦
Nat.brecOn (motive := fun x ↦ ∀ (x_2 : ℕ), x_2 + x = x + x_2) x_1
(fun x f x_2 ↦
(match (motive :=
∀ (x x_3 : ℕ) (x_4 : Nat.below (motive := fun x ↦ ∀ (x_4 : ℕ), x_4 + x = x + x_4) x_3), x + x_3 = x_3 + x)
x_2, x with
| n, 0 => fun x ↦ Eq.symm (Nat.zero_add n)
| n, m.succ => fun x ↦
have this := congrArg Nat.succ (x.1 n);
Eq.mpr (id (congrArg (fun _a ↦ n + (m + 1) = _a) (Nat.succ_add m n))) this)
f)
x
metakuntyyy (Jul 11 2025 at 11:04):
If you are fine with less details, you can also try #explode theorem_you want
metakuntyyy (Jul 11 2025 at 11:05):
This gives you the steps of each theorem used in a table.
0 │ │ x✝¹ ├ ℕ
1 │ │ x✝ ├ ℕ
2 │ │ x✝¹ │ ┌ ℕ
3 │ │ f │ ├ Nat.below (motive := fun x ↦ ∀ (x_1 : ℕ), x_1 + x = x + x_1) x✝¹
4 │ │ x✝ │ ├ ℕ
5 │ │ n │ │ ┌ ℕ
6 │ │ x✝ │ │ ├ Nat.below (motive := fun x ↦ ∀ (x_1 : ℕ), x_1 + x = x + x_1) 0
7 │ │ Nat.zero_add │ │ │ 0 + n = n
8 │7 │ Eq.symm │ │ │ n + 0 = 0 + n
9 │5,6,8 │ ∀I │ │ ∀ (n : ℕ)
(x : Nat.below (motive := fun x ↦ ∀ (x_1 : ℕ), x_1 + x = x + x_1) 0), n + 0 = 0 + n
10│ │ n │ │ ┌ ℕ
11│ │ m │ │ ├ ℕ
12│ │ x✝ │ │ ├ Nat.below (motive := fun x ↦ ∀ (x_1 : ℕ), x_1 + x = x + x_1) m.succ
13│ │ x✝.1 │ │ │ (fun x ↦ ∀ (x_1 : ℕ), x_1 + x = x + x_1) m
14│13 │ ∀E │ │ │ n + m = m + n
15│14 │ congrArg │ │ │ (n + m).succ = (m + n).succ
16│ │ this │ │ │ ┌ (n + m).succ = (m + n).succ
17│ │ Nat.succ_add │ │ │ │ m.succ + n = (m + n).succ
18│17 │ congrArg │ │ │ │ (n + (m + 1) = m.succ + n) = (n + (m + 1) = (m + n).succ)
19│18 │ id │ │ │ │ (n + (m + 1) = m + 1 + n) = (n + (m + 1) = (m + n).succ)
20│19,16 │ Eq.mpr │ │ │ │ n + (m + 1) = m + 1 + n
21│16,20 │ ∀I │ │ │ (n + m).succ = (m + n).succ → n + (m + 1) = m + 1 + n
22│15,21 │ letFun │ │ │ n + (m + 1) = m + 1 + n
23│10,11,12,22│ ∀I │ │ ∀ (n m : ℕ)
(x : Nat.below (motive := fun x ↦ ∀ (x_1 : ℕ), x_1 + x = x + x_1) m.succ), n + (m + 1) = m + 1 + n
24│9,23 │ Nat.add_comm.match_1_1 │ │ x✝ + x✝¹ = x✝¹ + x✝
25│2,3,4,24 │ ∀I │ ∀ (x : ℕ) (f : Nat.below (motive := fun x ↦ ∀ (x_1 : ℕ), x_1 + x = x + x_1) x)
(x_1 : ℕ), x_1 + x = x + x_1
26│25 │ Nat.brecOn │ x✝¹ + x✝ = x✝ + x✝¹
27│0,1,26 │ ∀I │ ∀ (x x_1 : ℕ), x + x_1 = x_1 + x
metakuntyyy (Jul 11 2025 at 11:07):
I guess you can't really go wrong with Lean.Expr, It can contain a lot of information though.
Ping J (Jul 11 2025 at 12:10):
Cheers!
will try them out and see which fits
Robin Arnez (Jul 11 2025 at 12:20):
If you want to really go down to the axioms, then:
theorem one_add_two : 1 + 2 = 1 + 2 := rfl
/-
I. Γ ⊢ f : ∀ x : α, β[x] &&& Γ ⊢ a : α ==> f a : β[a]
II. Γ ⊢ Sort u : Sort (u + 1)
III. Γ ⊢ a : α ==> Γ ⊢ a ≡ a
IV. Γ ⊢ f ≡ g &&& Γ ⊢ f : ∀ x : α, β[x] &&& Γ ⊢ a ≡ b &&& Γ ⊢ a : α ==> Γ ⊢ f a ≡ g b
V. Γ ⊢ α : Sort u ==> Γ, x : α ⊢ x : α
VI. Γ, x : α ⊢ X[x] : β[x] &&& Γ ⊢ a : α ==> Γ ⊢ (fun x : α => X[x]) a ≡ X[a]
VII. Γ ⊢ a ≡ b &&& Γ ⊢ b ≡ c ==> Γ ⊢ a ≡ c
VIII. Γ ⊢ a ≡ b ==> Γ ⊢ b ≡ a
IX. Γ ⊢ a : α &&& Γ ⊢ α ≡ β ==> Γ ⊢ a : β
1. Γ ⊢ @rfl.{1} : ∀ {α : Type} {a : α}, @Eq.{1} α a a (definition of `def rfl`)
2. Γ ⊢ Nat : Type (definition of `inductive Nat`)
3. Γ ⊢ @rfl.{1} Nat : ∀ {a : Nat}, @Eq.{1} Nat a a (I 1 & 2)
4. Γ ⊢ @OfNat.ofNat.{0} : ∀ {α : Type} (x✝ : Nat) [self : OfNat α x✝], α (definition of `def OfNat.ofNat`)
5. Γ ⊢ @OfNat.ofNat.{0} Nat : ∀ (x✝ : Nat) [self : OfNat Nat x✝], Nat (I 4 & 2)
6. Γ ⊢ nat_lit 1 : Nat (definition of `nat_lit`)
7. Γ ⊢ @OfNat.ofNat.{0} Nat (nat_lit 1) : ∀ [self : OfNat Nat (nat_lit 1)], Nat (I 5 & 6)
8. Γ ⊢ @instOfNatNat : ∀ (n : Nat), OfNat Nat n (definition of `def instOfNatNat`)
9. Γ ⊢ @instOfNatNat (nat_lit 1) : OfNat Nat (nat_lit 1) (I 8 & 6)
10. Γ ⊢ @OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1)) : Nat (I 7 & 9)
11. Γ ⊢ nat_lit 2 : Nat (definition of `nat_lit`)
12. Γ ⊢ @OfNat.ofNat.{0} Nat (nat_lit 2) : ∀ [self : OfNat Nat (nat_lit 2)], Nat (I 5 & 11)
13. Γ ⊢ @instOfNatNat (nat_lit 2) : OfNat Nat (nat_lit 2) (I 8 & 11)
14. Γ ⊢ @OfNat.ofNat.{0} Nat (nat_lit 2) (@instOfNatNat (nat_lit 2)) : Nat (I 12 & 13)
15. Γ ⊢ @HAdd.hAdd.{0, 0, 0} : ∀ {α : Type} {β : Type} {γ : outParam.{2} Type} [self : HAdd.{0, 0, 0} α β γ], α → β → γ (definition of `def HAdd.hAdd`)
16. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat : ∀ {β : Type} {γ : outParam.{2} Type} [self : HAdd.{0, 0, 0} Nat β γ], Nat → β → γ (I 15 & 2)
17. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat Nat : ∀ {γ : outParam.{2} Type} [self : HAdd.{0, 0, 0} Nat Nat γ], Nat → Nat → γ (I 16 & 2)
18. Γ ⊢ outParam.{2} ≡ fun (α : Type 1) => α (definition of `def outParam`)
19. Γ ⊢ outParam.{2} : ∀ (α : Type 1), Type 1 (definition of `def outParam`)
20. Γ ⊢ Type : Type 1 (II)
21. Γ ⊢ Type ≡ Type (III 20)
22. Γ ⊢ outParam.{2} Type ≡ (fun (α : Type 1) => α) Type (IV 18 & 19 & 21 & 20)
23. Γ ⊢ Type 1 : Type 2 (II)
24. Γ, α : Type 1 ⊢ α : Type 1 (V 23)
25. Γ ⊢ (fun (α : Type 1) => α) Type ≡ Type (VI 24 & 20)
26. Γ ⊢ outParam.{2} Type ≡ Type (VII 22 & 25)
27. Γ ⊢ Type ≡ outParam.{2} Type (VIII 26)
28. Γ ⊢ Nat : outParam.{2} Type (IX 2 & 27)
29. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat Nat Nat : ∀ [self : HAdd.{0, 0, 0} Nat Nat Nat], Nat → Nat → Nat (I 16 & 28)
30. Γ ⊢ @instHAdd.{0} : ∀ {α : Type} [Add.{0} α], HAdd.{0, 0, 0} α α α (definition of `def instHAdd`)
31. Γ ⊢ @instHAdd.{0} Nat : [Add.{0} Nat], HAdd.{0, 0, 0} Nat Nat Nat (I 30 & 2)
32. Γ ⊢ instAddNat : Add.{0} Nat (definition of `def instAddNat`)
33. Γ ⊢ @instHAdd.{0} Nat instAddNat : HAdd.{0, 0, 0} Nat Nat Nat (I 31 & 32)
34. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) : Nat → Nat → Nat (I 29 & 33)
35. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1))) : Nat → Nat (I 34 & 10)
36. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1))) (@OfNat.ofNat.{0} Nat (nat_lit 2) (@instOfNatNat (nat_lit 2))) : Nat (I 35 & 14)
37. Γ ⊢ @rfl.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1))) (@OfNat.ofNat.{0} Nat (nat_lit 2) (@instOfNatNat (nat_lit 2)))) : @Eq.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1))) (@OfNat.ofNat.{0} Nat (nat_lit 2) (@instOfNatNat (nat_lit 2)))) (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1))) (@OfNat.ofNat.{0} Nat (nat_lit 2) (@instOfNatNat (nat_lit 2))))
-/
(I originally wanted to do 1 + 2 = 3 but I realized that this would be a much more difficult task)
The axioms I-IX are part of #leantt
metakuntyyy (Jul 11 2025 at 12:25):
Another hint, if you look at the proof script and only see "trivial" tactics then the proof object will be "trivial" itself. Most tactics will be trivial tactics so there won't be much to worry about. Some tactics implement more complex algorithms like Fourier-Motzkin and by that point you can pretty much forget inspecting the proof object.
Ping J (Jul 11 2025 at 12:27):
Robin Arnez said:
If you want to really go down to the axioms, then:
theorem one_add_two : 1 + 2 = 1 + 2 := rfl /- I. Γ ⊢ f : ∀ x : α, β[x] &&& Γ ⊢ a : α ==> f a : β[a] II. Γ ⊢ Sort u : Sort (u + 1) III. Γ ⊢ a : α ==> Γ ⊢ a ≡ a IV. Γ ⊢ f ≡ g &&& Γ ⊢ f : ∀ x : α, β[x] &&& Γ ⊢ a ≡ b &&& Γ ⊢ a : α ==> Γ ⊢ f a ≡ g b V. Γ ⊢ α : Sort u ==> Γ, x : α ⊢ x : α VI. Γ, x : α ⊢ X[x] : β[x] &&& Γ ⊢ a : α ==> Γ ⊢ (fun x : α => X[x]) a ≡ X[a] VII. Γ ⊢ a ≡ b &&& Γ ⊢ b ≡ c ==> Γ ⊢ a ≡ c VIII. Γ ⊢ a ≡ b ==> Γ ⊢ b ≡ a IX. Γ ⊢ a : α &&& Γ ⊢ α ≡ β ==> Γ ⊢ a : β 1. Γ ⊢ @rfl.{1} : ∀ {α : Type} {a : α}, @Eq.{1} α a a (definition of `def rfl`) 2. Γ ⊢ Nat : Type (definition of `inductive Nat`) 3. Γ ⊢ @rfl.{1} Nat : ∀ {a : Nat}, @Eq.{1} Nat a a (I 1 & 2) 4. Γ ⊢ @OfNat.ofNat.{0} : ∀ {α : Type} (x✝ : Nat) [self : OfNat α x✝], α (definition of `def OfNat.ofNat`) 5. Γ ⊢ @OfNat.ofNat.{0} Nat : ∀ (x✝ : Nat) [self : OfNat Nat x✝], Nat (I 4 & 2) 6. Γ ⊢ nat_lit 1 : Nat (definition of `nat_lit`) 7. Γ ⊢ @OfNat.ofNat.{0} Nat (nat_lit 1) : ∀ [self : OfNat Nat (nat_lit 1)], Nat (I 5 & 6) 8. Γ ⊢ @instOfNatNat : ∀ (n : Nat), OfNat Nat n (definition of `def instOfNatNat`) 9. Γ ⊢ @instOfNatNat (nat_lit 1) : OfNat Nat (nat_lit 1) (I 8 & 6) 10. Γ ⊢ @OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1)) : Nat (I 7 & 9) 11. Γ ⊢ nat_lit 2 : Nat (definition of `nat_lit`) 12. Γ ⊢ @OfNat.ofNat.{0} Nat (nat_lit 2) : ∀ [self : OfNat Nat (nat_lit 2)], Nat (I 5 & 11) 13. Γ ⊢ @instOfNatNat (nat_lit 2) : OfNat Nat (nat_lit 2) (I 8 & 11) 14. Γ ⊢ @OfNat.ofNat.{0} Nat (nat_lit 2) (@instOfNatNat (nat_lit 2)) : Nat (I 12 & 13) 15. Γ ⊢ @HAdd.hAdd.{0, 0, 0} : ∀ {α : Type} {β : Type} {γ : outParam.{2} Type} [self : HAdd.{0, 0, 0} α β γ], α → β → γ (definition of `def HAdd.hAdd`) 16. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat : ∀ {β : Type} {γ : outParam.{2} Type} [self : HAdd.{0, 0, 0} Nat β γ], Nat → β → γ (I 15 & 2) 17. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat Nat : ∀ {γ : outParam.{2} Type} [self : HAdd.{0, 0, 0} Nat Nat γ], Nat → Nat → γ (I 16 & 2) 18. Γ ⊢ outParam.{2} ≡ fun (α : Type 1) => α (definition of `def outParam`) 19. Γ ⊢ outParam.{2} : ∀ (α : Type 1), Type 1 (definition of `def outParam`) 20. Γ ⊢ Type : Type 1 (II) 21. Γ ⊢ Type ≡ Type (III 20) 22. Γ ⊢ outParam.{2} Type ≡ (fun (α : Type 1) => α) Type (IV 18 & 19 & 21 & 20) 23. Γ ⊢ Type 1 : Type 2 (II) 24. Γ, α : Type 1 ⊢ α : Type 1 (V 23) 25. Γ ⊢ (fun (α : Type 1) => α) Type ≡ Type (VI 24 & 20) 26. Γ ⊢ outParam.{2} Type ≡ Type (VII 22 & 25) 27. Γ ⊢ Type ≡ outParam.{2} Type (VIII 26) 28. Γ ⊢ Nat : outParam.{2} Type (IX 2 & 27) 29. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat Nat Nat : ∀ [self : HAdd.{0, 0, 0} Nat Nat Nat], Nat → Nat → Nat (I 16 & 28) 30. Γ ⊢ @instHAdd.{0} : ∀ {α : Type} [Add.{0} α], HAdd.{0, 0, 0} α α α (definition of `def instHAdd`) 31. Γ ⊢ @instHAdd.{0} Nat : [Add.{0} Nat], HAdd.{0, 0, 0} Nat Nat Nat (I 30 & 2) 32. Γ ⊢ instAddNat : Add.{0} Nat (definition of `def instAddNat`) 33. Γ ⊢ @instHAdd.{0} Nat instAddNat : HAdd.{0, 0, 0} Nat Nat Nat (I 31 & 32) 34. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) : Nat → Nat → Nat (I 29 & 33) 35. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1))) : Nat → Nat (I 34 & 10) 36. Γ ⊢ @HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1))) (@OfNat.ofNat.{0} Nat (nat_lit 2) (@instOfNatNat (nat_lit 2))) : Nat (I 35 & 14) 37. Γ ⊢ @rfl.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1))) (@OfNat.ofNat.{0} Nat (nat_lit 2) (@instOfNatNat (nat_lit 2)))) : @Eq.{1} Nat (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1))) (@OfNat.ofNat.{0} Nat (nat_lit 2) (@instOfNatNat (nat_lit 2)))) (@HAdd.hAdd.{0, 0, 0} Nat Nat Nat (@instHAdd.{0} Nat instAddNat) (@OfNat.ofNat.{0} Nat (nat_lit 1) (@instOfNatNat (nat_lit 1))) (@OfNat.ofNat.{0} Nat (nat_lit 2) (@instOfNatNat (nat_lit 2)))) -/(I originally wanted to do
1 + 2 = 3but I realized that this would be a much more difficult task)
The axioms I-IX are part of #leantt
whoa! lovely.
how might i get that format of theorems? (did you do it by hand !?)
Ping J (Jul 11 2025 at 12:28):
metakuntyyy said:
Another hint, if you look at the proof script and only see "trivial" tactics then the proof object will be "trivial" itself. Most tactics will be trivial tactics so there won't be much to worry about. Some tactics implement more complex algorithms like Fourier-Motzkin and by that point you can pretty much forget inspecting the proof object.
Interesting, i'll keep it in mind, cheers~
Robin Arnez (Jul 11 2025 at 12:43):
Ping J schrieb:
Robin Arnez said:
If you want to really go down to the axioms, then:
theorem one_add_two : 1 + 2 = 1 + 2 := rfl /- ... -/(I originally wanted to do
1 + 2 = 3but I realized that this would be a much more difficult task)
The axioms I-IX are part of #leanttwhoa! lovely.
how might i get that format of theorems? (did you do it by hand !?)
Yeah, I did it by hand. But I might write a program to do 1 + 2 = 3 for me :-)
Ping J (Jul 11 2025 at 12:56):
XD still wanting help~ i do need to go all the way down to this level of detail
would love to hear how this can be done while i pour the 50k LoC elaborator on myself
Robin Arnez (Jul 11 2025 at 16:09):
I actually managed to write a small type-checker which implements a small portion of lean's typing axioms and can already reproduce what I've manually done above
Robin Arnez (Jul 11 2025 at 16:11):
Example:
def a : 1 + 2 = 1 + 2 := rfl
set_option pp.natLit true
set_option pp.funBinderTypes true
#eval evalDecl `a
produces
1. Γ ⊢ @rfl : ∀ {α : Type} {a : α}, a = a (typing of `def rfl`)
2. Γ ⊢ Nat : Type (typing of `inductive Nat`)
3. Γ ⊢ @rfl Nat : ∀ {a : Nat}, a = a (IV 1 & 2)
4. Γ ⊢ @HAdd.hAdd : {α β : Type} → {γ : outParam Type} → [self : HAdd α β γ] → α → β → γ (typing of `def HAdd.hAdd`)
5. Γ ⊢ @HAdd.hAdd Nat : {β : Type} → {γ : outParam Type} → [self : HAdd Nat β γ] → Nat → β → γ (IV 4 & 2)
6. Γ ⊢ @HAdd.hAdd Nat Nat : {γ : outParam Type} → [self : HAdd Nat Nat γ] → Nat → Nat → γ (IV 5 & 2)
7. Γ ⊢ outParam ≡ fun (α : Type 1) => α (definition of `def outParam`)
8. Γ ⊢ outParam : Type 1 → Type 1 (typing of `def outParam`)
9. Γ ⊢ Type : Type 1 (III)
10. Γ ⊢ Type ≡ Type (VIII 9)
11. Γ ⊢ outParam Type ≡ (fun (α : Type 1) => α) Type (XII 7 & 8 & 10 & 9)
12. Γ ⊢ Type 1 : Type 2 (III)
13. Γ, α : Type 1 ⊢ α : Type 1 (II 12)
14. Γ ⊢ (fun (α : Type 1) => α) Type ≡ Type (XV 13 & 9)
15. Γ ⊢ outParam Type ≡ Type (X 11 & 14)
16. Γ ⊢ Type ≡ outParam Type (IX 15)
17. Γ ⊢ Nat : outParam Type (VII 2 & 16)
18. Γ ⊢ @HAdd.hAdd Nat Nat Nat : [self : HAdd Nat Nat Nat] → Nat → Nat → Nat (IV 6 & 17)
19. Γ ⊢ @instHAdd : {α : Type} → [Add α] → HAdd α α α (typing of `def instHAdd`)
20. Γ ⊢ @instHAdd Nat : [Add Nat] → HAdd Nat Nat Nat (IV 19 & 2)
21. Γ ⊢ instAddNat : Add Nat (typing of `def instAddNat`)
22. Γ ⊢ instHAdd : HAdd Nat Nat Nat (IV 20 & 21)
23. Γ ⊢ HAdd.hAdd : Nat → Nat → Nat (IV 18 & 22)
24. Γ ⊢ @OfNat.ofNat : {α : Type} → (x : Nat) → [self : OfNat α x] → α (typing of `def OfNat.ofNat`)
25. Γ ⊢ OfNat.ofNat : (x : Nat) → [self : OfNat Nat x] → Nat (IV 24 & 2)
26. Γ ⊢ nat_lit 1 : Nat (definition of nat_lit)
27. Γ ⊢ @OfNat.ofNat Nat (nat_lit 1) : [self : OfNat Nat (nat_lit 1)] → Nat (IV 25 & 26)
28. Γ ⊢ instOfNatNat : (n : Nat) → OfNat Nat n (typing of `def instOfNatNat`)
29. Γ ⊢ instOfNatNat (nat_lit 1) : OfNat Nat (nat_lit 1) (IV 28 & 26)
30. Γ ⊢ 1 : Nat (IV 27 & 29)
31. Γ ⊢ HAdd.hAdd 1 : Nat → Nat (IV 23 & 30)
32. Γ ⊢ nat_lit 2 : Nat (definition of nat_lit)
33. Γ ⊢ @OfNat.ofNat Nat (nat_lit 2) : [self : OfNat Nat (nat_lit 2)] → Nat (IV 25 & 32)
34. Γ ⊢ instOfNatNat (nat_lit 2) : OfNat Nat (nat_lit 2) (IV 28 & 32)
35. Γ ⊢ 2 : Nat (IV 33 & 34)
36. Γ ⊢ 1 + 2 : Nat (IV 31 & 35)
37. Γ ⊢ rfl : 1 + 2 = 1 + 2 (IV 3 & 36)
Aaron Liu (Jul 11 2025 at 16:12):
now do 1 + 2 = 3 :)
Robin Arnez (Jul 11 2025 at 16:17):
Well: unimplemented kind: projection #0.1
In other words: time to implement that stuff :-)
Robin Arnez (Jul 11 2025 at 16:43):
okay now it complains
1 + 2 and 3 are not (or at least maybe not) definitionally equivalent
which is I guess reasonable to expect for now
Robin Arnez (Jul 11 2025 at 17:00):
It is able to handle
def a : ¬(False ∧ True) := by
intro h
exact h.1.elim
set_option pp.natLit true
set_option pp.funBinderTypes true
#eval evalDecl `a
though, outputting
1. Γ, h : False ∧ True ⊢ @False.elim : ∀ {C : Prop}, False → C (typing of `def False.elim`)
2. Γ, h : False ∧ True ⊢ False : Prop (typing of `inductive False`)
3. Γ, h : False ∧ True ⊢ False.elim : False → False (IV 1 & 2)
4. Γ, h : False ∧ True ⊢ @And.left : ∀ {a b : Prop}, a ∧ b → a (typing of `theorem And.left`)
5. Γ, h : False ∧ True ⊢ @And.left False : ∀ {b : Prop}, False ∧ b → False (IV 4 & 2)
6. Γ, h : False ∧ True ⊢ True : Prop (typing of `inductive True`)
7. Γ, h : False ∧ True ⊢ And.left : False ∧ True → False (IV 5 & 6)
8. Γ ⊢ And : Prop → Prop → Prop (typing of `inductive And`)
9. Γ ⊢ False : Prop (typing of `inductive False`)
10. Γ ⊢ And False : Prop → Prop (IV 8 & 9)
11. Γ ⊢ True : Prop (typing of `inductive True`)
12. Γ ⊢ False ∧ True : Prop (IV 10 & 11)
13. Γ, h : False ∧ True ⊢ h : False ∧ True (II 12)
14. Γ, h : False ∧ True ⊢ h.left : False (IV 7 & 13)
15. Γ, h : False ∧ True ⊢ False.elim h.left : False (IV 3 & 14)
16. Γ ⊢ fun (h : False ∧ True) => False.elim h.left : False ∧ True → False (V 15)
17. Γ ⊢ Not ≡ fun (a : Prop) => a → False (definition of `def Not`)
18. Γ ⊢ Not : Prop → Prop (typing of `def Not`)
19. Γ ⊢ False ∧ True ≡ False ∧ True (VIII 12)
20. Γ ⊢ ¬(False ∧ True) ≡ (fun (a : Prop) => a → False) (False ∧ True) (XII 17 & 18 & 19 & 12)
21. Γ ⊢ Prop : Type (III)
22. Γ, a : Prop ⊢ a : Prop (II 21)
23. Γ, a : Prop, a✝ : a ⊢ False : Prop (typing of `inductive False`)
24. Γ, a : Prop ⊢ a → False : Sort (imax 0 0) (VI 22)
25. Γ ⊢ (fun (a : Prop) => a → False) (False ∧ True) ≡ False ∧ True → False (XV 24 & 12)
26. Γ ⊢ ¬(False ∧ True) ≡ False ∧ True → False (X 20 & 25)
27. Γ ⊢ False ∧ True → False ≡ ¬(False ∧ True) (IX 26)
28. Γ ⊢ fun (h : False ∧ True) => False.elim h.left : ¬(False ∧ True) (VII 16 & 27)
Aaron Liu (Jul 11 2025 at 17:02):
Great! Now do
def a (P : Prop) : ¬¬(P ∨ ¬P) :=
fun hnPnP => hnPnP (.inr fun hP => hnPnP (.inl hP))
set_option pp.natLit true
set_option pp.funBinderTypes true
#eval evalDecl `a
Robin Arnez (Jul 11 2025 at 17:02):
1. Γ, P : Prop ⊢ Not : Prop → Prop (typing of `def Not`)
2. Γ, P : Prop ⊢ Or : Prop → Prop → Prop (typing of `inductive Or`)
3. Γ ⊢ Prop : Type (III)
4. Γ, P : Prop ⊢ P : Prop (II 3)
5. Γ, P : Prop ⊢ Or P : Prop → Prop (IV 2 & 4)
6. Γ, P : Prop ⊢ ¬P : Prop (IV 1 & 4)
7. Γ, P : Prop ⊢ P ∨ ¬P : Prop (IV 5 & 6)
8. Γ, P : Prop ⊢ ¬(P ∨ ¬P) : Prop (IV 1 & 7)
9. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ hnPnP : ¬(P ∨ ¬P) (II 8)
10. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ Not ≡ fun (a : Prop) => a → False (definition of `def Not`)
11. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ Not : Prop → Prop (typing of `def Not`)
12. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ Or : Prop → Prop → Prop (typing of `inductive Or`)
13. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ P : Prop (I 4 & 8)
14. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ Or P : Prop → Prop (IV 12 & 13)
15. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ ¬P : Prop (IV 11 & 13)
16. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ P ∨ ¬P : Prop (IV 14 & 15)
17. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ P ∨ ¬P ≡ P ∨ ¬P (VIII 16)
18. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ ¬(P ∨ ¬P) ≡ (fun (a : Prop) => a → False) (P ∨ ¬P) (XII 10 & 11 & 17 & 16)
19. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ Prop : Type (III)
20. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), a : Prop ⊢ a : Prop (II 19)
21. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), a : Prop, a✝ : a ⊢ False : Prop (typing of `inductive False`)
22. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), a : Prop ⊢ a → False : Sort (imax 0 0) (VI 20)
23. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ (fun (a : Prop) => a → False) (P ∨ ¬P) ≡ P ∨ ¬P → False (XV 22 & 16)
24. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ ¬(P ∨ ¬P) ≡ P ∨ ¬P → False (X 18 & 23)
25. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ hnPnP : P ∨ ¬P → False (VII 9 & 24)
26. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ @Or.inr : ∀ {a b : Prop}, b → a ∨ b (typing of `constructor Or.inr`)
27. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ @Or.inr P : ∀ {b : Prop}, b → P ∨ b (IV 26 & 13)
28. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ Or.inr : ¬P → P ∨ ¬P (IV 27 & 15)
29. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ hnPnP : ¬(P ∨ ¬P) (I 9 & 13)
30. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ Not ≡ fun (a : Prop) => a → False (definition of `def Not`)
31. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ Not : Prop → Prop (typing of `def Not`)
32. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ Or : Prop → Prop → Prop (typing of `inductive Or`)
33. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ P : Prop (I 13 & 13)
34. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ Or P : Prop → Prop (IV 32 & 33)
35. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ ¬P : Prop (IV 31 & 33)
36. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ P ∨ ¬P : Prop (IV 34 & 35)
37. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ P ∨ ¬P ≡ P ∨ ¬P (VIII 36)
38. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ ¬(P ∨ ¬P) ≡ (fun (a : Prop) => a → False) (P ∨ ¬P) (XII 30 & 31 & 37 & 36)
39. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ Prop : Type (III)
40. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P, a : Prop ⊢ a : Prop (II 39)
41. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P, a : Prop, a✝ : a ⊢ False : Prop (typing of `inductive False`)
42. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P, a : Prop ⊢ a → False : Sort (imax 0 0) (VI 40)
43. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ (fun (a : Prop) => a → False) (P ∨ ¬P) ≡ P ∨ ¬P → False (XV 42 & 36)
44. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ ¬(P ∨ ¬P) ≡ P ∨ ¬P → False (X 38 & 43)
45. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ hnPnP : P ∨ ¬P → False (VII 29 & 44)
46. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ @Or.inl : ∀ {a b : Prop}, a → a ∨ b (typing of `constructor Or.inl`)
47. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ @Or.inl P : ∀ {b : Prop}, P → P ∨ b (IV 46 & 33)
48. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ Or.inl : P → P ∨ ¬P (IV 47 & 35)
49. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ hP : P (II 13)
50. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ Or.inl hP : P ∨ ¬P (IV 48 & 49)
51. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P), hP : P ⊢ hnPnP (Or.inl hP) : False (IV 45 & 50)
52. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ fun (hP : P) => hnPnP (Or.inl hP) : P → False (V 51)
53. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ P ≡ P (VIII 13)
54. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ ¬P ≡ (fun (a : Prop) => a → False) P (XII 10 & 11 & 53 & 13)
55. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ (fun (a : Prop) => a → False) P ≡ P → False (XV 22 & 13)
56. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ ¬P ≡ P → False (X 54 & 55)
57. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ P → False ≡ ¬P (IX 56)
58. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ fun (hP : P) => hnPnP (Or.inl hP) : ¬P (VII 52 & 57)
59. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ Or.inr fun (hP : P) => hnPnP (Or.inl hP) : P ∨ ¬P (IV 28 & 58)
60. Γ, P : Prop, hnPnP : ¬(P ∨ ¬P) ⊢ hnPnP (Or.inr fun (hP : P) => hnPnP (Or.inl hP)) : False (IV 25 & 59)
61. Γ, P : Prop ⊢ fun (hnPnP : ¬(P ∨ ¬P)) => hnPnP (Or.inr fun (hP : P) => hnPnP (Or.inl hP)) : ¬(P ∨ ¬P) → False (V 60)
62. Γ ⊢ fun (P : Prop) (hnPnP : ¬(P ∨ ¬P)) =>
hnPnP (Or.inr fun (hP : P) => hnPnP (Or.inl hP)) : ∀ (P : Prop), ¬(P ∨ ¬P) → False (V 61)
63. Γ, P : Prop ⊢ Not ≡ fun (a : Prop) => a → False (definition of `def Not`)
64. Γ, P : Prop ⊢ ¬(P ∨ ¬P) ≡ ¬(P ∨ ¬P) (VIII 8)
65. Γ, P : Prop ⊢ ¬¬(P ∨ ¬P) ≡ (fun (a : Prop) => a → False) ¬(P ∨ ¬P) (XII 63 & 1 & 64 & 8)
66. Γ, P : Prop ⊢ Prop : Type (III)
67. Γ, P : Prop, a : Prop ⊢ a : Prop (II 66)
68. Γ, P : Prop, a : Prop, a✝ : a ⊢ False : Prop (typing of `inductive False`)
69. Γ, P : Prop, a : Prop ⊢ a → False : Sort (imax 0 0) (VI 67)
70. Γ, P : Prop ⊢ (fun (a : Prop) => a → False) ¬(P ∨ ¬P) ≡ ¬(P ∨ ¬P) → False (XV 69 & 8)
71. Γ, P : Prop ⊢ ¬¬(P ∨ ¬P) ≡ ¬(P ∨ ¬P) → False (X 65 & 70)
72. Γ, P : Prop ⊢ ¬(P ∨ ¬P) → False ≡ ¬¬(P ∨ ¬P) (IX 71)
73. Γ ⊢ Prop ≡ Prop (VIII 3)
74. Γ ⊢ ∀ (P : Prop), ¬(P ∨ ¬P) → False ≡ ∀ (P : Prop), ¬¬(P ∨ ¬P) (XIV 73 & 72)
75. Γ ⊢ fun (P : Prop) (hnPnP : ¬(P ∨ ¬P)) =>
hnPnP (Or.inr fun (hP : P) => hnPnP (Or.inl hP)) : ∀ (P : Prop), ¬¬(P ∨ ¬P) (VII 62 & 74)
Robin Arnez (Jul 11 2025 at 17:08):
It can also do
def a (a : Nat) : 3 * a < 14 → a < 5 := by
omega
lol
1. Γ, a : Nat, a✝ : 3 * a <
14 ⊢ @Decidable.byContradiction : ∀ {p : Prop} [dec : Decidable p],
(¬p → False) → p (typing of `theorem Decidable.byContradiction`)
2. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ @LT.lt : {α : Type} → [self : LT α] → α → α → Prop (typing of `def LT.lt`)
3. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ Nat : Type (typing of `inductive Nat`)
4. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ @LT.lt Nat : [self : LT Nat] → Nat → Nat → Prop (IV 2 & 3)
5. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ instLTNat : LT Nat (typing of `def instLTNat`)
6. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT.lt : Nat → Nat → Prop (IV 4 & 5)
7. Γ ⊢ Nat : Type (typing of `inductive Nat`)
8. Γ, a : Nat ⊢ a : Nat (II 7)
9. Γ, a : Nat ⊢ @LT.lt : {α : Type} → [self : LT α] → α → α → Prop (typing of `def LT.lt`)
10. Γ, a : Nat ⊢ Nat : Type (typing of `inductive Nat`)
11. Γ, a : Nat ⊢ @LT.lt Nat : [self : LT Nat] → Nat → Nat → Prop (IV 9 & 10)
12. Γ, a : Nat ⊢ instLTNat : LT Nat (typing of `def instLTNat`)
13. Γ, a : Nat ⊢ LT.lt : Nat → Nat → Prop (IV 11 & 12)
14. Γ, a : Nat ⊢ @HMul.hMul : {α β : Type} →
{γ : outParam Type} → [self : HMul α β γ] → α → β → γ (typing of `def HMul.hMul`)
15. Γ, a : Nat ⊢ @HMul.hMul Nat : {β : Type} → {γ : outParam Type} → [self : HMul Nat β γ] → Nat → β → γ (IV 14 & 10)
16. Γ, a : Nat ⊢ @HMul.hMul Nat Nat : {γ : outParam Type} → [self : HMul Nat Nat γ] → Nat → Nat → γ (IV 15 & 10)
17. Γ, a : Nat ⊢ outParam ≡ fun (α : Type 1) => α (definition of `def outParam`)
18. Γ, a : Nat ⊢ outParam : Type 1 → Type 1 (typing of `def outParam`)
19. Γ, a : Nat ⊢ Type : Type 1 (III)
20. Γ, a : Nat ⊢ Type ≡ Type (VIII 19)
21. Γ, a : Nat ⊢ outParam Type ≡ (fun (α : Type 1) => α) Type (XII 17 & 18 & 20 & 19)
22. Γ, a : Nat ⊢ Type 1 : Type 2 (III)
23. Γ, a : Nat, α : Type 1 ⊢ α : Type 1 (II 22)
24. Γ, a : Nat ⊢ (fun (α : Type 1) => α) Type ≡ Type (XV 23 & 19)
25. Γ, a : Nat ⊢ outParam Type ≡ Type (X 21 & 24)
26. Γ, a : Nat ⊢ Type ≡ outParam Type (IX 25)
27. Γ, a : Nat ⊢ Nat : outParam Type (VII 10 & 26)
28. Γ, a : Nat ⊢ @HMul.hMul Nat Nat Nat : [self : HMul Nat Nat Nat] → Nat → Nat → Nat (IV 16 & 27)
29. Γ, a : Nat ⊢ @instHMul : {α : Type} → [Mul α] → HMul α α α (typing of `def instHMul`)
30. Γ, a : Nat ⊢ @instHMul Nat : [Mul Nat] → HMul Nat Nat Nat (IV 29 & 10)
31. Γ, a : Nat ⊢ instMulNat : Mul Nat (typing of `def instMulNat`)
32. Γ, a : Nat ⊢ instHMul : HMul Nat Nat Nat (IV 30 & 31)
33. Γ, a : Nat ⊢ HMul.hMul : Nat → Nat → Nat (IV 28 & 32)
34. Γ, a : Nat ⊢ @OfNat.ofNat : {α : Type} → (x : Nat) → [self : OfNat α x] → α (typing of `def OfNat.ofNat`)
35. Γ, a : Nat ⊢ OfNat.ofNat : (x : Nat) → [self : OfNat Nat x] → Nat (IV 34 & 10)
36. Γ, a : Nat ⊢ nat_lit 3 : Nat (definition of nat_lit)
37. Γ, a : Nat ⊢ @OfNat.ofNat Nat (nat_lit 3) : [self : OfNat Nat (nat_lit 3)] → Nat (IV 35 & 36)
38. Γ, a : Nat ⊢ instOfNatNat : (n : Nat) → OfNat Nat n (typing of `def instOfNatNat`)
39. Γ, a : Nat ⊢ instOfNatNat (nat_lit 3) : OfNat Nat (nat_lit 3) (IV 38 & 36)
40. Γ, a : Nat ⊢ 3 : Nat (IV 37 & 39)
41. Γ, a : Nat ⊢ HMul.hMul 3 : Nat → Nat (IV 33 & 40)
42. Γ, a : Nat ⊢ 3 * a : Nat (IV 41 & 8)
43. Γ, a : Nat ⊢ LT.lt (3 * a) : Nat → Prop (IV 13 & 42)
44. Γ, a : Nat ⊢ nat_lit 14 : Nat (definition of nat_lit)
45. Γ, a : Nat ⊢ @OfNat.ofNat Nat (nat_lit 14) : [self : OfNat Nat (nat_lit 14)] → Nat (IV 35 & 44)
46. Γ, a : Nat ⊢ instOfNatNat (nat_lit 14) : OfNat Nat (nat_lit 14) (IV 38 & 44)
47. Γ, a : Nat ⊢ 14 : Nat (IV 45 & 46)
48. Γ, a : Nat ⊢ 3 * a < 14 : Prop (IV 43 & 47)
49. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a : Nat (I 8 & 48)
50. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT.lt a : Nat → Prop (IV 6 & 49)
51. Γ, a : Nat, a✝ : 3 * a <
14 ⊢ @OfNat.ofNat : {α : Type} → (x : Nat) → [self : OfNat α x] → α (typing of `def OfNat.ofNat`)
52. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ OfNat.ofNat : (x : Nat) → [self : OfNat Nat x] → Nat (IV 51 & 3)
53. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ nat_lit 5 : Nat (definition of nat_lit)
54. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ @OfNat.ofNat Nat (nat_lit 5) : [self : OfNat Nat (nat_lit 5)] → Nat (IV 52 & 53)
55. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ instOfNatNat : (n : Nat) → OfNat Nat n (typing of `def instOfNatNat`)
56. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ instOfNatNat (nat_lit 5) : OfNat Nat (nat_lit 5) (IV 55 & 53)
57. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ 5 : Nat (IV 54 & 56)
58. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a < 5 : Prop (IV 50 & 57)
59. Γ, a : Nat, a✝ : 3 * a <
14 ⊢ @Decidable.byContradiction (a < 5) : ∀ [dec : Decidable (a < 5)], (¬a < 5 → False) → a < 5 (IV 1 & 58)
60. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ Nat.decLt : (n m : Nat) → Decidable (n < m) (typing of `def Nat.decLt`)
61. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a.decLt : (m : Nat) → Decidable (a < m) (IV 60 & 49)
62. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a.decLt 5 : Decidable (a < 5) (IV 61 & 57)
63. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ Decidable : Prop → Type (typing of `inductive Decidable`)
64. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ @LT.lt Nat : [self : LT Nat] → Nat → Nat → Prop (IV 2 & 3)
65. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT : Type → Type (typing of `inductive LT`)
66. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT ≡ LT (VIII 65)
67. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ Nat ≡ Nat (VIII 3)
68. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT Nat ≡ LT Nat (XII 66 & 65 & 67 & 3)
69. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ instLTNat : LT Nat (VII 5 & 68)
70. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT.lt : Nat → Nat → Prop (IV 64 & 69)
71. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT.lt a : Nat → Prop (IV 70 & 49)
72. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a < 5 : Prop (IV 71 & 57)
73. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ @LT.lt ≡ fun (α : Type) [self : LT α] => self.1 (definition of `def LT.lt`)
74. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ Nat ≡ Nat (VIII 3)
75. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ @LT.lt Nat ≡ (@fun (α : Type) [self : LT α] => self.1) Nat (XII 73 & 2 & 74 & 3)
76. Γ, a : Nat, a✝ : 3 * a < 14, α : Type ⊢ LT : Type → Type (typing of `inductive LT`)
77. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ Type : Type 1 (III)
78. Γ, a : Nat, a✝ : 3 * a < 14, α : Type ⊢ α : Type (II 77)
79. Γ, a : Nat, a✝ : 3 * a < 14, α : Type ⊢ LT α : Type (IV 76 & 78)
80. Γ, a : Nat, a✝ : 3 * a < 14, α : Type, self : LT α ⊢ self : LT α (II 79)
81. Γ, a : Nat, a✝ : 3 * a < 14, α : Type, self : LT α ⊢ self.1 ≡ α → α → Prop (projection LT 0 80)
82. Γ, a : Nat, a✝ : 3 * a < 14, α : Type ⊢ fun [self : LT α] => self.1 : [self : LT α] → α → α → Prop (V 81)
83. Γ, a : Nat, a✝ : 3 * a <
14 ⊢ (@fun (α : Type) [self : LT α] => self.1) Nat ≡ fun [self : LT Nat] => self.1 (XV 82 & 3)
84. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ @LT.lt Nat ≡ fun [self : LT Nat] => self.1 (X 75 & 83)
85. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ instLTNat ≡ instLTNat (VIII 69)
86. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT.lt ≡ fun [self : LT Nat] => self.1 (XII 84 & 64 & 85 & 69)
87. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT Nat : Type (IV 65 & 3)
88. Γ, a : Nat, a✝ : 3 * a < 14, self : LT Nat ⊢ self : LT Nat (II 87)
89. Γ, a : Nat, a✝ : 3 * a < 14, self : LT Nat ⊢ self.1 ≡ Nat → Nat → Prop (projection LT 0 88)
90. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ fun [self : LT Nat] => self.1 ≡ instLTNat.1 (XV 89 & 69)
91. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT.lt ≡ instLTNat.1 (X 86 & 90)
92. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a ≡ a (VIII 49)
93. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT.lt a ≡ instLTNat.1 a (XII 91 & 70 & 92 & 49)
94. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ 5 ≡ 5 (VIII 57)
95. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a < 5 ≡ instLTNat.1 a 5 (XII 93 & 71 & 94 & 57)
96. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ @LT.lt Nat ≡ (@fun (α : Type) [self : LT α] => self.1) Nat (XII 73 & 2 & 67 & 3)
97. Γ, a : Nat, a✝ : 3 * a <
14 ⊢ (@fun (α : Type) [self : LT α] => self.1) Nat ≡ fun [self : LT Nat] => self.1 (XV 82 & 3)
98. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ @LT.lt Nat ≡ fun [self : LT Nat] => self.1 (X 96 & 97)
99. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT.lt ≡ fun [self : LT Nat] => self.1 (XII 98 & 4 & 85 & 5)
100. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT Nat : Type (IV 65 & 3)
101. Γ, a : Nat, a✝ : 3 * a < 14, self : LT Nat ⊢ self : LT Nat (II 100)
102. Γ, a : Nat, a✝ : 3 * a < 14, self : LT Nat ⊢ self.1 ≡ Nat → Nat → Prop (projection LT 0 101)
103. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ fun [self : LT Nat] => self.1 ≡ instLTNat.1 (XV 102 & 5)
104. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT.lt ≡ instLTNat.1 (X 99 & 103)
105. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ LT.lt a ≡ instLTNat.1 a (XII 104 & 6 & 92 & 49)
106. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a < 5 ≡ instLTNat.1 a 5 (XII 105 & 50 & 94 & 57)
107. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ instLTNat.1 a 5 ≡ a < 5 (IX 106)
108. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a < 5 ≡ a < 5 (X 95 & 107)
109. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ Decidable ≡ Decidable (VIII 63)
110. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ Decidable (a < 5) ≡ Decidable (a < 5) (XII 109 & 63 & 108 & 72)
111. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a.decLt 5 : Decidable (a < 5) (VII 62 & 110)
112. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ Decidable.byContradiction : (¬a < 5 → False) → a < 5 (IV 59 & 111)
113. Γ, a : Nat, a✝ : 3 * a <
14, a✝ : ¬a < 5 ⊢ _root_.a._proof_1 : ∀ (a : Nat), 3 * a < 14 → ¬a < 5 → False (typing of `theorem a._proof_1`)
114. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ Not : Prop → Prop (typing of `def Not`)
115. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ ¬a < 5 : Prop (IV 114 & 58)
116. Γ, a : Nat, a✝ : 3 * a < 14, a✝ : ¬a < 5 ⊢ a : Nat (I 49 & 115)
117. Γ, a : Nat, a✝ : 3 * a < 14, a✝ : ¬a < 5 ⊢ _root_.a._proof_1 a : 3 * a < 14 → ¬a < 5 → False (IV 113 & 116)
118. Γ, a : Nat, a✝ : 3 * a < 14 ⊢ a✝ : 3 * a < 14 (II 48)
119. Γ, a : Nat, a✝ : 3 * a < 14, a✝ : ¬a < 5 ⊢ a✝¹ : 3 * a < 14 (I 118 & 115)
...
126. Γ ⊢ fun (a : Nat) (a_1 : 3 * a < 14) =>
Decidable.byContradiction fun (a_2 : ¬a < 5) => _root_.a._proof_1 a a_1 a_2 : ∀ (a : Nat), 3 * a < 14 → a < 5 (V 125)
Aaron Liu (Jul 11 2025 at 17:09):
now I have
def a (P : Prop) : Subsingleton (Decidable P) :=
⟨Decidable.rec
(fun hnP => Decidable.rec (fun _ => rfl) (fun hP => (hnP hP).rec))
(fun hP => Decidable.rec (fun hnP => (hnP hP).rec) (fun _ => rfl))⟩
set_option pp.natLit true
set_option pp.funBinderTypes true
#eval evalDecl `a
I wonder how far we can go until it breaks
Aaron Liu (Jul 11 2025 at 17:10):
Robin Arnez said:
It can also do
def a (a : Nat) : 3 * a < 14 → a < 5 := by omegalol
well the bulk omega proof got hidden away
Robin Arnez (Jul 11 2025 at 17:11):
Aaron Liu schrieb:
now I have
def a (P : Prop) : Subsingleton (Decidable P) := ⟨Decidable.rec (fun hnP => Decidable.rec (fun _ => rfl) (fun hP => (hnP hP).rec)) (fun hP => Decidable.rec (fun hnP => (hnP hP).rec) (fun _ => rfl))⟩ set_option pp.natLit true set_option pp.funBinderTypes true #eval evalDecl `aI wonder how far we can go until it breaks
That doesn't compile..?
Aaron Liu (Jul 11 2025 at 17:12):
for me it works fine on the web server
Robin Arnez (Jul 11 2025 at 17:12):
Oh I'm dumb I need to use Decidable.falseTrueCases
Robin Arnez (Jul 11 2025 at 17:12):
(for reference I'm on lean4#8309)
Robin Arnez (Jul 11 2025 at 17:14):
Oh I haven't implemented proof irrelevance lol
Robin Arnez (Jul 11 2025 at 17:14):
Of course it won't work
Aaron Liu (Jul 11 2025 at 17:17):
changing Decidable to a subtype of Bool is an idea
Robin Arnez (Jul 11 2025 at 17:31):
Okay there you go: proof.txt
Aaron Liu (Jul 11 2025 at 17:32):
I think I got the wrong encoding
Robin Arnez (Jul 11 2025 at 17:32):
Yeah idk it should be utf-8?
Aaron Liu (Jul 11 2025 at 17:32):
the Γs are showing up as Γ
Robin Arnez (Jul 11 2025 at 17:34):
should work now
Robin Arnez (Jul 11 2025 at 17:35):
you can search XVII to see proof irrelevance
Aaron Liu (Jul 11 2025 at 17:37):
this is amazing
Aaron Liu (Jul 11 2025 at 17:39):
I still have more
import Mathlib.Data.Fintype.Units
import Mathlib.Data.Sign
def a : ∀ {x y : ℤˣ}, SignType.sign (x : ℤ) = SignType.sign (y : ℤ) → x = y := by
decide
set_option pp.natLit true
set_option pp.funBinderTypes true
#eval evalDecl `a
Robin Arnez (Jul 11 2025 at 17:40):
oh I don't think it can do that
Aaron Liu (Jul 11 2025 at 17:40):
what why
Robin Arnez (Jul 11 2025 at 17:40):
I don't have recursors implemented yet :-)
Robin Arnez (Jul 11 2025 at 17:41):
or well, iota reduction
Robin Arnez (Jul 11 2025 at 17:41):
(that's why it can't 1 + 2 = 3)
Aaron Liu (Jul 11 2025 at 17:42):
maybe do something simpler first then
def a : true ≠ false :=
@Eq.rec Bool true (fun b _ => Bool.rec False True b) trivial false
set_option pp.natLit true
set_option pp.funBinderTypes true
#eval evalDecl `a
Robin Arnez (Jul 11 2025 at 17:46):
Hmm can you make an example for projections first? That's what I'm implementing right now :-)
Aaron Liu (Jul 11 2025 at 17:49):
am I just an example factory?
import Mathlib.Logic.Embedding.Basic
def a.{u, v} {α : Type u} {β : α → Type v} (f : (a : α) → β a) : α ↪ (a : α) × β a where
toFun a := ⟨a, f a⟩
inj' _ _ := congrArg Sigma.fst
set_option pp.natLit true
set_option pp.funBinderTypes true
#eval evalDecl `a
Robin Arnez (Jul 11 2025 at 18:02):
Here: proof.txt
Although I redefined Embedding without mathlib
Robin Arnez (Jul 11 2025 at 18:03):
search proj iota for projection stuff
Aaron Liu (Jul 11 2025 at 18:04):
looks amazing
Aaron Liu (Jul 11 2025 at 18:06):
good job
Robin Arnez (Jul 11 2025 at 18:51):
Okay wow it managed to do
def a : 0 + 0 = 0 := rfl
Robin Arnez (Jul 11 2025 at 18:51):
10000 inference steps!
Robin Arnez (Jul 11 2025 at 18:53):
(more than)
Robin Arnez (Jul 11 2025 at 18:54):
as before, you can see the iota steps by searching (iota
Kenny Lau (Jul 11 2025 at 18:58):
isn't that the 6th peano axiom
Kevin Buzzard (Jul 11 2025 at 21:15):
Math is hard!
Kevin Buzzard (Jul 11 2025 at 21:15):
Maybe this is why it took Russell and Whitehead hundreds of pages to prove 1+1=2
Ping J (Jul 12 2025 at 13:40):
thanks for the amazing work!
and sorry for the slackiness.. i'm on it, am brushing up skills since i'm relatively new to lean
Robin Arnez (Jul 13 2025 at 15:22):
It actually managed to do 1 + 2 = 3!
I optimized it a bit so it's actually smaller than the 0 + 0 = 0 proof above.
Aaron Liu (Jul 13 2025 at 15:30):
5872 lines
Aaron Liu (Jul 13 2025 at 15:30):
amazing
Aaron Liu (Jul 13 2025 at 15:31):
now do funext
Robin Arnez (Jul 13 2025 at 15:42):
Oh it fails with a funny error:
unimplemented kind: let declaration let eqv := fun (f : (x : #4) → @#3 x) (g : (x : #4) → @#3 x) =>
∀ (x : #4), @f x = @g x;
let extfunApp := fun (f : Quot eqv) (x : #4) =>
@Quot.liftOn ((x : #4) → @#3 x) (@#3 x) eqv f (fun (f : (x : #4) → @#3 x) => @f x)
fun (x_1 : (x : #4) → @#3 x) (x_2 : (x : #4) → @#3 x) (h : eqv x_1 x_2) => h x;
id (congrArg extfunApp (Quot.sound #0))
In other words: let is unimplemented :-) (I didn't need it before lol)
After I fix that we should get a Quot.lift-related error.
Aaron Liu (Jul 13 2025 at 15:43):
I have made a version without let
universe u v
example : type_of% @funext.{u, v} :=
fun {α : Sort u} {β : α → Sort v} {f g : (x : α) → β x} (h : ∀ (x : α), @Eq (β x) (f x) (g x)) =>
@congrArg
(@Quot ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), @Eq (β x) (f x) (g x)) ((x : α) → β x)
(@Quot.mk ((x : α) → β x) (fun (f g : (x : α) → β x) => ∀ (x : α), @Eq (β x) (f x) (g x)) f)
(@Quot.mk ((x : α) → β x) (fun (f g : (x : α) → β x) => ∀ (x : α), @Eq (β x) (f x) (g x)) g)
(fun (f : @Quot ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), @Eq (β x) (f x) (g x)) (x : α) =>
@Quot.lift ((x : α) → β x) (fun (f g : (x : α) → β x) => ∀ (x : α), @Eq (β x) (f x) (g x))
(β x) (fun (f : (x : α) → β x) => f x) (fun (f g : (x : α) → β x) (h : ∀ (x : α), @Eq (β x) (f x) (g x)) => h x) f)
(@Quot.sound ((x : α) → β x) (fun (f g : (x : α) → β x) => ∀ (x : α), @Eq (β x) (f x) (g x)) f g h)
Aaron Liu (Jul 13 2025 at 15:44):
everything is explicit
Robin Arnez (Jul 13 2025 at 15:58):
Yeah Quot.lift related error:
Γ, α : Sort
u, β : α →
Sort
v, f : (x : α) →
β
x, g : (x : α) →
β
x, h : ∀ (x : α),
f x =
g
x, x : α ⊢ Quot.lift (fun (f : (x : α) → β x) => f x)
⋯ and f / Quot.lift (fun (f : (x : α) → β x) => f x) ⋯ and f are not (or at least maybe not) definitionally equivalent
Aaron Liu (Jul 13 2025 at 16:03):
yeah those don't look definitionally equivalent to me
Robin Arnez (Jul 13 2025 at 16:03):
It's because of congruence
Aaron Liu (Jul 13 2025 at 16:04):
what's that
Robin Arnez (Jul 13 2025 at 16:04):
Probably had a Quot.lift ... (Quot.mk a) = f b before and then decided to separate it into
Quot.lift ... = f, Quot.mk a = b
Aaron Liu (Jul 13 2025 at 16:04):
are those even the same type
Robin Arnez (Jul 13 2025 at 16:05):
Maybe not, it checks types after checking defeq
Robin Arnez (Jul 13 2025 at 16:06):
Although the types not being equal probably also hindered it in trying to prove definitional equality
Robin Arnez (Jul 13 2025 at 16:08):
There you go.
Aaron Liu (Jul 13 2025 at 16:10):
it's shorter
Aaron Liu (Jul 13 2025 at 16:10):
shorter than 1 + 2 = 3
Robin Arnez (Jul 13 2025 at 16:10):
Yeah, less reduction involved
Robin Arnez (Jul 13 2025 at 16:11):
Y'know, Nat.add being Nat.brecOn + match etc.
Aaron Liu (Jul 13 2025 at 16:15):
I found the iota Quot Quot.mk rule
Aaron Liu (Jul 13 2025 at 16:17):
there are newlines in weird places
Robin Arnez (Jul 13 2025 at 16:20):
Hmm let me try disabling the column limit altogether
Is this better? some kind of funext.txt
Aaron Liu (Jul 13 2025 at 16:20):
the rows are so long
Robin Arnez (Jul 13 2025 at 16:29):
What about this? The context looks more like a goal context now.
Aaron Liu (Jul 13 2025 at 16:35):
not sure about this one
54. Γ,
α : Sort u,
β : α → Sort v
⊢
@congrArg
(Quot fun (f g : (x : α) → β x) =>
∀ (x : α),
f x =
g
x) : ∀ {β_1 : Sort (imax u v)} {a₁ a₂ : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x}
(f : (Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1), a₁ = a₂ → f a₁ = f a₂ (IV 9 & 53)
there's a line break between the g and the x
Aaron Liu (Jul 13 2025 at 16:35):
that's so weird
Robin Arnez (Jul 13 2025 at 16:38):
Yeah I forgot to make the spaces in : to soft line-breaks
This better?
Aaron Liu (Jul 13 2025 at 16:39):
good enough I guess
Aaron Liu (Jul 13 2025 at 16:39):
It's sort of hard to tell when one deduction step ends and another begins
Aaron Liu (Jul 13 2025 at 16:40):
the numbers could be made to stand out more
Robin Arnez (Jul 13 2025 at 16:47):
Does indentation help? some kind of funext.txt
Aaron Liu (Jul 13 2025 at 16:47):
that looks better
Aaron Liu (Jul 13 2025 at 16:48):
the indentation is still a bit weird though
Aaron Liu (Jul 13 2025 at 16:48):
74. Γ,
α : Sort u,
β : α → Sort v,
f : Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x
⊢
@Quot.lift ((x : α) → β x) fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x :
{β_1 : Sort v} →
(f : ((x : α) → β x) → β_1) →
(∀ (a b : (x : α) → β x), (fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) a b → f a = f b) →
(Quot fun (f g : (x : α) → β x) => ∀ (x : α), f x = g x) → β_1 (I 73 & 53)
Aaron Liu (Jul 13 2025 at 16:48):
why is it flat for three lines
Robin Arnez (Jul 13 2025 at 16:55):
Uhh I clearly don't know enough about MessageData and Format
Robin Arnez (Jul 13 2025 at 16:55):
Let me see what normal lean syntax looks like
Last updated: Dec 20 2025 at 21:32 UTC