Tag Info

Accepted

Does the canonicity of natural number imply that of all types?

Your question is quite vague, so let me give you both an intuition on why this ought to be true, and a counterexample. As for intuition, let me show how supposing only canonicity for $\mathbb{N}$ (...
• 5,036
Accepted

Can you build W-types out of natural numbers predicatively?

The answer is no. According to Anton Setzer's PhD thesis: Proof theoretical strength of Martin-Löf Type Theory with W-type and one universe: Aczel has shown in [Acz77] that Martin-Löf’s type theory ...
• 2,221

Proof by Exhaustive Computation for small initial segment of natural numbers (in Coq)

You can prove in userland that these kind of problems are decidable (I am not too familiar with the stdlib so it can probably be golfed down): ...
• 1,126
Accepted

What is the well-established η law for naturals?

I find it's best to think of $\eta$ laws for inductive types in terms of their categorical semantics as initial algebras. Recall that initiality for $(\mathbb{N},0,\mathsf{succ})$, regarded as an ...
Accepted

Implementing and verifying algorithms for solving equations in Lean

For single variable equations its very doable indeed, but you should decide what sort of interaction you want, verified code or a tactic. Both should be possible with Lean + mathlib as it is today. I ...
• 615

How to Prove Theorem le_zero in Lean4: If x ≤ 0, then x = 0?

this is my proof that uses the rules of the game cases hx contrapose! h symm intro t apply eq_zero_of_add_right_eq_zero at t apply h at t exact t Not sure if ...
• 161
Accepted

How do I approach the final step in proving the cancellation law in Coq?

You can prove your theorem S_n_eq_S_m_if_n_eq_m by congruence: ...
• 6,176
Accepted

Strong induction for nat in Coq

A classic solution is to define a stronger property, which you prove by induction. ...

Proving that a minimum example exists if any example exists in nat

Here's the start of a cute solution: ...
• 1,757

proof-based Pos type class

7 > 0 is a statement that can be either true or false. However what you need to provide is a proof of 7 > 0. Repeating the ...
• 3,927
Accepted

Is every type-theoretic function ℕ → A extensionally equal to one written in terms of the ℕ-eliminator

With function extensionality this is trivially true, because f = elim (f 0) (\n _ -> f (suc n)). Without function extensionality I suspect it is not true, but ...
• 3,927
Accepted

Using the contrapositive in lean 4

First, to answer your direct question, you can complete your proof with the following. apply ih contrapose h apply succ_inj exact h After ...
• 8,655