Trouble with universal quantifier in forward proof

Stream: general

[Sorawee Porncharoenwase]

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.

[Sorawee Porncharoenwase]

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...

[Sorawee Porncharoenwase]

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

[Eric Wieser]

I think you can replace specialize with exact there

[Ruben Van de Velde]

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,

[Eric Wieser]

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