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: Oct 13 2024 at 01:02 UTC