Equation compiler _main function

Stream: general

[Fabian Glöckle]

Hello everyone,
I am defining a recursive property on expr(precisely, containing something as a subexpression) and want to show it is decidable. In a simplified (dysfunctional) version:

meta def expr.contains (x : expr) : expr → Prop
| (app fn arg) := (expr.contains fn) ∨ (expr.contains arg)
| _ := false

meta instance expr.decidable_contains (x : expr) : ∀ (y : expr), decidable (expr.contains x y)
| (app fn arg) := match (expr.decidable_contains fn, expr.decidable_contains arg) with
                  | (is_true h₁, _) := is_true (or.inl h₁)
                  | (_, is_true h₂) := is_true (or.inr h₂)
                  | (is_false h₁, is_false h₂) := is_false (not_or h₁ h₂)
                  end
| _ := is_false not_false

This gives the following error:

type mismatch at application
  or.inl h₁
term
  h₁
has type
  expr.contains x fn
but is expected to have type
  [expr.contains._main] fn

What is the mistake? It seems to me that the function _main defined by the equation compiler should not leak through at this point, should it?

[Anne Baanen]

This seems suspiciously like the issue I'm debugging. Could you write the following lines above your definition and paste the output?

set_option trace.type_context.smart_unfolding true
set_option trace.type_context.is_def_eq_detail true

[Fabian Glöckle]

For smart_unfolding:

[type_context.smart_unfolding] using simple unfolding [1]
opt_param bool tt
[type_context.smart_unfolding] using simple unfolding [1]
expr.contains x fn
[type_context.smart_unfolding] using simple unfolding [1]
expr.contains._main fn
[type_context.smart_unfolding] using simple unfolding [1]
expr.cases_on fn (λ (a : ℕ), id_rhs Prop false) (λ (a : level), id_rhs Prop false)
  (λ (a_a : name) (a_a_1 : list level), id_rhs Prop false)
  (λ (a_unique a_pretty : name) (a_type : expr), id_rhs Prop false)
  (λ (a_unique a_pretty : name) (a_bi : binder_info) (a_type : expr), id_rhs Prop false)
  (λ (a_a a_a_1 : expr), id_rhs Prop ([expr.contains._main] a_a ∨ [expr.contains._main] a_a_1))
  (λ (a_var_name : name) (a_bi : binder_info) (a_var_type a_body : expr), id_rhs Prop false)
  (λ (a_var_name : name) (a_bi : binder_info) (a_var_type a_body : expr), id_rhs Prop false)
  (λ (a_var_name : name) (a_type a_assignment a_body : expr), id_rhs Prop false)
  (λ (a_a : macro_def) (a_a_1 : list expr), id_rhs Prop false)
[type_context.smart_unfolding] using simple unfolding [1]
expr.contains x (app fn arg)
[type_context.smart_unfolding] using simple unfolding [1]
expr.contains._main (app fn arg)
[type_context.smart_unfolding] using simple unfolding [1]
expr.cases_on (app fn arg) (λ (a : ℕ), id_rhs Prop false) (λ (a : level), id_rhs Prop false)
  (λ (a_a : name) (a_a_1 : list level), id_rhs Prop false)
  (λ (a_unique a_pretty : name) (a_type : expr), id_rhs Prop false)
  (λ (a_unique a_pretty : name) (a_bi : binder_info) (a_type : expr), id_rhs Prop false)
  (λ (a_a a_a_1 : expr), id_rhs Prop ([expr.contains._main] a_a ∨ [expr.contains._main] a_a_1))
  (λ (a_var_name : name) (a_bi : binder_info) (a_var_type a_body : expr), id_rhs Prop false)
  (λ (a_var_name : name) (a_bi : binder_info) (a_var_type a_body : expr), id_rhs Prop false)
  (λ (a_var_name : name) (a_type a_assignment a_body : expr), id_rhs Prop false)
  (λ (a_a : macro_def) (a_a_1 : list expr), id_rhs Prop false)
[...]

[Anne Baanen]

Aha, I think I see what is going on: expr.contains x (app fn arg) should be directly unfolded to (expr.contains fn) ∨ (expr.contains arg), but instead it is unfolded with simple unfolding, going via expr.contains._main, so you end up with (expr.contains._main fn). And expr.contains fn does not match any of the cases, so it is not unfolded any further.

[Floris van Doorn]

The problem here is that expr.contains is a meta definition, and that for meta definitions, the right equations are not generated.

If I write this:

meta instance expr.decidable_contains (x : expr) : ∀ (y : expr), decidable (expr.contains x y)
| (app fn arg) := match (expr.decidable_contains fn, expr.decidable_contains arg) with
                  | (is_true h₁, _) := is_true begin unfold expr.contains, end
                  | (_, is_true h₂) := is_true (or.inr h₂)
                  | (is_false h₁, is_false h₂) := is_false (not_or h₁ h₂)
                  end
| _ := is_false not_false

then we see the error message

unfold tactic failed, expr.contains does not have equational lemmas nor is a projection

If I make everything non-meta, then the error disappears.

inductive my_expr
| var      {} : nat → my_expr
| mvar        : name → name → my_expr → my_expr
| local_const : name → name → binder_info → my_expr → my_expr
| app         : my_expr → my_expr → my_expr
| lam         : name → binder_info → my_expr → my_expr → my_expr
| pi          : name → binder_info → my_expr → my_expr → my_expr
| elet        : name → my_expr → my_expr → my_expr → my_expr

open my_expr

def my_expr.contains (x : my_expr) : my_expr → Prop
| (app fn arg) := my_expr.contains fn ∨ my_expr.contains arg
| _ := false

instance my_expr.decidable_contains (x : my_expr) : ∀ (y : my_expr), decidable (my_expr.contains x y)
| (app fn arg) := match (my_expr.decidable_contains fn, my_expr.decidable_contains arg) with
                  | (is_true h₁, _) := is_true (or.inl h₁)
                  | (_, is_true h₂) := is_true (or.inr h₂)
                  | (is_false h₁, is_false h₂) := is_false (not_or h₁ h₂)
                  end
| _ := is_false sorry

Lean doesn't really support proving anything about meta defs.

[Reid Barton]

The Coq users will say you should just write meta def expr.contains (x : expr) : expr -> bool in the first place

[Fabian Glöckle]

For is_def_eq_detail:

[...]
[type_context.is_def_eq_detail] [1]: expr.contains x fn =?= [expr.contains._main] fn
[type_context.is_def_eq_detail] unfold left: expr.contains
[type_context.is_def_eq_detail] [2]: expr.contains._main fn =?= [expr.contains._main] fn
[type_context.is_def_eq_detail] unfold left: expr.contains._main
[type_context.is_def_eq_detail] [3]: expr.cases_on fn (λ (a : ℕ), id_rhs Prop false) (λ (a : level), id_rhs Prop false)
  (λ (a_a : name) (a_a_1 : list level), id_rhs Prop false)
  (λ (a_unique a_pretty : name) (a_type : expr), id_rhs Prop false)
  (λ (a_unique a_pretty : name) (a_bi : binder_info) (a_type : expr), id_rhs Prop false)
  (λ (a_a a_a_1 : expr), id_rhs Prop ([expr.contains._main] a_a ∨ [expr.contains._main] a_a_1))
  (λ (a_var_name : name) (a_bi : binder_info) (a_var_type a_body : expr), id_rhs Prop false)
  (λ (a_var_name : name) (a_bi : binder_info) (a_var_type a_body : expr), id_rhs Prop false)
  (λ (a_var_name : name) (a_type a_assignment a_body : expr), id_rhs Prop false)
  (λ (a_a : macro_def) (a_a_1 : list expr), id_rhs Prop false) =?= [expr.contains._main] fn
[type_context.is_def_eq_detail] after whnf_core: expr.rec (λ (a : ℕ), (λ (a : ℕ), id_rhs Prop false) a) (λ (a : level), (λ (a : level), id_rhs Prop false) a)
  (λ (a : name) (a_1 : list level), (λ (a_a : name) (a_a_1 : list level), id_rhs Prop false) a a_1)
  (λ (unique pretty : name) (type : expr) (ih : (λ (a : expr), Prop) type),
     (λ (a_unique a_pretty : name) (a_type : expr), id_rhs Prop false) unique pretty type)
  (λ (unique pretty : name) (bi : binder_info) (type : expr) (ih : (λ (a : expr), Prop) type),
     (λ (a_unique a_pretty : name) (a_bi : binder_info) (a_type : expr), id_rhs Prop false) unique pretty bi type)
  (λ (a a_1 : expr) (ih_a : (λ (a : expr), Prop) a) (ih_a : (λ (a : expr), Prop) a_1),
     (λ (a_a a_a_1 : expr), id_rhs Prop ([expr.contains._main] a_a ∨ [expr.contains._main] a_a_1)) a a_1)
  (λ (var_name : name) (bi : binder_info) (var_type body : expr) (ih_var_type : (λ (a : expr), Prop) var_type)
   (ih_body : (λ (a : expr), Prop) body),
     (λ (a_var_name : name) (a_bi : binder_info) (a_var_type a_body : expr), id_rhs Prop false) var_name bi var_type
       body)
  (λ (var_name : name) (bi : binder_info) (var_type body : expr) (ih_var_type : (λ (a : expr), Prop) var_type)
   (ih_body : (λ (a : expr), Prop) body),
     (λ (a_var_name : name) (a_bi : binder_info) (a_var_type a_body : expr), id_rhs Prop false) var_name bi var_type
       body)
  (λ (var_name : name) (type assignment body : expr) (ih_type : (λ (a : expr), Prop) type)
   (ih_assignment : (λ (a : expr), Prop) assignment) (ih_body : (λ (a : expr), Prop) body),
     (λ (a_var_name : name) (a_type a_assignment a_body : expr), id_rhs Prop false) var_name type assignment body)
  (λ (a : macro_def) (a_1 : list expr), (λ (a_a : macro_def) (a_a_1 : list expr), id_rhs Prop false) a a_1)
  fn =?= [expr.contains._main] fn
[type_context.is_def_eq_detail] [4]: expr.rec =?= [expr.contains._main]
[type_context.is_def_eq_detail] on failure: expr.rec =?= [expr.contains._main]
[type_context.is_def_eq_detail] on failure: expr.rec (λ (a : ℕ), (λ (a : ℕ), id_rhs Prop false) a) (λ (a : level), (λ (a : level), id_rhs Prop false) a)
  (λ (a : name) (a_1 : list level), (λ (a_a : name) (a_a_1 : list level), id_rhs Prop false) a a_1)
  (λ (unique pretty : name) (type : expr) (ih : (λ (a : expr), Prop) type),
     (λ (a_unique a_pretty : name) (a_type : expr), id_rhs Prop false) unique pretty type)
  (λ (unique pretty : name) (bi : binder_info) (type : expr) (ih : (λ (a : expr), Prop) type),
     (λ (a_unique a_pretty : name) (a_bi : binder_info) (a_type : expr), id_rhs Prop false) unique pretty bi type)
  (λ (a a_1 : expr) (ih_a : (λ (a : expr), Prop) a) (ih_a : (λ (a : expr), Prop) a_1),
     (λ (a_a a_a_1 : expr), id_rhs Prop ([expr.contains._main] a_a ∨ [expr.contains._main] a_a_1)) a a_1)
  (λ (var_name : name) (bi : binder_info) (var_type body : expr) (ih_var_type : (λ (a : expr), Prop) var_type)
   (ih_body : (λ (a : expr), Prop) body),
     (λ (a_var_name : name) (a_bi : binder_info) (a_var_type a_body : expr), id_rhs Prop false) var_name bi var_type
       body)
  (λ (var_name : name) (bi : binder_info) (var_type body : expr) (ih_var_type : (λ (a : expr), Prop) var_type)
   (ih_body : (λ (a : expr), Prop) body),
     (λ (a_var_name : name) (a_bi : binder_info) (a_var_type a_body : expr), id_rhs Prop false) var_name bi var_type
       body)
  (λ (var_name : name) (type assignment body : expr) (ih_type : (λ (a : expr), Prop) type)
   (ih_assignment : (λ (a : expr), Prop) assignment) (ih_body : (λ (a : expr), Prop) body),
     (λ (a_var_name : name) (a_type a_assignment a_body : expr), id_rhs Prop false) var_name type assignment body)
  (λ (a : macro_def) (a_1 : list expr), (λ (a_a : macro_def) (a_a_1 : list expr), id_rhs Prop false) a a_1)
  fn =?= [expr.contains._main] fn
[...]

[Anne Baanen]

If I understand the elaborator correctly, you might still be able make your original definition work by first rewriting using a lemma of the form

meta lemma trick_the_unfolder : expr.contains = expr.contains._main := rfl

(since non-applied recursive definitions don't use the smart rewriter)

[Fabian Glöckle]

I see, thank you all

[Fabian Glöckle]

So I assume if I want to use list.anyon this, I will directly make it a -> bool function instead of proving decidabilty (like the Coq user says :D ).

[Mario Carneiro]

Reid Barton said:

The Coq Lean 4 users will say you should just write meta def expr.contains (x : expr) : expr -> bool in the first place

I fixed your quote. I think the stance on this has changed in lean 4