The Coq mailing list

[Vincent Semeria <vincent.semeria AT gmail.com>]

Concerning the proof that Coq is strongly normalizing, I imagine it proceeds by proving an integer n that bounds the number of beta-reductions in an arbitrary term t. I would accept that n is standard, and therefore that the normalization of t terminates, if n is obtained by a simple arithmetical formula from the syntax of t (length, number of redexes, quantifiers, lambdas, ...). Is it the case ?

On Tue, Jun 8, 2021 at 10:54 AM Slavomir Kaslev <slavomir.kaslev AT gmail.com> wrote:

On Mon, Jun 7, 2021 at 6:05 PM Vincent Semeria <vincent.semeria AT gmail.com> wrote:

That's an amusing way of defining numbers. But your c is the constant sequence at 1, so it does not seem to have a successor : it is not really a natural number.

As defined, succ c does exists and is equal to c:

def succ_c_eq_c : succ c = c :=

begin

have h : adjoin 1 (c.1) = c.1 := funext (λ n, nat.rec rfl (λ n ih, rfl) n),

simp [succ, h],

refl

end

live

Though one can still argue that c is not a natural number since nat.succ provably has no fixed points.

On Mon, Jun 7, 2021 at 4:41 PM Slavomir Kaslev <slavomir.kaslev AT gmail.com> wrote:

It's possible to give a constructive description a such a term c of type non-increasing binary sequences and then prove c_gt0 and c_non_standard (sorry of using Lean on the list):

def ℕ' := Σ' a : ℕ → fin 2, Π n : ℕ, a (n + 1) ≤ a n

def lt (a b : ℕ') : Prop := ∃ n : ℕ, a.1 n < b.1 n
instance : has_lt ℕ' := ⟨lt⟩

def zero : ℕ' := ⟨λ n, 0, λ n, by rw fin.le_def⟩
instance : has_zero ℕ' := ⟨zero⟩

def adjoin {A} (x₀ : A) (f : ℕ → A) : ℕ → A
| 0 := x₀
| (n+1) := f n

def fin2_le_1 (x : fin 2) : x ≤ 1 := nat.le_of_lt_succ x.2

def succ (a : ℕ') : ℕ' := ⟨adjoin 1 a.1, λ n, begin
induction n,
{ apply fin2_le_1 },
{ apply a.2 }
end⟩

def c : ℕ' := ⟨λ n, 1, λ n, by rw fin.le_def⟩

def c_gt0 : 0 < c := Exists.intro 0 nat.zero_lt_one

def c_non_standard (a : ℕ') (h : a < c) : succ a < c :=
begin
induction h with n h,
existsi n + 1,
exact h
end

(live in browser version)

On Wed, Jun 2, 2021 at 10:54 PM Vincent Semeria <vincent.semeria AT gmail.com> wrote:
>
> Dear Coq club,
>
> Is it possible to axiomatize a term c : nat, such as c is greater than all standard natural numbers ? The first 2 lines are easy,
> Axiom c : nat.
> Axiom c_gt0 : 0 < c.
>
> But then, could we consistently add this axiom ?
> Axiom c_non_standard : forall n:nat, n < c -> S n < c.
>
> If the last axiom is not consistent, we could modify Coq's type checker to interpret all names of the form c_gtSSSS...S0 as closed terms of the corresponding types SSSS...S0 < c. I am pretty sure that these terms are consistent, because if they introduced a proof of False, that proof would be a finite lambda-term with only a finite number of these c_gt terms. Then c could be replaced by the greatest of these terms, and we would obtain a proof of False in basic Coq.



--
Slavomir Kaslev

--

Slavomir Kaslev