Pedro Abreu has marked this topic as resolved.

@Gaëtan Gilbert I understand that your experience helped in solving this issue, but I am wondering if there is a methodical way to solve, or understand, these kind of situations. It would be nice even if you can explain your thought process while solving this issue.

when you get this "abstracting leads to a term which is ill-typed error" (usually from destruct induction or rewrite) it means the goal (including its hypotheses) is not sufficiently general in some way

in this case before we can `destruct (nth_error ...)`

we basically have to find a way to do `generalize (nth_error ...)`

ie replace `nth_error ...`

with a variable. If generalize would succeed then destruct would also succeed so we need to somehow encode the information the goal needs at the same time

The `pose (o:=nth_error l 10); pose proof (eqo := eq_refl : nth_error l 10 = o);clearbody o.`

(equivalently `remember (nth_error l 10) as o eqn:eqo`

except that puts the equation in the direction `eqo : o = ...`

and I wanted the other direction for some reason I forgot about but doesn't matter in any real way) produces this variable `o`

along with the info `eqo : nth_error l 10 = o`

which should be sufficient to use `o`

in our goal. Note that since `o`

is a variable of inductive type `option nat`

whose indices are all separate variables we can freely `destruct`

it (here `option`

has no indices but this still works with eg `foo : a = b`

if `b`

is a variable that doesn't appear in `a`

).

The next step is to use `o`

in the hypothesis. The goal conclusion fundamentally needs something of type which involves `nth_error ...`

AFAICT, so our modified hypothesis will need to be type cast to be used there. ```
pose (Hl' := rew [aux] eqo in Hl).
```

is basically the same as `pose proof (Hl' := Hl); rewrite eqo in Hl'`

ie duplicating `Hl`

then rewriting the equation in the copy, except we keep the info of how we got our rewritten copy. This info then lets us `replace Hl with (rew <- [aux] eqo in Hl')`

(which means doing the rewriting in reverse on Hl' produces our original Hl), then we drop the info with `clearbody`

and have a goal which doesn't need `Hl`

anymore, so we clear it. (I don't remember why there's a `simpl in Hl'`

, it does nothing)

The `destruct o`

is done at the end because if we do it earlier we have to do all the other twice.

Note that if we don't need the modified hypothesis in the goal and just want to get rid of the False branch we could do eg

```
Lemma some_DepRec_lemma (r : DepRec) (f : DepRec -> Prop) : f r.
Proof.
destruct r as [l Hl].
unfold someListProp in *.
pose proof (Hl' := Hl).
destruct (nth_error l 10) eqn:eqo in Hl'.
2:{ (* Hl' : False *) destruct Hl'. }
(* goal same as after the unfold with added hypotheses
n : nat
eqo : nth_error l 10 = Some n
Hl' : True *)
```

no need to deal with the explicit rewrite predicate `aux`

etc

If you want to learn more about how to deal with complicated dependent types and manipulation of equalities you can look into https://github.com/HoTT/Coq-HoTT

Most of it is applicable to vanilla Coq, the lemmas just have different names. The parts which aren't applicable are those which use univalence and those which use higher inductive types.

hope that helps

Last updated: Jun 20 2024 at 11:02 UTC