Cyclic value should trigger contradiction in the pool.

[craff]

An equation like x = S[x] learn in the pool does not yield a contradiction. Moreover, using any function on x is likely to loop after that. We should detect such cycle.

Strangely, such cycle never appears in PML2 while they were frequent in PML1 ...

[craff]

In fact, in PML1, this appears when dealing with the order on natural. Typically when assuming statements like x < x.

[craff]

There seems to be a use case in lib/int_proofs.pml now.

[craff]

How do we remove the label wait use case ?

[craff]

commit e274f49 is a progress ... But a proof of cantor diagonal argument produces a term fixpoint, not a cyclic value and PML loops also:

val diag : ∀idx ∈(nat ⇒ (nat ⇒ nat)), (∀f∈(nat → nat), ∃m, m∈nat | idx m ≡ f) ⇒ bot = fun idx xdi { let f : nat ⇒ nat = fun n { S[idx n n] }; let m = xdi f; deduce idx m ≡ f; let x = f m; // loops here ✂ }

closing definition does not solve the problem ... it should.

[craff]

idx m has to be blocked in the statement also! it works now

[craff]

@rlepigre we have a use case that works in examples/cantor_diagonal.pml.

Remark (in the file) about proving this for classical nat -> nat ... I do not know how to do that. It is not a contradiction in the model to have t = succ t for a term t of type nat as both term are indeed equivalent. Having a diverging term in nat is a contradiction with the model ... How to have this in the implementation is another problem...

I propose to close, as closing definition + the added cycle test in the pool seems enough ?

[craff]

This is now solved for a long time, let's close as suggested above.