implies vs forall

Stream: general

[Frédéric Le Roux]

In tactic programming, what would be the proper way to distinguish, among Pi expressions, between → - expressions (mathematical implications) and ∀- expressions ?

For the moment I test if to_string estarts with "Pi" (which is tt in the ∀ case but not in the → case), but this is bad...

[Simon Hudon]

Syntactically, the difference is that the implication is a ∀ x : P, Q where x does not appear free in Q. You can test for that

[Simon Hudon]

But are you sure you actually need to tell them apart?

[Frédéric Le Roux]

Yes, that's what I need. So do I have to go through Q and test if there is a free variable with the corresponding De Bruijn index? Or is there a more direct way?

[Jason Rute]

@Frédéric Le Roux These examples might help clarify Simon's point.

#check ∀ x : ℕ , x = x      -- ∀ (x : ℕ), x = x : Prop
#check ∀ x : ℕ , 1 = 1      -- ℕ → 1 = 1 : Prop
#check ∀ h : 0 = 1 , h = h  -- ∀ (h : 0 = 1), h = h : Prop
#check ∀ h : 0 = 1 , 1 = 2  -- 0 = 1 → 1 = 2 : Prop

Without knowing your use case it might be that you are actually trying to distinguish if the quantifier is quantifying over proofs in a Prop, like ∀ h : 0 = 1 vs. quantifying over elements in a type. There is a strong correlation between quantifying over proofs and getting pretty printed with a →, because usually one uses a Prop p as a hypothesis and doesn't care about the particular proof/witness h : p. And conversely, if you are quantifying over say a natural number x : ℕ, then you care about that particular number usually or you would just drop that assumption.

[Floris van Doorn]

I think e.is_pi \and \not e.is_arrow does this.

[Frédéric Le Roux]

It is really a semantic issue: I would like to distinguish between implications and universal quantifiers, as we usually do in maths.
Thanks Jason for clarifying. @Floris van Doorn At first I thought is_arrow ewas what I needed, but actually it just tests first if e is a Pi expression and then, writing e = ∀ x : P, Q, if Q has free variables. But as Simon put it, the problem is not just to know if Q has free variables but if it has x as a (free) variable.

[Frédéric Le Roux]

As Jason said, the pretty printer has a way to distinguish, but I don't find something useful in the expr file.

[Floris van Doorn]

I still don't understand. Normally, whenever you have expression, it does not contain bound variables (expr.var), unless you have already chopped of some Pi's/lambda's from it before, without substituting in the variables.

Therefore, I think that e.is_arrow does what you want. In the example below it correctly states that e is an arrow (even though it contains the variable y). Do you have an expression where there the e.is_arrow check doesn't do what you want?

open tactic
example (y : ℕ) : true :=
by do e ← to_expr ```(∀ x : ℕ, y = 1), trace e, trace e.is_arrow, trace e.is_pi

If your expression contains other de Bruijn variables (which usually shouldn't happen), then you can make your own definition of is_arrow that checks for has_var_idx 0 instead of has_var.

[Frédéric Le Roux]

Floris van Doorn said:

Do you have an expression where there the e.is_arrow check doesn't do what you want?

This happens because I do a recursive analysis of some expr, so I get sub-expressions with some unreplaced varin them.
I will try using has_var_idx 0, thanks!

[Frédéric Le Roux]

The following seems to work :-) :

| `(%%P → %%Q) := if has_var_idx Q 0 then return ff else return tt
| _ := return ff

[Mario Carneiro]

that implementation looks like it doesn't need to be a tactic

[Mario Carneiro]

This happens because I do a recursive analysis of some expr, so I get sub-expressions with some unreplaced varin them.
I will try using has_var_idx 0, thanks!

The expected way to do this sort of thing is to instantiate the variable as you go under a binder

[Floris van Doorn]

The expected way to do this sort of thing is to instantiate the variable as you go under a binder

Indeed. To elaborate on this, you want to use something like mk_local_pis (or implement something similar yourself):

open tactic
example : true :=
by do e ← to_expr ```(∀ y : ℕ, y = 1), (es, tgt) ← mk_local_pis e, trace e, trace es, trace tgt

[Frédéric Le Roux]

I needed to instanciate also in lam expression, so I came with the following.

meta def instanciate (e : expr) : tactic expr :=
match e with
| (pi pp_name binder type body) := do
    a ← mk_local' pp_name binder type,
    return $ instantiate_var body a
| (lam pp_name binder type body) := do
    a ← mk_local' pp_name binder type,
    return $ instantiate_var body a
| _ := return e
end

I hope that it works. It is great to find help here, anyway!