avoid nonterminating meta defs

Stream: new members

[Horatiu Cheval]

I am struggling with some termination proofs in some of my definitions, so I decided to work on some later stuff (which depends on those definitions) until I figure them out. So I declared them as meta, and now of course I have to propagate the meta.
Now, I want to write these meta definitions in robust way, such that they will be sound once I finally prove my initial definition is terminating (hopefully, if what I wrote is indeed correct) and I will remove the metas. An immediate problem is that the term being defined is accessible in the context of the definition, as below.

meta def x : ℕ :=
begin
/-
x : ℕ
⊢ ℕ
-/
end

I can remove it by starting with clear x. Is this solution reasonable? I didn't find a way to write something nonterminating or to prove false after starting with this. Are there other tricks to minimize your chance of accidentally writing unsound meta functions?

[Kevin Buzzard]

meta def a : false :=
begin
/-
a: false
⊢ false
-/
end

[Horatiu Cheval]

Sure, but if you first do clear

meta def a : false :=
begin
  clear a,
  -- ⊢ false
end

then are you safe?

[Kevin Buzzard]

I have never written a line of meta code in my life; I'm not the person to ask, sorry :-). All I know is that meta code isn't allowed in the proofs I'm interested in.

[Kevin Buzzard]

Why don't you just use sorry instead of meta? This is what we do in the lean liquid project. If we haven't got the technology to prove a theorem but we know it's true because we're mathematicians, we sorry the proof, and then we can use it in other theorems and come back to it later.

[Eric Wieser]

Note that you can avoid having to propagate the meta if you pass the meta functions as arguments into the non-meta ones

[Eric Wieser]

eg, instead of

meta def foo (a : A) : B := sorry

meta def bar (a : A) : B := foo a + 1

do

meta def foo (a : A) : B := sorry

-- impossible to nonterminate here
def bar_safe (a : A) (foo_ref : A -> B) : B := foo_ref a + 1

meta def bar (a : A) : B := bar_safe foo a

[Horatiu Cheval]

I'm not even really sure where to put the sorrys :) It's about a recursion which lean doesn't believe to be terminating, so I have to use well founded recursion which I am only now beginning to learn, that's why meta seemed like the easiest solution.

[Horatiu Cheval]

Eric Wieser said:

Note that you can avoid having to propagate the meta if you pass the meta functions as arguments into the non-meta ones

Thanks, that's an interesting solution, I'll try that

[Mario Carneiro]

I think rather than using meta for this, you should use a non-meta definition with using_well_founded {dec_tac := \lam _, `[sorry]}

[Mario Carneiro]

because if I understand correctly this is supposed to be a pure definition and it is simply difficult (but not false) to prove termination

[Horatiu Cheval]

That's right, thank you, I managed to sorry it with {dec_tac := `[sorry]}