Zulip Chat Archive

Stream: general

Topic: Trouble with universal quantifier in forward proof


view this post on Zulip Sorawee Porncharoenwase (Jan 21 2021 at 08:51):

I would like to prove this lemma using forward proof style, but I have trouble with it. Would appreciate any help!

import data.list.basic

example {p : Prop} {xs : list }
  (h1 : ( (i : ) (hi : i < xs.length), xs.nth_le i hi = 0)  p)
  (h2 :  (i : ) (hi : i < (xs.map id).length), (xs.map id).nth_le i hi = 0) :
p :=
begin
  apply h1,
  intros i hi,
  suffices : id (xs.nth_le i hi) = 0,
  { simp at this,
    assumption },
  rewrite  list.nth_le_map id,
  apply h2,
  rewrite list.length_map,
  assumption,
end

The above proof uses the backward proof style. With the forward proof style, I would need to apply h1 with h2. That means I need to rewrite one of them so that the implication is applicable. But how? Any rewrite would depend on the variable i which is universally quantified in the context. Having i in the context would make my life much easier, but I'm not sure if there's a sound inference rule that lets me do that.

view this post on Zulip Sorawee Porncharoenwase (Jan 21 2021 at 08:58):

Nvm, I clearly haven't thought this through. One cheesy way would be suffices : ∀ (i : ℕ) (hi : i < xs.length), xs.nth_le i hi = 0. That would then allow me to introduce i in the context. It's kinda annoying though...

view this post on Zulip Sorawee Porncharoenwase (Jan 21 2021 at 09:06):

Ah, this also works:

example {p : Prop} {xs : list }
  (h1 : ( (i : ) (hi : i < xs.length), xs.nth_le i hi = 0)  p)
  (h2 :  (i : ) (hi : i < (xs.map id).length), (xs.map id).nth_le i hi = 0) :
p :=
begin
  specialize h1 (by {
    intros i hi,
    specialize h2 i (by simpa),
    rewrite list.nth_le_map at h2,
    assumption,
  }),
  assumption,
end

view this post on Zulip Eric Wieser (Jan 21 2021 at 09:59):

I think you can replace specialize with exact there

view this post on Zulip Ruben Van de Velde (Jan 21 2021 at 11:14):

Alternatively (untested):

have h3 :  (i : ) (hi : i < xs.length), xs.nth_le i hi = 0,
{ intros i hi,
  specialize h2 i (by simpa),
  rewrite list.nth_le_map at h2,
  assumption },
exact h1 h2,

view this post on Zulip Eric Wieser (Jan 21 2021 at 11:36):

I don't remember what counts as forward any more, but you can turn the whole thing into term mode with

example {p : Prop} {xs : list }
  (h1 : ( (i : ) (hi : i < xs.length), xs.nth_le i hi = 0)  p)
  (h2 :  (i : ) (hi : i < (xs.map id).length), (xs.map id).nth_le i hi = 0) :
p :=
h1 $ λ i hi, (list.nth_le_map id _ _).symm.trans $ h2 i $ (list.map_id xs).symm  hi

Last updated: May 11 2021 at 13:22 UTC