Adding my own constructors to pre-existing inductive types?

Stream: general

[Marvin]

I am playing around with implementing different logics, where there are more modifiers of propositions that are themselves propositions (like how Not : Prop -> Prop is a Proposition itself wrapping a Proposition). An example of this is Prior's tense logic where we have Past(prop) and Future(prop) to temporally qualify when a proposition is true. So Future must be considered a Prop.

Is there a way for me to add these as cases to the original Prop adt?

I need this to be considered valid

def p : Prop := true
def q : Prop := Future(p)

[Malvin Gattinger]

Are you sure that the Prop type is what you want, and not make your own type Formula for the tense logic formulas?

For a concrete example, here is the defintiion of the syntax of Classical Linear Logic in Cslib. Note that the type Proposition here is not the same as the Lean Prop.

In general a related question is whether you want a so-called shallow or deep embedding of tense logic into Lean. It also depends on what you then want to do with the formulas: do you care about the syntax, do you ever want to print them, or do you only want to have the Prop they represent?

[Ruben Van de Velde]

No, you cannot add constructors to a pre-existing inductive type. You'll need to create your own

[Marvin]

Malvin Gattinger said:

Are you sure that the Prop type is what you want, and not make your own type Formula for the tense logic formulas?

I assumed that the builtin Prop is already tightly involved with all the theorem proving capabilities and I didn't think it would be correct to try reimplement that.

I would like to write proofs in exactly the same way that normal lean already allows, just with a tense wrapped around each proposition.

[Marvin]

Ruben Van de Velde said:

No, you cannot add constructors to a pre-existing inductive type. You'll need to create your own

Another idea I had is to make a second inductive type just for Tense, with constructors Past and Future, and then provide an implicit coercion from Tense -> Prop to make it feel in effect as if they were themselves propositions.

Would anything like this be a good idea?

[Malvin Gattinger]

Let's step back a bit. What things about Future(p) would you want to prove then? Note that Lean itself has no idea about tense logic, you need to tell it first what "Future" should mean. So if you want to make a Lean proof that some statement is a tautology in tense logic then you first need to define what it means for such a statement to be true, valid or provable.

[Marvin]

Malvin Gattinger said:

Let's step back a bit. What things about Future(p) would you want to prove then?

I'm encoding some natural language sentences to try to do basic philosophy argumentation. I will write things like

p1 : kill alice john -> guilty alice
-- means "if alice killed john, then alice is guilty"

where many of these words are just semantic primitives (axioms) and don't need do be defined further. A similar project in Rocq is this https://arno.uvt.nl/show.cgi?fid=133761

I already have the above working, I just need to add tense modifiers now.

Past(kill alice john) -> (Now(murderer alice) ∧ Future(murderer alice))
-- if alice killed john in the past, she is a murderer now and in the future

[Malvin Gattinger]

Ah, if you are already working with axiom then maybe you also want to use it for "Future" etc. like this?

inductive Person | alice | john

axiom murderer : Person → Prop

axiom kill : Person → Person → Prop

axiom Past : Prop → Prop
axiom Now : Prop → Prop
axiom Future : Prop → Prop

/-- If alice killed john in the past, she is a murderer now and in the future -/
example : Past (kill alice john) → (Now (murderer alice) ∧ Future (murderer alice)) := by
  -- You will probably need more assumptions and/or axioms to prove this.
  sorry

(This is an #mwe - you can click on the top right corner to open it on live.lean-lang.org )

[Henrik Böving]

Just to clarify, the premise of this thread is wrong:

Is there a way for me to add these as cases to the original Prop adt?

Prop is not an algebraic datatype. If you want to speak in Haskell terms its more of a kind than a type.

[Marvin]

Malvin Gattinger said:

axiom Past : Prop → Prop
axiom Now : Prop → Prop
axiom Future : Prop → Prop

ah this is already what I had gone with, but I assumed it wouldn't be the recommended way. Or I worried that it was going to cause me weird error messages about non-computability. (new to Lean and I keep running into that)

[Malvin Gattinger]

Well, it is something I have never done before and also never seen someone doing, in the sense that using axiom a lot is uncommon in Lean, I think. Because you can easily define axioms that will allow you to prove anything.

[Marvin]

If you can think of a better way to encode tense logic, please let me know. I'll keep working and see how this approach goes

[Robin Arnez]

Well, you should be able to replace most axioms with opaque at least

[Robin Arnez]

At least the ones that define relations, maybe not those that assert things