## Stream: general

### Topic: Trouble with universal quantifier in forward proof

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

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

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


#### Eric Wieser (Jan 21 2021 at 09:59):

I think you can replace specialize with exact there

#### 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,


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