# Zulip Chat Archive

## Stream: new members

### Topic: Exact too strict?

#### Guilherme Espada (Mar 15 2021 at 11:06):

Given the context:

```
sol : eval (t_if t_cond ?m_1 ?m_2) (t_if condd_w ?m_1 ?m_2)
⊢ eval (t_if t_cond t_l t_r) ?m_3[_]
```

It seems to me that I should be able to solve this using exact sol. However, lean complains with:

```
invalid type ascription, term has type
eval (t_if t_cond ?m_1 ?m_2) (t_if condd_w ?m_1 ?m_2)
but is expected to have type
eval (t_if t_cond t_l t_r) ?m_1[_]
```

I tried to use generalize_hyp, however, I am unsure how to specify the wildcards too.

How can I solve this?

Thanks

#### Kevin Buzzard (Mar 16 2021 at 07:05):

Could you post a #mwe ?

#### Mario Carneiro (Mar 16 2021 at 08:16):

The expression `?m_1[_]`

is called a deferred substitution. It arises when you substitute for a metavariable that isn't known yet. Lean won't unify such goals because they are underdetermined; it's basically like asking the question "solve for `f`

given `f 1 = 2`

"

#### Mario Carneiro (Mar 16 2021 at 08:18):

To solve this you have to unify the metavariable in its original context. An #mwe will help to point out where this is more specifically

#### Guilherme Espada (Mar 16 2021 at 10:10):

I tried to minify the example as much as possible. Nevertheless, I apologize for the size of it:

```
import tactic.suggest
import data.finset
import data.finmap
import data.list
import data.finmap
@[derive decidable_eq]
inductive ttype
| ty_func (l r:ttype): ttype
| ty_bool : ttype
open ttype
instance : inhabited ttype := inhabited.mk ty_bool
@[derive decidable_eq]
inductive term
|t_true : term
|t_false : term
|t_if (cond l r: term): term
open term
instance : inhabited term := inhabited.mk t_true
inductive eval : term → term → Prop
| e_if_true {t2 t3} : eval (t_if t_true t2 t3) (t2)
| e_if_false {t2 t3} : eval (t_if t_false t2 t3) (t3)
| e_if {t1 t1' t2 t3} : eval t1 t1' → eval (t_if t1 t2 t3) (t_if t1' t2 t3)
abbreviation ctxtype := finmap (λ x:string, ttype)
@[simp]
def in_ctx (key: string) (val: ttype) (ctx:ctxtype) := ctx.lookup key = (option.some val)
inductive typ : ctxtype → term → ttype → Prop
| typ_true {ctx} : typ ctx t_true ty_bool
| typ_false {ctx} : typ ctx t_true ty_bool
| typ_if {ctx cond l r T} : typ ctx cond ty_bool -> typ ctx l T -> typ ctx r T -> typ ctx (t_if cond l r) T
def closed : ctxtype → term → Prop
| ctx t_true := true
| ctx t_false := false
| ctx (t_if cond l r) := closed ctx cond ∧ closed ctx l ∧ closed ctx r
def is_value : term → Prop
| t_true := true
| t_false := true
| _ := false
theorem progress {t T} : closed ∅ t → typ ∅ t T → (is_value t) ∨ (∃ t', eval t t') :=
begin
intros cl ty,
induction t generalizing T,
any_goals {
rw is_value,
left,
trivial,
},
all_goals {
right,
},
{
rw closed at cl,
cases cl with cl_t,
cases cl_right,
have cond := t_ih_cond cl_t,
have l := t_ih_l cl_right_left,
have r := t_ih_r cl_right_right,
cases ty,
have condd := cond ty_a,
have ll := l ty_a_1,
have rr := r ty_a_2,
cases condd,
{
sorry,
},
{
split,
cases condd,
have sol:= eval.e_if condd_h,
exact sol, % here
}
}
end
```

The issue arises near the end of the file.

Thanks

#### Mario Carneiro (Mar 16 2021 at 10:41):

I'm getting an error at `ty_a`

, I guess you are using an old version of lean?

#### Mario Carneiro (Mar 16 2021 at 10:43):

The issue is at the `split`

, which you used to destructure an existential without saying what you want to insert for the witness. You should use `use`

or `existsi`

instead and provide the witness

#### Mario Carneiro (Mar 16 2021 at 10:48):

Oh, actually the problem is that you did `split`

and `cases condd`

in the wrong order, meaning that the witness was not introduced into the context until after you needed it. This works (replacing the lines after `have rr`

:

```
rcases condd with hcond | ⟨vcond, hcond⟩,
{ sorry },
{ refine ⟨_, eval.e_if hcond⟩ }
```

#### Guilherme Espada (Mar 16 2021 at 11:04):

Thanks! I was stuck on this one for a while!

#### Guilherme Espada (Mar 16 2021 at 11:09):

In order to upgrade my lean version, do I just need to change the version on my leanpkg.toml?

#### Guilherme Espada (Mar 16 2021 at 11:14):

I guess I had to ask elan to update too, but it seems to work :)

Last updated: May 14 2021 at 00:42 UTC