Typing fails unexpectedly

[QGarchery]

Hi everyone,

I have trouble understanding why the type inference algorithm fails on some inputs. For example, let's say that we have

constant symbol Term : TYPE
constant symbol Prop : TYPE
symbol prf : Prop ⇒ TYPE

(encoding first order logic, following this example) and we now want to define term equality in this way :

symbol equals : Term ⇒ Term ⇒ Prop
rule prf (equals &x &y) → ∀ P, prf (P &x) ⇒ prf (P &y)

we get :

[...] Cannot solve ?6[?y] ≡ Prop
Cannot solve ?6[?x] ≡ Prop
Unable to prove SR for rule [prf (equals &x &y) → ∀(P:∀(y:Term), ?6[y]), prf (P &x) ⇒ prf (P &y)].

Why is it not possible to unify ?6 with Prop ?

Annotating P with the type Term ⇒ Prop works and is a method that I could use in this particular case. Note, however, that I am interested in the typing algorithm and that my question is about the reason why it fails.

Another example where adding types solves the issue but intuitively we should not have to do so is with the definition of the conjunction :

symbol prop_and : Prop ⇒ Prop ⇒ Prop
rule prf (prop_and &A &B) → ∀ C, (prf &A ⇒  prf &B ⇒  prf C) ⇒ prf C

When trying to prove the following property :

definition and_elim_1 : ∀ A B, prf (prop_and A B) ⇒ prf A
≔  λ A B ab, ab A (λ a _, a)

we get :

[...] The definition of [and_elim_1] or its type have unsolved metavariables.
We have and_elim_1 : ∀(A:Prop) (B:Prop), prf (prop_and A B) ⇒ prf A ≔ λA B ab, ab A (λa _, a).

Why do we have to specify the type of ab ?

[fblanqui]

Hi Quentin.

The current unification algorithm is not very clever, but it is a difficult problem as you may know.

Here, you want to define a rewriting rule containing extra variables wrt the LHS. I am working on this right now. See #328.

When you write rule prf (equals &x &y) → ∀ P, prf (P &x) ⇒ prf (P &y), it in fact means rule prf (equals &x &y) → ∀ P:?X, prf (P &x) ⇒ prf (P &y) where X is some extra (meta) variable. Such a rule is not admissible unless these extra meta variables can be instantiated by some term built from the LHS pattern variables &x and &y here.

As P is applied, ?X can be instantiated by a product type. But because we are in a dependent type theory, this type may be a dependent type ∀z:?A,?B[z]. The problem is then to solve the equation ?B[?x]=Prop where ?x stands for &x, which we don't know how to solve because ?x is not a (bound) variable but a metavariable itself (it could be instantiated as well).

In fact, here, as there is no constraint on ?x, we could probably replace it by a variable x. In which case, we would get the constraint ?B[x]=Prop which is easy to solve.

Frédéric.

[fblanqui]

Duplicate of #303

[QGarchery]

Thank you for your quick and clear answer !

Can you explain why the second example is also not accepted? Now it seems to me that the issue is different : this is not a rewrite rule and we have given the type of ab, it is prf (prop_and A B).

[fblanqui]

Indeed, the second example seems different, although a definition l := r is equivalent to a rule l -> r. I will try to have a look at it tomorrow.

[fblanqui]

Bugs fixed in #303. Should be merged soon.

[QGarchery]

Awesome !

[fblanqui]

Now fixed in master.