Skip to main content
19 votes
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}$ (...
Meven Lennon-Bertrand's user avatar
14 votes
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 ...
Couchy's user avatar
  • 2,221
5 votes

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): ...
gallais's user avatar
  • 1,126
5 votes
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 ...
C.B. Aberlé's user avatar
3 votes
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 ...
Alex J Best's user avatar
3 votes

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 ...
Rainb's user avatar
  • 161
3 votes
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: ...
ice1000's user avatar
  • 6,176
3 votes
Accepted

Strong induction for nat in Coq

A classic solution is to define a stronger property, which you prove by induction. ...
Pierre Castéran's user avatar
2 votes

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

Here's the start of a cute solution: ...
Li-yao Xia's user avatar
  • 1,757
2 votes

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 ...
Trebor's user avatar
  • 3,927
2 votes
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 ...
Trebor's user avatar
  • 3,927
2 votes
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 ...
Jason Rute's user avatar
  • 8,655
2 votes

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

Here is a proof without congruence, closer to your paper proof. What you want is probably the injection tactic, more about ...
Villetaneuse's user avatar
1 vote
Accepted

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

If you can use MathComp, ssrnat provides ex_minn, which I think gives you exactly what you are trying to prove (e.g., see ...
Björn Brandenburg's user avatar

Only top scored, non community-wiki answers of a minimum length are eligible