## Stream: new members

### Topic: avoid nonterminating meta defs

#### Horatiu Cheval (Apr 28 2021 at 19:31):

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 (Apr 28 2021 at 21:05):

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


#### Horatiu Cheval (Apr 28 2021 at 21:14):

Sure, but if you first do clear

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


then are you safe?

#### Kevin Buzzard (Apr 28 2021 at 21:15):

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 (Apr 28 2021 at 21:17):

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 (Apr 28 2021 at 21:19):

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 (Apr 28 2021 at 21:22):

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 (Apr 28 2021 at 21:26):

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 (Apr 28 2021 at 21:31):

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 (Apr 29 2021 at 02:51):

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 (Apr 29 2021 at 02:52):

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 (Apr 29 2021 at 06:35):

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

Last updated: Dec 20 2023 at 11:08 UTC