Prop or Type for Derivations?

Stream: computer science

[Chris Henson]

I was porting a variant of this definition from PLFA and was a bit torn on if this should be in Prop or Type. Any thoughts either way? I've written both and am curious what people find more idiomatic.

[Aaron Liu]

I was writing some lambda calculus code and made my typing judgement a Type (max u v), and then immediately proved unique typing and unique typing judgements, so that I wouldn't have trouble with disequal typing judgements.

[Aaron Liu]

In this case it looks like judgements are your terms, and you want to distinguish between different judgements for the same type, so do make it a Type.

[Aaron Liu]

if you make it a Prop you get that all terms of the same type are equal (you probably don't want that).

[Chris Henson]

Ah yeah, that's a pretty good argument. It becomes something like beta eta equivalence classes if you work in Prop. (Which could be desirable for some situations, but wasn't what I wanted here)

[Aaron Liu]

I don't see how you could possibly get beta-eta equivalence classes just from making it a Prop

[Chris Henson]

My thought was that In Prop, every typing derivation with the same context and type would be equal. So any type preserving transformation on derivations is equal, e.g. beta or eta reduction.

[Aaron Liu]

You also get additional equalities, like 1 = 0

[Shreyas Srinivas]

This depends on how you frame it. You can get around the limit by adding more parameters to your Prop

[Shreyas Srinivas]

If you set "Is (Judgement) by (derivation)" as your Prop, then you won't run into the proof irrelevance headache, because your props will be distinguished for different derivations. It's just way more inconvenient

[Shreyas Srinivas]

Fwiw, Mario already did this : #lean4 > Prettyprinting the result of an #eval @ 💬

[Chris Henson]

Shreyas Srinivas said:

If you set "Is (Judgement) by (derivation)" as your Prop, then you won't run into the proof irrelevance headache, because your props will be distinguished for different derivations. It's just way more inconvenient

I understand the idea here, but is this different from having untyped terms paramaterizing our derivations?

[Fabrizio Montesi]

This is a recurring question when formalising inference systems in Lean.

[Fabrizio Montesi]

For example, you can ask yourself the same question when formalising the inference systems for an operational semantics, derivations in logic, etc.

In classical linear logic right now, we have that a Proof ends in Prop: https://github.com/cs-lean/cslib/blob/cacc4910658d1599560b0e81b035d3e1fde16cfe/Cslib/Logic/LinearLogic/CLL/Basic.lean#L153

inductive Proof : @Sequent Atom → Prop where

This means that I cannot really say whether a Proof is cut-free with a simple function. People usually work around with similar devices to what @Shreyas Srinivas said or weaker variations, like making another inductive with extra parameters (like a counter of the number of cuts within) and prove a characterisation theorem.

[Fabrizio Montesi]

Essentially, the general question is what to do when making a deep embedding of an inference system.
This is gonna be relevant for Phil's PLFL as well, I guess, will trigger.

[Shreyas Srinivas]

Basically you have to ask yourself how much impredicativity is useful for your inductive type definition. If it is important then you might be willing to take on the painful task of parametrising your props with the derivation tree.

[Shreyas Srinivas]

Chris Henson said:

Shreyas Srinivas said:

If you set "Is (Judgement) by (derivation)" as your Prop, then you won't run into the proof irrelevance headache, because your props will be distinguished for different derivations. It's just way more inconvenient

I understand the idea here, but is this different from having untyped terms paramaterizing our derivations?

A derivation tree is distinct from the last sequent in it. So technically yes

[Fabrizio Montesi]

Shreyas Srinivas said:

Basically you have to ask yourself how much impredicativity is useful for your inductive type definition. If it is important then you might be willing to take on the painful task of parametrising your props with the derivation tree.

Another thing I was playing with was to define Proof : Sequent → Type, and then have a Provable : Sequent → Prop defined as 'there exists a Proofof the sequent'. (Provable is called Valid or Derivable in some texts.)

I still have to explore the ergonomics of this though.

[Fabrizio Montesi]

Something like this: https://github.com/cs-lean/cslib/blob/1784e7fa311c7596867844bd4bb90d8ead49b2a1/Cslib/Logic/LinearLogic/CLL/Basic.lean#L171

Logical equivalences are stated in terms of Provable, whereas cutFree is stated on Proof (here: https://github.com/cs-lean/cslib/blob/provable/Cslib/Logic/LinearLogic/CLL/CutElimination.lean).

[Fabrizio Montesi]

Had an exchange with Phil Wadler and we agreed the approach using Type for inference systems seems sensible. That's what he's using in PLFA/PLFL as well.

I'd like to hear more about where we should care for proof irrelevance though, to see if Provable is useful and adequate.

[Fabrizio Montesi]

Think I've managed to define cut-free proofs, cut admissibility, and cut elimination in a decent way, without having to resort to Type.
You can check it out at: https://github.com/leanprover/cslib/blob/main/Cslib/Logics/LinearLogic/CLL/CutElimination.lean

[Thomas Waring]

on this, i’ve started having a look at formalising “non idempotent intersection types” as a way of getting a feel for @Chris Henson’s lambda calculus work — it seemed necessary to have a Type of derivations there because you start to be interested in eg the size of the derivation, which i think you would lose with proof irrelevance

[Thomas Waring]

(see slides https://pageperso.lis-lab.fr/~giulio.guerrieri/ECI2024/day4.pdf)

[Fabrizio Montesi]

I've recently added an example of how to do that for CLL: https://cs-lean.github.io/Cslib/Logics/LinearLogic/CLL/CutElimination.html#CLL.Proof.HasSize
Basically you define something like this:

inductive Proof.HasSize : {Γ : Sequent Atom} → ⊢Γ → Nat → Prop where ...

[Thomas Waring]

right i follow — how would this work for induction measures (say, height or complexity of cuts) since it's not a function on proofs, would it go through using some lemma like "every proof has a unique size"?

[Fabrizio Montesi]

I still have to explore this fully, but I guess that either you go by induction/cases on the inductive that defines the measure (like Proof.HasSize) or you incorporate the measure explicitly in the theorem statement. An example of the first is:

theorem foo (p : ⊢Γ) (hsize : p.HasSize n) : ... := by
  induction hsize

[Aaron Liu]

Thomas Waring said:

right i follow — how would this work for induction measures (say, height or complexity of cuts) since it's not a function on proofs, would it go through using some lemma like "every proof has a unique size"?

You can't do that for proofs

[Shreyas Srinivas]

I think they are talking about deduction trees. Not lean prop proofs

[Aaron Liu]

oh, should have said so, then it's just recursive pattern matching like everything else

[Dexin Zhang]

Props are defeq, and saying a Prop is cut-free/height-bounded sounds weird since there could be both a cut-free proof and a proof with cut on the same sequent.

[Shreyas Srinivas]

They are not talking about Lean Props. See my previous message

[Dexin Zhang]

Conceptually not, but the Lean definition CLL.Proof.CutFree is.

[Shreyas Srinivas]

No it’s a predicate on Proof

[Dexin Zhang]

And a Proof is a Prop

[Shreyas Srinivas]

No it is a predicate on sequents

[Dexin Zhang]

If you have a derivation tree, you have h : Proof Γ as a Prop. And then you have h.CutFree which is a predicate on a Prop.

[Dexin Zhang]

What I mean is, you can legally construct two derivations h1 : Proof Γ and h2 : Proof Γ, one using cut and one is cut-free. However Lean's type system gives h1 = h2, and h1.CutFree h2.CutFree both hold.

[Aaron Liu]

Shreyas Srinivas said:

No it is a predicate on sequents

The predicate seems to say "this sequent has a proof" without recording anywhere which proof it is

[Aaron Liu]

So if you say a Proof is cut-free what this actually says is that there exists some cut-free proof of that sequent

[Aaron Liu]

which is fine if that's what you intended but usually that's not what I would think it's supposed to mean

[Fabrizio Montesi]

That Proof was once called Provable, which matches what you're saying. I was trying the Prop thing but I agree it has its quirks... also, if we just used Type, we'd get actual algorithms for manipulating proofs.

[Fabrizio Montesi]

However I'm not fully convinced that requiring a precise Proof is what we want for the definition of logical equivalence. That's why I proposed to have the current Proof as a Type, and then a Prop called Provable defined as 'there exists a Proof of Gamma'. Thoughts?

[Thomas Waring]

Fabrizio Montesi said:

if we just used Type, we'd get actual algorithms for manipulating proofs.

I’m inclined to agree with this — it doesn’t seem to me that things would be especially more difficult with Type valued derivations, & that also opens up semantics / realisability flavoured applications (ie translations on derivation trees)

[Fabrizio Montesi]

I'd be happy to switch Proof to Type, but it'd be nice to discuss how to define Proposition.equiv under that change.

[Fabrizio Montesi]

My idea was to define it by replacing Proof with Provable. But then lots of proofs about equivalences have to extract the underlying proof from the existential (which I guess would be fine?).

[Shreyas Srinivas]

One thing to watch out for. You will run headlong into the predicativity of type, especially if you have higher order predicates

[Fabrizio Montesi]

Can you flesh that out a bit?

[Dexin Zhang]

An alternative is to define CutFreeProof : Sequent Γ → Prop that merely says "there exists a cut-free proof for this sequent"

[Shreyas Srinivas]

Fabrizio Montesi said:

Can you flesh that out a bit?

If you want to write exists predicate(something) , <some property of predicate>, I believe there are some universe bumps along the way.

[Fabrizio Montesi]

Dexin Zhang said:

An alternative is to define CutFreeProof : Sequent Γ → Prop that merely says "there exists a cut-free proof for this sequent"

That doesn't sound too bad actually. It'd basically be Proof but without the cut rule.

[Fabrizio Montesi]

Shreyas Srinivas said:

Fabrizio Montesi said:

Can you flesh that out a bit?

If you want to write exists predicate(something) , <some property of predicate>, I believe there are some universe bumps along the way.

Mmh, right, that could very well be -- although I don't have a specific example in mind.

[Shreyas Srinivas]

Fabrizio Montesi said:

Dexin Zhang said:

An alternative is to define CutFreeProof : Sequent Γ → Prop that merely says "there exists a cut-free proof for this sequent"

That doesn't sound too bad actually. It'd basically be Proof but without the cut rule.

You might want to specifically define a proof that says IsProofOf Proposition proof-tree

[Shreyas Srinivas]

This can be a prop

[Shreyas Srinivas]

Then for each proof and proof tree, you have a different proposition

[Shreyas Srinivas]

Shreyas Srinivas said:

Basically you have to ask yourself how much impredicativity is useful for your inductive type definition. If it is important then you might be willing to take on the painful task of parametrising your props with the derivation tree.

Which is what I suggested a while back

[Thomas Waring]

I've put together a formalisation of the basics of natural deduction for intuitionistic propositional logic (Gentzen's system NJ) using Type valued derivations — see here. I'll pr it if it seems of interest to cslib (maybe as it relates to STLC @Chris Henson?), but in the meantime it can serve as an example of how such a development might look.

In particular, I have a type Derivation : Sequent Atom → Type _, and a predicate Derivable : Sequent Atom → Prop expressing that there exists some derivation, so each result is duplicated, though the Prop version is always a one-liner.

[Thomas Waring]

Fabrizio Montesi said:

I'd be happy to switch Proof to Type, but it'd be nice to discuss how to define Proposition.equiv under that change.

I dealt with this by defining

protected structure Equivalent (A B : Proposition Atom) : Prop where
  mp : Derivable ⟨{A}, B⟩
  mpr : Derivable ⟨{B},A⟩

(ie an iff), and from there it was easy to show that it's an equivalence relation and has relevant substitution properties eg

theorem equivalent_derivability (Γ : Ctx Atom) {A B : Proposition Atom} (h : IPL.NJ.Equivalent A B)
    : Derivable ⟨Γ, A⟩ ↔ Derivable ⟨Γ, B⟩

[Fabrizio Montesi]

That's great, Thomas!

I'll have a look asap. I'm almost done battling CCS, too, and I'd like to coordinate for your pr there (will write in the other thread).

[Fabrizio Montesi]

That

/-- Contexts are finsets of propositions. -/
abbrev Ctx (Atom) := Finset (Proposition Atom)

is fishy, shouldn't it be a Multiset? See CLL.MProof.

[Thomas Waring]

i went for Finset to avoid explicit contraction, same as multisets avoid explicit exchange

[Fabrizio Montesi]

Oh, fishy but useful. :)

[Fabrizio Montesi]

Q: Why did you go for a custom inductive in Derivable instead of just using an existential? Simpler definition, I guess?

[Thomas Waring]

Fabrizio Montesi said:

Oh, fishy but useful. :)

yah, see also having weakening as a derived rule

[Thomas Waring]

Fabrizio Montesi said:

Q: Why did you go for a custom inductive in Derivable instead of just using an existential? Simpler definition, I guess?

simpler definition, it seemed vaguely ugly to define it as Exists D, True, also this way i get to give a name to the constructor

[Fabrizio Montesi]

Played a bit with this in the context of linear logic, following my original Provable proposal, to see how it'd look. I'd like to discuss the general pattern since then we can just agree to do the same across logics (and, possibly, inference systems..!).

First of all, I'd like notation to distinguish proof/derivation trees from the proposition that something is provable. I'm using ⇓ for the former and ⊢ for the latter for now.

Second, I think we can just use Nonempty for Provable (or Derivable). It's equivalent to what you're doing, @Thomas Waring.

I've adapted the linear logic development to these conventions, you can see it here: https://github.com/leanprover/cslib/blob/logic-provable/Cslib/Logics/LinearLogic/CLL/Basic.lean

This gives us actual algorithms to manipulate CLL proofs, which I think is good.

The downside is that now in all theorems about equivalences we gotta go through Provable.fromProof/toProof (the latter being noncomputable), but that looks ok to me.

This got me wondering, however: don't we just want the same for equivalences? That is, algorithms that rewrite proofs into proofs with equivalent propositions. These algorithms are basically what's already in there for the proofs of equivalences, since they're all constructive. Getting the Prop equivalence is then trivial.

Example:

def Proposition.equiv (a b : Proposition Atom) := ⇓[a⫠, b] × ⇓[b⫠, a]

def Proposition.Equiv (a b : Proposition Atom) := ⊢[a⫠, b] ∧ ⊢[b⫠, a]

theorem Proposition.foo (h : Proposition.equiv a b) : Proposition.Equiv a b := by
  obtain ⟨p, q⟩ := h
  apply Provable.fromProof at p
  apply Provable.fromProof at q
  constructor <;> assumption

[Fabrizio Montesi]

Note that I'm leaving the symbol ⊨ out of this, since we'll probably wanna use it for semantics.

[Thomas Waring]

Fabrizio Montesi said:

This got me wondering, however: don't we just want the same for equivalences?

yes I agree

Fabrizio Montesi said:

Second, I think we can just use Nonempty for Provable

okay great — I got scared off by the difference (if any) between a Prop and an instance but if it works then absolutely that's better.

[Thomas Waring]

Fabrizio Montesi said:

First of all, I'd like notation to distinguish proof/derivation trees from the proposition that something is provable. I'm using ⇓ for the former and ⊢ for the latter for now.

One small query here — to me ⊢ reads as notation for the sequent itself, though you're right that it's often used to mean "is provable" (maybe in future we can annotate the notation with the system in question, eg CLL ⊢ ...). Would we run into issues once sequents are no longer one-sided (say for ILL)? Something like ⊢ Γ⊢A seems confusing to me.

[Fabrizio Montesi]

Thomas Waring said:

Fabrizio Montesi said:

First of all, I'd like notation to distinguish proof/derivation trees from the proposition that something is provable. I'm using ⇓ for the former and ⊢ for the latter for now.

One small query here — to me ⊢ reads as notation for the sequent itself, though you're right that it's often used to mean "is provable" (maybe in future we can annotate the notation with the system in question, eg CLL ⊢ ...). Would we run into issues once sequents are no longer one-sided (say for ILL)? Something like ⊢ Γ⊢A seems confusing to me.

I started thinking about the same issue, I agree it'll get confusing. Consider also type systems, etc. :\

[Thomas Waring]

Fabrizio Montesi said:

Note that I'm leaving the symbol ⊨ out of this, since we'll probably wanna use it for semantics.

on this, i have soundness & completeness (for tautologies) for Heyting-algebra semantics of IPL

[Fabrizio Montesi]

Re notation:
I should add that it's not that bad, just that it might be a bit confusing and annoying.

If one has two sided sequents, one can define

@[inherit_doc]
scoped notation Γ "⇓" a  => Proof (Γ,a)

Or something like that (similar for the turnstile).

Also, I think turnstile is supposed to mean 'provable', since it's the symbol used to assert/validate a context/sequent (the Gammas).

[Fabrizio Montesi]

I should give another read to Martin Lof's lectures one of these days... :o)
https://ncatlab.org/nlab/files/MartinLofOnTheMeaning96.pdf

[Fabrizio Montesi]

Alright, I've pushed what I have to CLL for now. :)

I'm not sure that this is easy to generalise as typeclasses to share across logics though yet... mmmh... what do you think?

[Thomas Waring]

great, i’ll take a proper look today

given we don’t yet have results that apply to all logics i don’t think there’s much use in setting up typeclasses — probably easier to stick an informal convention to match terminology & notation as much as is appropriate

[Thomas Waring]

if it seems in-scope i can assemble my natural deduction & heyting semantics into a pr? maybe the latter less-so than the former, let me know

[Thomas Waring]

One small difference in our idioms — I've been putting in two results for your one, one def explicitly giving a Proof, then a one-line theorem deriving the Provable version. For example:

/-- Double negation introduction -/
def Derivation.dni {A B : Proposition Atom} : Derivation ⟨{A},impl (impl A B) B⟩ := by
  apply implI (A := A.impl B)
  apply implE (A := A) <;> apply ax' (by grind)

theorem Derivable.dni {A B : Proposition Atom} : Derivable ⟨{A},impl (impl A B) B⟩ :=
  ⟨Derivation.dni⟩

Not sure if we would ever need the added constructivity, but it probably can't hurt?

[Fabrizio Montesi]

Thomas Waring said:

One small difference in our idioms — I've been putting in two results for your one, one def explicitly giving a Proof, then a one-line theorem deriving the Provable version. For example:

/-- Double negation introduction -/
def Derivation.dni {A B : Proposition Atom} : Derivation ⟨{A},impl (impl A B) B⟩ := by
  apply implI (A := A.impl B)
  apply implE (A := A) <;> apply ax' (by grind)

theorem Derivable.dni {A B : Proposition Atom} : Derivable ⟨{A},impl (impl A B) B⟩ :=
  ⟨Derivation.dni⟩

Not sure if we would ever need the added constructivity, but it probably can't hurt?

I agree this is the way to go, I haven't done it like that only because of lack of time.

I really need to start having a system for handling TODO and issues... will come back to that in another thread.

[Fabrizio Montesi]

Thomas Waring said:

if it seems in-scope i can assemble my natural deduction & heyting semantics into a pr? maybe the latter less-so than the former, let me know

Very much in scope, yes! Let's start with the first, I imagine there's a bit of code to review.

Re typeclasses: we could at least have some classes to manage notation, maybe? Like, HasLogicalEquiv, which gives the \equiv notation?

[Thomas Waring]

Great, I'll open a PR sometime today :-) I agree about notation typeclasses, so far I haven't defined any so I'll probably put the PR it as is & add that when appropriate