Having Inductive type living in Prop?

[NotBad4U]

Hi everyone,

as the title suggests, I would like to know if Lambdapi could be modified to support inductive type with type Prop. Being able to define something like this:

inductive T: Prop ≔

For now, it outputs the error message: "The type of test is not supported", but is it because it is not possible to support it theoretically or does some work needs to be done?

[amelieled]

Hi Alessio! How are you? During my internship, we have discussed a lot about that with Catherine and Frédéric. This feature could be very useful (and necessary) also for translating semantics.

If I remember correctly, Frédéric didn't agree that I should implement this, because it wasn't clear to him how to do it more generally. To put it another way, we could code Prop's case easily, but that would be too specific. Worse, the spirit of logical framework is potentially lost.

[fblanqui]

What is Prop?

[fblanqui]

Do you mean things like inductive predicates?

Prop:TYPE
Prf:Prop -> TYPE
inductive N:TYPE := O:N | s:N -> N
le:N -> N -> Prop
le_refl x: Prf(le x x)
le_succ x y: Prf(le x y) -> Prf(le x (s y))

[fblanqui]

It just needs to be implemented. The current inductive command needs to be extended for looking at terms of the form (Prf (le )) instead of (le ) in TYPE-level inductive types. One also has to check that the generated recursor and recursor rules are correct. The declaration could be like:

inductive le:N -> N -> Prop := le_refl x: Prf(le x x) | le_succ x y : Prf(le x y) -> Prf(le x (s y))

where Prop and Prf are the builtins for "Prop" and "P".