Zulip Chat Archive

Stream: new members

Topic: Exact too strict?


view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 07:05):

Could you post a #mwe ?

view this post on Zulip 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"

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 }

view this post on Zulip Guilherme Espada (Mar 16 2021 at 11:04):

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

view this post on Zulip 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?

view this post on Zulip 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