Declare injectivity on some arguments only

Gaspi commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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 commented 4 years ago

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

dwarfmaster commented 3 years ago

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

fblanqui commented 3 years ago

A possible workaround is to declare a unification rule.

Deducteam / lambdapi