Exact too strict?

Stream: new members

[Guilherme Espada]

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]

Could you post a #mwe ?

[Mario Carneiro]

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]

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]

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]

I'm getting an error at ty_a, I guess you are using an old version of lean?

[Mario Carneiro]

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]

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]

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

[Guilherme Espada]

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

[Guilherme Espada]

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