Declare injectivity on some arguments only

[Gaspi]

This seems to be a better place to discuss the following issue: Deducteam/Dedukti/issues/151

Problem

Consider the following example encoding an even predicate on natural numbers:

// Encoding
symbol const Sort : TYPE
symbol const sets : Sort
symbol const prop : Sort
symbol const Univ : Sort ⇒ TYPE
symbol Term (s : Sort) : Univ s ⇒ TYPE

// Natural
symbol const nat : Univ sets
symbol const Z : Term sets nat
symbol const S : Term sets nat ⇒ Term sets nat
symbol plus : Term sets nat ⇒ Term sets nat ⇒ Term sets nat

// Even predicate
symbol const even : Term sets nat ⇒ Univ prop
// Single constructor
symbol const double_of : ∀ n : Term sets nat, Term prop (even (plus n n))
// Match
symbol match_even :
  ∀ s : Sort,
  ∀ P : (∀ n : Term sets nat, Term prop (even n) ⇒ Univ s),
  (∀ n : Term sets nat, Term s (P (plus n n) (double_of n))) ⇒
  ∀ n : Term sets nat,
  ∀ x : Term prop (even n),
  Term s (P n x)

rule match_even &s &P &case_double &k (double_of &n) → &case_double &n

The last rule is deemed ill-typed by lambdapi even though it doesn't break subject reduction since:

• well-typed instance of the LHS satisfy Term prop (even &k) ≡ Term prop (even (plus &n &n))
• Term is {2}-injective, whenever Term s a ≡ Term s b, we have a ≡ b
• LHS inferred type is Term &s (P &k (double_of &n))
• RHS inferred type is Term &s (P (plus &n &n) (double_of &n))

Solutions

In the full encoding it is not true that Term is injective (Term u0 (lift nat) ≡ Term sets nat with u0 ≢ sets) so using injective definition (symbol injective Term ...) is a bit unsatisfactory as this file would typecheck but so could many illegal rewrite rules.

In order to type check rules of this kind I suggest (at least one of) the following features be implemented:

• S-injectivity declaration (assumed or checked) or inference
• typechecking hints, similar to "brackets" or "dot patterns" implemented in Dedukti
• possibility to extend conversion with unsafe unchecked rewrite rules (rely on paper proof)

Motivation

I'd like to add a lambdapi output to the CoqInE tool but there is no hope to type check its output until this issue is resolved.

[rlepigre]

I think it makes sense to allow "unsafe" rewrite rules, that's a very good idea. I think we should do that first, and they investigate relaxed (but "safe") mechanism for rule SR checking. What do you think @fblanqui?

I would propose the obvious syntax: add an optional unsafe keyword in front of an unsafe rule block declaration.

[fblanqui]

Thanks @Gaspi for your issue. Last week-end, I was thinking in submitting very soon a new PR allowing users to specify in which arguments a symbol is injective. I prefer to do this first, before allowing wilder features.

[Gaspi]

Great, I'm looking forward to it, thanks! As long as it's not too much work to implement I agree that declaring S-injectivity (even unchecked) is the best way to do this.

[fblanqui]

Your example works if you declare Term as injective. For the moment, we cannot declare injectivity on specific arguments.

[dwarfmaster]

Any news on that front ? I'd be very interested by a way to specify injectivity on some arguments only.

[fblanqui]

A possible workaround is to declare a unification rule.