# Zulip Chat Archive

## Stream: new members

### Topic: Compound statment to admit second goal of have

#### Ken Roe (Jul 21 2018 at 16:38):

I tried the following to do a "have" and admit the second goal. What is the correct syntax:

theorem dummy (n :ℕ) : n = 3 := begin have h:n=1+2;(skip|admit) end

#### Kevin Buzzard (Jul 21 2018 at 16:40):

theorem dummy (n :ℕ) : n = 3 := begin have h:n=1+2, { -- here we only see the first goal sorry }, { -- here we only see the second goal sorry } end

Is that what you mean?

#### Ken Roe (Jul 21 2018 at 16:41):

thanks

#### Kevin Buzzard (Jul 21 2018 at 16:42):

No problem. Note that the `have h: ...`

turns one goal `G`

into two goals -- first the proof of `h`

, and second the proof of `G`

assuming `h`

(in addition to anything else which we were assuming when we wrote the `have`

).

If you would rather have the goals the other way around, you can use `suffices`

:-)

#### Ken Roe (Jul 21 2018 at 16:45):

Actually, I tried the following:

theorem dummy (n :ℕ) : n = 3 := begin have h:n=1+2,{ skip },{ admit }, end

I would like to end up in a state where only the first goal is open and the second goal is solved.

#### Mario Carneiro (Jul 21 2018 at 16:47):

Since `n = 3`

and `n = 1 + 2`

are definitionally the same goal, you can use `change`

:

theorem dummy (n :ℕ) : n = 3 := begin change n = 1 + 2, end

#### Mario Carneiro (Jul 21 2018 at 16:49):

If the transformation from one goal to the other is not definitional but easy, you can use `suffices`

:

theorem dummy (n :ℕ) : n = 3 := begin suffices h : n = 1 + 2, {exact h}, end

#### Kevin Buzzard (Jul 21 2018 at 16:54):

Here are some more tips. If you have two goals, you can use `tactic.swap`

to switch them. If you have more than one goal and you want to work on one of them, you can write `show <statement of goal>`

and it will switch this goal to the top. One of my students was even telling me about some sort of `rotate`

tactic but I've never used it.

#### Mario Carneiro (Jul 21 2018 at 16:55):

the mathlib `swap`

tactic takes an optional argument; `swap n`

moves the nth goal to the top

#### Ken Roe (Jul 21 2018 at 17:05):

Igt appears "have h:a, swap, admit" does what I want. Now, I want to figure out something more complex:

open tactic open monad open expr open smt_tactic def andFuns (a : ℕ → Prop) (b : ℕ → Prop) : ℕ → Prop := (λ q, (a q) ∧ (b q)). def existsFuns {t : Type} (a : t → ℕ → Prop) : ℕ → Prop := (λ n, (∃ (e:t), a e n). def test := (λ x, x > 3) def test2 := (λ x, x < 8) theorem test1 (v: ℕ) : (λ (e:ℕ), (andFuns test test2) (v+1)) v := begin have h: (andFuns (λ (e:ℕ), test e) (λ (e:ℕ), test2 e)) v, swap,admit, end

In the above theorem, I would like to create a tactic that automates the conversion of "(λ (e:ℕ), (andFuns test test2) (v+1)) v" to "h(andFuns (λ (e:ℕ), test e) (λ (e:ℕ), test2 e)) v".

I have created the following meta tactic which has many syntax errors. How do I correct the errors:

meta def divide_lambda : name → binder_info → expr → expr → expr → expr → expr | n b e1 ``(andFuns %%l %%r) v y := (app (app `(andFuns) (divide_lambda n b e1 l v y)) (divide_lambda n b e1 r v y)) | n b e1 x y v := (app (lam n b e1 (app x y)) v). meta def transform_lambda_app : expr → option expr | (app (lam n b e1 (app x y)) val) := some (divide_lambda n b eq x y val) | _ := none. meta def split_lambda : tactic unit := do { t ← target, nt ← transform_lambda_app t, (have h:nt;swap;admit) }.

#### Mario Carneiro (Jul 21 2018 at 17:16):

I'm confused - `(λ (e:ℕ), (andFuns test test2) (v+1)) v`

and `h(andFuns (λ (e:ℕ), test e) (λ (e:ℕ), test2 e)) v`

are not the same

#### Mario Carneiro (Jul 21 2018 at 17:16):

are the `v`

supposed to be de bruijn variables?

#### Ken Roe (Jul 21 2018 at 17:21):

I didn't state the theorem quite right:

theorem test1 (v: ℕ) : (λ (e:ℕ), (andFuns test test2) (e+1)) v := begin have h: (andFuns (λ (e:ℕ), test (e+1)) (λ (v:ℕ), test2 (e+1))) v, swap,admit, end

Hopefully this make more sense.

#### Mario Carneiro (Jul 21 2018 at 17:24):

You should be able to use `change`

instead of `swap, admit`

if you got it right

#### Mario Carneiro (Jul 21 2018 at 17:25):

theorem test1 (v: ℕ) : (λ (e:ℕ), (andFuns test test2) (e+1)) v := begin change (andFuns (λ (e:ℕ), test (e+1)) (λ (e:ℕ), test2 (e+1))) v, end

#### Mario Carneiro (Jul 21 2018 at 17:28):

Here is fixing the syntax errors, although it doesn't work yet:

meta def divide_lambda : name → binder_info → expr → expr → expr → expr → expr | n b e1 `(andFuns %%l %%r) v y := (app (app `(andFuns) (divide_lambda n b e1 l v y)) (divide_lambda n b e1 r v y)) | n b e1 x y v := (app (lam n b e1 (app x y)) v). meta def transform_lambda_app : expr → option expr | (app (lam n b e1 (app x y)) val) := some (divide_lambda n b e1 x y val) | _ := none. meta def split_lambda : tactic unit := do { t ← target, nt ← transform_lambda_app t, change nt } theorem test1 (v: ℕ) : (λ (e:ℕ), (andFuns test test2) (e+1)) v := begin split_lambda, end

#### Ken Roe (Jul 21 2018 at 17:30):

It looks like change works. The theorem looks like this now:

theorem test1 (v: ℕ) : (λ (e:ℕ), (andFuns test test2) (e+1)) v := begin change (andFuns (λ (e:ℕ), test (e+1)) (λ (e:ℕ), test2 (e+1))) v, end

Now the challenge is to get the tactic working that generates the expression. The tactic code now looks like this:

meta def divide_lambda : name → binder_info → expr → expr → expr → expr → expr | n b e1 ``(andFuns %%l %%r) v y := (app (app `(andFuns) (divide_lambda n b e1 l v y)) (divide_lambda n b e1 r v y)) | n b e1 x y v := (app (lam n b e1 (app x y)) v). meta def transform_lambda_app : expr → option expr | (app (lam n b e1 (app x y)) val) := some (divide_lambda n b eq x y val) | _ := none. meta def split_lambda : tactic unit := do { t ← target, nt ← transform_lambda_app t, (change nt) }.

I'm getting the error "invalid pattern, must be an application, constant, variable, type ascription, aliasing pattern or inaccessible term" in divide_lambda on the pattern "n b e1 ``(andFuns %%l %%r) v y".

#### Mario Carneiro (Jul 21 2018 at 17:32):

use single backtick on line 2

#### Mario Carneiro (Jul 21 2018 at 17:34):

For me the tactic fails in `transform_lambda_app`

because right after the `begin`

the goal says `⊢ andFuns test test2 (v + 1)`

so there is no lambda in sight

#### Mario Carneiro (Jul 21 2018 at 17:35):

I wasn't aware of this - it looks like lean is really eager to unfold raw lambda-app beta reductions

#### Mario Carneiro (Jul 21 2018 at 17:39):

I'm not exactly sure what your goal is; perhaps this is a suitable compromise:

theorem test1 (v: ℕ) : id (λ (e:ℕ), (andFuns test test2) (e+1)) v := begin -- split_lambda, change id (andFuns (λ (e:ℕ), test (e+1)) (λ (e:ℕ), test2 (e+1))) v, end

#### Mario Carneiro (Jul 21 2018 at 17:45):

This works, with the `id`

to protect the lambda at the start:

meta def divide_lambda : name → binder_info → expr → expr → expr → expr | n b e1 `(andFuns %%l %%r) y := (app (app `(andFuns) (divide_lambda n b e1 l y)) (divide_lambda n b e1 r y)) | n b e1 x y := (lam n b e1 (app x y)) meta def transform_lambda_app : expr → option expr | (app (lam n b e1 (app x y)) val) := some (app (divide_lambda n b e1 x y) val) | (app `(id %%(lam n b e1 (app x y))) val) := some (app (divide_lambda n b e1 x y) val) | _ := none meta def split_lambda : tactic unit := do { t ← target, trace t.to_raw_fmt, nt ← transform_lambda_app t, change nt } theorem test1 (v: ℕ) : id (λ (e:ℕ), (andFuns test test2) (e+1)) v := begin split_lambda, end

#### Ken Roe (Jul 21 2018 at 19:13):

Thanks--Now for the next trick, I would like to extend split_lambda to be able to propagate an expression into a closure. Note that now, the tactic may need to rename variables,

def existsFuns {t : Type} (a : t → ℕ → Prop) : ℕ → Prop := (λ n, (∃ (e:t), a e n)). theorem capture (v: ℕ) (q : ℕ) : id (λ (e:ℕ), (andFuns (existsFuns (λ (x y : ℕ), x = y)) test) (e+q)) v := begin change andFuns (existsFuns (λ (x e : ℕ), (λ y, x=y) (e+q))) (λ (e:ℕ), test (e + q)) v, end

Notice how the (e+q) is propagated inside a closure involving "x". The variable may in some cases need to be renamed. Is there a way to get a fresh variable name and to rename the variables when reconstructing lambda expressions?

end

#### Mario Carneiro (Jul 21 2018 at 19:39):

You don't have to worry about variable capture for the most part. Lean uses unique names in all lambdas, so it shouldn't be a problem

#### Mario Carneiro (Jul 21 2018 at 19:41):

The tactics `mk_fresh_name`

and `get_unused_name`

can be used to generate unique and human-readable names respectively

#### Ken Roe (Jul 21 2018 at 20:55):

OK--I've updated my tactic. It looks like this now:

meta def divide_lambda : name → binder_info → expr → expr → expr → expr | n b e1 `(andFuns %%l %%r) y := (app (app `(andFuns) (divide_lambda n b e1 l y)) (divide_lambda n b e1 r y)) | n b e1 `(existsFuns (λ (v:ℕ), %%ll)) y := (app `(existsFuns (λ (v:ℕ), %%(divide_lambda n b e1 ll y)))) | n b e1 x y := (lam n b e1 (app x y)) meta def transform_lambda_app : expr → option expr | (app (lam n b e1 (app x y)) val) := some (app (divide_lambda n b e1 x y) val) | (app `(id %%(lam n b e1 (app x y))) val) := some (app (divide_lambda n b e1 x y) val) | _ := none meta def split_lambda : tactic unit := do { t ← target, trace t.to_raw_fmt, nt ← transform_lambda_app t, trace nt.to_raw_fmt, change nt }

I' trying to use it in this theorem:

theorem capture (v: ℕ) (q : ℕ) : id (λ (e:ℕ), (andFuns (existsFuns (λ x:ℕ, test3 x)) test) (e+q)) v := begin split_lambda, --change -- andFuns (existsFuns (λ (y e:ℕ), test3 y (e+q))) -- (λ (e:ℕ), test (e + q)) v, end

It seems like no output goal is being generated. I suspect the tactic is crashing somehow. Is the pattern matching being done properly in divide_lambda?

#### Mario Carneiro (Jul 21 2018 at 21:01):

I get an error `trying to evaluate sorry`

in the test theorem, which means that there is a syntax error in the tactic

#### Mario Carneiro (Jul 21 2018 at 21:02):

and the error at `divide_lambda`

says the `existsFuns`

branch has incorrect type `expr -> expr`

instead of `expr`

#### Mario Carneiro (Jul 21 2018 at 21:02):

because you used `expr.app`

applied to only one argument

#### Ken Roe (Jul 21 2018 at 21:33):

OK-- I fixed divide_lambda

meta def divide_lambda : name → binder_info → expr → expr → expr → expr | n b e1 `(andFuns %%l %%r) y := (app (app `(andFuns) (divide_lambda n b e1 l y)) (divide_lambda n b e1 r y)) | n b e1 `(existsFuns (λ (v:ℕ), %%ll)) y := `(existsFuns (λ (v:ℕ), %%(divide_lambda n b e1 ll y))) | n b e1 x y := (lam n b e1 (app x y))

but I get the error:

tactic.change failed, given type andFuns (existsFuns (λ (v e : ℕ), test3 e (e + q))) (λ (e : ℕ), test (e + q)) v is not definitionally equal to id (λ (e : ℕ), andFuns (existsFuns (λ (x : ℕ), test3 x)) test (e + q)) v

It appears the bound variable "x" is being changed to "e". Why is this happening? It appears the capture mechanism is not naming variables properly.

Last updated: May 08 2021 at 19:11 UTC