# Zulip Chat Archive

## 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: Dec 20 2023 at 11:08 UTC