hypothesis can't be used

Stream: lean4

[Arthur Paulino]

Hi! I want to apologize upfront for yet-another-long-mwe, but this time I am not being able to use a hypothesis in my context with simp or rw

https://gist.github.com/arthurpaulino/22807b35054a638838974b73ad789315

The issue is that h' can't be used on lines 394 and 395. I'm not entirely sure if I'm doing something wrong, but I suspect this should have worked

Thanks in advance for your attention :pray:

[Leonardo de Moura]

The following threads should clarify what is going on
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Circumventing.20.22motive.20not.20type-correct.22
https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Cannot.20rewrite.20term.20being.20cased.20on

[Leonardo de Moura]

To minimize the problem, we have to change how we encode the match h : ... with ... notation. It will happen, but not in the near future.

[Arthur Paulino]

Ah, alright, thanks!!
Let me read those :+1:

[Leonardo de Moura]

The second one is the most relevant.

[James Gallicchio]

Both those topics are mine, and I'm still pretty lost about how to do the right generalization -- maybe we can learn how to work around this together @Arthur Paulino :joy:

[Arthur Paulino]

Sure, from what I understood, I have to manually provide a motive for my consume function (and I don't know what a motive is yet). Now that Leo has pointed out the root cause of the issue, I'll try to minimize my #mwe later and work on it. For now I'll just sorry that part out

[Arthur Paulino]

@James Gallicchio how far are you on the investigation?

[James Gallicchio]

Oh, actually, your case is maybe simple to solve, lemme try to fill this sorry in...

[Julian Berman]

Arthur Paulino said:

Sure, from what I understood, I have to manually provide a motive for my consume function (and I don't know what a motive is yet). Now that Leo has pointed out the root cause of the issue, I'll try to minimize my #mwe later and work on it. For now I'll just sorry that part out

Off-topic, but I don't know what a motive is precisely either yet, even though I know it's present in a particularly common Lean 3 error message. If you get a good handle on what one is, the glossary would benefit from having an entry for it!

[James Gallicchio]

I think a motive is a (potentially dependent) type which a recursor is eliminating into. The "target" type of a recursion/induction. So for inductive arguments trying to prove \forall n. P(n), the P is the motive. Or for a recursive function from MyType to Nat, the motive is fun (_ : MyType) => Nat

[James Gallicchio]

James Gallicchio said:

Oh, actually, your case is maybe simple to solve, lemme try to fill this sorry in...

after spending 15 min on this i give up :joy: but it seems quite similar to the example Mario solved here

[Mario Carneiro]

Here's a fix for this proof:

theorem State.retProgression :
    ∃ n, (ret v c k^[n]).isEnd ∨ (ret v c k^[n]).isProg := by
  induction k generalizing v c with
  | app e es k hi =>
    cases v with
    | lam lm =>
      cases lm with
      | mk ns h p =>
        cases h' : consume p ns es with
        | none =>
          refine ⟨1, ?_⟩
          simp [stepN, step, h']
          let isOk := fun (s : State) => s.isEnd ∨ s.isProg
          suffices ∀ o h, o = none →
            isOk (step.match_2 _ _ _ (fun x h' => State) o h _ _ _) from this _ rfl h'
          intro o h h2; subst h2; simp
          sorry
        | some x =>
          sorry
    | _ => exact ⟨1, sorry⟩
  | _ => sorry

[Arthur Paulino]

I don't understand that yet, but it gives me the errors:

application type mismatch
  match ?m.40719 with
  | Except.error m => ?m.40720 m
  | Except.ok x => fun h' => State
argument
  fun x h' => State
has type
  (x : Value) → ?m.40727 x → Type : Sort (max 2 ?u.40724)
but is expected to have type
  (v : Value) → ?m.40718 (Except.ok v) : Sort (imax 1 ?u.40717)

And

function expected at
  match ?m.40719 with
  | Except.error m => ?m.40720 m
  | Except.ok v => ?m.40752 v
term has type
  ?m.40718 ?m.40719

Thanks for helping out :pray:

[Mario Carneiro]

It looks like some of the captured variables are different, try moving the (fun x h' => State) argument earlier

[Mario Carneiro]

Here's the type of State.step.match_2 for me:

#check @State.step.match_2

State.step.match_2 : (es : NEList Expression) →
  (ns : NEList String) →
    (p : Program) →
      (motive : (x : Option (Option (NEList String) × Program)) → consume p ns es = x → Sort u_1) →
        (x : Option (Option (NEList String) × Program)) →
          (h' : consume p ns es = x) →
            ((l : NEList String) →
                (p_1 : Program) → (h' : consume p ns es = some (some l, p_1)) → motive (some (some l, p_1)) h') →
              ((p_1 : Program) → (h' : consume p ns es = some (none, p_1)) → motive (some (none, p_1)) h') →
                ((h' : consume p ns es = none) → motive none h') → motive x h'

[Mario Carneiro]

I obtained the term in the suffices by setting set_option pp.match false and then locating the (fun x h' => State) (this is motive), (consume p ns es) (which is o) and (_ : consume p ns es = consume p ns es) (which is h) arguments in the match expression in the goal

[Mario Carneiro]

I expect there is some lean version mismatch that has caused things to work out differently for you

[Mario Carneiro]

I'm running Lean (version 4.0.0-nightly-2022-04-16, commit 726b735c6df7, Release)

[Arthur Paulino]

I'm using today's nightly. Will check that soon!

[Arthur Paulino]

#check @State.step.match_2
-- State.step.match_2 : (motive : Except String Value → Sort u_1) →
--   (x : Except String Value) → ((m : String) → motive (Except.error m)) → ((v : Value) → motive (Except.ok v)) → motive x

[James Gallicchio]

Once again consulting the Mario oracle to find the correct chant of generalization to proceed in a proof:

constant UninitPointed.{u} (α : Type u) : NonemptyType.{u}

def Uninit.{u} (α : Type u) : Type u := (UninitPointed α).type

namespace Uninit

instance : Nonempty (Uninit α) := (UninitPointed α).property

unsafe def uninitUnsafe {α} : Uninit α := unsafeCast ()
@[implementedBy uninitUnsafe]
constant uninit {α} : Uninit α

unsafe def initUnsafe (a : α) : Uninit α := unsafeCast a
@[implementedBy initUnsafe]
constant init (a : α) : Uninit α

instance : Inhabited (Uninit α) := ⟨uninit⟩

noncomputable constant getValue? : Uninit α → Option α

def ofOption : Option α → Uninit α
| none => uninit
| some a => init a

axiom getValue_ofOption : ∀ {α} (a : Option α), getValue? (ofOption a) = a
axiom ofOption_getValue : ∀ {α} (a : Uninit α), ofOption (getValue? a) = a

noncomputable def isInit (a : Uninit α) : Bool := Option.isSome (getValue? a)

unsafe def getValueUnsafe (a : Uninit α) (h : (getValue? a).isSome) : α := unsafeCast a

@[implementedBy getValueUnsafe]
def getValue (a : Uninit α) (h : (getValue? a).isSome) : α :=
  match getValue? a, h with
  | some a, h => a
  | none, h => by contradiction

set_option pp.match false

@[simp]
theorem getValue_init (h) : (init a).getValue h = a := by
  unfold getValue
  unfold getValue.match_1
  sorry

[James Gallicchio]

I will attempt a few more random generalizations in the meantime

[Leonardo de Moura]

Here is an option using the generalize tactic

@[simp]
theorem getValue_init (h) : (init a).getValue h = a := by
  unfold getValue
  generalize h' : getValue? (init a) = x, h = hx
  split
  next a h => sorry
  next => contradiction

[Leonardo de Moura]

The notation h = hx is a bit cryptic, but it is there because the type of h depends on getValue? (init a). We should add a better notation for this.

[Leonardo de Moura]

We can also use h = h, but it looks even more cryptic. BTW, the use of = in the generalize tactic is also a bit misleading. Any suggestions on how to improve this notation?

[Mario Carneiro]

Aside: Any chance generalize can support at? Mathlib has a generalize_hyp command which does not do anything except this relatively straightforward generalization

[Leonardo de Moura]

Mario Carneiro said:

Aside: Any chance generalize can support at? Mathlib has a generalize_hyp command which does not do anything except this relatively straightforward generalization

Yes, we can add support for at.

[Mario Carneiro]

Is that h = hx syntax new in lean 4 generalize? I don't recognize it from lean 3

[Leonardo de Moura]

generalize in Lean 4 can take a telescope and simultaneously generalize many terms.

[Mario Carneiro]

how about hx := h instead of h = hx?

[Mario Carneiro]

the = is backwards but I think we have precedent for using hx := <- h at this point if we want it the other way around

[Mario Carneiro]

ah crap, maybe that doesn't work as well in lean 4 since that's actually an expression

[Mario Carneiro]

I suppose you can parse the arrow anyway, rw does that too

[Leonardo de Moura]

What about the fact that the types of h and hx are different?

[Mario Carneiro]

oh I see... (x, h) := (e1, e2)? Possibly without parens too

[Mario Carneiro]

it might be harder to read for a long telescope though

[Mario Carneiro]

maybe it's just better to live with the slightly mismatched types

[Leonardo de Moura]

Thanks for the feedback. The suggestions are already better than the current notation.

[Mario Carneiro]

:+1:

[Leonardo de Moura]

If you have more ideas, please keep posting them here.

[Kyle Miller]

Another idea: have the syntax look more like binders rather than patterns, like generalize (h : a = b) (e = f) (h' : c = d)

[Leonardo de Moura]

@Kyle Miller Thanks for sharing. I have a question. Some of the equalities are actually heterogeneous. Should we enforce it in the new notation? That is, sign an error if one uses =, but the equality is heterogeneous.

[James Gallicchio]

Personally I'd prefer some sort of English which makes it read better, something like
generalize h' : getValue? (init a), h as x, hx
It would feel a bit more similar to the other tactics where you list new identifiers at the end

[James Gallicchio]

But thank you! The generalize tactic actually seems perfect for circumventing this issue

[James Gallicchio]

Wait, can you generalize multiple terms at once? If not, then I feel like the most natural would be
generalize h' : getValue? (init a) as x in h1, h2, ...
where the hypotheses h1, ... keep their names but have new types

[Arthur Paulino]

Was it where Mario was getting at with the at suggestion?

[James Gallicchio]

ooh potentially, I don't know what generalize_hyp does

[Arthur Paulino]

_hyp in Lean 3 meta code base usually means that you're doing something with a variable in the context instead of with the target. The at word is a good indicator that one can do at h1 h2 |- or at * (it's common syntax in mathlib)

[Arthur Paulino]

Using as makes a lot of sense when you read it out loud. But I don't know other tactics that make use of "as" in their syntax (is this a concern?)

[James Gallicchio]

It's similar to ML binding patterns x as p, where x is bound to whatever matches p

[Mario Carneiro]

Arthur Paulino said:

Using as makes a lot of sense when you read it out loud. But I don't know other tactics that make use of "as" in their syntax (is this a concern?)

It is a concern, because these sorts of filler words have to be keywords for the most part, which precludes their use in identifiers. as comes up quite a bit in theorems about lists where the lists are called as and bs

[Mario Carneiro]

as a result it's generally best to stick to a somewhat restrictive grammar of filler words in tactics like with, using, from, or more unusual words like generalizing

[Mario Carneiro]

set is precedent for this kind of input, it uses set x : t := val with h where h receives the equation x = val

[Mario Carneiro]

and you could easily have a comma or indent-newline sequence of such things for generalize

[Mario Carneiro]

I think you could also add a type ascription on h if you wanted to change the type of it to something defeq or get an error if it's a heq and you didn't expect that, e.g. generalize x := val with (h : x = val)

[Mario Carneiro]

I would probably leave the ascription off most of the time but it works syntactically

[Leonardo de Moura]

I just pushed a commit that improves the split tactic. It uses a custom generalization procedure, and can now handle match expressions such as match h : Q.F.force with .... It is not heavily tested yet, but can already handle examples by @James Gallicchio and @Arthur Paulino that used to fail.
https://github.com/leanprover/lean4/blob/94b5a9b460ce0a258b77503198f5319f8739e84a/tests/lean/run/james1.lean
https://github.com/leanprover/lean4/blob/94b5a9b460ce0a258b77503198f5319f8739e84a/tests/lean/run/arthur2.lean
From the first test:

def deq (Q : LazyBatchQueue τ) : Option (τ × LazyBatchQueue τ) :=
  match h : Q.F.force with
  | some (x, F') =>
    some (x,
      ⟨F', Q.F_len - 1,
        by simp [LazyList.F_force_some_len_minus_one h, Q.h_lens]⟩)
  | none => none

theorem deq_correct (Q : LazyBatchQueue τ) : deq Q = none ↔ Q.F.force = none := by
  simp [deq]
  split <;> simp [*]

[Arthur Paulino]

Thanks!!!

[Leonardo de Moura]

BTW, the new generalizer for the split tactic can also handle the geValue example above:

def getValue (a : Uninit α) (h : (getValue? a).isSome) : α :=
  match getValue? a, h with
  | some a, h => a
  | none, h => by contradiction

@[simp]
theorem getValue_init (h) : (init a).getValue h = a := by
  unfold getValue
  split
  next a' h' heq₁ heq₂ =>
   /-
      a' : α
      h' : Option.isSome (some a') = true
      heq₁ : getValue? (init a) = some a'
      heq₂ : HEq h h'
      ⊢ a' = a
   -/
   sorry
  next => contradiction

[James Gallicchio]

This is already helping me make lots of progress, thank you so much!

[Evgeniy Kuznetsov]

@Leonardo de Moura , just discovered nightly-2022-05-04 split regression:

class Foo (f: Type) where
  foo : Option f

def bar (self: Foo f) := if let .some _ := self.foo then True else True

example [self: Foo f]:
  bar self → True ∧ bar self := by
  unfold bar
  intro hi
  constructor; trivial
  split <;> simp

tactic 'split' failed
case right
f : Type
self : Foo f
hi :
  match Foo.foo with
  | some val => True
  | x => True
⊢ match Foo.foo with
  | some val => True
  | x => True