Cyclic value should trigger contradiction in the pool.

[rlepigre]

Cyclic value should trigger contradiction in the pool.

[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.